awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
rw : (n + 1) * n.descFactorial n = n.succ !
⊢ n.succ.descFactorial n.succ = n.succ !
have rw₁ : (n + 1) * n ! = n.succ !
Tactic: rw [succ_descFactorial_succ, descFactorial_self n, factorial_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
rw : (n + 1) * n.descFactorial n = n.succ !
rw₁ : (n + 1) * n ! = n.succ !
⊢ n.succ.descFactorial n.succ = n.succ !
have rw₂ : (n + 1) * n ! = (n + 1) * n !
Tactic: rw [succ_descFactorial_succ, descFactorial_self n, factorial_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
⊢ n.descFactorial k.succ = 0 ↔ n < k.succ
have rw : n ≤ k → n ≠ k → n ≤ k
Tactic: rw [descFactorial_succ, mul_eq_zero, descFactorial_eq_zero_iff_lt, Nat.lt_succ_iff,
      Nat.sub_eq_zero_iff_le, Nat.lt_iff_le_and_ne, or_iff_left_iff_imp, and_imp]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
⊢ (n + 0).descFactorial 0 = (n + 1).ascFactorial 0
have rw : (n + 0).descFactorial 0 = 1
Tactic: rw [ascFactorial_zero, descFactorial_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
rw : (n + 0).descFactorial 0 = 1
⊢ (n + 0).descFactorial 0 = (n + 1).ascFactorial 0
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [ascFactorial_zero, descFactorial_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
⊢ (n + k.succ).descFactorial k.succ = (n + 1).ascFactorial k.succ
have rw : (n + k).succ.descFactorial k.succ = (n + 1).ascFactorial k.succ
Tactic: rw [Nat.add_succ, succ_descFactorial_succ, ascFactorial_succ,
      add_descFactorial_eq_ascFactorial _ k, Nat.add_right_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : (n + k).succ.descFactorial k.succ = (n + 1).ascFactorial k.succ
⊢ (n + k.succ).descFactorial k.succ = (n + 1).ascFactorial k.succ
have rw₁ : (n + k + 1) * (n + k).descFactorial k = (n + 1).ascFactorial k.succ
Tactic: rw [Nat.add_succ, succ_descFactorial_succ, ascFactorial_succ,
      add_descFactorial_eq_ascFactorial _ k, Nat.add_right_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : (n + k).succ.descFactorial k.succ = (n + 1).ascFactorial k.succ
rw₁ : (n + k + 1) * (n + k).descFactorial k = (n + 1).ascFactorial k.succ
⊢ (n + k.succ).descFactorial k.succ = (n + 1).ascFactorial k.succ
have rw₂ : (n + k + 1) * (n + k).descFactorial k = (n + 1 + k) * (n + 1).ascFactorial k
Tactic: rw [Nat.add_succ, succ_descFactorial_succ, ascFactorial_succ,
      add_descFactorial_eq_ascFactorial _ k, Nat.add_right_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : (n + k).succ.descFactorial k.succ = (n + 1).ascFactorial k.succ
rw₁ : (n + k + 1) * (n + k).descFactorial k = (n + 1).ascFactorial k.succ
rw₂ : (n + k + 1) * (n + k).descFactorial k = (n + 1 + k) * (n + 1).ascFactorial k
⊢ (n + k.succ).descFactorial k.succ = (n + 1).ascFactorial k.succ
have rw₃ : (n + k + 1) * (n + 1).ascFactorial k = (n + 1 + k) * (n + 1).ascFactorial k
Tactic: rw [Nat.add_succ, succ_descFactorial_succ, ascFactorial_succ,
      add_descFactorial_eq_ascFactorial _ k, Nat.add_right_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : (n + k).succ.descFactorial k.succ = (n + 1).ascFactorial k.succ
rw₁ : (n + k + 1) * (n + k).descFactorial k = (n + 1).ascFactorial k.succ
rw₂ : (n + k + 1) * (n + k).descFactorial k = (n + 1 + k) * (n + 1).ascFactorial k
rw₃ : (n + k + 1) * (n + 1).ascFactorial k = (n + 1 + k) * (n + 1).ascFactorial k
⊢ (n + k.succ).descFactorial k.succ = (n + 1).ascFactorial k.succ
have rw₄ : (n + 1 + k) * (n + 1).ascFactorial k = (n + 1 + k) * (n + 1).ascFactorial k
Tactic: rw [Nat.add_succ, succ_descFactorial_succ, ascFactorial_succ,
      add_descFactorial_eq_ascFactorial _ k, Nat.add_right_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
⊢ (n + 0 - 1).descFactorial 0 = n.ascFactorial 0
have rw : (n + 0 - 1).descFactorial 0 = 1
Tactic: rw [ascFactorial_zero, descFactorial_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
rw : (n + 0 - 1).descFactorial 0 = 1
⊢ (n + 0 - 1).descFactorial 0 = n.ascFactorial 0
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [ascFactorial_zero, descFactorial_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
⊢ (n + k.succ - 1).descFactorial k.succ = n.ascFactorial k.succ
have rw : (n + k.succ - 1 - k) * (n + k.succ - 1).descFactorial k = n.ascFactorial k.succ
Tactic: rw [descFactorial_succ, ascFactorial_succ, ← succ_add_eq_add_succ,
      add_descFactorial_eq_ascFactorial' _ k, ← succ_ascFactorial, succ_add_sub_one,
      Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : (n + k.succ - 1 - k) * (n + k.succ - 1).descFactorial k = n.ascFactorial k.succ
⊢ (n + k.succ - 1).descFactorial k.succ = n.ascFactorial k.succ
have rw₁ : (n + k.succ - 1 - k) * (n + k.succ - 1).descFactorial k = (n + k) * n.ascFactorial k
Tactic: rw [descFactorial_succ, ascFactorial_succ, ← succ_add_eq_add_succ,
      add_descFactorial_eq_ascFactorial' _ k, ← succ_ascFactorial, succ_add_sub_one,
      Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : (n + k.succ - 1 - k) * (n + k.succ - 1).descFactorial k = n.ascFactorial k.succ
rw₁ : (n + k.succ - 1 - k) * (n + k.succ - 1).descFactorial k = (n + k) * n.ascFactorial k
⊢ (n + k.succ - 1).descFactorial k.succ = n.ascFactorial k.succ
have rw₂ : (n.succ + k - 1 - k) * (n.succ + k - 1).descFactorial k = (n + k) * n.ascFactorial k
Tactic: rw [descFactorial_succ, ascFactorial_succ, ← succ_add_eq_add_succ,
      add_descFactorial_eq_ascFactorial' _ k, ← succ_ascFactorial, succ_add_sub_one,
      Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : (n + k.succ - 1 - k) * (n + k.succ - 1).descFactorial k = n.ascFactorial k.succ
rw₁ : (n + k.succ - 1 - k) * (n + k.succ - 1).descFactorial k = (n + k) * n.ascFactorial k
rw₂ : (n.succ + k - 1 - k) * (n.succ + k - 1).descFactorial k = (n + k) * n.ascFactorial k
⊢ (n + k.succ - 1).descFactorial k.succ = n.ascFactorial k.succ
have rw₃ : (n.succ + k - 1 - k) * n.succ.ascFactorial k = (n + k) * n.ascFactorial k
Tactic: rw [descFactorial_succ, ascFactorial_succ, ← succ_add_eq_add_succ,
      add_descFactorial_eq_ascFactorial' _ k, ← succ_ascFactorial, succ_add_sub_one,
      Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : (n + k.succ - 1 - k) * (n + k.succ - 1).descFactorial k = n.ascFactorial k.succ
rw₁ : (n + k.succ - 1 - k) * (n + k.succ - 1).descFactorial k = (n + k) * n.ascFactorial k
rw₂ : (n.succ + k - 1 - k) * (n.succ + k - 1).descFactorial k = (n + k) * n.ascFactorial k
rw₃ : (n.succ + k - 1 - k) * n.succ.ascFactorial k = (n + k) * n.ascFactorial k
⊢ (n + k.succ - 1).descFactorial k.succ = n.ascFactorial k.succ
have rw₄ : (n.succ + k - 1 - k) * n.succ.ascFactorial k = n * n.succ.ascFactorial k
Tactic: rw [descFactorial_succ, ascFactorial_succ, ← succ_add_eq_add_succ,
      add_descFactorial_eq_ascFactorial' _ k, ← succ_ascFactorial, succ_add_sub_one,
      Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : (n + k.succ - 1 - k) * (n + k.succ - 1).descFactorial k = n.ascFactorial k.succ
rw₁ : (n + k.succ - 1 - k) * (n + k.succ - 1).descFactorial k = (n + k) * n.ascFactorial k
rw₂ : (n.succ + k - 1 - k) * (n.succ + k - 1).descFactorial k = (n + k) * n.ascFactorial k
rw₃ : (n.succ + k - 1 - k) * n.succ.ascFactorial k = (n + k) * n.ascFactorial k
rw₄ : (n.succ + k - 1 - k) * n.succ.ascFactorial k = n * n.succ.ascFactorial k
⊢ (n + k.succ - 1).descFactorial k.succ = n.ascFactorial k.succ
have rw₅ : (n + k - k) * n.succ.ascFactorial k = n * n.succ.ascFactorial k
Tactic: rw [descFactorial_succ, ascFactorial_succ, ← succ_add_eq_add_succ,
      add_descFactorial_eq_ascFactorial' _ k, ← succ_ascFactorial, succ_add_sub_one,
      Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
rw : (n + k.succ - 1 - k) * (n + k.succ - 1).descFactorial k = n.ascFactorial k.succ
rw₁ : (n + k.succ - 1 - k) * (n + k.succ - 1).descFactorial k = (n + k) * n.ascFactorial k
rw₂ : (n.succ + k - 1 - k) * (n.succ + k - 1).descFactorial k = (n + k) * n.ascFactorial k
rw₃ : (n.succ + k - 1 - k) * n.succ.ascFactorial k = (n + k) * n.ascFactorial k
rw₄ : (n.succ + k - 1 - k) * n.succ.ascFactorial k = n * n.succ.ascFactorial k
rw₅ : (n + k - k) * n.succ.ascFactorial k = n * n.succ.ascFactorial k
⊢ (n + k.succ - 1).descFactorial k.succ = n.ascFactorial k.succ
have rw₆ : n * n.succ.ascFactorial k = n * n.succ.ascFactorial k
Tactic: rw [descFactorial_succ, ascFactorial_succ, ← succ_add_eq_add_succ,
      add_descFactorial_eq_ascFactorial' _ k, ← succ_ascFactorial, succ_add_sub_one,
      Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
h : 0 ≤ n
⊢ (n - 0)! * n.descFactorial 0 = n !
have rw : (n - 0)! * 1 = n !
Tactic: rw [descFactorial_zero, Nat.mul_one, Nat.sub_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
h : 0 ≤ n
rw : (n - 0)! * 1 = n !
⊢ (n - 0)! * n.descFactorial 0 = n !
have rw₁ : (n - 0)! = n !
Tactic: rw [descFactorial_zero, Nat.mul_one, Nat.sub_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
h : 0 ≤ n
rw : (n - 0)! * 1 = n !
rw₁ : (n - 0)! = n !
⊢ (n - 0)! * n.descFactorial 0 = n !
have rw₂ : n ! = n !
Tactic: rw [descFactorial_zero, Nat.mul_one, Nat.sub_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k : ℕ
h : k.succ ≤ 0
⊢ (0 - k.succ)! * descFactorial 0 k.succ = 0!
have exfalso : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
h : k.succ ≤ n.succ
⊢ (n.succ - k.succ)! * n.succ.descFactorial k.succ = n.succ !
have rw : (n.succ - k.succ)! * ((n + 1) * n.descFactorial k) = n.succ !
Tactic: rw [succ_descFactorial_succ, succ_sub_succ, ← Nat.mul_assoc, Nat.mul_comm (n - k)!,
      Nat.mul_assoc, factorial_mul_descFactorial (Nat.succ_le_succ_iff.1 h), factorial_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
h : k.succ ≤ n.succ
rw : (n.succ - k.succ)! * ((n + 1) * n.descFactorial k) = n.succ !
⊢ (n.succ - k.succ)! * n.succ.descFactorial k.succ = n.succ !
have rw₁ : (n - k)! * ((n + 1) * n.descFactorial k) = n.succ !
Tactic: rw [succ_descFactorial_succ, succ_sub_succ, ← Nat.mul_assoc, Nat.mul_comm (n - k)!,
      Nat.mul_assoc, factorial_mul_descFactorial (Nat.succ_le_succ_iff.1 h), factorial_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
h : k.succ ≤ n.succ
rw : (n.succ - k.succ)! * ((n + 1) * n.descFactorial k) = n.succ !
rw₁ : (n - k)! * ((n + 1) * n.descFactorial k) = n.succ !
⊢ (n.succ - k.succ)! * n.succ.descFactorial k.succ = n.succ !
have rw₂ : (n - k)! * (n + 1) * n.descFactorial k = n.succ !
Tactic: rw [succ_descFactorial_succ, succ_sub_succ, ← Nat.mul_assoc, Nat.mul_comm (n - k)!,
      Nat.mul_assoc, factorial_mul_descFactorial (Nat.succ_le_succ_iff.1 h), factorial_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
h : k.succ ≤ n.succ
rw : (n.succ - k.succ)! * ((n + 1) * n.descFactorial k) = n.succ !
rw₁ : (n - k)! * ((n + 1) * n.descFactorial k) = n.succ !
rw₂ : (n - k)! * (n + 1) * n.descFactorial k = n.succ !
⊢ (n.succ - k.succ)! * n.succ.descFactorial k.succ = n.succ !
have rw₃ : (n + 1) * (n - k)! * n.descFactorial k = n.succ !
Tactic: rw [succ_descFactorial_succ, succ_sub_succ, ← Nat.mul_assoc, Nat.mul_comm (n - k)!,
      Nat.mul_assoc, factorial_mul_descFactorial (Nat.succ_le_succ_iff.1 h), factorial_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
h : k.succ ≤ n.succ
rw : (n.succ - k.succ)! * ((n + 1) * n.descFactorial k) = n.succ !
rw₁ : (n - k)! * ((n + 1) * n.descFactorial k) = n.succ !
rw₂ : (n - k)! * (n + 1) * n.descFactorial k = n.succ !
rw₃ : (n + 1) * (n - k)! * n.descFactorial k = n.succ !
⊢ (n.succ - k.succ)! * n.succ.descFactorial k.succ = n.succ !
have rw₄ : (n + 1) * ((n - k)! * n.descFactorial k) = n.succ !
Tactic: rw [succ_descFactorial_succ, succ_sub_succ, ← Nat.mul_assoc, Nat.mul_comm (n - k)!,
      Nat.mul_assoc, factorial_mul_descFactorial (Nat.succ_le_succ_iff.1 h), factorial_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
h : k.succ ≤ n.succ
rw : (n.succ - k.succ)! * ((n + 1) * n.descFactorial k) = n.succ !
rw₁ : (n - k)! * ((n + 1) * n.descFactorial k) = n.succ !
rw₂ : (n - k)! * (n + 1) * n.descFactorial k = n.succ !
rw₃ : (n + 1) * (n - k)! * n.descFactorial k = n.succ !
rw₄ : (n + 1) * ((n - k)! * n.descFactorial k) = n.succ !
⊢ (n.succ - k.succ)! * n.succ.descFactorial k.succ = n.succ !
have rw₅ : (n + 1) * n ! = n.succ !
Tactic: rw [succ_descFactorial_succ, succ_sub_succ, ← Nat.mul_assoc, Nat.mul_comm (n - k)!,
      Nat.mul_assoc, factorial_mul_descFactorial (Nat.succ_le_succ_iff.1 h), factorial_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
h : k.succ ≤ n.succ
rw : (n.succ - k.succ)! * ((n + 1) * n.descFactorial k) = n.succ !
rw₁ : (n - k)! * ((n + 1) * n.descFactorial k) = n.succ !
rw₂ : (n - k)! * (n + 1) * n.descFactorial k = n.succ !
rw₃ : (n + 1) * (n - k)! * n.descFactorial k = n.succ !
rw₄ : (n + 1) * ((n - k)! * n.descFactorial k) = n.succ !
rw₅ : (n + 1) * n ! = n.succ !
⊢ (n.succ - k.succ)! * n.succ.descFactorial k.succ = n.succ !
have rw₆ : (n + 1) * n ! = (n + 1) * n !
Tactic: rw [succ_descFactorial_succ, succ_sub_succ, ← Nat.mul_assoc, Nat.mul_comm (n - k)!,
      Nat.mul_assoc, factorial_mul_descFactorial (Nat.succ_le_succ_iff.1 h), factorial_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k m n : ℕ
hkm : k ≤ m
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m
have pos : ∀ (hmn : m ≤ n), (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m
Tactic: by_cases hmn : m ≤ n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k m n : ℕ
hkm : k ≤ m
pos : ∀ (hmn : m ≤ n), (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m
have neg : ∀ (hmn : ¬m ≤ n), (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m
Tactic: by_cases hmn : m ≤ n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m
have pos : (n - m)! * ((n - k).descFactorial (m - k) * n.descFactorial k) = (n - m)! * n.descFactorial m
Tactic: apply Nat.mul_left_cancel (n - m).factorial_pos
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ (n - m)! * ((n - k).descFactorial (m - k) * n.descFactorial k) = (n - m)! * n.descFactorial m
have pos : (n - m)! * ((n - k).descFactorial (m - k) * n.descFactorial k) = n !
Tactic: rw [factorial_mul_descFactorial hmn, show n - m = (n - k) - (m - k) by lia, ← Nat.mul_assoc,
      factorial_mul_descFactorial (show m - k ≤ n - k by lia),
      factorial_mul_descFactorial (le_trans hkm hmn)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
pos : (n - m)! * ((n - k).descFactorial (m - k) * n.descFactorial k) = n !
⊢ (n - m)! * ((n - k).descFactorial (m - k) * n.descFactorial k) = (n - m)! * n.descFactorial m
have pos₁ : (n - k - (m - k))! * ((n - k).descFactorial (m - k) * n.descFactorial k) = n !
Tactic: rw [factorial_mul_descFactorial hmn, show n - m = (n - k) - (m - k) by lia, ← Nat.mul_assoc,
      factorial_mul_descFactorial (show m - k ≤ n - k by lia),
      factorial_mul_descFactorial (le_trans hkm hmn)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
pos : (n - m)! * ((n - k).descFactorial (m - k) * n.descFactorial k) = n !
pos₁ : (n - k - (m - k))! * ((n - k).descFactorial (m - k) * n.descFactorial k) = n !
⊢ (n - m)! * ((n - k).descFactorial (m - k) * n.descFactorial k) = (n - m)! * n.descFactorial m
have pos₂ : (n - k - (m - k))! * (n - k).descFactorial (m - k) * n.descFactorial k = n !
Tactic: rw [factorial_mul_descFactorial hmn, show n - m = (n - k) - (m - k) by lia, ← Nat.mul_assoc,
      factorial_mul_descFactorial (show m - k ≤ n - k by lia),
      factorial_mul_descFactorial (le_trans hkm hmn)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
pos : (n - m)! * ((n - k).descFactorial (m - k) * n.descFactorial k) = n !
pos₁ : (n - k - (m - k))! * ((n - k).descFactorial (m - k) * n.descFactorial k) = n !
pos₂ : (n - k - (m - k))! * (n - k).descFactorial (m - k) * n.descFactorial k = n !
⊢ (n - m)! * ((n - k).descFactorial (m - k) * n.descFactorial k) = (n - m)! * n.descFactorial m
have pos₃ : (n - k)! * n.descFactorial k = n !
Tactic: rw [factorial_mul_descFactorial hmn, show n - m = (n - k) - (m - k) by lia, ← Nat.mul_assoc,
      factorial_mul_descFactorial (show m - k ≤ n - k by lia),
      factorial_mul_descFactorial (le_trans hkm hmn)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
pos : (n - m)! * ((n - k).descFactorial (m - k) * n.descFactorial k) = n !
pos₁ : (n - k - (m - k))! * ((n - k).descFactorial (m - k) * n.descFactorial k) = n !
pos₂ : (n - k - (m - k))! * (n - k).descFactorial (m - k) * n.descFactorial k = n !
pos₃ : (n - k)! * n.descFactorial k = n !
⊢ (n - m)! * ((n - k).descFactorial (m - k) * n.descFactorial k) = (n - m)! * n.descFactorial m
have pos₄ : n ! = n !
Tactic: rw [factorial_mul_descFactorial hmn, show n - m = (n - k) - (m - k) by lia, ← Nat.mul_assoc,
      factorial_mul_descFactorial (show m - k ≤ n - k by lia),
      factorial_mul_descFactorial (le_trans hkm hmn)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m
have neg : (n - k).descFactorial (m - k) * n.descFactorial k = 0
Tactic: rw [descFactorial_eq_zero_iff_lt.mpr (show n < m by lia)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = 0
have pos : ∀ (hkn : k ≤ n), (n - k).descFactorial (m - k) * n.descFactorial k = 0
Tactic: by_cases hkn : k ≤ n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
pos : ∀ (hkn : k ≤ n), (n - k).descFactorial (m - k) * n.descFactorial k = 0
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = 0
have neg : ∀ (hkn : ¬k ≤ n), (n - k).descFactorial (m - k) * n.descFactorial k = 0
Tactic: by_cases hkn : k ≤ n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : k ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = 0
have pos : 0 * n.descFactorial k = 0
Tactic: rw [descFactorial_eq_zero_iff_lt.mpr (show n - k < m - k by lia), Nat.zero_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : k ≤ n
pos : 0 * n.descFactorial k = 0
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = 0
have pos₁ : Eq (α := ℕ) 0 0
Tactic: rw [descFactorial_eq_zero_iff_lt.mpr (show n - k < m - k by lia), Nat.zero_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : ¬k ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = 0
have neg : (n - k).descFactorial (m - k) * 0 = 0
Tactic: rw [descFactorial_eq_zero_iff_lt.mpr (show n < k by lia), Nat.mul_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : ¬k ≤ n
neg : (n - k).descFactorial (m - k) * 0 = 0
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = 0
have neg₁ : Eq (α := ℕ) 0 0
Tactic: rw [descFactorial_eq_zero_iff_lt.mpr (show n < k by lia), Nat.mul_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
h : k ≤ n
⊢ n.descFactorial k = n ! / (n - k)!
have apply : (n - k)! * n.descFactorial k = (n - k)! * (n ! / (n - k)!)
Tactic: apply Nat.mul_left_cancel (n - k).factorial_pos
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
h : k ≤ n
⊢ (n - k)! * n.descFactorial k = (n - k)! * (n ! / (n - k)!)
have rw : n ! = (n - k)! * (n ! / (n - k)!)
Tactic: rw [factorial_mul_descFactorial h]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k m : ℕ
h : k ≤ m
⊢ k.descFactorial n ≤ m.descFactorial n
have zero : k.descFactorial 0 ≤ k.descFactorial 0
Tactic: induction n with
  | zero => rfl
  | succ n ih =>
    rw [descFactorial_succ, descFactorial_succ]
    exact Nat.mul_le_mul (Nat.sub_le_sub_right h n) ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k m : ℕ
h : k ≤ m
zero : k.descFactorial 0 ≤ k.descFactorial 0
⊢ k.descFactorial n ≤ m.descFactorial n
have succ : ∀ (n : ℕ) (ih : k.descFactorial n ≤ m.descFactorial n), k.descFactorial (n + 1) ≤ m.descFactorial (n + 1)
Tactic: induction n with
  | zero => rfl
  | succ n ih =>
    rw [descFactorial_succ, descFactorial_succ]
    exact Nat.mul_le_mul (Nat.sub_le_sub_right h n) ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
⊢ HPow.hPow (β := ℕ) (n + 1 - 0) 0 ≤ n.descFactorial 0
have rw : HPow.hPow (β := ℕ) (n + 1 - 0) 0 ≤ 1
Tactic: rw [descFactorial_zero, Nat.pow_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
rw : HPow.hPow (β := ℕ) (n + 1 - 0) 0 ≤ 1
⊢ HPow.hPow (β := ℕ) (n + 1 - 0) 0 ≤ n.descFactorial 0
have rw₁ : LE.le (α := ℕ) 1 1
Tactic: rw [descFactorial_zero, Nat.pow_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
⊢ (n + 1 - (k + 1)) ^ (k + 1) ≤ n.descFactorial (k + 1)
have rw : (n - k) * (n - k) ^ k ≤ (n - k) * n.descFactorial k
Tactic: rw [descFactorial_succ, Nat.pow_succ, succ_sub_succ, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
⊢ (n - k) * (n - k) ^ k ≤ (n - k) * n.descFactorial k
have h : (n - k) ^ k ≤ n.descFactorial k
Tactic: apply Nat.mul_le_mul_left
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n : ℕ
h : HAdd.hAdd (α := ℕ) 0 2 ≤ n
⊢ (n - HAdd.hAdd (α := ℕ) 0 1) ^ HAdd.hAdd (α := ℕ) 0 2 < n.descFactorial (HAdd.hAdd (α := ℕ) 0 2)
have rw : (n - HAdd.hAdd (α := ℕ) 0 1) * (n - HAdd.hAdd (α := ℕ) 0 1) < (n - 1) * n
Tactic: rw [descFactorial_succ, Nat.pow_succ, Nat.pow_one, descFactorial_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) ^ (k + 1 + 2) < n.descFactorial (k + 1 + 2)
have rw : (n - (k + 1 + 1)) * (n - (k + 1 + 1)) ^ (k + 2) < (n - (k + 2)) * n.descFactorial (k + 2)
Tactic: rw [descFactorial_succ, Nat.pow_succ, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) * (n - (k + 1 + 1)) ^ (k + 2) < (n - (k + 2)) * n.descFactorial (k + 2)
have refine : (n - (k + 1 + 1)) ^ (k + 2) < n.descFactorial (k + 2)
Tactic: refine Nat.mul_lt_mul_of_pos_left ?_ (Nat.sub_pos_of_lt h)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) ^ (k + 2) < n.descFactorial (k + 2)
have refine : (n.succ - (k + 1 + 1)) ^ (k + 2) < n.descFactorial (k + 2)
Tactic: refine Nat.lt_of_le_of_lt (Nat.pow_le_pow_left (Nat.sub_le_sub_right n.le_succ _) _) ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.Basic (goal)
Goal:
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n.succ - (k + 1 + 1)) ^ (k + 2) < n.descFactorial (k + 2)
have rw : (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)
Tactic: rw [succ_sub_succ]