case inl
m n✝ i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! ≤ (i + (n + 1))!

case inr
m n✝ i n : ℕ
h✝ : i < 2
⊢ i + (n + 1)! ≤ (i + (n + 1))!
m n✝ i n : ℕ
⊢ i + (n + 1)! ≤ (i + (n + 1))!
cases (le_or_lt (2 : ℕ) i)
case inl
m n✝ i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! ≤ (i + n + 1)!
case inl
m n✝ i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! ≤ (i + (n + 1))!
rw [← add_assoc]
case inl.h
m n✝ i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! < (i + n + 1)!
case inl
m n✝ i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! ≤ (i + n + 1)!
apply Nat.le_of_lt
case inl.h.hi
m n✝ i n : ℕ
h✝ : 2 ≤ i
⊢ 2 ≤ i
case inl.h
m n✝ i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! < (i + n + 1)!
apply add_factorial_succ_lt_factorial_add_succ
no goals
case inl.h.hi
m n✝ i n : ℕ
h✝ : 2 ≤ i
⊢ 2 ≤ i
assumption
no goals
m n✝ i n : ℕ
h✝ : 0 < 2
⊢ 0 + (n + 1)! ≤ (0 + (n + 1))!
simp
m n✝ i n : ℕ
h✝ : 1 < 2
⊢ 1 ≤ (n + 1) * (n + 1)!
m n✝ i n : ℕ
h✝ : 1 < 2
⊢ 1 + (n + 1)! ≤ (1 + (n + 1))!
rw [← add_assoc, ← Nat.succ_eq_add_one (1 + n), factorial_succ (1 + n),
  add_mul, one_mul, add_comm 1 n, add_le_add_iff_right]
case ha
m n✝ i n : ℕ
h✝ : 1 < 2
⊢ 1 ≤ n + 1

case hb
m n✝ i n : ℕ
h✝ : 1 < 2
⊢ 1 ≤ (n + 1)!
m n✝ i n : ℕ
h✝ : 1 < 2
⊢ 1 ≤ (n + 1) * (n + 1)!
apply one_le_mul
no goals
case ha
m n✝ i n : ℕ
h✝ : 1 < 2
⊢ 1 ≤ n + 1
apply Nat.le_add_left
no goals
case hb
m n✝ i n : ℕ
h✝ : 1 < 2
⊢ 1 ≤ (n + 1)!
apply factorial_pos
no goals
m n✝¹ i n✝ n : ℕ
h✝ : succ (succ n) < 2
⊢ succ (succ n) + (n✝ + 1)! ≤ (succ (succ n) + (n✝ + 1))!
contradiction