awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
rw : (n + 1 + 1) * (n + 1).choose (k + 1) = ((n + 1).choose (k + 1) + (n + 1).choose (k + 1 + 1)) * (k + 1 + 1)
rw₁ :
  (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1).choose (k + 1) * (k + 1 + 1) + (n + 1).choose (k + 1 + 1) * (k + 1 + 1)
rw₂ : (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1).choose (k + 1) * (k + 1 + 1) + (n + 1) * n.choose (k + 1)
rw₃ :
  (n + 1 + 1) * (n + 1).choose (k + 1) =
    (n + 1).choose (k + 1) * (k + 1) + (n + 1).choose (k + 1) + (n + 1) * n.choose (k + 1)
rw₄ : (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1) * n.choose k + (n + 1).choose (k + 1) + (n + 1) * n.choose (k + 1)
rw₅ : (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1) * n.choose k + (n + 1) * n.choose (k + 1) + (n + 1).choose (k + 1)
rw₆ : (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1) * (n.choose k + n.choose (k + 1)) + (n + 1).choose (k + 1)
⊢ (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1 + 1).choose (k + 1 + 1) * (k + 1 + 1)
have rw₇ : (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1) * (n + 1).choose (k + 1) + (n + 1).choose (k + 1)
Tactic: rw [choose_succ_succ' (n + 1) (k + 1), Nat.add_mul _ _ (k + 1 + 1), ← add_one_mul_choose_eq n,
      mul_add_one, ← add_one_mul_choose_eq n, Nat.add_right_comm _ _ (_ * _), ← Nat.mul_add,
      ← choose_succ_succ', ← add_one_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
rw : (n + 1 + 1) * (n + 1).choose (k + 1) = ((n + 1).choose (k + 1) + (n + 1).choose (k + 1 + 1)) * (k + 1 + 1)
rw₁ :
  (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1).choose (k + 1) * (k + 1 + 1) + (n + 1).choose (k + 1 + 1) * (k + 1 + 1)
rw₂ : (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1).choose (k + 1) * (k + 1 + 1) + (n + 1) * n.choose (k + 1)
rw₃ :
  (n + 1 + 1) * (n + 1).choose (k + 1) =
    (n + 1).choose (k + 1) * (k + 1) + (n + 1).choose (k + 1) + (n + 1) * n.choose (k + 1)
rw₄ : (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1) * n.choose k + (n + 1).choose (k + 1) + (n + 1) * n.choose (k + 1)
rw₅ : (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1) * n.choose k + (n + 1) * n.choose (k + 1) + (n + 1).choose (k + 1)
rw₆ : (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1) * (n.choose k + n.choose (k + 1)) + (n + 1).choose (k + 1)
rw₇ : (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1) * (n + 1).choose (k + 1) + (n + 1).choose (k + 1)
⊢ (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1 + 1).choose (k + 1 + 1) * (k + 1 + 1)
have rw₈ : (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1 + 1) * (n + 1).choose (k + 1)
Tactic: rw [choose_succ_succ' (n + 1) (k + 1), Nat.add_mul _ _ (k + 1 + 1), ← add_one_mul_choose_eq n,
      mul_add_one, ← add_one_mul_choose_eq n, Nat.add_right_comm _ _ (_ * _), ← Nat.mul_add,
      ← choose_succ_succ', ← add_one_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : k.succ ≤ n + 1
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
have inl : ∀ (hk₁ : k.succ < n + 1), (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
Tactic: rcases lt_or_eq_of_le hk with hk₁ | hk₁
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (goal)
Goal:
n k : ℕ
hk : k.succ ≤ n + 1
inl : ∀ (hk₁ : k.succ < n + 1), (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
have inr : ∀ (hk₁ : k.succ = n + 1), (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
Tactic: rcases lt_or_eq_of_le hk with hk₁ | hk₁
-- 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.choose k * k.succ ! * (n - k)! = (k + 1) * n !
have rw : n.choose k * k.succ ! * (n - k)! = (k + 1) * (n.choose k * k ! * (n - k)!)
Tactic: rw [← choose_mul_factorial_mul_factorial (le_of_succ_le_succ hk)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (hypothesis)
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 h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
Tactic: have h : choose n k * k.succ ! * (n - k)! = (k + 1) * n ! := by
        rw [← choose_mul_factorial_mul_factorial (le_of_succ_le_succ hk)]
        simp [factorial_succ, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]
-- 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 !
⊢ (n - k)! = (n - k) * (n - k.succ)!
have rw : (n.succ - k.succ)! = (n.succ - k.succ) * (n - k.succ)!
Tactic: rw [← succ_sub_succ, succ_sub (le_of_lt_succ hk₁), factorial_succ]
-- 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 !
rw : (n.succ - k.succ)! = (n.succ - k.succ) * (n - k.succ)!
⊢ (n - k)! = (n - k) * (n - k.succ)!
have rw₁ : (n - k.succ).succ ! = (n - k.succ).succ * (n - k.succ)!
Tactic: rw [← succ_sub_succ, succ_sub (le_of_lt_succ hk₁), factorial_succ]
-- 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 !
rw : (n.succ - k.succ)! = (n.succ - k.succ) * (n - k.succ)!
rw₁ : (n - k.succ).succ ! = (n - k.succ).succ * (n - k.succ)!
⊢ (n - k)! = (n - k) * (n - k.succ)!
have rw₂ : (n - k.succ + 1) * (n - k.succ)! = (n - k.succ).succ * (n - k.succ)!
Tactic: rw [← succ_sub_succ, succ_sub (le_of_lt_succ hk₁), factorial_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (hypothesis)
Goal:
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
have h₁ : (n - k)! = (n - k) * (n - k.succ)!
Tactic: have h₁ : (n - k)! = (n - k) * (n - k.succ)! := by
        rw [← succ_sub_succ, succ_sub (le_of_lt_succ hk₁), factorial_succ]
-- 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)!
⊢ n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
have rw : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * (n.choose k.succ * k.succ ! * (n - k.succ)!)
Tactic: rw [← choose_mul_factorial_mul_factorial (le_of_lt_succ hk₁)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (hypothesis)
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)!
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
have h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
Tactic: have h₂ : choose n (succ k) * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n ! := by
        rw [← choose_mul_factorial_mul_factorial (le_of_lt_succ hk₁)]
        simp [factorial_succ, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Basic (hypothesis)
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 !
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
have h₃ : k * n ! ≤ n * n !
Tactic: have h₃ : k * n ! ≤ n * n ! := Nat.mul_le_mul_right _ (le_of_succ_le_succ hk)
-- 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 !
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
have inl : (n.choose k + n.choose k.succ) * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
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
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)!
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
have inl₁ : (n.choose k * k.succ ! + n.choose k.succ * k.succ !) * (n + 1 - k.succ)! = (n + 1)!
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
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)!
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
have inl₂ : n.choose k * k.succ ! * (n + 1 - k.succ)! + n.choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
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
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)!
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
have inl₃ : n.choose k * k.succ ! * (n - k)! + n.choose k.succ * k.succ ! * (n - k)! = (n + 1)!
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
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)!
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
have inl₄ : (k + 1) * n ! + n.choose k.succ * k.succ ! * (n - k)! = (n + 1)!
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
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)!
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
have inl₅ : (k + 1) * n ! + n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n + 1)!
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
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)!
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
have inl₆ : (k + 1) * n ! + (n - k) * n ! = (n + 1)!
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
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)!
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
have inl₇ : k * n ! + 1 * n ! + (n - k) * n ! = (n + 1)!
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
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)!
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
have inl₈ : k * n ! + 1 * n ! + (n * n ! - k * n !) = (n + 1)!
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
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)!
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
have inl₉ : k * n ! + 1 * n ! + (n * n ! - k * 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
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 !
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
have inl₁₀ : k * n ! + 1 * n ! + n * n ! - k * 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
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 !
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
have inl₁₁ : k * n ! + (1 * n ! + n * n !) - k * 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
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 !
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
have inl₁₂ : k * n ! + (1 + n) * n ! - k * 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
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 !
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
have inl₁₃ : (1 + n) * 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]