have h : Real.sqrt 1 ≠ 0 := sqrt_ne_zero'.2 zero_lt_one
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
⊢ Tendsto centralBinomialLower atTop (𝓝 (Real.sqrt π)⁻¹)
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
⊢ Tendsto centralBinomialLower atTop (𝓝 (Real.sqrt π)⁻¹)