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

State before:
n t : ℕ
hn : n ≠ 0
ht : t ≠ 0
⊢ ↑(Nat.choose n t) < (rexp 1 * ↑n / ↑t) ^ t
Tactic:
refine' (Nat.choose_le_pow' t n).trans_lt _
State after:
n t : ℕ
hn : n ≠ 0
ht : t ≠ 0
⊢ ↑n ^ t / ↑t ! < (rexp 1 * ↑n / ↑t) ^ t

State before:
n t : ℕ
hn : n ≠ 0
ht : t ≠ 0
⊢ ↑n ^ t / ↑t ! < (rexp 1 * ↑n / ↑t) ^ t
Tactic:
refine' (div_lt_div_of_lt_left _ _ (factorial_bound_exp_of_ne_zero ht)).trans_eq _
State after:
case refine'_1
n t : ℕ
hn : n ≠ 0
ht : t ≠ 0
⊢ 0 < ↑n ^ t

case refine'_2
n t : ℕ
hn : n ≠ 0
ht : t ≠ 0
⊢ 0 < (↑t / rexp 1) ^ t

case refine'_3
n t : ℕ
hn : n ≠ 0
ht : t ≠ 0
⊢ ↑n ^ t / (↑t / rexp 1) ^ t = (rexp 1 * ↑n / ↑t) ^ t

State before:
case refine'_3
n t : ℕ
hn : n ≠ 0
ht : t ≠ 0
⊢ ↑n ^ t / (↑t / rexp 1) ^ t = (rexp 1 * ↑n / ↑t) ^ t
Tactic:
rw [← div_pow, div_div_eq_mul_div, mul_comm]
State after:
no goals

State before:
case refine'_1
n t : ℕ
hn : n ≠ 0
ht : t ≠ 0
⊢ 0 < ↑n ^ t
Tactic:
positivity
State after:
no goals

State before:
case refine'_2
n t : ℕ
hn : n ≠ 0
ht : t ≠ 0
⊢ 0 < (↑t / rexp 1) ^ t
Tactic:
positivity
State after:
no goals