awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
⊢ ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
have zero : ∑ L ∈ fixedLengthDigits hb 0, L.sum = 0 * b ^ HSub.hSub (α := ℕ) 0 1 * b.choose 2
Tactic: induction l with
  | zero => simp
  | succ l hr =>
      by_cases hl : l = 0
      · simp [hl, fixedLengthDigits_one, Finset.sum_range_id, choose_two_right]
      rw [fixedLengthDigits_succ_eq_disjiUnion, Finset.sum_disjiUnion]
      simp only [consFixedLengthDigits, cons.injEq, true_and, implies_true, Set.injOn_of_eq_iff_eq,
        Finset.sum_image, sum_cons]
      rw [Finset.sum_comm]
      simp_rw [Finset.sum_add_distrib, Finset.sum_const, Finset.sum_nsmul, Finset.sum_range_id, hr,
        nsmul_eq_mul, Finset.card_range, add_tsub_cancel_right, cast_id, card_fixedLengthDigits,
        choose_two_right]
      rw [show b ^ l = b * b ^ (l - 1) by rw [← Nat.pow_succ', Nat.sub_one, Nat.succ_pred hl]]
      ring
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
zero : ∑ L ∈ fixedLengthDigits hb 0, L.sum = 0 * b ^ HSub.hSub (α := ℕ) 0 1 * b.choose 2
⊢ ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
have succ : ∀ (l : ℕ) (hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2),
  ∑ L ∈ fixedLengthDigits hb (l + 1), L.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
Tactic: induction l with
  | zero => simp
  | succ l hr =>
      by_cases hl : l = 0
      · simp [hl, fixedLengthDigits_one, Finset.sum_range_id, choose_two_right]
      rw [fixedLengthDigits_succ_eq_disjiUnion, Finset.sum_disjiUnion]
      simp only [consFixedLengthDigits, cons.injEq, true_and, implies_true, Set.injOn_of_eq_iff_eq,
        Finset.sum_image, sum_cons]
      rw [Finset.sum_comm]
      simp_rw [Finset.sum_add_distrib, Finset.sum_const, Finset.sum_nsmul, Finset.sum_range_id, hr,
        nsmul_eq_mul, Finset.card_range, add_tsub_cancel_right, cast_id, card_fixedLengthDigits,
        choose_two_right]
      rw [show b ^ l = b * b ^ (l - 1) by rw [← Nat.pow_succ', Nat.sub_one, Nat.succ_pred hl]]
      ring
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
⊢ ∑ x ∈ Finset.range (b ^ l), (b.digits x).sum = l * b ^ (l - 1) * b.choose 2
have rw : Eq (α := ℕ) (∑ x ∈ Finset.range (b ^ l), (b.digits x).sum) (∑ L ∈ List.fixedLengthDigits hb l, L.sum)
Tactic: rw [← List.sum_fixedLengthDigits_sum hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
⊢ Eq (α := ℕ) (∑ x ∈ Finset.range (b ^ l), (b.digits x).sum) (∑ L ∈ List.fixedLengthDigits hb l, L.sum)
have refine : ∀ (L : List ℕ) (hL : L ∈ List.fixedLengthDigits hb l), L.sum = (b.digits (ofDigits b L)).sum
Tactic: refine (Finset.sum_nbij (ofDigits b) (by exact (bijOn_ofDigits' hb l).1)
    (bijOn_ofDigits' hb l).2.1 (bijOn_ofDigits' hb l).2.2 fun L hL ↦ ?_).symm
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ List.fixedLengthDigits hb l
⊢ L.sum = (b.digits (ofDigits b L)).sum
have rw : L.sum = L.sum
Tactic: rw [sum_digits_ofDigits_eq_sum hb ((List.mem_fixedLengthDigits_iff hb).mp hL)]
-- Lean 4 proof step from Mathlib.Data.Nat.Dist (goal)
Goal:
n k m : ℕ
⊢ (n * k).dist (m * k) = n.dist m * k
have rw : n * k - m * k + (m * k - n * k) = n.dist m * k
Tactic: rw [dist, dist, right_distrib, tsub_mul n, tsub_mul m]
-- Lean 4 proof step from Mathlib.Data.Nat.Dist (goal)
Goal:
n k m : ℕ
rw : n * k - m * k + (m * k - n * k) = n.dist m * k
⊢ (n * k).dist (m * k) = n.dist m * k
have rw₁ : n * k - m * k + (m * k - n * k) = (n - m + (m - n)) * k
Tactic: rw [dist, dist, right_distrib, tsub_mul n, tsub_mul m]
-- Lean 4 proof step from Mathlib.Data.Nat.Dist (goal)
Goal:
n k m : ℕ
rw : n * k - m * k + (m * k - n * k) = n.dist m * k
rw₁ : n * k - m * k + (m * k - n * k) = (n - m + (m - n)) * k
⊢ (n * k).dist (m * k) = n.dist m * k
have rw₂ : n * k - m * k + (m * k - n * k) = (n - m) * k + (m - n) * k
Tactic: rw [dist, dist, right_distrib, tsub_mul n, tsub_mul m]
-- Lean 4 proof step from Mathlib.Data.Nat.Dist (goal)
Goal:
n k m : ℕ
rw : n * k - m * k + (m * k - n * k) = n.dist m * k
rw₁ : n * k - m * k + (m * k - n * k) = (n - m + (m - n)) * k
rw₂ : n * k - m * k + (m * k - n * k) = (n - m) * k + (m - n) * k
⊢ (n * k).dist (m * k) = n.dist m * k
have rw₃ : n * k - m * k + (m * k - n * k) = n * k - m * k + (m - n) * k
Tactic: rw [dist, dist, right_distrib, tsub_mul n, tsub_mul m]
-- Lean 4 proof step from Mathlib.Data.Nat.Dist (goal)
Goal:
n k m : ℕ
rw : n * k - m * k + (m * k - n * k) = n.dist m * k
rw₁ : n * k - m * k + (m * k - n * k) = (n - m + (m - n)) * k
rw₂ : n * k - m * k + (m * k - n * k) = (n - m) * k + (m - n) * k
rw₃ : n * k - m * k + (m * k - n * k) = n * k - m * k + (m - n) * k
⊢ (n * k).dist (m * k) = n.dist m * k
have rw₄ : n * k - m * k + (m * k - n * k) = n * k - m * k + (m * k - n * k)
Tactic: rw [dist, dist, right_distrib, tsub_mul n, tsub_mul m]
-- Lean 4 proof step from Mathlib.Data.Nat.Dist (goal)
Goal:
k n m : ℕ
⊢ (k * n).dist (k * m) = k * n.dist m
have rw : (n * k).dist (k * m) = k * n.dist m
Tactic: rw [mul_comm k n, mul_comm k m, dist_mul_right, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Dist (goal)
Goal:
k n m : ℕ
rw : (n * k).dist (k * m) = k * n.dist m
⊢ (k * n).dist (k * m) = k * n.dist m
have rw₁ : (n * k).dist (m * k) = k * n.dist m
Tactic: rw [mul_comm k n, mul_comm k m, dist_mul_right, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Dist (goal)
Goal:
k n m : ℕ
rw : (n * k).dist (k * m) = k * n.dist m
rw₁ : (n * k).dist (m * k) = k * n.dist m
⊢ (k * n).dist (k * m) = k * n.dist m
have rw₂ : n.dist m * k = k * n.dist m
Tactic: rw [mul_comm k n, mul_comm k m, dist_mul_right, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Dist (goal)
Goal:
k n m : ℕ
rw : (n * k).dist (k * m) = k * n.dist m
rw₁ : (n * k).dist (m * k) = k * n.dist m
rw₂ : n.dist m * k = k * n.dist m
⊢ (k * n).dist (k * m) = k * n.dist m
have rw₃ : k * n.dist m = k * n.dist m
Tactic: rw [mul_comm k n, mul_comm k m, dist_mul_right, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Dist (goal)
Goal:
i j : ℕ
⊢ i.dist j = max i j - min i j
have inl : i ≤ j → i.dist j = max i j - min i j
Tactic: cases le_total i j
-- Lean 4 proof step from Mathlib.Data.Nat.Dist (goal)
Goal:
i j : ℕ
inl : i ≤ j → i.dist j = max i j - min i j
⊢ i.dist j = max i j - min i j
have inr : j ≤ i → i.dist j = max i j - min i j
Tactic: cases le_total i j
-- Lean 4 proof step from Mathlib.Data.Nat.EvenOddRec (goal)
Goal:
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
n : ℕ
⊢ evenOddRec (P := fun (x : ℕ) ↦ P x) h0 h_even h_odd (2 * n) =
    h_even n (evenOddRec (P := fun (x : ℕ) ↦ P x) h0 h_even h_odd n)
have apply : (match (motive := (x : Bool) → (x_1 : ℕ) → P x_1 → (fun (x : ℕ) ↦ P x) (bit x x_1)) false, 0, h0 with
    | false, i, hi => h_even i hi
    | true, i, hi => h_odd i hi) =
    h0 ∨
  (n = 0 → false = true)
Tactic: apply binaryRec_eq false n
-- Lean 4 proof step from Mathlib.Data.Nat.EvenOddRec (goal)
Goal:
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
n : ℕ
⊢ evenOddRec (P := fun (x : ℕ) ↦ P x) h0 h_even h_odd (2 * n + 1) =
    h_odd n (evenOddRec (P := fun (x : ℕ) ↦ P x) h0 h_even h_odd n)
have apply : (match (motive := (x : Bool) → (x_1 : ℕ) → P x_1 → (fun (x : ℕ) ↦ P x) (bit x x_1)) false, 0, h0 with
    | false, i, hi => h_even i hi
    | true, i, hi => h_odd i hi) =
    h0 ∨
  (n = 0 → true = true)
Tactic: apply binaryRec_eq true n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
m n : ℕ
h : m ≤ n
⊢ m ! ∣ n !
have refl : m ! ∣ m !
Tactic: induction h with
  | refl => exact Nat.dvd_refl _
  | step _ ih => exact Nat.dvd_trans ih (Nat.dvd_mul_left _ _)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
m n : ℕ
h : m ≤ n
refl : m ! ∣ m !
⊢ m ! ∣ n !
have step : ∀ {m_1 : ℕ}, m.le m_1 → ∀ (ih : m ! ∣ m_1 !), m ! ∣ m_1.succ !
Tactic: induction h with
  | refl => exact Nat.dvd_refl _
  | step _ ih => exact Nat.dvd_trans ih (Nat.dvd_mul_left _ _)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
m n : ℕ
⊢ m ! * (m + 1) ^ (n + 1) ≤ (m + (n + 1))!
have rw : m ! * (m + 1) ^ n * (m + 1) ≤ (m + n)! * (m + n + 1)
Tactic: rw [← Nat.add_assoc, factorial_succ, Nat.mul_comm (_ + 1), Nat.pow_succ, ← Nat.mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
m n : ℕ
hn : 0 < n
⊢ n ! < m ! ↔ n < m
have refine : ∀ (h : n < m), n ! < m !
Tactic: refine ⟨fun h => not_le.mp fun hmn => Nat.not_le_of_gt h (factorial_le hmn), fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
hk : 0 < k
⊢ k ! < (k + 1)!
have rw : 0 < k * k !
Tactic: rw [factorial_succ, succ_mul, Nat.lt_add_left_iff_pos]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (hypothesis)
Goal:
m n : ℕ
hn : 0 < n
h : n < m
⊢ n ! < m !
have this : ∀ {n : ℕ}, 0 < n → n ! < (n + 1)!
Tactic: have : ∀ {n}, 0 < n → n ! < (n + 1)! := by
    intro k hk
    rw [factorial_succ, succ_mul, Nat.lt_add_left_iff_pos]
    exact Nat.mul_pos hk k.factorial_pos
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
m n : ℕ
hn : 0 < n
h : n < m
this : ∀ {n : ℕ}, 0 < n → n ! < (n + 1)!
⊢ n ! < m !
have refl : ∀ (hn : 0 < n), n ! < n.succ !
Tactic: induction h generalizing hn with
  | refl => exact this hn
  | step hnk ih => exact lt_trans (ih hn) <| this <| lt_trans hn <| lt_of_succ_le hnk
Cleared hypotheses: hn, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
m n : ℕ
hn : 0 < n
h : n < m
this : ∀ {n : ℕ}, 0 < n → n ! < (n + 1)!
refl : ∀ (hn : 0 < n), n ! < n.succ !
⊢ n ! < m !
have step : ∀ {m : ℕ} (hnk : n.succ.le m) (ih : ∀ (hn : 0 < n), n ! < m !) (hn : 0 < n), n ! < m.succ !
Tactic: induction h generalizing hn with
  | refl => exact this hn
  | step hnk ih => exact lt_trans (ih hn) <| this <| lt_trans hn <| lt_of_succ_le hnk
Cleared hypotheses: hn, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
⊢ n ! = 1 ↔ n ≤ 1
have mp : n ! = 1 → n ≤ 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
mp : n ! = 1 → n ≤ 1
⊢ n ! = 1 ↔ n ≤ 1
have mpr : n ≤ 1 → n ! = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
h : n ! = 1
⊢ n ≤ 1
have mp : ¬LT.lt (α := ℕ) 1 1
Tactic: rw [← not_lt, ← one_lt_factorial, h]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
m n : ℕ
hn : 1 < n
⊢ n ! = m ! ↔ n = m
have refine : ∀ (h : n ! = m !), n = m
Tactic: refine ⟨fun h => ?_, congr_arg _⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
m n : ℕ
hn : 1 < n
h : n ! = m !
⊢ n = m
have inl : ∀ (hnm : n < m), n = m
Tactic: obtain hnm | rfl | hnm := lt_trichotomy n m
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
m n : ℕ
hn : 1 < n
h : n ! = m !
inl : ∀ (hnm : n < m), n = m
⊢ n = m
have inr : ∀ (h : n ! = n !), n = n
Tactic: obtain hnm | rfl | hnm := lt_trichotomy n m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
m n : ℕ
hn : 1 < n
h : n ! = m !
inl : ∀ (hnm : n < m), n = m
inr : ∀ (h : n ! = n !), n = n
⊢ n = m
have inr₁ : ∀ (hnm : m < n), n = m
Tactic: obtain hnm | rfl | hnm := lt_trichotomy n m
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (hypothesis)
Goal:
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : n < m
⊢ n = m
have hnm₁ : m ! < m !
Tactic: rw [← factorial_lt <| lt_of_succ_lt hn, h] at hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (hypothesis)
Goal:
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : m < n
⊢ n = m
have hn₁ : 1 < m
Tactic: rw [← one_lt_factorial, h, one_lt_factorial] at hn
Cleared hypotheses: hn, h, hnm
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (hypothesis)
Goal:
m n : ℕ
hn : 1 < m
h : n ! = m !
hnm : m < n
⊢ n = m
have hnm₁ : m ! < m !
Tactic: rw [← factorial_lt <| lt_of_succ_lt hn, h] at hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
m n : ℕ
h : 1 < n ∨ 1 < m
⊢ n ! = m ! ↔ n = m
have inl : ∀ (hn : 1 < n), n ! = m ! ↔ n = m
Tactic: obtain hn | hm := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
m n : ℕ
h : 1 < n ∨ 1 < m
inl : ∀ (hn : 1 < n), n ! = m ! ↔ n = m
⊢ n ! = m ! ↔ n = m
have inr : ∀ (hm : 1 < m), n ! = m ! ↔ n = m
Tactic: obtain hn | hm := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
m n : ℕ
hm : 1 < m
⊢ n ! = m ! ↔ n = m
have inr : m ! = n ! ↔ n = m
Tactic: rw [eq_comm, factorial_inj hm, eq_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
m n : ℕ
hm : 1 < m
inr : m ! = n ! ↔ n = m
⊢ n ! = m ! ↔ n = m
have inr₁ : m = n ↔ n = m
Tactic: rw [eq_comm, factorial_inj hm, eq_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
m n : ℕ
hm : 1 < m
inr : m ! = n ! ↔ n = m
inr₁ : m = n ↔ n = m
⊢ n ! = m ! ↔ n = m
have inr₂ : n = m ↔ n = m
Tactic: rw [eq_comm, factorial_inj hm, eq_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (hypothesis)
Goal:
n : ℕ
hi : 3 ≤ n
⊢ n < n !
have this : 0 < n
Tactic: have : 0 < n := by lia
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (hypothesis)
Goal:
n : ℕ
hi : 3 ≤ n
this : 0 < n
⊢ n < n !
have hn : 1 < n.pred
Tactic: have hn : 1 < pred n := le_pred_of_lt (succ_le_iff.mp hi)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
hi : 3 ≤ n
this : 0 < n
hn : 1 < n.pred
⊢ n < n !
have rw : n.pred.succ < (n.pred + 1) * n.pred !
Tactic: rw [← succ_pred_eq_of_pos ‹0 < n›, factorial_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
i n : ℕ
hi : 2 ≤ i
⊢ i + (n + 1)! < (i + n + 1)!
have rw : i + (n + 1)! < (i + n) * (i + n)! + (i + n)!
Tactic: rw [factorial_succ (i + _), Nat.add_mul, Nat.one_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (hypothesis)
Goal:
i n : ℕ
hi : 2 ≤ i
⊢ i + (n + 1)! < (i + n) * (i + n)! + (i + n)!
have this : i + n ≤ (i + n)!
Tactic: have := (i + n).self_le_factorial
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ i + (n + 1)! < (i + n) * (i + n)! + (i + n)!
have refine_1 : i ≤ i + n
Tactic: refine Nat.add_lt_add_of_lt_of_le (Nat.lt_of_le_of_lt ?_ ((Nat.lt_mul_iff_one_lt_right ?_).2 ?_))
    (factorial_le ?_)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
refine_1 : i ≤ i + n
⊢ i + (n + 1)! < (i + n) * (i + n)! + (i + n)!
have refine_2 : 0 < i + n
Tactic: refine Nat.add_lt_add_of_lt_of_le (Nat.lt_of_le_of_lt ?_ ((Nat.lt_mul_iff_one_lt_right ?_).2 ?_))
    (factorial_le ?_)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
refine_1 : i ≤ i + n
refine_2 : 0 < i + n
⊢ i + (n + 1)! < (i + n) * (i + n)! + (i + n)!
have refine_3 : 1 < (i + n)!
Tactic: refine Nat.add_lt_add_of_lt_of_le (Nat.lt_of_le_of_lt ?_ ((Nat.lt_mul_iff_one_lt_right ?_).2 ?_))
    (factorial_le ?_)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
refine_1 : i ≤ i + n
refine_2 : 0 < i + n
refine_3 : 1 < (i + n)!
⊢ i + (n + 1)! < (i + n) * (i + n)! + (i + n)!
have refine_4 : n + 1 ≤ i + n
Tactic: refine Nat.add_lt_add_of_lt_of_le (Nat.lt_of_le_of_lt ?_ ((Nat.lt_mul_iff_one_lt_right ?_).2 ?_))
    (factorial_le ?_)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
i n : ℕ
hi : 2 ≤ i
hn : 1 ≤ n
⊢ i + n ! < (i + n)!
have refl : i + 1! < (i + 1)!
Tactic: cases hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
i n : ℕ
hi : 2 ≤ i
hn : 1 ≤ n
refl : i + 1! < (i + 1)!
⊢ i + n ! < (i + n)!
have step : ∀ {m : ℕ}, Nat.le 1 m → i + m.succ ! < (i + m.succ)!
Tactic: cases hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
i n : ℕ
⊢ i + (n + 1)! ≤ (i + (n + 1))!
have inl : 2 ≤ i → i + (n + 1)! ≤ (i + (n + 1))!
Tactic: cases (le_or_gt (2 : ℕ) i)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
i n : ℕ
inl : 2 ≤ i → i + (n + 1)! ≤ (i + (n + 1))!
⊢ i + (n + 1)! ≤ (i + (n + 1))!
have inr : i < 2 → i + (n + 1)! ≤ (i + (n + 1))!
Tactic: cases (le_or_gt (2 : ℕ) i)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
i n : ℕ
h : 2 ≤ i
⊢ i + (n + 1)! ≤ (i + (n + 1))!
have inl : i + (n + 1)! ≤ (i + n + 1)!
Tactic: rw [← Nat.add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
i n : ℕ
h : 2 ≤ i
⊢ i + (n + 1)! ≤ (i + n + 1)!
have inl : i + (n + 1)! < (i + n + 1)!
Tactic: apply Nat.le_of_lt
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
i n : ℕ
h : LT.lt (α := ℕ) 1 2
⊢ 1 + (n + 1)! ≤ (1 + (n + 1))!
have rw : 1 ≤ (n + 1) * (n + 1)!
Tactic: rw [← Nat.add_assoc, factorial_succ (1 + n), Nat.add_mul, Nat.one_mul, Nat.add_comm 1 n,
        Nat.add_le_add_iff_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
i n : ℕ
n1 : 1 ≤ n
⊢ i + n ! ≤ (i + n)!
have refl : i + 1! ≤ (i + 1)!
Tactic: rcases n1 with - | @h
Cleared hypotheses: n, n1
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
i n : ℕ
n1 : 1 ≤ n
refl : i + 1! ≤ (i + 1)!
⊢ i + n ! ≤ (i + n)!
have step : ∀ {h : ℕ}, Nat.le 1 h → i + h.succ ! ≤ (i + h.succ)!
Tactic: rcases n1 with - | @h
Cleared hypotheses: n, n1
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n m : ℕ
hnm : n ≤ m
⊢ n ! * n ^ (m - n) ≤ m !
have _ : n ! * (n + 1) ^ (m - n) ≤ m !
Tactic: calc
    _ ≤ n ! * (n + 1) ^ (m - n) := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left n.le_succ _)
    _ ≤ _ := by simpa [hnm] using @Nat.factorial_mul_pow_le_factorial n (m - n)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
⊢ (n + 1) * (n + 1) ^ n = (n + 1) ^ (n + 1)
have rw : (n + 1) * (n + 1) ^ n = (n + 1) * (n + 1) ^ n
Tactic: rw [pow_succ']
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
⊢ ascFactorial 0 (succ 0) = 0
have rw : HAdd.hAdd (α := ℕ) 0 0 * ascFactorial 0 0 = 0
Tactic: rw [ascFactorial_succ, ascFactorial_zero, Nat.zero_add, Nat.zero_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
rw : HAdd.hAdd (α := ℕ) 0 0 * ascFactorial 0 0 = 0
⊢ ascFactorial 0 (succ 0) = 0
have rw₁ : HAdd.hAdd (α := ℕ) 0 0 * 1 = 0
Tactic: rw [ascFactorial_succ, ascFactorial_zero, Nat.zero_add, Nat.zero_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k : ℕ
⊢ ascFactorial 0 (k + 1).succ = 0
have rw : (0 + (k + 1)) * ascFactorial 0 (k + 1) = 0
Tactic: rw [ascFactorial_succ, zero_ascFactorial k, Nat.mul_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k : ℕ
rw : (0 + (k + 1)) * ascFactorial 0 (k + 1) = 0
⊢ ascFactorial 0 (k + 1).succ = 0
have rw₁ : (0 + (k + 1)) * 0 = 0
Tactic: rw [ascFactorial_succ, zero_ascFactorial k, Nat.mul_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k : ℕ
rw : (0 + (k + 1)) * ascFactorial 0 (k + 1) = 0
rw₁ : (0 + (k + 1)) * 0 = 0
⊢ ascFactorial 0 (k + 1).succ = 0
have rw₂ : Eq (α := ℕ) 0 0
Tactic: rw [ascFactorial_succ, zero_ascFactorial k, Nat.mul_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k : ℕ
⊢ ascFactorial 1 (k + 1) = (k + 1)!
have rw : (1 + k) * ascFactorial 1 k = (k + 1)!
Tactic: rw [ascFactorial_succ, one_ascFactorial k, Nat.add_comm, factorial_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k : ℕ
rw : (1 + k) * ascFactorial 1 k = (k + 1)!
⊢ ascFactorial 1 (k + 1) = (k + 1)!
have rw₁ : (1 + k) * k ! = (k + 1)!
Tactic: rw [ascFactorial_succ, one_ascFactorial k, Nat.add_comm, factorial_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k : ℕ
rw : (1 + k) * ascFactorial 1 k = (k + 1)!
rw₁ : (1 + k) * k ! = (k + 1)!
⊢ ascFactorial 1 (k + 1) = (k + 1)!
have rw₂ : (k + 1) * k ! = (k + 1)!
Tactic: rw [ascFactorial_succ, one_ascFactorial k, Nat.add_comm, factorial_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k : ℕ
rw : (1 + k) * ascFactorial 1 k = (k + 1)!
rw₁ : (1 + k) * k ! = (k + 1)!
rw₂ : (k + 1) * k ! = (k + 1)!
⊢ ascFactorial 1 (k + 1) = (k + 1)!
have rw₃ : (k + 1) * k ! = (k + 1) * k !
Tactic: rw [ascFactorial_succ, one_ascFactorial k, Nat.add_comm, factorial_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
⊢ n * n.succ.ascFactorial 0 = (n + 0) * n.ascFactorial 0
have rw : n * n.succ.ascFactorial 0 = n * n.ascFactorial 0
Tactic: rw [Nat.add_zero, ascFactorial_zero, ascFactorial_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
rw : n * n.succ.ascFactorial 0 = n * n.ascFactorial 0
⊢ n * n.succ.ascFactorial 0 = (n + 0) * n.ascFactorial 0
have rw₁ : n * 1 = n * n.ascFactorial 0
Tactic: rw [Nat.add_zero, ascFactorial_zero, ascFactorial_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
rw : n * n.succ.ascFactorial 0 = n * n.ascFactorial 0
rw₁ : n * 1 = n * n.ascFactorial 0
⊢ n * n.succ.ascFactorial 0 = (n + 0) * n.ascFactorial 0
have rw₂ : n * 1 = n * 1
Tactic: rw [Nat.add_zero, ascFactorial_zero, ascFactorial_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
⊢ n * n.succ.ascFactorial (k + 1) = (n + (k + 1)) * n.ascFactorial (k + 1)
have rw : n * ((n.succ + k) * n.succ.ascFactorial k) = (n + (k + 1)) * n.ascFactorial (k + 1)
Tactic: rw [ascFactorial, Nat.mul_left_comm, succ_ascFactorial n k, ascFactorial, succ_add,
    ← Nat.add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : n * ((n.succ + k) * n.succ.ascFactorial k) = (n + (k + 1)) * n.ascFactorial (k + 1)
⊢ n * n.succ.ascFactorial (k + 1) = (n + (k + 1)) * n.ascFactorial (k + 1)
have rw₁ : (n.succ + k) * (n * n.succ.ascFactorial k) = (n + (k + 1)) * n.ascFactorial (k + 1)
Tactic: rw [ascFactorial, Nat.mul_left_comm, succ_ascFactorial n k, ascFactorial, succ_add,
    ← Nat.add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : n * ((n.succ + k) * n.succ.ascFactorial k) = (n + (k + 1)) * n.ascFactorial (k + 1)
rw₁ : (n.succ + k) * (n * n.succ.ascFactorial k) = (n + (k + 1)) * n.ascFactorial (k + 1)
⊢ n * n.succ.ascFactorial (k + 1) = (n + (k + 1)) * n.ascFactorial (k + 1)
have rw₂ : (n.succ + k) * ((n + k) * n.ascFactorial k) = (n + (k + 1)) * n.ascFactorial (k + 1)
Tactic: rw [ascFactorial, Nat.mul_left_comm, succ_ascFactorial n k, ascFactorial, succ_add,
    ← Nat.add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : n * ((n.succ + k) * n.succ.ascFactorial k) = (n + (k + 1)) * n.ascFactorial (k + 1)
rw₁ : (n.succ + k) * (n * n.succ.ascFactorial k) = (n + (k + 1)) * n.ascFactorial (k + 1)
rw₂ : (n.succ + k) * ((n + k) * n.ascFactorial k) = (n + (k + 1)) * n.ascFactorial (k + 1)
⊢ n * n.succ.ascFactorial (k + 1) = (n + (k + 1)) * n.ascFactorial (k + 1)
have rw₃ : (n.succ + k) * ((n + k) * n.ascFactorial k) = (n + (k + 1)) * ((n + k) * n.ascFactorial k)
Tactic: rw [ascFactorial, Nat.mul_left_comm, succ_ascFactorial n k, ascFactorial, succ_add,
    ← Nat.add_assoc]