refine' (centralBinom_limit.div (tendsto_coe_nat_div_add_atTop (1 / 4 : ℝ)).sqrt h).congr' _
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
⊢ Tendsto centralBinomialLower atTop (𝓝 ((Real.sqrt π)⁻¹ / Real.sqrt 1))
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
⊢ ((fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) / fun x => Real.sqrt (↑x / (↑x + 1 / 4))) =ᶠ[atTop]
    centralBinomialLower