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

State before:
n t : ℕ
⊢ (rexp 1 * ↑n / ↑t) ^ t = rexp ↑t * (↑n / ↑t) ^ t
Tactic:
rw [mul_div_assoc, mul_pow, ← exp_one_rpow t, rpow_nat_cast]
State after:
no goals