rwa [sqrt_mul, ← div_div, le_div_iff, div_eq_mul_one_div ((4 : ℝ) ^ n : ℝ), ← div_le_iff',
  one_div (sqrt π)]
n : ℕ
this✝ : 0 < π
this : centralBinomialLower n ≤ (Real.sqrt π)⁻¹
⊢ ↑(centralBinom n) ≤ 4 ^ n / Real.sqrt (π * (↑n + 1 / 4))
n : ℕ
this✝ : 0 < π
this : centralBinomialLower n ≤ (Real.sqrt π)⁻¹
⊢ 0 < 4 ^ n

n : ℕ
this✝ : 0 < π
this : centralBinomialLower n ≤ (Real.sqrt π)⁻¹
⊢ 0 < Real.sqrt (↑n + 1 / 4)

case hx
n : ℕ
this✝ : 0 < π
this : centralBinomialLower n ≤ (Real.sqrt π)⁻¹
⊢ 0 ≤ π