awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
m m' : Multiset ℕ
⊢ (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial
have empty : (0 + m').multinomial = (0 + m').sum.choose (sum 0) * multinomial 0 * m'.multinomial
Tactic: induction m using Multiset.induction_on with
  | empty => simp
  | cons x m hind =>
    simp only [cons_add, sum_cons, sum_add, multinomial_cons, hind, ← mul_assoc]
    congr 2
    rw [← Nat.choose_symm (Nat.le_add_right _ _), add_tsub_cancel_left, eq_comm,
      Nat.choose_mul (Nat.le_add_right _ _), ← Nat.choose_symm (Nat.le_add_right x _)]
    simp [add_tsub_cancel_left]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
m m' : Multiset ℕ
empty : (0 + m').multinomial = (0 + m').sum.choose (sum 0) * multinomial 0 * m'.multinomial
⊢ (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial
have cons : ∀ (x : ℕ) (m : Multiset ℕ) (hind : (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial),
  (x ::ₘ m + m').multinomial = (x ::ₘ m + m').sum.choose (x ::ₘ m).sum * (x ::ₘ m).multinomial * m'.multinomial
Tactic: induction m using Multiset.induction_on with
  | empty => simp
  | cons x m hind =>
    simp only [cons_add, sum_cons, sum_add, multinomial_cons, hind, ← mul_assoc]
    congr 2
    rw [← Nat.choose_symm (Nat.le_add_right _ _), add_tsub_cancel_left, eq_comm,
      Nat.choose_mul (Nat.le_add_right _ _), ← Nat.choose_symm (Nat.le_add_right x _)]
    simp [add_tsub_cancel_left]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
m : Multiset ℕ
k : ℕ
hk : (k • m).multinomial = (Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) * m.multinomial ^ k
⊢ ((k + 1) • m).multinomial = (Nat.multinomial (Finset.range (k + 1)) fun (x : ℕ) ↦ m.sum) * m.multinomial ^ (k + 1)
have succ : (m.sum + k • m.sum).choose m.sum * m.multinomial *
    ((Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) * m.multinomial ^ k) =
  ((m.sum + ∑ i ∈ Finset.range k, m.sum).choose m.sum * Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) *
    (m.multinomial * m.multinomial ^ k)
Tactic: rw [succ_nsmul', multinomial_add, hk, Finset.range_add_one,
      Nat.multinomial_insert (by simp), sum_add, sum_nsmul, pow_succ']
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
m : Multiset ℕ
k : ℕ
hk : (k • m).multinomial = (Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) * m.multinomial ^ k
⊢ (m.sum + k • m.sum).choose m.sum * m.multinomial *
      ((Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) * m.multinomial ^ k) =
    ((m.sum + ∑ i ∈ Finset.range k, m.sum).choose m.sum * Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) *
      (m.multinomial * m.multinomial ^ k)
have succ : (m.sum + k * m.sum).choose m.sum * m.multinomial *
    ((Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) * m.multinomial ^ k) =
  ((m.sum + k * m.sum).choose m.sum * Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) *
    (m.multinomial * m.multinomial ^ k)
Tactic: simp [smul_eq_mul, Finset.sum_const, Finset.card_range]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
k : ℕ
m : Multiset ℕ
⊢ (k • m).multinomial = (Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) * m.multinomial ^ k
have zero : (HSMul.hSMul (α := ℕ) 0 m).multinomial =
  (Nat.multinomial (Finset.range 0) fun (x : ℕ) ↦ m.sum) * HPow.hPow (β := ℕ) m.multinomial 0
Tactic: induction k with
  | zero => simp
  | succ k hk =>
    rw [succ_nsmul', multinomial_add, hk, Finset.range_add_one,
      Nat.multinomial_insert (by simp), sum_add, sum_nsmul, pow_succ']
    simp [smul_eq_mul, Finset.sum_const, Finset.card_range]
    ring
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Multinomial (goal)
Goal:
k : ℕ
m : Multiset ℕ
zero :
  (HSMul.hSMul (α := ℕ) 0 m).multinomial =
    (Nat.multinomial (Finset.range 0) fun (x : ℕ) ↦ m.sum) * HPow.hPow (β := ℕ) m.multinomial 0
⊢ (k • m).multinomial = (Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) * m.multinomial ^ k
have succ : ∀ (k : ℕ) (hk : (k • m).multinomial = (Nat.multinomial (Finset.range k) fun (x : ℕ) ↦ m.sum) * m.multinomial ^ k),
  ((k + 1) • m).multinomial = (Nat.multinomial (Finset.range (k + 1)) fun (x : ℕ) ↦ m.sum) * m.multinomial ^ (k + 1)
Tactic: induction k with
  | zero => simp
  | succ k hk =>
    rw [succ_nsmul', multinomial_add, hk, Finset.range_add_one,
      Nat.multinomial_insert (by simp), sum_add, sum_nsmul, pow_succ']
    simp [smul_eq_mul, Finset.sum_const, Finset.card_range]
    ring
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
⊢ (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
have h_first : ∀ (n : ℕ), t n 0 = y ^ n
Tactic: have h_first : ∀ n, t n 0 = y ^ n := fun n ↦ by
    simp only [t, choose_zero_right, pow_zero, cast_one, mul_one, one_mul, Nat.sub_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
⊢ (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
have h_last : ∀ (n : ℕ), t n n.succ = 0
Tactic: have h_last : ∀ n, t n n.succ = 0 := fun n ↦ by
    simp only [t, choose_succ_self, cast_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
⊢ t n.succ i.succ = x * t n i + y * t n i.succ
have h_le : i ≤ n
Tactic: have h_le : i ≤ n := le_of_lt_succ (mem_range.mp h_mem)
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.succ.choose i.succ) : R) =
    x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R)) + y * (x ^ i.succ * y ^ (n - i.succ) * (↑(n.choose i.succ) : R))
have rw : x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i) : R) +
    x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
  x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R)) + y * (x ^ i.succ * y ^ (n - i.succ) * (↑(n.choose i.succ) : R))
Tactic: rw [choose_succ_succ, cast_add, mul_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i) : R) +
      x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
    x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R)) + y * (x ^ i.succ * y ^ (n - i.succ) * (↑(n.choose i.succ) : R))
have e_a : x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i) : R) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
e_a : x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i) : R) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i) : R) +
      x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
    x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R)) + y * (x ^ i.succ * y ^ (n - i.succ) * (↑(n.choose i.succ) : R))
have e_a₁ : x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
  y * (x ^ i.succ * y ^ (n - i.succ) * (↑(n.choose i.succ) : R))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i) : R) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
have e_a : x * x ^ i * y ^ (n.succ - i.succ) * (↑(n.choose i) : R) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
Tactic: rw [pow_succ' x, succ_sub_succ, mul_assoc, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
e_a : x * x ^ i * y ^ (n.succ - i.succ) * (↑(n.choose i) : R) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i) : R) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
have e_a₁ : x * x ^ i * y ^ (n - i) * (↑(n.choose i) : R) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
Tactic: rw [pow_succ' x, succ_sub_succ, mul_assoc, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
e_a : x * x ^ i * y ^ (n.succ - i.succ) * (↑(n.choose i) : R) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
e_a₁ : x * x ^ i * y ^ (n - i) * (↑(n.choose i) : R) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i) : R) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
have e_a₂ : x * x ^ i * (y ^ (n - i) * (↑(n.choose i) : R)) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
Tactic: rw [pow_succ' x, succ_sub_succ, mul_assoc, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
e_a : x * x ^ i * y ^ (n.succ - i.succ) * (↑(n.choose i) : R) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
e_a₁ : x * x ^ i * y ^ (n - i) * (↑(n.choose i) : R) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
e_a₂ : x * x ^ i * (y ^ (n - i) * (↑(n.choose i) : R)) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i) : R) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
have e_a₃ : x * (x ^ i * (y ^ (n - i) * (↑(n.choose i) : R))) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
Tactic: rw [pow_succ' x, succ_sub_succ, mul_assoc, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
e_a : x * x ^ i * y ^ (n.succ - i.succ) * (↑(n.choose i) : R) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
e_a₁ : x * x ^ i * y ^ (n - i) * (↑(n.choose i) : R) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
e_a₂ : x * x ^ i * (y ^ (n - i) * (↑(n.choose i) : R)) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
e_a₃ : x * (x ^ i * (y ^ (n - i) * (↑(n.choose i) : R))) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i) : R) = x * (x ^ i * y ^ (n - i) * (↑(n.choose i) : R))
have e_a₄ : x * (x ^ i * (y ^ (n - i) * (↑(n.choose i) : R))) = x * (x ^ i * (y ^ (n - i) * (↑(n.choose i) : R)))
Tactic: rw [pow_succ' x, succ_sub_succ, mul_assoc, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
    y * (x ^ i.succ * y ^ (n - i.succ) * (↑(n.choose i.succ) : R))
have e_a : x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
  x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
Tactic: rw [← mul_assoc y, ← mul_assoc y, (h.symm.pow_right i.succ).eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
have pos : ∀ (h_eq : i = n),
  x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
Tactic: by_cases h_eq : i = n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
pos :
  ∀ (h_eq : i = n),
    x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
      x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
have neg : ∀ (h_eq : ¬i = n),
  x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
Tactic: by_cases h_eq : i = n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : i = n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
have pos : x ^ n.succ * y ^ (n.succ - n.succ) * (↑(n.choose n.succ) : R) =
  x ^ n.succ * y * y ^ (n - n.succ) * (↑(n.choose n.succ) : R)
Tactic: rw [h_eq, choose_succ_self, cast_zero, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : i = n
pos :
  x ^ n.succ * y ^ (n.succ - n.succ) * (↑(n.choose n.succ) : R) =
    x ^ n.succ * y * y ^ (n - n.succ) * (↑(n.choose n.succ) : R)
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
have pos₁ : x ^ n.succ * y ^ (n.succ - n.succ) * (↑0 : R) = x ^ n.succ * y * y ^ (n - n.succ) * (↑0 : R)
Tactic: rw [h_eq, choose_succ_self, cast_zero, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : i = n
pos :
  x ^ n.succ * y ^ (n.succ - n.succ) * (↑(n.choose n.succ) : R) =
    x ^ n.succ * y * y ^ (n - n.succ) * (↑(n.choose n.succ) : R)
pos₁ : x ^ n.succ * y ^ (n.succ - n.succ) * (↑0 : R) = x ^ n.succ * y * y ^ (n - n.succ) * (↑0 : R)
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
have pos₂ : x ^ n.succ * y ^ (n.succ - n.succ) * 0 = x ^ n.succ * y * y ^ (n - n.succ) * 0
Tactic: rw [h_eq, choose_succ_self, cast_zero, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : i = n
pos :
  x ^ n.succ * y ^ (n.succ - n.succ) * (↑(n.choose n.succ) : R) =
    x ^ n.succ * y * y ^ (n - n.succ) * (↑(n.choose n.succ) : R)
pos₁ : x ^ n.succ * y ^ (n.succ - n.succ) * (↑0 : R) = x ^ n.succ * y * y ^ (n - n.succ) * (↑0 : R)
pos₂ : x ^ n.succ * y ^ (n.succ - n.succ) * 0 = x ^ n.succ * y * y ^ (n - n.succ) * 0
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
have pos₃ : 0 = x ^ n.succ * y * y ^ (n - n.succ) * 0
Tactic: rw [h_eq, choose_succ_self, cast_zero, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : i = n
pos :
  x ^ n.succ * y ^ (n.succ - n.succ) * (↑(n.choose n.succ) : R) =
    x ^ n.succ * y * y ^ (n - n.succ) * (↑(n.choose n.succ) : R)
pos₁ : x ^ n.succ * y ^ (n.succ - n.succ) * (↑0 : R) = x ^ n.succ * y * y ^ (n - n.succ) * (↑0 : R)
pos₂ : x ^ n.succ * y ^ (n.succ - n.succ) * 0 = x ^ n.succ * y * y ^ (n - n.succ) * 0
pos₃ : 0 = x ^ n.succ * y * y ^ (n - n.succ) * 0
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
have pos₄ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [h_eq, choose_succ_self, cast_zero, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
have neg : x ^ i.succ * y ^ (n - i.succ).succ * (↑(n.choose i.succ) : R) =
  x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
Tactic: rw [succ_sub (lt_of_le_of_ne h_le h_eq)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
⊢ x ^ i.succ * y ^ (n - i.succ).succ * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
have neg : x ^ i.succ * (y * y ^ (n - i.succ)) * (↑(n.choose i.succ) : R) =
  x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
Tactic: rw [pow_succ' y, mul_assoc, mul_assoc, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
neg :
  x ^ i.succ * (y * y ^ (n - i.succ)) * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
⊢ x ^ i.succ * y ^ (n - i.succ).succ * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
have neg₁ : x ^ i.succ * (y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)) =
  x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
Tactic: rw [pow_succ' y, mul_assoc, mul_assoc, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
neg :
  x ^ i.succ * (y * y ^ (n - i.succ)) * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
neg₁ :
  x ^ i.succ * (y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
⊢ x ^ i.succ * y ^ (n - i.succ).succ * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
have neg₂ : x ^ i.succ * (y * (y ^ (n - i.succ) * (↑(n.choose i.succ) : R))) =
  x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
Tactic: rw [pow_succ' y, mul_assoc, mul_assoc, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
neg :
  x ^ i.succ * (y * y ^ (n - i.succ)) * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
neg₁ :
  x ^ i.succ * (y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
neg₂ :
  x ^ i.succ * (y * (y ^ (n - i.succ) * (↑(n.choose i.succ) : R))) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
⊢ x ^ i.succ * y ^ (n - i.succ).succ * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
have neg₃ : x ^ i.succ * (y * (y ^ (n - i.succ) * (↑(n.choose i.succ) : R))) =
  x ^ i.succ * y * (y ^ (n - i.succ) * (↑(n.choose i.succ) : R))
Tactic: rw [pow_succ' y, mul_assoc, mul_assoc, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
neg :
  x ^ i.succ * (y * y ^ (n - i.succ)) * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
neg₁ :
  x ^ i.succ * (y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
neg₂ :
  x ^ i.succ * (y * (y ^ (n - i.succ) * (↑(n.choose i.succ) : R))) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
neg₃ :
  x ^ i.succ * (y * (y ^ (n - i.succ) * (↑(n.choose i.succ) : R))) =
    x ^ i.succ * y * (y ^ (n - i.succ) * (↑(n.choose i.succ) : R))
⊢ x ^ i.succ * y ^ (n - i.succ).succ * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
have neg₄ : x ^ i.succ * (y * (y ^ (n - i.succ) * (↑(n.choose i.succ) : R))) =
  x ^ i.succ * (y * (y ^ (n - i.succ) * (↑(n.choose i.succ) : R)))
Tactic: rw [pow_succ' y, mul_assoc, mul_assoc, mul_assoc, mul_assoc]