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

State before:
n : ℕ
⊢ (↑n / rexp 1) ^ n ≤ ↑n !
Tactic:
rw [div_pow, ← rpow_nat_cast (exp 1), exp_one_rpow, div_le_iff, ← div_le_iff']
State after:
n : ℕ
⊢ ↑n ^ n / ↑n ! ≤ rexp ↑n

n : ℕ
⊢ 0 < ↑n !

n : ℕ
⊢ 0 < rexp ↑n

State before:
n : ℕ
⊢ ↑n ^ n / ↑n ! ≤ rexp ↑n
Tactic:
exact exp_factorial_bound (Nat.cast_nonneg _)
State after:
no goals

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

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