m n✝ i n : ℕ
hi : 2 ≤ i
⊢ i + (n + 1)! < (i + n) * (i + n)! + (i + n)!
m n✝ i n : ℕ
hi : 2 ≤ i
⊢ i + (n + 1)! < (i + n + 1)!
rw [← Nat.succ_eq_add_one (i + _), factorial_succ (i + _), add_mul, one_mul]
m n✝ i n : ℕ
hi : 2 ≤ i
this : i ≤ i + n
⊢ i + (n + 1)! < (i + n) * (i + n)! + (i + n)!
m n✝ i n : ℕ
hi : 2 ≤ i
⊢ i + (n + 1)! < (i + n) * (i + n)! + (i + n)!
have : i ≤ i + n := le.intro rfl
no goals
m n✝ i n : ℕ
hi : 2 ≤ i
this : i ≤ i + n
⊢ i + (n + 1)! < (i + n) * (i + n)! + (i + n)!
exact
  add_lt_add_of_lt_of_le
    (this.trans_lt
      ((lt_mul_iff_one_lt_right ((by decide : 0 < 2).trans_le (hi.trans this))).mpr
        (lt_iff_le_and_ne.mpr
          ⟨(i + n).factorial_pos, fun g =>
            Nat.not_succ_le_self 1 ((hi.trans this).trans (factorial_eq_one.mp g.symm))⟩)))
    (factorial_le
      ((le_of_eq (add_comm n 1)).trans
      ((add_le_add_iff_right n).mpr ((by decide : 1 ≤ 2).trans hi))))
no goals
m n✝ i n : ℕ
hi : 2 ≤ i
this : i ≤ i + n
⊢ 0 < 2
decide
no goals
m n✝ i n : ℕ
hi : 2 ≤ i
this : i ≤ i + n
⊢ 1 ≤ 2
decide