awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
zero : n.choose 0 * (n + 1) = (n + 1).choose 0 * (n + 1 - 0)
⊢ n.choose k * (n + 1) = (n + 1).choose k * (n + 1 - k)
have succ : ∀ (k : ℕ), n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))
Tactic: cases k with
  | zero => simp
  | succ k =>
    obtain hk | hk := le_or_gt (k + 1) (n + 1)
    · rw [choose_succ_succ, Nat.add_mul, succ_sub_succ, ← choose_succ_right_eq, ← succ_sub_succ,
        Nat.mul_sub_left_distrib, Nat.add_sub_cancel' (Nat.mul_le_mul_left _ hk)]
    · rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), Nat.zero_mul,
        Nat.zero_mul]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
⊢ (m * n + n).choose n = (m + 1) * (m * n + n - 1).choose (n - 1)
have rw : (m * n + n).choose n * ((m * n)! * n !) = (m + 1) * (m * n + n - 1).choose (n - 1) * ((m * n)! * n !)
Tactic: rw [← Nat.mul_left_inj (Nat.mul_ne_zero (factorial_ne_zero (m * n)) (factorial_ne_zero n))]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (hypothesis)
Goal:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
⊢ (m * n + n).choose n * ((m * n)! * n !) = (m + 1) * (m * n + n - 1).choose p * ((m * n)! * n !)
have hp : n = p + 1
Tactic: have hp : n = p + 1 := (succ_pred_eq_of_ne_zero hn).symm
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * n + n).choose n * ((m * n)! * n !) = (m + 1) * (m * n + n - 1).choose p * ((m * n)! * n !)
have simp : (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
  (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!)
Tactic: simp only [hp, add_succ_sub_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! = (m * (p + 1) + (p + 1))!
have rw : (m * (p + 1) + (p + 1))! = (m * (p + 1) + (p + 1))!
Tactic: rw [add_choose_mul_factorial_mul_factorial]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p + 1)! = (m * (p + 1) + p + 1) * (m * (p + 1) + p)!
have rw : (m * (p + 1) + p + 1) * (m * (p + 1) + p)! = (m * (p + 1) + p + 1) * (m * (p + 1) + p)!
Tactic: rw [factorial_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p)! * ((p + 1) * (m + 1)) = (m * (p + 1) + p).choose p * (m * (p + 1))! * p ! * ((p + 1) * (m + 1))
have rw : (m * (p + 1) + p)! * ((p + 1) * (m + 1)) = (m * (p + 1) + p)! * ((p + 1) * (m + 1))
Tactic: rw [add_choose_mul_factorial_mul_factorial]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1) * p ! * (m + 1)) =
    (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1))
have rw : (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1) * p ! * (m + 1)) =
  (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1) * p ! * (m + 1))
Tactic: rw [factorial_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!)
have by : (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
  (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)!
Tactic: calc
    (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!)
      = (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! := by lia
    _ = (m * (p + 1) + (p + 1))! := by rw [add_choose_mul_factorial_mul_factorial]
    _ = ((m * (p + 1) + p) + 1)! := by lia
    _ = ((m * (p + 1) + p) + 1) * (m * (p + 1) + p)! := by rw [factorial_succ]
    _ = (m * (p + 1) + p)! * ((p + 1) * (m + 1)) := by lia
    _ = ((m * (p + 1) + p).choose p * (m * (p + 1))! * (p)!) * ((p + 1) * (m + 1)) := by
      rw [add_choose_mul_factorial_mul_factorial]
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * (((p + 1) * (p)!) * (m + 1)) := by lia
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1)) := by rw [factorial_succ]
    _ = (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!) := by lia
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
by :
  (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)!
⊢ (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!)
have by₁ : (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! = (m * (p + 1) + (p + 1))!
Tactic: calc
    (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!)
      = (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! := by lia
    _ = (m * (p + 1) + (p + 1))! := by rw [add_choose_mul_factorial_mul_factorial]
    _ = ((m * (p + 1) + p) + 1)! := by lia
    _ = ((m * (p + 1) + p) + 1) * (m * (p + 1) + p)! := by rw [factorial_succ]
    _ = (m * (p + 1) + p)! * ((p + 1) * (m + 1)) := by lia
    _ = ((m * (p + 1) + p).choose p * (m * (p + 1))! * (p)!) * ((p + 1) * (m + 1)) := by
      rw [add_choose_mul_factorial_mul_factorial]
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * (((p + 1) * (p)!) * (m + 1)) := by lia
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1)) := by rw [factorial_succ]
    _ = (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!) := by lia
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
by :
  (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)!
by₁ : (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! = (m * (p + 1) + (p + 1))!
⊢ (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!)
have by₂ : (m * (p + 1) + (p + 1))! = (m * (p + 1) + p + 1)!
Tactic: calc
    (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!)
      = (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! := by lia
    _ = (m * (p + 1) + (p + 1))! := by rw [add_choose_mul_factorial_mul_factorial]
    _ = ((m * (p + 1) + p) + 1)! := by lia
    _ = ((m * (p + 1) + p) + 1) * (m * (p + 1) + p)! := by rw [factorial_succ]
    _ = (m * (p + 1) + p)! * ((p + 1) * (m + 1)) := by lia
    _ = ((m * (p + 1) + p).choose p * (m * (p + 1))! * (p)!) * ((p + 1) * (m + 1)) := by
      rw [add_choose_mul_factorial_mul_factorial]
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * (((p + 1) * (p)!) * (m + 1)) := by lia
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1)) := by rw [factorial_succ]
    _ = (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!) := by lia
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
by :
  (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)!
by₁ : (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! = (m * (p + 1) + (p + 1))!
by₂ : (m * (p + 1) + (p + 1))! = (m * (p + 1) + p + 1)!
⊢ (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!)
have by₃ : (m * (p + 1) + p + 1)! = (m * (p + 1) + p + 1) * (m * (p + 1) + p)!
Tactic: calc
    (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!)
      = (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! := by lia
    _ = (m * (p + 1) + (p + 1))! := by rw [add_choose_mul_factorial_mul_factorial]
    _ = ((m * (p + 1) + p) + 1)! := by lia
    _ = ((m * (p + 1) + p) + 1) * (m * (p + 1) + p)! := by rw [factorial_succ]
    _ = (m * (p + 1) + p)! * ((p + 1) * (m + 1)) := by lia
    _ = ((m * (p + 1) + p).choose p * (m * (p + 1))! * (p)!) * ((p + 1) * (m + 1)) := by
      rw [add_choose_mul_factorial_mul_factorial]
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * (((p + 1) * (p)!) * (m + 1)) := by lia
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1)) := by rw [factorial_succ]
    _ = (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!) := by lia
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
by :
  (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)!
by₁ : (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! = (m * (p + 1) + (p + 1))!
by₂ : (m * (p + 1) + (p + 1))! = (m * (p + 1) + p + 1)!
by₃ : (m * (p + 1) + p + 1)! = (m * (p + 1) + p + 1) * (m * (p + 1) + p)!
⊢ (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!)
have by₄ : (m * (p + 1) + p + 1) * (m * (p + 1) + p)! = (m * (p + 1) + p)! * ((p + 1) * (m + 1))
Tactic: calc
    (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!)
      = (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! := by lia
    _ = (m * (p + 1) + (p + 1))! := by rw [add_choose_mul_factorial_mul_factorial]
    _ = ((m * (p + 1) + p) + 1)! := by lia
    _ = ((m * (p + 1) + p) + 1) * (m * (p + 1) + p)! := by rw [factorial_succ]
    _ = (m * (p + 1) + p)! * ((p + 1) * (m + 1)) := by lia
    _ = ((m * (p + 1) + p).choose p * (m * (p + 1))! * (p)!) * ((p + 1) * (m + 1)) := by
      rw [add_choose_mul_factorial_mul_factorial]
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * (((p + 1) * (p)!) * (m + 1)) := by lia
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1)) := by rw [factorial_succ]
    _ = (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!) := by lia
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
by :
  (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)!
by₁ : (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! = (m * (p + 1) + (p + 1))!
by₂ : (m * (p + 1) + (p + 1))! = (m * (p + 1) + p + 1)!
by₃ : (m * (p + 1) + p + 1)! = (m * (p + 1) + p + 1) * (m * (p + 1) + p)!
by₄ : (m * (p + 1) + p + 1) * (m * (p + 1) + p)! = (m * (p + 1) + p)! * ((p + 1) * (m + 1))
⊢ (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!)
have by₅ : (m * (p + 1) + p)! * ((p + 1) * (m + 1)) = (m * (p + 1) + p).choose p * (m * (p + 1))! * p ! * ((p + 1) * (m + 1))
Tactic: calc
    (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!)
      = (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! := by lia
    _ = (m * (p + 1) + (p + 1))! := by rw [add_choose_mul_factorial_mul_factorial]
    _ = ((m * (p + 1) + p) + 1)! := by lia
    _ = ((m * (p + 1) + p) + 1) * (m * (p + 1) + p)! := by rw [factorial_succ]
    _ = (m * (p + 1) + p)! * ((p + 1) * (m + 1)) := by lia
    _ = ((m * (p + 1) + p).choose p * (m * (p + 1))! * (p)!) * ((p + 1) * (m + 1)) := by
      rw [add_choose_mul_factorial_mul_factorial]
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * (((p + 1) * (p)!) * (m + 1)) := by lia
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1)) := by rw [factorial_succ]
    _ = (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!) := by lia
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
by :
  (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)!
by₁ : (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! = (m * (p + 1) + (p + 1))!
by₂ : (m * (p + 1) + (p + 1))! = (m * (p + 1) + p + 1)!
by₃ : (m * (p + 1) + p + 1)! = (m * (p + 1) + p + 1) * (m * (p + 1) + p)!
by₄ : (m * (p + 1) + p + 1) * (m * (p + 1) + p)! = (m * (p + 1) + p)! * ((p + 1) * (m + 1))
by₅ : (m * (p + 1) + p)! * ((p + 1) * (m + 1)) = (m * (p + 1) + p).choose p * (m * (p + 1))! * p ! * ((p + 1) * (m + 1))
⊢ (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!)
have by₆ : (m * (p + 1) + p).choose p * (m * (p + 1))! * p ! * ((p + 1) * (m + 1)) =
  (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1) * p ! * (m + 1))
Tactic: calc
    (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!)
      = (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! := by lia
    _ = (m * (p + 1) + (p + 1))! := by rw [add_choose_mul_factorial_mul_factorial]
    _ = ((m * (p + 1) + p) + 1)! := by lia
    _ = ((m * (p + 1) + p) + 1) * (m * (p + 1) + p)! := by rw [factorial_succ]
    _ = (m * (p + 1) + p)! * ((p + 1) * (m + 1)) := by lia
    _ = ((m * (p + 1) + p).choose p * (m * (p + 1))! * (p)!) * ((p + 1) * (m + 1)) := by
      rw [add_choose_mul_factorial_mul_factorial]
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * (((p + 1) * (p)!) * (m + 1)) := by lia
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1)) := by rw [factorial_succ]
    _ = (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!) := by lia
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
by :
  (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)!
by₁ : (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! = (m * (p + 1) + (p + 1))!
by₂ : (m * (p + 1) + (p + 1))! = (m * (p + 1) + p + 1)!
by₃ : (m * (p + 1) + p + 1)! = (m * (p + 1) + p + 1) * (m * (p + 1) + p)!
by₄ : (m * (p + 1) + p + 1) * (m * (p + 1) + p)! = (m * (p + 1) + p)! * ((p + 1) * (m + 1))
by₅ : (m * (p + 1) + p)! * ((p + 1) * (m + 1)) = (m * (p + 1) + p).choose p * (m * (p + 1))! * p ! * ((p + 1) * (m + 1))
by₆ :
  (m * (p + 1) + p).choose p * (m * (p + 1))! * p ! * ((p + 1) * (m + 1)) =
    (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1) * p ! * (m + 1))
⊢ (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!)
have by₇ : (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1) * p ! * (m + 1)) =
  (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1))
Tactic: calc
    (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!)
      = (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! := by lia
    _ = (m * (p + 1) + (p + 1))! := by rw [add_choose_mul_factorial_mul_factorial]
    _ = ((m * (p + 1) + p) + 1)! := by lia
    _ = ((m * (p + 1) + p) + 1) * (m * (p + 1) + p)! := by rw [factorial_succ]
    _ = (m * (p + 1) + p)! * ((p + 1) * (m + 1)) := by lia
    _ = ((m * (p + 1) + p).choose p * (m * (p + 1))! * (p)!) * ((p + 1) * (m + 1)) := by
      rw [add_choose_mul_factorial_mul_factorial]
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * (((p + 1) * (p)!) * (m + 1)) := by lia
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1)) := by rw [factorial_succ]
    _ = (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!) := by lia
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
by :
  (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)!
by₁ : (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! = (m * (p + 1) + (p + 1))!
by₂ : (m * (p + 1) + (p + 1))! = (m * (p + 1) + p + 1)!
by₃ : (m * (p + 1) + p + 1)! = (m * (p + 1) + p + 1) * (m * (p + 1) + p)!
by₄ : (m * (p + 1) + p + 1) * (m * (p + 1) + p)! = (m * (p + 1) + p)! * ((p + 1) * (m + 1))
by₅ : (m * (p + 1) + p)! * ((p + 1) * (m + 1)) = (m * (p + 1) + p).choose p * (m * (p + 1))! * p ! * ((p + 1) * (m + 1))
by₆ :
  (m * (p + 1) + p).choose p * (m * (p + 1))! * p ! * ((p + 1) * (m + 1)) =
    (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1) * p ! * (m + 1))
by₇ :
  (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1) * p ! * (m + 1)) =
    (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1))
⊢ (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!)
have by₈ : (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1)) =
  (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!)
Tactic: calc
    (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!)
      = (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! := by lia
    _ = (m * (p + 1) + (p + 1))! := by rw [add_choose_mul_factorial_mul_factorial]
    _ = ((m * (p + 1) + p) + 1)! := by lia
    _ = ((m * (p + 1) + p) + 1) * (m * (p + 1) + p)! := by rw [factorial_succ]
    _ = (m * (p + 1) + p)! * ((p + 1) * (m + 1)) := by lia
    _ = ((m * (p + 1) + p).choose p * (m * (p + 1))! * (p)!) * ((p + 1) * (m + 1)) := by
      rw [add_choose_mul_factorial_mul_factorial]
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * (((p + 1) * (p)!) * (m + 1)) := by lia
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1)) := by rw [factorial_succ]
    _ = (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!) := by lia
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)
have pos : ∀ (hm : m = 0), (m * n).choose n = m * (m * n - 1).choose (n - 1)
Tactic: by_cases hm : m = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
pos : ∀ (hm : m = 0), (m * n).choose n = m * (m * n - 1).choose (n - 1)
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)
have neg : ∀ (hm : ¬m = 0), (m * n).choose n = m * (m * n - 1).choose (n - 1)
Tactic: by_cases hm : m = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)
have pos : 0 < n
Tactic: simp only [hm, Nat.zero_mul, Nat.choose_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (hypothesis)
Goal:
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
p : ℕ := m - 1
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)
have hp : m = p + 1
Tactic: have hp : m = p + 1 := (succ_pred_eq_of_ne_zero hm).symm
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
p : ℕ := m - 1
hp : m = p + 1
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)
have neg : ((p + 1) * n).choose n = (p + 1) * ((p + 1) * n - 1).choose (n - 1)
Tactic: simp only [hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
p : ℕ := m - 1
hp : m = p + 1
⊢ ((p + 1) * n).choose n = (p + 1) * ((p + 1) * n - 1).choose (n - 1)
have neg : (p * n + 1 * n).choose n = (p + 1) * (p * n + 1 * n - 1).choose (n - 1)
Tactic: rw [Nat.add_mul, Nat.one_mul, choose_mul_add hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
p : ℕ := m - 1
hp : m = p + 1
neg : (p * n + 1 * n).choose n = (p + 1) * (p * n + 1 * n - 1).choose (n - 1)
⊢ ((p + 1) * n).choose n = (p + 1) * ((p + 1) * n - 1).choose (n - 1)
have neg₁ : (p * n + n).choose n = (p + 1) * (p * n + n - 1).choose (n - 1)
Tactic: rw [Nat.add_mul, Nat.one_mul, choose_mul_add hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
p : ℕ := m - 1
hp : m = p + 1
neg : (p * n + 1 * n).choose n = (p + 1) * (p * n + 1 * n - 1).choose (n - 1)
neg₁ : (p * n + n).choose n = (p + 1) * (p * n + n - 1).choose (n - 1)
⊢ ((p + 1) * n).choose n = (p + 1) * ((p + 1) * n - 1).choose (n - 1)
have neg₂ : (p + 1) * (p * n + n - 1).choose (n - 1) = (p + 1) * (p * n + n - 1).choose (n - 1)
Tactic: rw [Nat.add_mul, Nat.one_mul, choose_mul_add hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
⊢ (n + 1).ascFactorial k = k ! * (n + k).choose k
have rw : (n + 1).ascFactorial k = (n + k).choose k * k !
Tactic: rw [Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
⊢ (n + 1).ascFactorial k = (n + k).choose k * k !
have apply : (n + 1).ascFactorial k * (n + k - k)! = (n + k).choose k * k ! * (n + k - k)!
Tactic: apply Nat.mul_right_cancel (n + k - k).factorial_pos
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
⊢ (n + 1).ascFactorial k * (n + k - k)! = (n + k).choose k * k ! * (n + k - k)!
have rw : (n + 1).ascFactorial k * (n + k - k)! = (n + k)!
Tactic: rw [choose_mul_factorial_mul_factorial <| Nat.le_add_left k n, Nat.add_sub_cancel_right,
    ← factorial_mul_ascFactorial, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
rw : (n + 1).ascFactorial k * (n + k - k)! = (n + k)!
⊢ (n + 1).ascFactorial k * (n + k - k)! = (n + k).choose k * k ! * (n + k - k)!
have rw₁ : (n + 1).ascFactorial k * n ! = (n + k)!
Tactic: rw [choose_mul_factorial_mul_factorial <| Nat.le_add_left k n, Nat.add_sub_cancel_right,
    ← factorial_mul_ascFactorial, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
rw : (n + 1).ascFactorial k * (n + k - k)! = (n + k)!
rw₁ : (n + 1).ascFactorial k * n ! = (n + k)!
⊢ (n + 1).ascFactorial k * (n + k - k)! = (n + k).choose k * k ! * (n + k - k)!
have rw₂ : (n + 1).ascFactorial k * n ! = n ! * (n + 1).ascFactorial k
Tactic: rw [choose_mul_factorial_mul_factorial <| Nat.le_add_left k n, Nat.add_sub_cancel_right,
    ← factorial_mul_ascFactorial, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
rw : (n + 1).ascFactorial k * (n + k - k)! = (n + k)!
rw₁ : (n + 1).ascFactorial k * n ! = (n + k)!
rw₂ : (n + 1).ascFactorial k * n ! = n ! * (n + 1).ascFactorial k
⊢ (n + 1).ascFactorial k * (n + k - k)! = (n + k).choose k * k ! * (n + k - k)!
have rw₃ : n ! * (n + 1).ascFactorial k = n ! * (n + 1).ascFactorial k
Tactic: rw [choose_mul_factorial_mul_factorial <| Nat.le_add_left k n, Nat.add_sub_cancel_right,
    ← factorial_mul_ascFactorial, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
⊢ n.ascFactorial k = k ! * (n + k - 1).choose k
have zero : ascFactorial 0 k = k ! * (0 + k - 1).choose k
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
zero : ascFactorial 0 k = k ! * (0 + k - 1).choose k
⊢ n.ascFactorial k = k ! * (n + k - 1).choose k
have succ : ∀ (n : ℕ), (n + 1).ascFactorial k = k ! * (n + 1 + k - 1).choose k
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
k : ℕ
⊢ ascFactorial 0 k = k ! * (0 + k - 1).choose k
have zero : ascFactorial 0 0 = 0! * (HAdd.hAdd (α := ℕ) 0 0 - 1).choose 0
Tactic: cases k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
k : ℕ
zero : ascFactorial 0 0 = 0! * (HAdd.hAdd (α := ℕ) 0 0 - 1).choose 0
⊢ ascFactorial 0 k = k ! * (0 + k - 1).choose k
have zero₁ : ∀ (n : ℕ), ascFactorial 0 (n + 1) = (n + 1)! * (0 + (n + 1) - 1).choose (n + 1)
Tactic: cases k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
⊢ ascFactorial 0 0 = 0! * (HAdd.hAdd (α := ℕ) 0 0 - 1).choose 0
have zero : 1 = 0! * (HAdd.hAdd (α := ℕ) 0 0 - 1).choose 0
Tactic: rw [ascFactorial_zero, choose_zero_right, factorial_zero, Nat.mul_one]