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

State before:
n : ℕ
⊢ Real.sqrt (↑n + 1 / 4) / Real.sqrt (↑n + 1 + 1 / 4) ≤ (↑n + 1 / 2) / (↑n + 1)
Tactic:
rw [← Real.sqrt_div, sqrt_le_left, div_pow, div_le_div_iff]
State after:
n : ℕ
⊢ (↑n + 1 / 4) * (↑n + 1) ^ 2 ≤ (↑n + 1 / 2) ^ 2 * (↑n + 1 + 1 / 4)

case b0
n : ℕ
⊢ 0 < ↑n + 1 + 1 / 4

case d0
n : ℕ
⊢ 0 < (↑n + 1) ^ 2

n : ℕ
⊢ 0 ≤ (↑n + 1 / 2) / (↑n + 1)

case hx
n : ℕ
⊢ 0 ≤ ↑n + 1 / 4

State before:
case b0
n : ℕ
⊢ 0 < ↑n + 1 + 1 / 4

case d0
n : ℕ
⊢ 0 < (↑n + 1) ^ 2

n : ℕ
⊢ 0 ≤ (↑n + 1 / 2) / (↑n + 1)

case hx
n : ℕ
⊢ 0 ≤ ↑n + 1 / 4
Tactic:
all_goals positivity
State after:
no goals

State before:
n : ℕ
⊢ (↑n + 1 / 4) * (↑n + 1) ^ 2 ≤ (↑n + 1 / 2) ^ 2 * (↑n + 1 + 1 / 4)
Tactic:
ring_nf
State after:
n : ℕ
⊢ ↑(Int.ofNat 1) / ↑4 + ↑n * (↑(Int.ofNat 3) / ↑2) + ↑n ^ 2 * (↑(Int.ofNat 9) / ↑4) + ↑n ^ 3 ≤
    ↑(Int.ofNat 5) / ↑16 + ↑n * (↑(Int.ofNat 3) / ↑2) + ↑n ^ 2 * (↑(Int.ofNat 9) / ↑4) + ↑n ^ 3

State before:
n : ℕ
⊢ ↑(Int.ofNat 1) / ↑4 + ↑n * (↑(Int.ofNat 3) / ↑2) + ↑n ^ 2 * (↑(Int.ofNat 9) / ↑4) + ↑n ^ 3 ≤
    ↑(Int.ofNat 5) / ↑16 + ↑n * (↑(Int.ofNat 3) / ↑2) + ↑n ^ 2 * (↑(Int.ofNat 9) / ↑4) + ↑n ^ 3
Tactic:
gcongr ?_ + _ + _ + _
State after:
case bc.bc.bc
n : ℕ
⊢ ↑(Int.ofNat 1) / ↑4 ≤ ↑(Int.ofNat 5) / ↑16

State before:
case bc.bc.bc
n : ℕ
⊢ ↑(Int.ofNat 1) / ↑4 ≤ ↑(Int.ofNat 5) / ↑16
Tactic:
norm_num1
State after:
no goals

State before:
case hx
n : ℕ
⊢ 0 ≤ ↑n + 1 / 4
Tactic:
positivity
State after:
no goals