Theorem: centralBinomialLower_bound (ExponentialRamsey/Prereq/Mathlib/Analysis/SpecialFunctions/ExplicitStirling.lean)

State before:
n : ℕ
⊢ 4 ^ n / Real.sqrt (π * (↑n + 1 / 3)) ≤ ↑(centralBinom n)
Tactic:
have := pi_pos
State after:
n : ℕ
this : 0 < π
⊢ 4 ^ n / Real.sqrt (π * (↑n + 1 / 3)) ≤ ↑(centralBinom n)

State before:
n : ℕ
this : 0 < π
⊢ 4 ^ n / Real.sqrt (π * (↑n + 1 / 3)) ≤ ↑(centralBinom n)
Tactic:
have := centralBinomialUpper_monotone.le_of_tendsto centralBinomialUpper_limit n
State after:
n : ℕ
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ ≤ centralBinomialUpper n
⊢ 4 ^ n / Real.sqrt (π * (↑n + 1 / 3)) ≤ ↑(centralBinom n)

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

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

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

State before:
n : ℕ
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ ≤ centralBinomialUpper n
⊢ 0 < 4 ^ n

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

case hx
n : ℕ
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ ≤ centralBinomialUpper n
⊢ 0 ≤ π
Tactic:
all_goals positivity
State after:
no goals

State before:
case hx
n : ℕ
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ ≤ centralBinomialUpper n
⊢ 0 ≤ π
Tactic:
positivity
State after:
no goals