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

State before:
n : ℕ
⊢ (↑n + 1 / 2) / (↑n + 1) ≤ Real.sqrt (↑n + 1 / 3) / Real.sqrt (↑n + 1 + 1 / 3)
Tactic:
rw [← Real.sqrt_div]
State after:
n : ℕ
⊢ (↑n + 1 / 2) / (↑n + 1) ≤ Real.sqrt ((↑n + 1 / 3) / (↑n + 1 + 1 / 3))

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

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

case hx
n : ℕ
⊢ 0 ≤ ↑n + 1 / 3
Tactic:
refine' Real.le_sqrt_of_sq_le _
State after:
n : ℕ
⊢ ((↑n + 1 / 2) / (↑n + 1)) ^ 2 ≤ (↑n + 1 / 3) / (↑n + 1 + 1 / 3)

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

State before:
n : ℕ
⊢ ((↑n + 1 / 2) / (↑n + 1)) ^ 2 ≤ (↑n + 1 / 3) / (↑n + 1 + 1 / 3)

case hx
n : ℕ
⊢ 0 ≤ ↑n + 1 / 3
Tactic:
rw [div_pow, div_le_div_iff]
State after:
n : ℕ
⊢ (↑n + 1 / 2) ^ 2 * (↑n + 1 + 1 / 3) ≤ (↑n + 1 / 3) * (↑n + 1) ^ 2

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

case d0
n : ℕ
⊢ 0 < ↑n + 1 + 1 / 3

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

State before:
case b0
n : ℕ
⊢ 0 < (↑n + 1) ^ 2

case d0
n : ℕ
⊢ 0 < ↑n + 1 + 1 / 3

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

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

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

State before:
case bc.bc.bc.h
n : ℕ
⊢ ↑(Int.ofNat 19) / ↑12 ≤ ↑(Int.ofNat 5) / ↑3
Tactic:
norm_num1
State after:
no goals

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