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

State before:
n t : ℕ
⊢ ↑(Nat.choose n t) ≤ (rexp 1 * ↑n / ↑t) ^ t
Tactic:
cases' Nat.eq_zero_or_pos t with h h
State after:
case inl
n t : ℕ
h : t = 0
⊢ ↑(Nat.choose n t) ≤ (rexp 1 * ↑n / ↑t) ^ t

case inr
n t : ℕ
h : t > 0
⊢ ↑(Nat.choose n t) ≤ (rexp 1 * ↑n / ↑t) ^ t

State before:
case inr
n t : ℕ
h : t > 0
⊢ ↑(Nat.choose n t) ≤ (rexp 1 * ↑n / ↑t) ^ t
Tactic:
refine' (Nat.choose_le_pow' t n).trans _
State after:
case inr
n t : ℕ
h : t > 0
⊢ ↑n ^ t / ↑t ! ≤ (rexp 1 * ↑n / ↑t) ^ t

State before:
case inr
n t : ℕ
h : t > 0
⊢ ↑n ^ t / ↑t ! ≤ (rexp 1 * ↑n / ↑t) ^ t
Tactic:
refine' (div_le_div_of_le_left _ _ factorial_bound_exp).trans _
State after:
case inr.refine'_1
n t : ℕ
h : t > 0
⊢ 0 ≤ ↑n ^ t

case inr.refine'_2
n t : ℕ
h : t > 0
⊢ 0 < (↑t / rexp 1) ^ t

case inr.refine'_3
n t : ℕ
h : t > 0
⊢ ↑n ^ t / (↑t / rexp 1) ^ t ≤ (rexp 1 * ↑n / ↑t) ^ t

State before:
case inr.refine'_3
n t : ℕ
h : 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 inl
n t : ℕ
h : t = 0
⊢ ↑(Nat.choose n t) ≤ (rexp 1 * ↑n / ↑t) ^ t
Tactic:
simp [h]
State after:
no goals

State before:
case inr.refine'_1
n t : ℕ
h : t > 0
⊢ 0 ≤ ↑n ^ t
Tactic:
positivity
State after:
no goals

State before:
case inr.refine'_2
n t : ℕ
h : t > 0
⊢ 0 < (↑t / rexp 1) ^ t
Tactic:
positivity
State after:
no goals