awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h_last : ∀ (n : ℕ), t n n.succ = 0
⊢ (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
have h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
Tactic: have h_middle :
      ∀ n i : ℕ, i ∈ range n.succ → (t n.succ i.succ) = x * t n i + y * t n i.succ := by
    intro n i h_mem
    have h_le : i ≤ n := le_of_lt_succ (mem_range.mp h_mem)
    dsimp only [t]
    rw [choose_succ_succ, cast_add, mul_add]
    congr 1
    · rw [pow_succ' x, succ_sub_succ, mul_assoc, mul_assoc, mul_assoc]
    · rw [← mul_assoc y, ← mul_assoc y, (h.symm.pow_right i.succ).eq]
      by_cases h_eq : i = n
      · rw [h_eq, choose_succ_self, cast_zero, mul_zero, mul_zero]
      · rw [succ_sub (lt_of_le_of_ne h_le h_eq)]
        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
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
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ HPow.hPow (β := ℕ) (x + y) 0 = ∑ m ∈ range (HAdd.hAdd (α := ℕ) 0 1), t 0 m
have zero : 1 = t 0 0
Tactic: rw [pow_zero, sum_range_succ, range_zero, sum_empty, zero_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
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
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ 1 = HPow.hPow (β := ℕ) x 0 * y ^ HSub.hSub (α := ℕ) 0 0 * (↑(Nat.choose 0 0) : R)
have zero : 1 = 1 * y ^ HSub.hSub (α := ℕ) 0 0 * (↑(Nat.choose 0 0) : R)
Tactic: rw [pow_zero, pow_zero, choose_self, cast_one, mul_one, mul_one]
-- 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
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
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
zero : 1 = 1 * y ^ HSub.hSub (α := ℕ) 0 0 * (↑(Nat.choose 0 0) : R)
⊢ 1 = HPow.hPow (β := ℕ) x 0 * y ^ HSub.hSub (α := ℕ) 0 0 * (↑(Nat.choose 0 0) : R)
have zero₁ : 1 = HMul.hMul (α := R) 1 1 * (↑(Nat.choose 0 0) : R)
Tactic: rw [pow_zero, pow_zero, choose_self, cast_one, mul_one, mul_one]
-- 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
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
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
zero : 1 = 1 * y ^ HSub.hSub (α := ℕ) 0 0 * (↑(Nat.choose 0 0) : R)
zero₁ : 1 = HMul.hMul (α := R) 1 1 * (↑(Nat.choose 0 0) : R)
⊢ 1 = HPow.hPow (β := ℕ) x 0 * y ^ HSub.hSub (α := ℕ) 0 0 * (↑(Nat.choose 0 0) : R)
have zero₂ : 1 = HMul.hMul (α := R) 1 1 * (↑1 : R)
Tactic: rw [pow_zero, pow_zero, choose_self, cast_one, mul_one, mul_one]
-- 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
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
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
zero : 1 = 1 * y ^ HSub.hSub (α := ℕ) 0 0 * (↑(Nat.choose 0 0) : R)
zero₁ : 1 = HMul.hMul (α := R) 1 1 * (↑(Nat.choose 0 0) : R)
zero₂ : 1 = HMul.hMul (α := R) 1 1 * (↑1 : R)
⊢ 1 = HPow.hPow (β := ℕ) x 0 * y ^ HSub.hSub (α := ℕ) 0 0 * (↑(Nat.choose 0 0) : R)
have zero₃ : 1 = HMul.hMul (α := R) 1 1 * 1
Tactic: rw [pow_zero, pow_zero, choose_self, cast_one, mul_one, mul_one]
-- 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
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
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
zero : 1 = 1 * y ^ HSub.hSub (α := ℕ) 0 0 * (↑(Nat.choose 0 0) : R)
zero₁ : 1 = HMul.hMul (α := R) 1 1 * (↑(Nat.choose 0 0) : R)
zero₂ : 1 = HMul.hMul (α := R) 1 1 * (↑1 : R)
zero₃ : 1 = HMul.hMul (α := R) 1 1 * 1
⊢ 1 = HPow.hPow (β := ℕ) x 0 * y ^ HSub.hSub (α := ℕ) 0 0 * (↑(Nat.choose 0 0) : R)
have zero₄ : 1 = HMul.hMul (α := R) 1 1
Tactic: rw [pow_zero, pow_zero, choose_self, cast_one, mul_one, mul_one]
-- 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
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
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
zero : 1 = 1 * y ^ HSub.hSub (α := ℕ) 0 0 * (↑(Nat.choose 0 0) : R)
zero₁ : 1 = HMul.hMul (α := R) 1 1 * (↑(Nat.choose 0 0) : R)
zero₂ : 1 = HMul.hMul (α := R) 1 1 * (↑1 : R)
zero₃ : 1 = HMul.hMul (α := R) 1 1 * 1
zero₄ : 1 = HMul.hMul (α := R) 1 1
⊢ 1 = HPow.hPow (β := ℕ) x 0 * y ^ HSub.hSub (α := ℕ) 0 0 * (↑(Nat.choose 0 0) : R)
have zero₅ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [pow_zero, pow_zero, choose_self, cast_one, mul_one, mul_one]
-- 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
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
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ HAdd.hAdd (α := R) (∑ i ∈ range (n + 1), x * t n i) (∑ i ∈ range (n + 1), y * t n i) =
    ∑ x_1 ∈ range n.succ, x * t n x_1 + (∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1))
have succ : ∑ i ∈ range (n + 1), y * t n i = ∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1)
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
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
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ ∑ i ∈ range (n + 1), y * t n i = ∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1)
have succ : ∑ k ∈ range n, y * t n (k + 1) + y * t n 0 = ∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1)
Tactic: rw [sum_range_succ', sum_range_succ, h_first, h_last, mul_zero, add_zero, _root_.pow_succ']
-- 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
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
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
succ : ∑ k ∈ range n, y * t n (k + 1) + y * t n 0 = ∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1)
⊢ ∑ i ∈ range (n + 1), y * t n i = ∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1)
have succ₁ : ∑ k ∈ range n, y * t n (k + 1) + y * t n 0 = ∑ x ∈ range n, y * t n x.succ + y * t n n.succ + y ^ (n + 1)
Tactic: rw [sum_range_succ', sum_range_succ, h_first, h_last, mul_zero, add_zero, _root_.pow_succ']
-- 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
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
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
succ : ∑ k ∈ range n, y * t n (k + 1) + y * t n 0 = ∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1)
succ₁ : ∑ k ∈ range n, y * t n (k + 1) + y * t n 0 = ∑ x ∈ range n, y * t n x.succ + y * t n n.succ + y ^ (n + 1)
⊢ ∑ i ∈ range (n + 1), y * t n i = ∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1)
have succ₂ : ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = ∑ x ∈ range n, y * t n x.succ + y * t n n.succ + y ^ (n + 1)
Tactic: rw [sum_range_succ', sum_range_succ, h_first, h_last, mul_zero, add_zero, _root_.pow_succ']
-- 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
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
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
succ : ∑ k ∈ range n, y * t n (k + 1) + y * t n 0 = ∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1)
succ₁ : ∑ k ∈ range n, y * t n (k + 1) + y * t n 0 = ∑ x ∈ range n, y * t n x.succ + y * t n n.succ + y ^ (n + 1)
succ₂ : ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = ∑ x ∈ range n, y * t n x.succ + y * t n n.succ + y ^ (n + 1)
⊢ ∑ i ∈ range (n + 1), y * t n i = ∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1)
have succ₃ : ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = ∑ x ∈ range n, y * t n x.succ + y * 0 + y ^ (n + 1)
Tactic: rw [sum_range_succ', sum_range_succ, h_first, h_last, mul_zero, add_zero, _root_.pow_succ']
-- 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
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
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
succ : ∑ k ∈ range n, y * t n (k + 1) + y * t n 0 = ∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1)
succ₁ : ∑ k ∈ range n, y * t n (k + 1) + y * t n 0 = ∑ x ∈ range n, y * t n x.succ + y * t n n.succ + y ^ (n + 1)
succ₂ : ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = ∑ x ∈ range n, y * t n x.succ + y * t n n.succ + y ^ (n + 1)
succ₃ : ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = ∑ x ∈ range n, y * t n x.succ + y * 0 + y ^ (n + 1)
⊢ ∑ i ∈ range (n + 1), y * t n i = ∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1)
have succ₄ : ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = HAdd.hAdd (α := R) (∑ x ∈ range n, y * t n x.succ) 0 + y ^ (n + 1)
Tactic: rw [sum_range_succ', sum_range_succ, h_first, h_last, mul_zero, add_zero, _root_.pow_succ']
-- 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
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
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
succ : ∑ k ∈ range n, y * t n (k + 1) + y * t n 0 = ∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1)
succ₁ : ∑ k ∈ range n, y * t n (k + 1) + y * t n 0 = ∑ x ∈ range n, y * t n x.succ + y * t n n.succ + y ^ (n + 1)
succ₂ : ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = ∑ x ∈ range n, y * t n x.succ + y * t n n.succ + y ^ (n + 1)
succ₃ : ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = ∑ x ∈ range n, y * t n x.succ + y * 0 + y ^ (n + 1)
succ₄ : ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = HAdd.hAdd (α := R) (∑ x ∈ range n, y * t n x.succ) 0 + y ^ (n + 1)
⊢ ∑ i ∈ range (n + 1), y * t n i = ∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1)
have succ₅ : ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = ∑ x ∈ range n, y * t n x.succ + y ^ (n + 1)
Tactic: rw [sum_range_succ', sum_range_succ, h_first, h_last, mul_zero, add_zero, _root_.pow_succ']
-- 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
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
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
succ : ∑ k ∈ range n, y * t n (k + 1) + y * t n 0 = ∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1)
succ₁ : ∑ k ∈ range n, y * t n (k + 1) + y * t n 0 = ∑ x ∈ range n, y * t n x.succ + y * t n n.succ + y ^ (n + 1)
succ₂ : ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = ∑ x ∈ range n, y * t n x.succ + y * t n n.succ + y ^ (n + 1)
succ₃ : ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = ∑ x ∈ range n, y * t n x.succ + y * 0 + y ^ (n + 1)
succ₄ : ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = HAdd.hAdd (α := R) (∑ x ∈ range n, y * t n x.succ) 0 + y ^ (n + 1)
succ₅ : ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = ∑ x ∈ range n, y * t n x.succ + y ^ (n + 1)
⊢ ∑ i ∈ range (n + 1), y * t n i = ∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1)
have succ₆ : ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = ∑ x ∈ range n, y * t n x.succ + y * y ^ n
Tactic: rw [sum_range_succ', sum_range_succ, h_first, h_last, mul_zero, add_zero, _root_.pow_succ']
-- 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 : ℕ
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
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
have zero : HPow.hPow (β := ℕ) (x + y) 0 = ∑ m ∈ range (HAdd.hAdd (α := ℕ) 0 1), t 0 m
Tactic: induction n with
  | zero =>
    rw [pow_zero, sum_range_succ, range_zero, sum_empty, zero_add]
    dsimp only [t]
    rw [pow_zero, pow_zero, choose_self, cast_one, mul_one, mul_one]
  | succ n ih =>
    rw [sum_range_succ', h_first, sum_congr rfl (h_middle n), sum_add_distrib, add_assoc,
      pow_succ' (x + y), ih, add_mul, mul_sum, mul_sum]
    congr 1
    rw [sum_range_succ', sum_range_succ, h_first, h_last, mul_zero, add_zero, _root_.pow_succ']
Cleared hypotheses: 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 : ℕ
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
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
zero : HPow.hPow (β := ℕ) (x + y) 0 = ∑ m ∈ range (HAdd.hAdd (α := ℕ) 0 1), t 0 m
⊢ (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
have succ : ∀ (n : ℕ) (ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m), (x + y) ^ (n + 1) = ∑ m ∈ range (n + 1 + 1), t (n + 1) m
Tactic: induction n with
  | zero =>
    rw [pow_zero, sum_range_succ, range_zero, sum_empty, zero_add]
    dsimp only [t]
    rw [pow_zero, pow_zero, choose_self, cast_one, mul_one, mul_one]
  | succ n ih =>
    rw [sum_range_succ', h_first, sum_congr rfl (h_middle n), sum_add_distrib, add_assoc,
      pow_succ' (x + y), ih, add_mul, mul_sum, mul_sum]
    congr 1
    rw [sum_range_succ', sum_range_succ, h_first, h_last, mul_zero, add_zero, _root_.pow_succ']
Cleared hypotheses: 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 : ℕ
⊢ (x + y) ^ n = ∑ m ∈ @antidiagonal _ instAddMonoid _ n, n.choose m.1 • (x ^ m.1 * y ^ m.2)
have simp_rw : (x + y) ^ n = ∑ k ∈ range n.succ, n.choose k • (x ^ k * y ^ (n - k))
Tactic: simp_rw [Nat.sum_antidiagonal_eq_sum_range_succ fun m p ↦ n.choose m • (x ^ m * y ^ p),
    nsmul_eq_mul, cast_comm, h.add_pow]
-- 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 : ℕ
simp_rw : (x + y) ^ n = ∑ k ∈ range n.succ, n.choose k • (x ^ k * y ^ (n - k))
⊢ (x + y) ^ n = ∑ m ∈ @antidiagonal _ instAddMonoid _ n, n.choose m.1 • (x ^ m.1 * y ^ m.2)
have simp_rw₁ : (x + y) ^ n = ∑ x_1 ∈ range n.succ, (↑(n.choose x_1) : R) * (x ^ x_1 * y ^ (n - x_1))
Tactic: simp_rw [Nat.sum_antidiagonal_eq_sum_range_succ fun m p ↦ n.choose m • (x ^ m * y ^ p),
    nsmul_eq_mul, cast_comm, h.add_pow]
-- 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 : ℕ
simp_rw : (x + y) ^ n = ∑ k ∈ range n.succ, n.choose k • (x ^ k * y ^ (n - k))
simp_rw₁ : (x + y) ^ n = ∑ x_1 ∈ range n.succ, (↑(n.choose x_1) : R) * (x ^ x_1 * y ^ (n - x_1))
⊢ (x + y) ^ n = ∑ m ∈ @antidiagonal _ instAddMonoid _ n, n.choose m.1 • (x ^ m.1 * y ^ m.2)
have simp_rw₂ : (x + y) ^ n = ∑ x_1 ∈ range n.succ, x ^ x_1 * y ^ (n - x_1) * (↑(n.choose x_1) : R)
Tactic: simp_rw [Nat.sum_antidiagonal_eq_sum_range_succ fun m p ↦ n.choose m • (x ^ m * y ^ p),
    nsmul_eq_mul, cast_comm, h.add_pow]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
n : ℕ
⊢ (x - y) ^ n = ∑ m ∈ range (n + 1), HPow.hPow (α := R) (-1) (m + n) * x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
have rw : Eq.{u_1 + 1} (α := R) (∑ m ∈ range (n + 1), x ^ m * (-y) ^ (n - m) * (↑(n.choose m) : R))
  (∑ m ∈ range (n + 1), HPow.hPow (α := R) (-1) (m + n) * x ^ m * y ^ (n - m) * (↑(n.choose m) : R))
Tactic: rw [sub_eq_add_neg, add_pow]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (∑ m ∈ range (n + 1), x ^ m * (-y) ^ (n - m) * (↑(n.choose m) : R))
    (∑ m ∈ range (n + 1), HPow.hPow (α := R) (-1) (m + n) * x ^ m * y ^ (n - m) * (↑(n.choose m) : R))
have a : ∀ (m : ℕ) (hm : m ∈ range (n + 1)),
  x ^ m * (-y) ^ (n - m) * (↑(n.choose m) : R) =
    HPow.hPow (α := R) (-1) (m + n) * x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
Tactic: congr! 1 with m hm
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
x y : R
n m : ℕ
hm : m ∈ range (n + 1)
⊢ HPow.hPow (α := R) (-1) (n - m) = HPow.hPow (α := R) (-1) (n + m)
have hm₁ : m < n + 1
Tactic: rw [mem_range] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
x y : R
n m : ℕ
hm : m ∈ range (n + 1)
⊢ x ^ m * (-y) ^ (n - m) * (↑(n.choose m) : R) =
    HPow.hPow (α := R) (-1) (m + n) * x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
have this : HPow.hPow (α := R) (-1) (n - m) = HPow.hPow (α := R) (-1) (n + m)
Tactic: have : (-1 : R) ^ (n - m) = (-1) ^ (n + m) := by
    rw [mem_range] at hm
    simp [show n + m = n - m + 2 * m by lia, pow_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
n m : ℕ
hm : m ∈ range (n + 1)
this : HPow.hPow (α := R) (-1) (n - m) = HPow.hPow (α := R) (-1) (n + m)
⊢ x ^ m * (-y) ^ (n - m) * (↑(n.choose m) : R) =
    HPow.hPow (α := R) (-1) (m + n) * x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
have a : x ^ m * (HPow.hPow (α := R) (-1) (n + m) * y ^ (n - m)) * (↑(n.choose m) : R) =
  HPow.hPow (α := R) (-1) (m + n) * x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
Tactic: rw [neg_pow, this]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (hypothesis)
Goal:
n : ℕ
⊢ ∑ m ∈ range (n + 1), n.choose m = HPow.hPow (α := ℕ) 2 n
have this : ∑ m ∈ range (n + 1), HPow.hPow (α := ℕ) 1 m * HPow.hPow (α := ℕ) 1 (n - m) * (↑(n.choose m) : ℕ) =
  HAdd.hAdd (α := ℕ) 1 1 ^ n
Tactic: have := (add_pow 1 1 n).symm
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
m i : ℕ
hi : i ∈ range (m + 1)
⊢ i ≤ 2 * m + 1
have linarith : 2 * m + 1 < i →
  HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 0 (↑m : ℤ) + (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 1 + 1 - (↑i : ℤ)) +
      (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1 - HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) =
    0
Tactic: linarith [mem_range.1 hi]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
m i : ℕ
hi : i ∈ range (m + 1)
linarith :
  2 * m + 1 < i →
    HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 0 (↑m : ℤ) + (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 1 + 1 - (↑i : ℤ)) +
        (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1 - HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) =
      0
⊢ i ≤ 2 * m + 1
have linarith₁ : 2 * m + 1 < i → GT.gt (α := ℤ) 2 0
Tactic: linarith [mem_range.1 hi]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
m : ℕ
this : Eq (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i)) (∑ i ∈ range (m + 1), (2 * m + 1).choose i)
⊢ HMul.hMul (α := ℕ) 2 (∑ i ∈ range (m + 1), (2 * m + 1).choose i) =
    HAdd.hAdd (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose i)
      (∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i))
have rw : HAdd.hAdd (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose i) (∑ i ∈ range (m + 1), (2 * m + 1).choose i) =
  HAdd.hAdd (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose i)
    (∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i))
Tactic: rw [two_mul, this]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
m : ℕ
this : Eq (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i)) (∑ i ∈ range (m + 1), (2 * m + 1).choose i)
rw :
  HAdd.hAdd (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose i) (∑ i ∈ range (m + 1), (2 * m + 1).choose i) =
    HAdd.hAdd (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose i)
      (∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i))
⊢ HMul.hMul (α := ℕ) 2 (∑ i ∈ range (m + 1), (2 * m + 1).choose i) =
    HAdd.hAdd (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose i)
      (∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i))
have rw₁ : HAdd.hAdd (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose i) (∑ i ∈ range (m + 1), (2 * m + 1).choose i) =
  HAdd.hAdd (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose i) (∑ i ∈ range (m + 1), (2 * m + 1).choose i)
Tactic: rw [two_mul, this]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
m : ℕ
this : Eq (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i)) (∑ i ∈ range (m + 1), (2 * m + 1).choose i)
⊢ HAdd.hAdd (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose i)
      (∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i)) =
    HAdd.hAdd (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose i) (∑ i ∈ Ico (m + 1) (2 * m + 2), (2 * m + 1).choose i)
have rw : HAdd.hAdd (α := ℕ) (∑ i ∈ Ico 0 (m + 1), (2 * m + 1).choose i)
    (∑ j ∈ Ico (2 * m + 1 + 1 - (m + 1)) (2 * m + 1 + 1 - 0), (2 * m + 1).choose j) =
  HAdd.hAdd (α := ℕ) (∑ i ∈ Ico 0 (m + 1), (2 * m + 1).choose i) (∑ i ∈ Ico (m + 1) (2 * m + 2), (2 * m + 1).choose i)
Tactic: rw [range_eq_Ico, sum_Ico_reflect _ _ (by lia)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
m : ℕ
this : Eq (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i)) (∑ i ∈ range (m + 1), (2 * m + 1).choose i)
⊢ HAdd.hAdd (α := ℕ) (∑ i ∈ Ico 0 (m + 1), (2 * m + 1).choose i)
      (∑ j ∈ Ico (2 * m + 1 + 1 - (m + 1)) (2 * m + 1 + 1 - 0), (2 * m + 1).choose j) =
    HAdd.hAdd (α := ℕ) (∑ i ∈ Ico 0 (m + 1), (2 * m + 1).choose i) (∑ i ∈ Ico (m + 1) (2 * m + 2), (2 * m + 1).choose i)
have e_a : 2 * m + 1 + 1 - (m + 1) = m + 1
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
m : ℕ
this : Eq (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i)) (∑ i ∈ range (m + 1), (2 * m + 1).choose i)
⊢ HPow.hPow (α := ℕ) 2 (2 * m + 1) = 2 * HPow.hPow (α := ℕ) 4 m
have rw : 2 * HPow.hPow (α := ℕ) (β := ℕ) 2 2 ^ m = 2 * HPow.hPow (α := ℕ) 4 m
Tactic: rw [pow_succ, pow_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (hypothesis)
Goal:
n : ℕ
⊢ (2 * n + 1).choose n ≤ HPow.hPow (α := ℕ) 4 n
have t : (2 * n + 1).choose n ≤ ∑ i ∈ range (n + 1), (2 * n + 1).choose i
Tactic: have t : (2 * n + 1).choose n ≤ ∑ i ∈ range (n + 1), (2 * n + 1).choose i :=
    single_le_sum (fun x _ ↦ by lia) (self_mem_range_succ n)