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

State before:
n : ℕ
hn : n ≠ 0
⊢ (↑n / rexp 1) ^ n < ↑n !
Tactic:
rw [div_pow, ← rpow_nat_cast (exp 1), exp_one_rpow, div_lt_iff, ← div_lt_iff']
State after:
n : ℕ
hn : n ≠ 0
⊢ ↑n ^ n / ↑n ! < rexp ↑n

n : ℕ
hn : n ≠ 0
⊢ 0 < ↑n !

n : ℕ
hn : n ≠ 0
⊢ 0 < rexp ↑n

State before:
n : ℕ
hn : n ≠ 0
⊢ ↑n ^ n / ↑n ! < rexp ↑n
Tactic:
exact exp_factorial_bound_of_ne_zero (Nat.cast_nonneg _) hn
State after:
no goals

State before:
n : ℕ
hn : n ≠ 0
⊢ 0 < ↑n !
Tactic:
positivity
State after:
no goals

State before:
n : ℕ
hn : n ≠ 0
⊢ 0 < rexp ↑n
Tactic:
positivity
State after:
no goals