awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
rw₃ : (n.succ + k) * ((n + k) * n.ascFactorial k) = (n + (k + 1)) * ((n + k) * n.ascFactorial k)
⊢ n * n.succ.ascFactorial (k + 1) = (n + (k + 1)) * n.ascFactorial (k + 1)
have rw₄ : (n + k).succ * ((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]
-- 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)
rw₃ : (n.succ + k) * ((n + k) * n.ascFactorial k) = (n + (k + 1)) * ((n + k) * n.ascFactorial k)
rw₄ : (n + k).succ * ((n + k) * n.ascFactorial k) = (n + (k + 1)) * ((n + k) * n.ascFactorial k)
⊢ n * n.succ.ascFactorial (k + 1) = (n + (k + 1)) * n.ascFactorial (k + 1)
have rw₅ : (n + k).succ * ((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]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
⊢ n ! * (n + 1).ascFactorial 0 = (n + 0)!
have rw : n ! * 1 = (n + 0)!
Tactic: rw [ascFactorial_zero, Nat.add_zero, Nat.mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
rw : n ! * 1 = (n + 0)!
⊢ n ! * (n + 1).ascFactorial 0 = (n + 0)!
have rw₁ : n ! * 1 = n !
Tactic: rw [ascFactorial_zero, Nat.add_zero, Nat.mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
rw : n ! * 1 = (n + 0)!
rw₁ : n ! * 1 = n !
⊢ n ! * (n + 1).ascFactorial 0 = (n + 0)!
have rw₂ : n ! = n !
Tactic: rw [ascFactorial_zero, Nat.add_zero, Nat.mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
⊢ n ! * (n + 1).ascFactorial (k + 1) = (n + (k + 1))!
have rw : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + (k + 1))!
Tactic: rw [ascFactorial_succ, ← Nat.add_assoc, factorial_succ, Nat.mul_comm (n + 1 + k),
      ← Nat.mul_assoc, factorial_mul_ascFactorial n k, Nat.mul_comm, Nat.add_right_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + (k + 1))!
⊢ n ! * (n + 1).ascFactorial (k + 1) = (n + (k + 1))!
have rw₁ : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + k + 1)!
Tactic: rw [ascFactorial_succ, ← Nat.add_assoc, factorial_succ, Nat.mul_comm (n + 1 + k),
      ← Nat.mul_assoc, factorial_mul_ascFactorial n k, Nat.mul_comm, Nat.add_right_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + (k + 1))!
rw₁ : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + k + 1)!
⊢ n ! * (n + 1).ascFactorial (k + 1) = (n + (k + 1))!
have rw₂ : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + k + 1) * (n + k)!
Tactic: rw [ascFactorial_succ, ← Nat.add_assoc, factorial_succ, Nat.mul_comm (n + 1 + k),
      ← Nat.mul_assoc, factorial_mul_ascFactorial n k, Nat.mul_comm, Nat.add_right_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + (k + 1))!
rw₁ : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + k + 1)!
rw₂ : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + k + 1) * (n + k)!
⊢ n ! * (n + 1).ascFactorial (k + 1) = (n + (k + 1))!
have rw₃ : n ! * ((n + 1).ascFactorial k * (n + 1 + k)) = (n + k + 1) * (n + k)!
Tactic: rw [ascFactorial_succ, ← Nat.add_assoc, factorial_succ, Nat.mul_comm (n + 1 + k),
      ← Nat.mul_assoc, factorial_mul_ascFactorial n k, Nat.mul_comm, Nat.add_right_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + (k + 1))!
rw₁ : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + k + 1)!
rw₂ : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + k + 1) * (n + k)!
rw₃ : n ! * ((n + 1).ascFactorial k * (n + 1 + k)) = (n + k + 1) * (n + k)!
⊢ n ! * (n + 1).ascFactorial (k + 1) = (n + (k + 1))!
have rw₄ : n ! * (n + 1).ascFactorial k * (n + 1 + k) = (n + k + 1) * (n + k)!
Tactic: rw [ascFactorial_succ, ← Nat.add_assoc, factorial_succ, Nat.mul_comm (n + 1 + k),
      ← Nat.mul_assoc, factorial_mul_ascFactorial n k, Nat.mul_comm, Nat.add_right_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + (k + 1))!
rw₁ : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + k + 1)!
rw₂ : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + k + 1) * (n + k)!
rw₃ : n ! * ((n + 1).ascFactorial k * (n + 1 + k)) = (n + k + 1) * (n + k)!
rw₄ : n ! * (n + 1).ascFactorial k * (n + 1 + k) = (n + k + 1) * (n + k)!
⊢ n ! * (n + 1).ascFactorial (k + 1) = (n + (k + 1))!
have rw₅ : (n + k)! * (n + 1 + k) = (n + k + 1) * (n + k)!
Tactic: rw [ascFactorial_succ, ← Nat.add_assoc, factorial_succ, Nat.mul_comm (n + 1 + k),
      ← Nat.mul_assoc, factorial_mul_ascFactorial n k, Nat.mul_comm, Nat.add_right_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + (k + 1))!
rw₁ : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + k + 1)!
rw₂ : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + k + 1) * (n + k)!
rw₃ : n ! * ((n + 1).ascFactorial k * (n + 1 + k)) = (n + k + 1) * (n + k)!
rw₄ : n ! * (n + 1).ascFactorial k * (n + 1 + k) = (n + k + 1) * (n + k)!
rw₅ : (n + k)! * (n + 1 + k) = (n + k + 1) * (n + k)!
⊢ n ! * (n + 1).ascFactorial (k + 1) = (n + (k + 1))!
have rw₆ : (n + 1 + k) * (n + k)! = (n + k + 1) * (n + k)!
Tactic: rw [ascFactorial_succ, ← Nat.add_assoc, factorial_succ, Nat.mul_comm (n + 1 + k),
      ← Nat.mul_assoc, factorial_mul_ascFactorial n k, Nat.mul_comm, Nat.add_right_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + (k + 1))!
rw₁ : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + k + 1)!
rw₂ : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + k + 1) * (n + k)!
rw₃ : n ! * ((n + 1).ascFactorial k * (n + 1 + k)) = (n + k + 1) * (n + k)!
rw₄ : n ! * (n + 1).ascFactorial k * (n + 1 + k) = (n + k + 1) * (n + k)!
rw₅ : (n + k)! * (n + 1 + k) = (n + k + 1) * (n + k)!
rw₆ : (n + 1 + k) * (n + k)! = (n + k + 1) * (n + k)!
⊢ n ! * (n + 1).ascFactorial (k + 1) = (n + (k + 1))!
have rw₇ : (n + k + 1) * (n + k)! = (n + k + 1) * (n + k)!
Tactic: rw [ascFactorial_succ, ← Nat.add_assoc, factorial_succ, Nat.mul_comm (n + 1 + k),
      ← Nat.mul_assoc, factorial_mul_ascFactorial n k, Nat.mul_comm, Nat.add_right_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
h : 0 < n
⊢ (n - 1)! * n.ascFactorial k = (n + k - 1)!
have rw : n.pred ! * n.ascFactorial k = (n.pred + k)!
Tactic: rw [Nat.sub_add_comm h, Nat.sub_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
h : 0 < n
⊢ n.pred ! * n.ascFactorial k = (n.pred + k)!
have nth_rw : n.pred ! * (n - succ 0 + succ 0).ascFactorial k = (n.pred + k)!
Tactic: nth_rw 2 [Nat.eq_add_of_sub_eq h rfl]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
h : 0 < n
⊢ n.pred ! * (n - succ 0 + succ 0).ascFactorial k = (n.pred + k)!
have rw : n.pred ! * (n.pred + succ 0).ascFactorial k = (n.pred + k)!
Tactic: rw [Nat.sub_one, factorial_mul_ascFactorial]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
h : 0 < n
rw : n.pred ! * (n.pred + succ 0).ascFactorial k = (n.pred + k)!
⊢ n.pred ! * (n - succ 0 + succ 0).ascFactorial k = (n.pred + k)!
have rw₁ : (n.pred + k)! = (n.pred + k)!
Tactic: rw [Nat.sub_one, factorial_mul_ascFactorial]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
l k : ℕ
⊢ ascFactorial 0 l * (0 + l).ascFactorial k = ascFactorial 0 (l + k)
have zero : ascFactorial 0 0 * (HAdd.hAdd (α := ℕ) 0 0).ascFactorial k = ascFactorial 0 (0 + k)
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
l k : ℕ
zero : ascFactorial 0 0 * (HAdd.hAdd (α := ℕ) 0 0).ascFactorial k = ascFactorial 0 (0 + k)
⊢ ascFactorial 0 l * (0 + l).ascFactorial k = ascFactorial 0 (l + k)
have zero₁ : ∀ (n : ℕ), ascFactorial 0 (n + 1) * (0 + (n + 1)).ascFactorial k = ascFactorial 0 (n + 1 + k)
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
l k n' : ℕ
⊢ (n' + 1).ascFactorial l * (n' + 1 + l).ascFactorial k = (n' + 1).ascFactorial (l + k)
have succ : n' ! * ((n' + 1).ascFactorial l * (n' + 1 + l).ascFactorial k) = n' ! * (n' + 1).ascFactorial (l + k)
Tactic: apply Nat.mul_left_cancel (factorial_pos n')
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
l k n' : ℕ
⊢ n' ! * ((n' + 1).ascFactorial l * (n' + 1 + l).ascFactorial k) = n' ! * (n' + 1).ascFactorial (l + k)
have succ : (n' + l)! * (n' + (1 + l)).ascFactorial k = (n' + (l + k))!
Tactic: simp only [Nat.add_assoc, ← Nat.mul_assoc, factorial_mul_ascFactorial]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
l k n' : ℕ
⊢ (n' + l)! * (n' + (1 + l)).ascFactorial k = (n' + (l + k))!
have succ : (n' + l)! * (n' + (l + 1)).ascFactorial k = (n' + (l + k))!
Tactic: rw [Nat.add_comm 1 l, ← Nat.add_assoc, factorial_mul_ascFactorial, Nat.add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
l k n' : ℕ
succ : (n' + l)! * (n' + (l + 1)).ascFactorial k = (n' + (l + k))!
⊢ (n' + l)! * (n' + (1 + l)).ascFactorial k = (n' + (l + k))!
have succ₁ : (n' + l)! * (n' + l + 1).ascFactorial k = (n' + (l + k))!
Tactic: rw [Nat.add_comm 1 l, ← Nat.add_assoc, factorial_mul_ascFactorial, Nat.add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
l k n' : ℕ
succ : (n' + l)! * (n' + (l + 1)).ascFactorial k = (n' + (l + k))!
succ₁ : (n' + l)! * (n' + l + 1).ascFactorial k = (n' + (l + k))!
⊢ (n' + l)! * (n' + (1 + l)).ascFactorial k = (n' + (l + k))!
have succ₂ : (n' + l + k)! = (n' + (l + k))!
Tactic: rw [Nat.add_comm 1 l, ← Nat.add_assoc, factorial_mul_ascFactorial, Nat.add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
l k n' : ℕ
succ : (n' + l)! * (n' + (l + 1)).ascFactorial k = (n' + (l + k))!
succ₁ : (n' + l)! * (n' + l + 1).ascFactorial k = (n' + (l + k))!
succ₂ : (n' + l + k)! = (n' + (l + k))!
⊢ (n' + l)! * (n' + (1 + l)).ascFactorial k = (n' + (l + k))!
have succ₃ : (n' + (l + k))! = (n' + (l + k))!
Tactic: rw [Nat.add_comm 1 l, ← Nat.add_assoc, factorial_mul_ascFactorial, Nat.add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n l k : ℕ
⊢ n.ascFactorial l * (n + l).ascFactorial k = n.ascFactorial (l + k)
have zero : ascFactorial 0 l * (0 + l).ascFactorial k = ascFactorial 0 (l + k)
Tactic: cases n with
  | zero =>
    cases l
    · simp only [ascFactorial_zero, Nat.add_zero, Nat.one_mul, Nat.zero_add]
    · simp only [Nat.add_right_comm, zero_ascFactorial, Nat.zero_add, Nat.zero_mul]
  | succ n' =>
    apply Nat.mul_left_cancel (factorial_pos n')
    simp only [Nat.add_assoc, ← Nat.mul_assoc, factorial_mul_ascFactorial]
    rw [Nat.add_comm 1 l, ← Nat.add_assoc, factorial_mul_ascFactorial, Nat.add_assoc]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n l k : ℕ
zero : ascFactorial 0 l * (0 + l).ascFactorial k = ascFactorial 0 (l + k)
⊢ n.ascFactorial l * (n + l).ascFactorial k = n.ascFactorial (l + k)
have succ : ∀ (n' : ℕ), (n' + 1).ascFactorial l * (n' + 1 + l).ascFactorial k = (n' + 1).ascFactorial (l + k)
Tactic: cases n with
  | zero =>
    cases l
    · simp only [ascFactorial_zero, Nat.add_zero, Nat.one_mul, Nat.zero_add]
    · simp only [Nat.add_right_comm, zero_ascFactorial, Nat.zero_add, Nat.zero_mul]
  | succ n' =>
    apply Nat.mul_left_cancel (factorial_pos n')
    simp only [Nat.add_assoc, ← Nat.mul_assoc, factorial_mul_ascFactorial]
    rw [Nat.add_comm 1 l, ← Nat.add_assoc, factorial_mul_ascFactorial, Nat.add_assoc]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
⊢ (n - k) * (n - k + 1).ascFactorial k = (n - k).ascFactorial (k + 1)
have rw : (n - k + k) * (n - k).ascFactorial k = (n - k).ascFactorial (k + 1)
Tactic: rw [succ_ascFactorial, ascFactorial_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : (n - k + k) * (n - k).ascFactorial k = (n - k).ascFactorial (k + 1)
⊢ (n - k) * (n - k + 1).ascFactorial k = (n - k).ascFactorial (k + 1)
have rw₁ : (n - k + k) * (n - k).ascFactorial k = (n - k + k) * (n - k).ascFactorial k
Tactic: rw [succ_ascFactorial, ascFactorial_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
⊢ HPow.hPow (β := ℕ) n 0 ≤ n.ascFactorial 0
have rw : HPow.hPow (β := ℕ) n 0 ≤ 1
Tactic: rw [ascFactorial_zero, Nat.pow_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
rw : HPow.hPow (β := ℕ) n 0 ≤ 1
⊢ HPow.hPow (β := ℕ) n 0 ≤ n.ascFactorial 0
have rw₁ : LE.le (α := ℕ) 1 1
Tactic: rw [ascFactorial_zero, Nat.pow_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
⊢ n ^ (k + 1) ≤ n.ascFactorial (k + 1)
have rw : n * n ^ k ≤ n * n.succ.ascFactorial k
Tactic: rw [Nat.pow_succ, Nat.mul_comm, ascFactorial_succ, ← succ_ascFactorial]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
⊢ (n + 1) ^ (k + 2) < (n + 1).ascFactorial (k + 2)
have rw : (n + 1) * (n + 1) ^ (k + 1) < (n + 1 + (k + 1)) * (n + 1).ascFactorial (k + 1)
Tactic: rw [Nat.pow_succ, ascFactorial, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
⊢ (n + 1).ascFactorial 0 ≤ HPow.hPow (β := ℕ) (n + 0) 0
have rw : 1 ≤ HPow.hPow (β := ℕ) (n + 0) 0
Tactic: rw [ascFactorial_zero, Nat.pow_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
rw : 1 ≤ HPow.hPow (β := ℕ) (n + 0) 0
⊢ (n + 1).ascFactorial 0 ≤ HPow.hPow (β := ℕ) (n + 0) 0
have rw₁ : LE.le (α := ℕ) 1 1
Tactic: rw [ascFactorial_zero, Nat.pow_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
⊢ (n + 1).ascFactorial (k + 1) ≤ (n + (k + 1)) ^ (k + 1)
have rw : (n + 1).ascFactorial k * (n + k + 1) ≤ (n + k + 1) ^ k * (n + k + 1)
Tactic: rw [ascFactorial_succ, Nat.pow_succ, Nat.mul_comm, ← Nat.add_assoc, Nat.add_right_comm n 1 k]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
h : 2 ≤ k + 2
⊢ (n + 1).ascFactorial (k + 2) < (n + (k + 2)) ^ (k + 2)
have rw : (n + (k + 1).succ) * (n + 1).ascFactorial (k + 1) < (n + (k + 2)) * (n + (k + 2)) ^ (k + 1)
Tactic: rw [Nat.pow_succ, Nat.mul_comm, ascFactorial_succ, succ_add_eq_add_succ n (k + 1)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k : ℕ
⊢ descFactorial 0 (k + 1) = 0
have rw : (0 - k) * descFactorial 0 k = 0
Tactic: rw [descFactorial_succ, Nat.zero_sub, Nat.zero_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k : ℕ
rw : (0 - k) * descFactorial 0 k = 0
⊢ descFactorial 0 (k + 1) = 0
have rw₁ : 0 * descFactorial 0 k = 0
Tactic: rw [descFactorial_succ, Nat.zero_sub, Nat.zero_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k : ℕ
rw : (0 - k) * descFactorial 0 k = 0
rw₁ : 0 * descFactorial 0 k = 0
⊢ descFactorial 0 (k + 1) = 0
have rw₂ : Eq (α := ℕ) 0 0
Tactic: rw [descFactorial_succ, Nat.zero_sub, Nat.zero_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
⊢ (n + 1).descFactorial (HAdd.hAdd (α := ℕ) 0 1) = (n + 1) * n.descFactorial 0
have rw : (n + 1).descFactorial (HAdd.hAdd (α := ℕ) 0 1) = (n + 1) * 1
Tactic: rw [descFactorial_zero, descFactorial_one, Nat.mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
rw : (n + 1).descFactorial (HAdd.hAdd (α := ℕ) 0 1) = (n + 1) * 1
⊢ (n + 1).descFactorial (HAdd.hAdd (α := ℕ) 0 1) = (n + 1) * n.descFactorial 0
have rw₁ : n + 1 = (n + 1) * 1
Tactic: rw [descFactorial_zero, descFactorial_one, Nat.mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
rw : (n + 1).descFactorial (HAdd.hAdd (α := ℕ) 0 1) = (n + 1) * 1
rw₁ : n + 1 = (n + 1) * 1
⊢ (n + 1).descFactorial (HAdd.hAdd (α := ℕ) 0 1) = (n + 1) * n.descFactorial 0
have rw₂ : n + 1 = n + 1
Tactic: rw [descFactorial_zero, descFactorial_one, Nat.mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
⊢ (n + 1).descFactorial (k.succ + 1) = (n + 1) * n.descFactorial k.succ
have rw : (n + 1 - (k + 1)) * (n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial k.succ
Tactic: rw [descFactorial_succ, succ_descFactorial_succ _ k, descFactorial_succ, succ_sub_succ,
      Nat.mul_left_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : (n + 1 - (k + 1)) * (n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial k.succ
⊢ (n + 1).descFactorial (k.succ + 1) = (n + 1) * n.descFactorial k.succ
have rw₁ : (n + 1 - (k + 1)) * ((n + 1) * n.descFactorial k) = (n + 1) * n.descFactorial k.succ
Tactic: rw [descFactorial_succ, succ_descFactorial_succ _ k, descFactorial_succ, succ_sub_succ,
      Nat.mul_left_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : (n + 1 - (k + 1)) * (n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial k.succ
rw₁ : (n + 1 - (k + 1)) * ((n + 1) * n.descFactorial k) = (n + 1) * n.descFactorial k.succ
⊢ (n + 1).descFactorial (k.succ + 1) = (n + 1) * n.descFactorial k.succ
have rw₂ : (n + 1 - (k + 1)) * ((n + 1) * n.descFactorial k) = (n + 1) * ((n - k) * n.descFactorial k)
Tactic: rw [descFactorial_succ, succ_descFactorial_succ _ k, descFactorial_succ, succ_sub_succ,
      Nat.mul_left_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : (n + 1 - (k + 1)) * (n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial k.succ
rw₁ : (n + 1 - (k + 1)) * ((n + 1) * n.descFactorial k) = (n + 1) * n.descFactorial k.succ
rw₂ : (n + 1 - (k + 1)) * ((n + 1) * n.descFactorial k) = (n + 1) * ((n - k) * n.descFactorial k)
⊢ (n + 1).descFactorial (k.succ + 1) = (n + 1) * n.descFactorial k.succ
have rw₃ : (n - k) * ((n + 1) * n.descFactorial k) = (n + 1) * ((n - k) * n.descFactorial k)
Tactic: rw [descFactorial_succ, succ_descFactorial_succ _ k, descFactorial_succ, succ_sub_succ,
      Nat.mul_left_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : (n + 1 - (k + 1)) * (n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial k.succ
rw₁ : (n + 1 - (k + 1)) * ((n + 1) * n.descFactorial k) = (n + 1) * n.descFactorial k.succ
rw₂ : (n + 1 - (k + 1)) * ((n + 1) * n.descFactorial k) = (n + 1) * ((n - k) * n.descFactorial k)
rw₃ : (n - k) * ((n + 1) * n.descFactorial k) = (n + 1) * ((n - k) * n.descFactorial k)
⊢ (n + 1).descFactorial (k.succ + 1) = (n + 1) * n.descFactorial k.succ
have rw₄ : (n + 1) * ((n - k) * n.descFactorial k) = (n + 1) * ((n - k) * n.descFactorial k)
Tactic: rw [descFactorial_succ, succ_descFactorial_succ _ k, descFactorial_succ, succ_sub_succ,
      Nat.mul_left_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
⊢ (n + 1 - 0) * (n + 1).descFactorial 0 = (n + 1) * n.descFactorial 0
have rw : (n + 1) * (n + 1).descFactorial 0 = (n + 1) * n.descFactorial 0
Tactic: rw [Nat.sub_zero, descFactorial_zero, descFactorial_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
rw : (n + 1) * (n + 1).descFactorial 0 = (n + 1) * n.descFactorial 0
⊢ (n + 1 - 0) * (n + 1).descFactorial 0 = (n + 1) * n.descFactorial 0
have rw₁ : (n + 1) * 1 = (n + 1) * n.descFactorial 0
Tactic: rw [Nat.sub_zero, descFactorial_zero, descFactorial_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
rw : (n + 1) * (n + 1).descFactorial 0 = (n + 1) * n.descFactorial 0
rw₁ : (n + 1) * 1 = (n + 1) * n.descFactorial 0
⊢ (n + 1 - 0) * (n + 1).descFactorial 0 = (n + 1) * n.descFactorial 0
have rw₂ : (n + 1) * 1 = (n + 1) * 1
Tactic: rw [Nat.sub_zero, descFactorial_zero, descFactorial_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
⊢ (n + 1 - (k + 1)) * (n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial (k + 1)
have rw : (n + 1 - (k + 1)) * ((n + 1 - k) * (n + 1).descFactorial k) = (n + 1) * n.descFactorial (k + 1)
Tactic: rw [descFactorial, succ_descFactorial _ k, descFactorial_succ, succ_sub_succ, Nat.mul_left_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : (n + 1 - (k + 1)) * ((n + 1 - k) * (n + 1).descFactorial k) = (n + 1) * n.descFactorial (k + 1)
⊢ (n + 1 - (k + 1)) * (n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial (k + 1)
have rw₁ : (n + 1 - (k + 1)) * ((n + 1) * n.descFactorial k) = (n + 1) * n.descFactorial (k + 1)
Tactic: rw [descFactorial, succ_descFactorial _ k, descFactorial_succ, succ_sub_succ, Nat.mul_left_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : (n + 1 - (k + 1)) * ((n + 1 - k) * (n + 1).descFactorial k) = (n + 1) * n.descFactorial (k + 1)
rw₁ : (n + 1 - (k + 1)) * ((n + 1) * n.descFactorial k) = (n + 1) * n.descFactorial (k + 1)
⊢ (n + 1 - (k + 1)) * (n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial (k + 1)
have rw₂ : (n + 1 - (k + 1)) * ((n + 1) * n.descFactorial k) = (n + 1) * ((n - k) * n.descFactorial k)
Tactic: rw [descFactorial, succ_descFactorial _ k, descFactorial_succ, succ_sub_succ, Nat.mul_left_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : (n + 1 - (k + 1)) * ((n + 1 - k) * (n + 1).descFactorial k) = (n + 1) * n.descFactorial (k + 1)
rw₁ : (n + 1 - (k + 1)) * ((n + 1) * n.descFactorial k) = (n + 1) * n.descFactorial (k + 1)
rw₂ : (n + 1 - (k + 1)) * ((n + 1) * n.descFactorial k) = (n + 1) * ((n - k) * n.descFactorial k)
⊢ (n + 1 - (k + 1)) * (n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial (k + 1)
have rw₃ : (n - k) * ((n + 1) * n.descFactorial k) = (n + 1) * ((n - k) * n.descFactorial k)
Tactic: rw [descFactorial, succ_descFactorial _ k, descFactorial_succ, succ_sub_succ, Nat.mul_left_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : (n + 1 - (k + 1)) * ((n + 1 - k) * (n + 1).descFactorial k) = (n + 1) * n.descFactorial (k + 1)
rw₁ : (n + 1 - (k + 1)) * ((n + 1) * n.descFactorial k) = (n + 1) * n.descFactorial (k + 1)
rw₂ : (n + 1 - (k + 1)) * ((n + 1) * n.descFactorial k) = (n + 1) * ((n - k) * n.descFactorial k)
rw₃ : (n - k) * ((n + 1) * n.descFactorial k) = (n + 1) * ((n - k) * n.descFactorial k)
⊢ (n + 1 - (k + 1)) * (n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial (k + 1)
have rw₄ : (n + 1) * ((n - k) * n.descFactorial k) = (n + 1) * ((n - k) * n.descFactorial k)
Tactic: rw [descFactorial, succ_descFactorial _ k, descFactorial_succ, succ_sub_succ, Nat.mul_left_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
⊢ descFactorial 0 0 = 0!
have rw : 1 = 0!
Tactic: rw [descFactorial_zero, factorial_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
rw : 1 = 0!
⊢ descFactorial 0 0 = 0!
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [descFactorial_zero, factorial_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
⊢ n.succ.descFactorial n.succ = n.succ !
have rw : (n + 1) * n.descFactorial n = n.succ !
Tactic: rw [succ_descFactorial_succ, descFactorial_self n, factorial_succ]