rw [this]
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
⊢ 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 π / Real.sqrt π ^ 2))