-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem eventually_pow_lt_factorial_sub (c d : ℕ) : ∀ᶠ n in atTop, c ^ n < (n - d)!

Proof state:
c d : ℕ
⊢ ∃ a, ∀ b ≥ a, c ^ b < (b - d)!

Tactic:
refine ⟨2 * (c ^ 2 + d + 1), ?_⟩

Result:
c d : ℕ
⊢ ∀ b ≥ 2 * (c ^ 2 + d + 1), c ^ b < (b - d)!

Proof state:
c d : ℕ
⊢ ∀ᶠ (n : ℕ) in atTop, c ^ n < (n - d)!

Tactic:
rw [eventually_atTop]

Result:
c d : ℕ
⊢ ∃ a, ∀ b ≥ a, c ^ b < (b - d)!

Proof state:
case h.e'_3.e_a
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ 2 * (c ^ 2 + d + 1) + d' + d' = 2 * (c ^ 2 + d' + d + 1)

Tactic:
omega

Result:
no goals

Proof state:
case intro.inr.hbd
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + 1) ^ (c ^ 2 + d' + d + 1)

Tactic:
exact Nat.pow_lt_pow_left (Nat.lt_succ_self _) (Nat.succ_ne_zero _)

Result:
no goals

Proof state:
case intro.inr.hac
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ 1 ≤ (c ^ 2)!

Tactic:
exact Nat.one_le_of_lt (Nat.factorial_pos _)

Result:
no goals

Proof state:
case intro.inr
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2)! * (c ^ 2 + 1) ^ (c ^ 2 + d' + d + 1)

Tactic:
rw [← one_mul (_ ^ _ : ℕ)]

Result:
case intro.inr
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ 1 * (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2)! * (c ^ 2 + 1) ^ (c ^ 2 + d' + d + 1)

Proof state:
c d n : ℕ
hn : n ≥ 2 * (c ^ 2 + d + 1)
⊢ c ^ n < (n - d)!

Tactic:
obtain ⟨d', rfl⟩ := Nat.exists_eq_add_of_le hn

Result:
case intro
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
⊢ c ^ (2 * (c ^ 2 + d + 1) + d') < (2 * (c ^ 2 + d + 1) + d' - d)!

Proof state:
case intro.inr
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ c ^ (2 * (c ^ 2 + d + 1) + d') * c ^ d' < (2 * (c ^ 2 + d + 1) + d' - d)!

Tactic:
convert_to (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!

Result:
case h.e'_3
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ c ^ (2 * (c ^ 2 + d + 1) + d') * c ^ d' = (c ^ 2) ^ (c ^ 2 + d' + d + 1)

case h.e'_4
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ (2 * (c ^ 2 + d + 1) + d' - d)! = (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!

case intro.inr
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!

Proof state:
case h.e'_3
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ c ^ (2 * (c ^ 2 + d + 1) + d' + d') = c ^ (2 * (c ^ 2 + d' + d + 1))

Tactic:
congr 1

Result:
case h.e'_3.e_a
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ 2 * (c ^ 2 + d + 1) + d' + d' = 2 * (c ^ 2 + d' + d + 1)

Proof state:
case intro.inr.hc
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ 0 < (c ^ 2)!

Tactic:
exact (Nat.factorial_pos _)

Result:
no goals

Proof state:
case intro.inr
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ c ^ (2 * (c ^ 2 + d + 1) + d') < (2 * (c ^ 2 + d + 1) + d' - d)!

Tactic:
refine (Nat.le_mul_of_pos_right _ (Nat.pow_pos (n := d') c0)).trans_lt ?_

Result:
case intro.inr
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ c ^ (2 * (c ^ 2 + d + 1) + d') * c ^ d' < (2 * (c ^ 2 + d + 1) + d' - d)!

Proof state:
c d : ℕ
⊢ ∀ b ≥ 2 * (c ^ 2 + d + 1), c ^ b < (b - d)!

Tactic:
intro n hn

Result:
c d n : ℕ
hn : n ≥ 2 * (c ^ 2 + d + 1)
⊢ c ^ n < (n - d)!

Proof state:
case intro.inl
d d' : ℕ
hn : 2 * (0 ^ 2 + d + 1) + d' ≥ 2 * (0 ^ 2 + d + 1)
⊢ 0 ^ (2 * (0 ^ 2 + d + 1) + d') < (2 * (0 ^ 2 + d + 1) + d' - d)!

Tactic:
simp [Nat.two_mul, ← Nat.add_assoc, Nat.add_right_comm _ 1, Nat.factorial_pos]

Result:
no goals

Proof state:
case intro.inr
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ 1 * (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2)! * (c ^ 2 + 1) ^ (c ^ 2 + d' + d + 1)

Tactic:
apply Nat.mul_lt_mul_of_le_of_lt

Result:
case intro.inr.hac
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ 1 ≤ (c ^ 2)!

case intro.inr.hbd
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + 1) ^ (c ^ 2 + d' + d + 1)

case intro.inr.hc
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ 0 < (c ^ 2)!

Proof state:
case h.e'_4
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ (2 * (c ^ 2 + d + 1) + d' - d)! = (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!

Tactic:
congr 1

Result:
case h.e'_4.e_a
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ 2 * (c ^ 2 + d + 1) + d' - d = c ^ 2 + (c ^ 2 + d' + d + 1) + 1

Proof state:
case intro
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
⊢ c ^ (2 * (c ^ 2 + d + 1) + d') < (2 * (c ^ 2 + d + 1) + d' - d)!

Tactic:
obtain (rfl | c0) := c.eq_zero_or_pos

Result:
case intro.inl
d d' : ℕ
hn : 2 * (0 ^ 2 + d + 1) + d' ≥ 2 * (0 ^ 2 + d + 1)
⊢ 0 ^ (2 * (0 ^ 2 + d + 1) + d') < (2 * (0 ^ 2 + d + 1) + d' - d)!

case intro.inr
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ c ^ (2 * (c ^ 2 + d + 1) + d') < (2 * (c ^ 2 + d + 1) + d' - d)!

Proof state:
case h.e'_4.e_a
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ 2 * (c ^ 2 + d + 1) + d' - d = c ^ 2 + (c ^ 2 + d' + d + 1) + 1

Tactic:
omega

Result:
no goals

Proof state:
case intro.inr
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!

Tactic:
refine (lt_of_lt_of_le ?_ Nat.factorial_mul_pow_le_factorial).trans_le <|
  (factorial_le (Nat.le_succ _))

Result:
case intro.inr
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2)! * (c ^ 2 + 1) ^ (c ^ 2 + d' + d + 1)

Proof state:
case h.e'_3
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ c ^ (2 * (c ^ 2 + d + 1) + d') * c ^ d' = (c ^ 2) ^ (c ^ 2 + d' + d + 1)

Tactic:
rw [← pow_mul, ← pow_add]

Result:
case h.e'_3
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) + d' ≥ 2 * (c ^ 2 + d + 1)
c0 : c > 0
⊢ c ^ (2 * (c ^ 2 + d + 1) + d' + d') = c ^ (2 * (c ^ 2 + d' + d + 1))