filter_upwards [eventually_gt_atTop 0] with n hn
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
case h
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
n : ℕ
hn : 0 < n
⊢ ((fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) / fun x => Real.sqrt (↑x / (↑x + 1 / 4))) n =
    centralBinomialLower n