have : (sqrt π)⁻¹ = sqrt π / sqrt π ^ 2 := by
  rw [inv_eq_one_div, sq, ← div_div, div_self]
  positivity
this : 0 < π
⊢ Tendsto (fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) atTop (𝓝 (Real.sqrt π)⁻¹)
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
⊢ Tendsto (fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) atTop (𝓝 (Real.sqrt π)⁻¹)