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

State before:
⊢ Monotone centralBinomialLower
Tactic:
refine' monotone_nat_of_le_succ _
State after:
⊢ ∀ (n : ℕ), centralBinomialLower n ≤ centralBinomialLower (n + 1)

State before:
⊢ ∀ (n : ℕ), centralBinomialLower n ≤ centralBinomialLower (n + 1)
Tactic:
intro n
State after:
n : ℕ
⊢ centralBinomialLower n ≤ centralBinomialLower (n + 1)

State before:
n : ℕ
⊢ centralBinomialLower n ≤ centralBinomialLower (n + 1)
Tactic:
rw [centralBinomialLower, centralBinomialLower, _root_.pow_succ, ←div_div]
State after:
n : ℕ
⊢ ↑(centralBinom n) * Real.sqrt (↑n + 1 / 4) / 4 ^ n ≤
    ↑(centralBinom (n + 1)) * Real.sqrt (↑(n + 1) + 1 / 4) / 4 / 4 ^ n

State before:
n : ℕ
⊢ ↑(centralBinom n) * Real.sqrt (↑n + 1 / 4) / 4 ^ n ≤
    ↑(centralBinom (n + 1)) * Real.sqrt (↑(n + 1) + 1 / 4) / 4 / 4 ^ n
Tactic:
refine' div_le_div_of_le (by positivity) _
State after:
n : ℕ
⊢ ↑(centralBinom n) * Real.sqrt (↑n + 1 / 4) ≤ ↑(centralBinom (n + 1)) * Real.sqrt (↑(n + 1) + 1 / 4) / 4

State before:
n : ℕ
⊢ ↑(centralBinom n) * Real.sqrt (↑n + 1 / 4) ≤ ↑(centralBinom (n + 1)) * Real.sqrt (↑(n + 1) + 1 / 4) / 4
Tactic:
rw [le_div_iff, mul_assoc, mul_comm, ← div_le_div_iff, centralBinom_ratio, mul_comm,
  mul_div_assoc, Nat.cast_add_one]
State after:
n : ℕ
⊢ 4 * (Real.sqrt (↑n + 1 / 4) / Real.sqrt (↑n + 1 + 1 / 4)) ≤ 4 * ((↑n + 1 / 2) / (↑n + 1))

case b0
n : ℕ
⊢ 0 < Real.sqrt (↑(n + 1) + 1 / 4)

case d0
n : ℕ
⊢ 0 < ↑(centralBinom n)

n : ℕ
⊢ 0 < 4

State before:
n : ℕ
⊢ 4 * (Real.sqrt (↑n + 1 / 4) / Real.sqrt (↑n + 1 + 1 / 4)) ≤ 4 * ((↑n + 1 / 2) / (↑n + 1))

case b0
n : ℕ
⊢ 0 < Real.sqrt (↑(n + 1) + 1 / 4)

case d0
n : ℕ
⊢ 0 < ↑(centralBinom n)

n : ℕ
⊢ 0 < 4
Tactic:
refine' mul_le_mul_of_nonneg_left (lower_monotone_aux n) (by positivity)
State after:
case b0
n : ℕ
⊢ 0 < Real.sqrt (↑(n + 1) + 1 / 4)

case d0
n : ℕ
⊢ 0 < ↑(centralBinom n)

n : ℕ
⊢ 0 < 4

State before:
n : ℕ
⊢ 0 ≤ 4 ^ n
Tactic:
positivity
State after:
no goals

State before:
n : ℕ
⊢ 0 ≤ 4
Tactic:
positivity
State after:
no goals

State before:
case b0
n : ℕ
⊢ 0 < Real.sqrt (↑(n + 1) + 1 / 4)
Tactic:
positivity
State after:
no goals

State before:
case d0
n : ℕ
⊢ 0 < ↑(centralBinom n)
Tactic:
rw [Nat.cast_pos]
State after:
case d0
n : ℕ
⊢ 0 < centralBinom n

State before:
case d0
n : ℕ
⊢ 0 < centralBinom n
Tactic:
exact centralBinom_pos _
State after:
no goals

State before:
n : ℕ
⊢ 0 < 4
Tactic:
positivity
State after:
no goals