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

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

State before:
n : ℕ
this : 0 < π
⊢ ↑(centralBinom n) ≤ 4 ^ n / Real.sqrt (π * (↑n + 1 / 4))
Tactic:
have := centralBinomialLower_monotone.ge_of_tendsto centralBinomialLower_limit n
State after:
n : ℕ
this✝ : 0 < π
this : centralBinomialLower n ≤ (Real.sqrt π)⁻¹
⊢ ↑(centralBinom n) ≤ 4 ^ n / Real.sqrt (π * (↑n + 1 / 4))

State before:
n : ℕ
this✝ : 0 < π
this : centralBinomialLower n ≤ (Real.sqrt π)⁻¹
⊢ ↑(centralBinom n) ≤ 4 ^ n / Real.sqrt (π * (↑n + 1 / 4))
Tactic:
rwa [sqrt_mul, ← div_div, le_div_iff, div_eq_mul_one_div ((4 : ℝ) ^ n : ℝ), ← div_le_iff',
  one_div (sqrt π)]
State after:
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 ≤ π

State before:
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 ≤ π
Tactic:
all_goals positivity
State after:
no goals

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