Theorem: Nat.asc_le_pow_mul_factorial (ExponentialRamsey/Prereq/Mathlib/Data/Nat/Factorial/Basic.lean)

State before:
s t : ℕ
⊢ ascFactorial t s ≤ s ! * (t + 1) ^ s
Tactic:
induction' s with s ih
State after:
case zero
t : ℕ
⊢ ascFactorial t zero ≤ zero ! * (t + 1) ^ zero

case succ
t s : ℕ
ih : ascFactorial t s ≤ s ! * (t + 1) ^ s
⊢ ascFactorial t (succ s) ≤ (succ s)! * (t + 1) ^ succ s

State before:
case succ
t s : ℕ
ih : ascFactorial t s ≤ s ! * (t + 1) ^ s
⊢ ascFactorial t (succ s) ≤ (succ s)! * (t + 1) ^ succ s
Tactic:
rw [ascFactorial_succ, factorial_succ, pow_succ', mul_mul_mul_comm]
State after:
case succ
t s : ℕ
ih : ascFactorial t s ≤ s ! * (t + 1) ^ s
⊢ (t + s + 1) * ascFactorial t s ≤ (s + 1) * (t + 1) * (s ! * (t + 1) ^ s)

State before:
case succ
t s : ℕ
ih : ascFactorial t s ≤ s ! * (t + 1) ^ s
⊢ (t + s + 1) * ascFactorial t s ≤ (s + 1) * (t + 1) * (s ! * (t + 1) ^ s)
Tactic:
refine' Nat.mul_le_mul _ ih
State after:
case succ
t s : ℕ
ih : ascFactorial t s ≤ s ! * (t + 1) ^ s
⊢ t + s + 1 ≤ (s + 1) * (t + 1)

State before:
case succ
t s : ℕ
ih : ascFactorial t s ≤ s ! * (t + 1) ^ s
⊢ t + s + 1 ≤ (s + 1) * (t + 1)
Tactic:
rw [add_comm t, add_one_mul s, mul_add_one s, add_assoc]
State after:
case succ
t s : ℕ
ih : ascFactorial t s ≤ s ! * (t + 1) ^ s
⊢ s + (t + 1) ≤ s * t + s + (t + 1)

State before:
case succ
t s : ℕ
ih : ascFactorial t s ≤ s ! * (t + 1) ^ s
⊢ s + (t + 1) ≤ s * t + s + (t + 1)
Tactic:
simp
State after:
no goals

State before:
case zero
t : ℕ
⊢ ascFactorial t zero ≤ zero ! * (t + 1) ^ zero
Tactic:
simp
State after:
no goals