awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
inl : (n.choose k + n.choose k.succ) * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
inl₁ : (n.choose k * k.succ ! + n.choose k.succ * k.succ !) * (n + 1 - k.succ)! = (n + 1)!
inl₂ : n.choose k * k.succ ! * (n + 1 - k.succ)! + n.choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
inl₃ : n.choose k * k.succ ! * (n - k)! + n.choose k.succ * k.succ ! * (n - k)! = (n + 1)!
inl₄ : (k + 1) * n ! + n.choose k.succ * k.succ ! * (n - k)! = (n + 1)!
inl₅ : (k + 1) * n ! + n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n + 1)!
inl₆ : (k + 1) * n ! + (n - k) * n ! = (n + 1)!
inl₇ : k * n ! + 1 * n ! + (n - k) * n ! = (n + 1)!
inl₈ : k * n ! + 1 * n ! + (n * n ! - k * n !) = (n + 1)!
inl₉ : k * n ! + 1 * n ! + (n * n ! - k * n !) = (n + 1) * n !
inl₁₀ : k * n ! + 1 * n ! + n * n ! - k * n ! = (n + 1) * n !
inl₁₁ : k * n ! + (1 * n ! + n * n !) - k * n ! = (n + 1) * n !
inl₁₂ : k * n ! + (1 + n) * n ! - k * n ! = (n + 1) * n !
inl₁₃ : (1 + n) * n ! = (n + 1) * n !
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
have inl₁₄ : (n + 1) * n ! = (n + 1) * n !
Tactic: rw [choose_succ_succ, Nat.add_mul, Nat.add_mul, succ_sub_succ, h, h₁, h₂, Nat.add_mul,
        Nat.mul_sub_right_distrib, factorial_succ, ← Nat.add_sub_assoc h₃, Nat.add_assoc,
        ← Nat.add_mul, Nat.add_sub_cancel_left, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ = n + 1
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
have inr : (n + 1).choose (n + 1) * (n + 1)! * (n + 1 - (n + 1))! = (n + 1)!
Tactic: rw [hk₁]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k s : ℕ
hsk : s ≤ k
⊢ n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)
have inl : ∀ (hnk : n < k), n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)
Tactic: obtain hnk | hkn := lt_or_ge n k
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k s : ℕ
hsk : s ≤ k
inl : ∀ (hnk : n < k), n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)
⊢ n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)
have inr : ∀ (hkn : k ≤ n), n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)
Tactic: obtain hnk | hkn := lt_or_ge n k
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (hypothesis)
Goal:
n k s : ℕ
hsk : s ≤ k
hkn : k ≤ n
⊢ n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)
have h : 0 < (n - k)! * (k - s)! * s !
Tactic: have h : 0 < (n - k)! * (k - s)! * s ! := by apply_rules [factorial_pos, Nat.mul_pos]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k s : ℕ
hsk : s ≤ k
hkn : k ≤ n
h : 0 < (n - k)! * (k - s)! * s !
⊢ n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)
have inr : n.choose k * k.choose s * ((n - k)! * (k - s)! * s !) =
  n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !)
Tactic: apply Nat.mul_right_cancel h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k s : ℕ
hsk : s ≤ k
hkn : k ≤ n
h : 0 < (n - k)! * (k - s)! * s !
⊢ n.choose k * k.choose s * ((n - k)! * (k - s)! * s !) =
    n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !)
have _ : n.choose k * k.choose s * ((n - k)! * (k - s)! * s !) =
  n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!)
Tactic: calc
    _ = n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!) := by
      grind [choose_mul_factorial_mul_factorial]
    _ = n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !) := by
      grind
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k s : ℕ
hsk : s ≤ k
hkn : k ≤ n
h : 0 < (n - k)! * (k - s)! * s !
_ :
  n.choose k * k.choose s * ((n - k)! * (k - s)! * s !) =
    n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!)
⊢ n.choose k * k.choose s * ((n - k)! * (k - s)! * s !) =
    n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !)
have _₁ : n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!) =
  n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !)
Tactic: calc
    _ = n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!) := by
      grind [choose_mul_factorial_mul_factorial]
    _ = n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !) := by
      grind
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : k ≤ n
⊢ n.choose k = n ! / (k ! * (n - k)!)
have rw : n.choose k = n.choose k * (k ! * (n - k)!) / (k ! * (n - k)!)
Tactic: rw [← choose_mul_factorial_mul_factorial hk, Nat.mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
i j : ℕ
⊢ (i + j).choose j = (i + j)! / (i ! * j !)
have rw : (i + j)! / (j ! * (i + j - j)!) = (i + j)! / (i ! * j !)
Tactic: rw [choose_eq_factorial_div_factorial (Nat.le_add_left j i), Nat.add_sub_cancel_right,
    Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
i j : ℕ
rw : (i + j)! / (j ! * (i + j - j)!) = (i + j)! / (i ! * j !)
⊢ (i + j).choose j = (i + j)! / (i ! * j !)
have rw₁ : (i + j)! / (j ! * i !) = (i + j)! / (i ! * j !)
Tactic: rw [choose_eq_factorial_div_factorial (Nat.le_add_left j i), Nat.add_sub_cancel_right,
    Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
i j : ℕ
rw : (i + j)! / (j ! * (i + j - j)!) = (i + j)! / (i ! * j !)
rw₁ : (i + j)! / (j ! * i !) = (i + j)! / (i ! * j !)
⊢ (i + j).choose j = (i + j)! / (i ! * j !)
have rw₂ : (i + j)! / (i ! * j !) = (i + j)! / (i ! * j !)
Tactic: rw [choose_eq_factorial_div_factorial (Nat.le_add_left j i), Nat.add_sub_cancel_right,
    Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
i j : ℕ
⊢ (i + j).choose j * i ! * j ! = (i + j)!
have rw : (i + j).choose j * i ! * j ! = (i + j).choose j * j ! * (i + j - j)!
Tactic: rw [← choose_mul_factorial_mul_factorial (Nat.le_add_left _ _), Nat.add_sub_cancel_right,
    Nat.mul_right_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
i j : ℕ
rw : (i + j).choose j * i ! * j ! = (i + j).choose j * j ! * (i + j - j)!
⊢ (i + j).choose j * i ! * j ! = (i + j)!
have rw₁ : (i + j).choose j * i ! * j ! = (i + j).choose j * j ! * i !
Tactic: rw [← choose_mul_factorial_mul_factorial (Nat.le_add_left _ _), Nat.add_sub_cancel_right,
    Nat.mul_right_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
i j : ℕ
rw : (i + j).choose j * i ! * j ! = (i + j).choose j * j ! * (i + j - j)!
rw₁ : (i + j).choose j * i ! * j ! = (i + j).choose j * j ! * i !
⊢ (i + j).choose j * i ! * j ! = (i + j)!
have rw₂ : (i + j).choose j * j ! * i ! = (i + j).choose j * j ! * i !
Tactic: rw [← choose_mul_factorial_mul_factorial (Nat.le_add_left _ _), Nat.add_sub_cancel_right,
    Nat.mul_right_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ n !
have rw : k ! * (n - k)! ∣ n.choose k * (k ! * (n - k)!)
Tactic: rw [← choose_mul_factorial_mul_factorial hk, Nat.mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
i j : ℕ
this : i ! * (i + j - i)! ∣ (i + j)!
⊢ i ! * j ! ∣ (i + j)!
have rwa : ∀ (this : i ! * j ! ∣ (i + j)!), i ! * j ! ∣ (i + j)!
Tactic: rwa [Nat.add_sub_cancel_left i j] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
i j : ℕ
⊢ i ! * j ! ∣ (i + j)!
have suffices : i ! * (i + j - i)! ∣ (i + j)!
Tactic: suffices i ! * (i + j - i)! ∣ (i + j)! by
    rwa [Nat.add_sub_cancel_left i j] at this
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : k ≤ n
⊢ n.choose (n - k) = n.choose k
have rw : n.choose (n - k) = n ! / (k ! * (n - k)!)
Tactic: rw [choose_eq_factorial_div_factorial hk, choose_eq_factorial_div_factorial (Nat.sub_le _ _),
    Nat.sub_sub_self hk, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : k ≤ n
rw : n.choose (n - k) = n ! / (k ! * (n - k)!)
⊢ n.choose (n - k) = n.choose k
have rw₁ : n ! / ((n - k)! * (n - (n - k))!) = n ! / (k ! * (n - k)!)
Tactic: rw [choose_eq_factorial_div_factorial hk, choose_eq_factorial_div_factorial (Nat.sub_le _ _),
    Nat.sub_sub_self hk, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : k ≤ n
rw : n.choose (n - k) = n ! / (k ! * (n - k)!)
rw₁ : n ! / ((n - k)! * (n - (n - k))!) = n ! / (k ! * (n - k)!)
⊢ n.choose (n - k) = n.choose k
have rw₂ : n ! / ((n - k)! * k !) = n ! / (k ! * (n - k)!)
Tactic: rw [choose_eq_factorial_div_factorial hk, choose_eq_factorial_div_factorial (Nat.sub_le _ _),
    Nat.sub_sub_self hk, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : k ≤ n
rw : n.choose (n - k) = n ! / (k ! * (n - k)!)
rw₁ : n ! / ((n - k)! * (n - (n - k))!) = n ! / (k ! * (n - k)!)
rw₂ : n ! / ((n - k)! * k !) = n ! / (k ! * (n - k)!)
⊢ n.choose (n - k) = n.choose k
have rw₃ : n ! / (k ! * (n - k)!) = n ! / (k ! * (n - k)!)
Tactic: rw [choose_eq_factorial_div_factorial hk, choose_eq_factorial_div_factorial (Nat.sub_le _ _),
    Nat.sub_sub_self hk, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (hypothesis)
Goal:
n a b : ℕ
h : n = a + b
this : n.choose (n - b) = n.choose b
⊢ n.choose a = n.choose b
have this₁ : (a + b).choose a = (a + b).choose b
Tactic: rw [h, Nat.add_sub_cancel_right] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n a b : ℕ
h : n = a + b
⊢ n.choose a = n.choose b
have suffices : n.choose (n - b) = n.choose b
Tactic: suffices choose n (n - b) = choose n b by
    rw [h, Nat.add_sub_cancel_right] at this; rwa [h]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m : ℕ
⊢ (2 * m + 1).choose (m + 1) = (2 * m + 1).choose m
have h : 2 * m + 1 = m + 1 + m
Tactic: apply choose_symm_of_eq_add
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m : ℕ
⊢ 2 * m + 1 = m + 1 + m
have h : 2 * m + 1 = 1 + m + m
Tactic: rw [Nat.add_comm m 1, Nat.add_assoc 1 m m, Nat.add_comm (2 * m) 1, Nat.two_mul m]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m : ℕ
h : 2 * m + 1 = 1 + m + m
⊢ 2 * m + 1 = m + 1 + m
have h₁ : 2 * m + 1 = 1 + (m + m)
Tactic: rw [Nat.add_comm m 1, Nat.add_assoc 1 m m, Nat.add_comm (2 * m) 1, Nat.two_mul m]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m : ℕ
h : 2 * m + 1 = 1 + m + m
h₁ : 2 * m + 1 = 1 + (m + m)
⊢ 2 * m + 1 = m + 1 + m
have h₂ : 1 + 2 * m = 1 + (m + m)
Tactic: rw [Nat.add_comm m 1, Nat.add_assoc 1 m m, Nat.add_comm (2 * m) 1, Nat.two_mul m]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
m : ℕ
h : 2 * m + 1 = 1 + m + m
h₁ : 2 * m + 1 = 1 + (m + m)
h₂ : 1 + 2 * m = 1 + (m + m)
⊢ 2 * m + 1 = m + 1 + m
have h₃ : 1 + (m + m) = 1 + (m + m)
Tactic: rw [Nat.add_comm m 1, Nat.add_assoc 1 m m, Nat.add_comm (2 * m) 1, Nat.two_mul m]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
⊢ (n + 1) * n.choose k = n.choose (k + 1) * (k + 1) + n.choose k * (k + 1)
have rw : (n + 1) * n.choose k = (n.choose (k + 1) + n.choose k) * (k + 1)
Tactic: rw [← Nat.add_mul, Nat.add_comm (choose _ _), ← choose_succ_succ, add_one_mul_choose_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
rw : (n + 1) * n.choose k = (n.choose (k + 1) + n.choose k) * (k + 1)
⊢ (n + 1) * n.choose k = n.choose (k + 1) * (k + 1) + n.choose k * (k + 1)
have rw₁ : (n + 1) * n.choose k = (n.choose k + n.choose (k + 1)) * (k + 1)
Tactic: rw [← Nat.add_mul, Nat.add_comm (choose _ _), ← choose_succ_succ, add_one_mul_choose_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
rw : (n + 1) * n.choose k = (n.choose (k + 1) + n.choose k) * (k + 1)
rw₁ : (n + 1) * n.choose k = (n.choose k + n.choose (k + 1)) * (k + 1)
⊢ (n + 1) * n.choose k = n.choose (k + 1) * (k + 1) + n.choose k * (k + 1)
have rw₂ : (n + 1) * n.choose k = n.succ.choose k.succ * (k + 1)
Tactic: rw [← Nat.add_mul, Nat.add_comm (choose _ _), ← choose_succ_succ, add_one_mul_choose_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
rw : (n + 1) * n.choose k = (n.choose (k + 1) + n.choose k) * (k + 1)
rw₁ : (n + 1) * n.choose k = (n.choose k + n.choose (k + 1)) * (k + 1)
rw₂ : (n + 1) * n.choose k = n.succ.choose k.succ * (k + 1)
⊢ (n + 1) * n.choose k = n.choose (k + 1) * (k + 1) + n.choose k * (k + 1)
have rw₃ : (n + 1).choose (k + 1) * (k + 1) = n.succ.choose k.succ * (k + 1)
Tactic: rw [← Nat.add_mul, Nat.add_comm (choose _ _), ← choose_succ_succ, add_one_mul_choose_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (hypothesis)
Goal:
n k : ℕ
⊢ n.choose (k + 1) * (k + 1) = n.choose k * (n - k)
have e : (n + 1) * n.choose k = n.choose (k + 1) * (k + 1) + n.choose k * (k + 1)
Tactic: have e : (n + 1) * choose n k = choose n (k + 1) * (k + 1) + choose n k * (k + 1) := by
    rw [← Nat.add_mul, Nat.add_comm (choose _ _), ← choose_succ_succ, add_one_mul_choose_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
e : (n + 1) * n.choose k = n.choose (k + 1) * (k + 1) + n.choose k * (k + 1)
⊢ n.choose (k + 1) * (k + 1) = n.choose k * (n - k)
have rw : (n + 1) * n.choose k - n.choose k * (k + 1) = n.choose k * (n - k)
Tactic: rw [← Nat.sub_eq_of_eq_add e, Nat.mul_comm, ← Nat.mul_sub_left_distrib, Nat.add_sub_add_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
e : (n + 1) * n.choose k = n.choose (k + 1) * (k + 1) + n.choose k * (k + 1)
rw : (n + 1) * n.choose k - n.choose k * (k + 1) = n.choose k * (n - k)
⊢ n.choose (k + 1) * (k + 1) = n.choose k * (n - k)
have rw₁ : n.choose k * (n + 1) - n.choose k * (k + 1) = n.choose k * (n - k)
Tactic: rw [← Nat.sub_eq_of_eq_add e, Nat.mul_comm, ← Nat.mul_sub_left_distrib, Nat.add_sub_add_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
e : (n + 1) * n.choose k = n.choose (k + 1) * (k + 1) + n.choose k * (k + 1)
rw : (n + 1) * n.choose k - n.choose k * (k + 1) = n.choose k * (n - k)
rw₁ : n.choose k * (n + 1) - n.choose k * (k + 1) = n.choose k * (n - k)
⊢ n.choose (k + 1) * (k + 1) = n.choose k * (n - k)
have rw₂ : n.choose k * (n + 1 - (k + 1)) = n.choose k * (n - k)
Tactic: rw [← Nat.sub_eq_of_eq_add e, Nat.mul_comm, ← Nat.mul_sub_left_distrib, Nat.add_sub_add_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
e : (n + 1) * n.choose k = n.choose (k + 1) * (k + 1) + n.choose k * (k + 1)
rw : (n + 1) * n.choose k - n.choose k * (k + 1) = n.choose k * (n - k)
rw₁ : n.choose k * (n + 1) - n.choose k * (k + 1) = n.choose k * (n - k)
rw₂ : n.choose k * (n + 1 - (k + 1)) = n.choose k * (n - k)
⊢ n.choose (k + 1) * (k + 1) = n.choose k * (n - k)
have rw₃ : n.choose k * (n - k) = n.choose k * (n - k)
Tactic: rw [← Nat.sub_eq_of_eq_add e, Nat.mul_comm, ← Nat.mul_sub_left_distrib, Nat.add_sub_add_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n : ℕ
⊢ (n + 1 + 1).choose (n + 1) = n + 1 + 1
have rw : (n + 1).choose n + (n + 1).choose n.succ = n + 1 + 1
Tactic: rw [choose_succ_succ, choose_succ_self_right n, choose_self]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n : ℕ
rw : (n + 1).choose n + (n + 1).choose n.succ = n + 1 + 1
⊢ (n + 1 + 1).choose (n + 1) = n + 1 + 1
have rw₁ : n + 1 + (n + 1).choose n.succ = n + 1 + 1
Tactic: rw [choose_succ_succ, choose_succ_self_right n, choose_self]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n : ℕ
rw : (n + 1).choose n + (n + 1).choose n.succ = n + 1 + 1
rw₁ : n + 1 + (n + 1).choose n.succ = n + 1 + 1
⊢ (n + 1 + 1).choose (n + 1) = n + 1 + 1
have rw₂ : n + 1 + 1 = n + 1 + 1
Tactic: rw [choose_succ_succ, choose_succ_self_right n, choose_self]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))
have succ : ∀ (hk : k + 1 ≤ n + 1), n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))
Tactic: obtain hk | hk := le_or_gt (k + 1) (n + 1)
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
succ : ∀ (hk : k + 1 ≤ n + 1), n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))
have succ₁ : ∀ (hk : n + 1 < k + 1), n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))
Tactic: obtain hk | hk := le_or_gt (k + 1) (n + 1)
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : k + 1 ≤ n + 1
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))
have succ : n.choose (k + 1) * (n + 1) = (n.choose k + n.choose k.succ) * (n + 1 - (k + 1))
Tactic: 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)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : k + 1 ≤ n + 1
succ : n.choose (k + 1) * (n + 1) = (n.choose k + n.choose k.succ) * (n + 1 - (k + 1))
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))
have succ₁ : n.choose (k + 1) * (n + 1) = n.choose k * (n + 1 - (k + 1)) + n.choose k.succ * (n + 1 - (k + 1))
Tactic: 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)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : k + 1 ≤ n + 1
succ : n.choose (k + 1) * (n + 1) = (n.choose k + n.choose k.succ) * (n + 1 - (k + 1))
succ₁ : n.choose (k + 1) * (n + 1) = n.choose k * (n + 1 - (k + 1)) + n.choose k.succ * (n + 1 - (k + 1))
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))
have succ₂ : n.choose (k + 1) * (n + 1) = n.choose k * (n - k) + n.choose k.succ * (n - k)
Tactic: 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)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : k + 1 ≤ n + 1
succ : n.choose (k + 1) * (n + 1) = (n.choose k + n.choose k.succ) * (n + 1 - (k + 1))
succ₁ : n.choose (k + 1) * (n + 1) = n.choose k * (n + 1 - (k + 1)) + n.choose k.succ * (n + 1 - (k + 1))
succ₂ : n.choose (k + 1) * (n + 1) = n.choose k * (n - k) + n.choose k.succ * (n - k)
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))
have succ₃ : n.choose (k + 1) * (n + 1) = n.choose (k + 1) * (k + 1) + n.choose k.succ * (n - k)
Tactic: 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)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : k + 1 ≤ n + 1
succ : n.choose (k + 1) * (n + 1) = (n.choose k + n.choose k.succ) * (n + 1 - (k + 1))
succ₁ : n.choose (k + 1) * (n + 1) = n.choose k * (n + 1 - (k + 1)) + n.choose k.succ * (n + 1 - (k + 1))
succ₂ : n.choose (k + 1) * (n + 1) = n.choose k * (n - k) + n.choose k.succ * (n - k)
succ₃ : n.choose (k + 1) * (n + 1) = n.choose (k + 1) * (k + 1) + n.choose k.succ * (n - k)
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))
have succ₄ : n.choose (k + 1) * (n + 1) = n.choose (k + 1) * (k + 1) + n.choose k.succ * (n.succ - k.succ)
Tactic: 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)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : k + 1 ≤ n + 1
succ : n.choose (k + 1) * (n + 1) = (n.choose k + n.choose k.succ) * (n + 1 - (k + 1))
succ₁ : n.choose (k + 1) * (n + 1) = n.choose k * (n + 1 - (k + 1)) + n.choose k.succ * (n + 1 - (k + 1))
succ₂ : n.choose (k + 1) * (n + 1) = n.choose k * (n - k) + n.choose k.succ * (n - k)
succ₃ : n.choose (k + 1) * (n + 1) = n.choose (k + 1) * (k + 1) + n.choose k.succ * (n - k)
succ₄ : n.choose (k + 1) * (n + 1) = n.choose (k + 1) * (k + 1) + n.choose k.succ * (n.succ - k.succ)
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))
have succ₅ : n.choose (k + 1) * (n + 1) = n.choose (k + 1) * (k + 1) + (n.choose k.succ * n.succ - n.choose k.succ * k.succ)
Tactic: 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)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : k + 1 ≤ n + 1
succ : n.choose (k + 1) * (n + 1) = (n.choose k + n.choose k.succ) * (n + 1 - (k + 1))
succ₁ : n.choose (k + 1) * (n + 1) = n.choose k * (n + 1 - (k + 1)) + n.choose k.succ * (n + 1 - (k + 1))
succ₂ : n.choose (k + 1) * (n + 1) = n.choose k * (n - k) + n.choose k.succ * (n - k)
succ₃ : n.choose (k + 1) * (n + 1) = n.choose (k + 1) * (k + 1) + n.choose k.succ * (n - k)
succ₄ : n.choose (k + 1) * (n + 1) = n.choose (k + 1) * (k + 1) + n.choose k.succ * (n.succ - k.succ)
succ₅ : n.choose (k + 1) * (n + 1) = n.choose (k + 1) * (k + 1) + (n.choose k.succ * n.succ - n.choose k.succ * k.succ)
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))
have succ₆ : n.choose (k + 1) * (n + 1) = n.choose (k + 1) * (n + 1)
Tactic: 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)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : n + 1 < k + 1
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))
have succ : n.choose (k + 1) * (n + 1) = 0 * (n + 1 - (k + 1))
Tactic: rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), Nat.zero_mul,
        Nat.zero_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : n + 1 < k + 1
succ : n.choose (k + 1) * (n + 1) = 0 * (n + 1 - (k + 1))
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))
have succ₁ : 0 * (n + 1) = 0 * (n + 1 - (k + 1))
Tactic: rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), Nat.zero_mul,
        Nat.zero_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : n + 1 < k + 1
succ : n.choose (k + 1) * (n + 1) = 0 * (n + 1 - (k + 1))
succ₁ : 0 * (n + 1) = 0 * (n + 1 - (k + 1))
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))
have succ₂ : 0 = 0 * (n + 1 - (k + 1))
Tactic: rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), Nat.zero_mul,
        Nat.zero_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : n + 1 < k + 1
succ : n.choose (k + 1) * (n + 1) = 0 * (n + 1 - (k + 1))
succ₁ : 0 * (n + 1) = 0 * (n + 1 - (k + 1))
succ₂ : 0 = 0 * (n + 1 - (k + 1))
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))
have succ₃ : Eq (α := ℕ) 0 0
Tactic: rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), Nat.zero_mul,
        Nat.zero_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
⊢ n.choose k * (n + 1) = (n + 1).choose k * (n + 1 - k)
have zero : n.choose 0 * (n + 1) = (n + 1).choose 0 * (n + 1 - 0)
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