awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this_1 : Commute y ((x + y) ^ i)
this : n - (i + 1) + (i + 1) = n
rw : (x + y) ^ i * y ^ (n - (i + 1) + (i + 1) - i) = (x + y) ^ i * y ^ (n - (i + 1) + (i + 1) - (i + 1) + 1)
rw₁ : (x + y) ^ i * y ^ (n - (i + 1) + (i + 1) - i) = (x + y) ^ i * y ^ (n - (i + 1) + 1)
rw₂ : (x + y) ^ i * y ^ (n - (1 + i) + (1 + i) - i) = (x + y) ^ i * y ^ (n - (1 + i) + 1)
⊢ (x + y) ^ i * y ^ (n - i) = (x + y) ^ i * y ^ (n - (i + 1) + 1)
have rw₃ : (x + y) ^ i * y ^ (n - (1 + i) + 1 + i - i) = (x + y) ^ i * y ^ (n - (1 + i) + 1)
Tactic: rw [← this, add_tsub_cancel_right, add_comm i 1, ← add_assoc, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this_1 : Commute y ((x + y) ^ i)
this : n - (i + 1) + (i + 1) = n
rw : (x + y) ^ i * y ^ (n - (i + 1) + (i + 1) - i) = (x + y) ^ i * y ^ (n - (i + 1) + (i + 1) - (i + 1) + 1)
rw₁ : (x + y) ^ i * y ^ (n - (i + 1) + (i + 1) - i) = (x + y) ^ i * y ^ (n - (i + 1) + 1)
rw₂ : (x + y) ^ i * y ^ (n - (1 + i) + (1 + i) - i) = (x + y) ^ i * y ^ (n - (1 + i) + 1)
rw₃ : (x + y) ^ i * y ^ (n - (1 + i) + 1 + i - i) = (x + y) ^ i * y ^ (n - (1 + i) + 1)
⊢ (x + y) ^ i * y ^ (n - i) = (x + y) ^ i * y ^ (n - (i + 1) + 1)
have rw₄ : (x + y) ^ i * y ^ (n - (1 + i) + 1) = (x + y) ^ i * y ^ (n - (1 + i) + 1)
Tactic: rw [← this, add_tsub_cancel_right, add_comm i 1, ← add_assoc, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
⊢ (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) ^ (n + 1)
have f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
Tactic: have f_succ : ∀ i, i ∈ range n → f (n + 1) i = y * f n i := fun i hi => by
      dsimp only [f]
      have : Commute y ((x + y) ^ i) := (h.symm.add_right (Commute.refl y)).pow_right i
      rw [← mul_assoc, this.eq, mul_assoc, ← pow_succ' y (n - 1 - i), add_tsub_cancel_right,
        ← tsub_add_eq_tsub_tsub, add_comm 1 i]
      have : i + 1 + (n - (i + 1)) = n := add_tsub_cancel_of_le (mem_range.mp hi)
      rw [add_comm (i + 1)] at this
      rw [← this, add_tsub_cancel_right, add_comm i 1, ← add_assoc, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
⊢ (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) ^ (n + 1)
have succ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) * (x + y) ^ n
Tactic: rw [pow_succ' (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc,
      (((Commute.refl x).add_right h).pow_right n).eq, sum_congr rfl f_succ, ← mul_sum,
      pow_succ' y, mul_assoc, ← mul_add y, ih]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
succ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) * (x + y) ^ n
⊢ (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) ^ (n + 1)
have succ₁ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
Tactic: rw [pow_succ' (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc,
      (((Commute.refl x).add_right h).pow_right n).eq, sum_congr rfl f_succ, ← mul_sum,
      pow_succ' y, mul_assoc, ← mul_add y, ih]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
succ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) * (x + y) ^ n
succ₁ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
⊢ (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) ^ (n + 1)
have succ₂ : (f (n + 1) n + ∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
Tactic: rw [pow_succ' (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc,
      (((Commute.refl x).add_right h).pow_right n).eq, sum_congr rfl f_succ, ← mul_sum,
      pow_succ' y, mul_assoc, ← mul_add y, ih]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
succ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) * (x + y) ^ n
succ₁ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₂ : (f (n + 1) n + ∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
⊢ (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) ^ (n + 1)
have succ₃ : f (n + 1) n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
Tactic: rw [pow_succ' (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc,
      (((Commute.refl x).add_right h).pow_right n).eq, sum_congr rfl f_succ, ← mul_sum,
      pow_succ' y, mul_assoc, ← mul_add y, ih]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
succ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) * (x + y) ^ n
succ₁ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₂ : (f (n + 1) n + ∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₃ : f (n + 1) n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
⊢ (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) ^ (n + 1)
have succ₄ : (x + y) ^ n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
Tactic: rw [pow_succ' (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc,
      (((Commute.refl x).add_right h).pow_right n).eq, sum_congr rfl f_succ, ← mul_sum,
      pow_succ' y, mul_assoc, ← mul_add y, ih]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
succ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) * (x + y) ^ n
succ₁ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₂ : (f (n + 1) n + ∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₃ : f (n + 1) n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₄ : (x + y) ^ n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
⊢ (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) ^ (n + 1)
have succ₅ : (x + y) ^ n * x + ((∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1)) = x * (x + y) ^ n + y * (x + y) ^ n
Tactic: rw [pow_succ' (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc,
      (((Commute.refl x).add_right h).pow_right n).eq, sum_congr rfl f_succ, ← mul_sum,
      pow_succ' y, mul_assoc, ← mul_add y, ih]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
succ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) * (x + y) ^ n
succ₁ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₂ : (f (n + 1) n + ∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₃ : f (n + 1) n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₄ : (x + y) ^ n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₅ : (x + y) ^ n * x + ((∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1)) = x * (x + y) ^ n + y * (x + y) ^ n
⊢ (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) ^ (n + 1)
have succ₆ : (x + y) ^ n * x + ((∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1)) = (x + y) ^ n * x + y * (x + y) ^ n
Tactic: rw [pow_succ' (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc,
      (((Commute.refl x).add_right h).pow_right n).eq, sum_congr rfl f_succ, ← mul_sum,
      pow_succ' y, mul_assoc, ← mul_add y, ih]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
succ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) * (x + y) ^ n
succ₁ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₂ : (f (n + 1) n + ∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₃ : f (n + 1) n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₄ : (x + y) ^ n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₅ : (x + y) ^ n * x + ((∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1)) = x * (x + y) ^ n + y * (x + y) ^ n
succ₆ : (x + y) ^ n * x + ((∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1)) = (x + y) ^ n * x + y * (x + y) ^ n
⊢ (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) ^ (n + 1)
have succ₇ : (x + y) ^ n * x + ((∑ x ∈ range n, y * f n x) * x + y ^ (n + 1)) = (x + y) ^ n * x + y * (x + y) ^ n
Tactic: rw [pow_succ' (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc,
      (((Commute.refl x).add_right h).pow_right n).eq, sum_congr rfl f_succ, ← mul_sum,
      pow_succ' y, mul_assoc, ← mul_add y, ih]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
succ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) * (x + y) ^ n
succ₁ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₂ : (f (n + 1) n + ∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₃ : f (n + 1) n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₄ : (x + y) ^ n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₅ : (x + y) ^ n * x + ((∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1)) = x * (x + y) ^ n + y * (x + y) ^ n
succ₆ : (x + y) ^ n * x + ((∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1)) = (x + y) ^ n * x + y * (x + y) ^ n
succ₇ : (x + y) ^ n * x + ((∑ x ∈ range n, y * f n x) * x + y ^ (n + 1)) = (x + y) ^ n * x + y * (x + y) ^ n
⊢ (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) ^ (n + 1)
have succ₈ : (x + y) ^ n * x + ((y * ∑ i ∈ range n, f n i) * x + y ^ (n + 1)) = (x + y) ^ n * x + y * (x + y) ^ n
Tactic: rw [pow_succ' (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc,
      (((Commute.refl x).add_right h).pow_right n).eq, sum_congr rfl f_succ, ← mul_sum,
      pow_succ' y, mul_assoc, ← mul_add y, ih]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
succ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) * (x + y) ^ n
succ₁ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₂ : (f (n + 1) n + ∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₃ : f (n + 1) n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₄ : (x + y) ^ n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₅ : (x + y) ^ n * x + ((∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1)) = x * (x + y) ^ n + y * (x + y) ^ n
succ₆ : (x + y) ^ n * x + ((∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1)) = (x + y) ^ n * x + y * (x + y) ^ n
succ₇ : (x + y) ^ n * x + ((∑ x ∈ range n, y * f n x) * x + y ^ (n + 1)) = (x + y) ^ n * x + y * (x + y) ^ n
succ₈ : (x + y) ^ n * x + ((y * ∑ i ∈ range n, f n i) * x + y ^ (n + 1)) = (x + y) ^ n * x + y * (x + y) ^ n
⊢ (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) ^ (n + 1)
have succ₉ : (x + y) ^ n * x + ((y * ∑ i ∈ range n, f n i) * x + y * y ^ n) = (x + y) ^ n * x + y * (x + y) ^ n
Tactic: rw [pow_succ' (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc,
      (((Commute.refl x).add_right h).pow_right n).eq, sum_congr rfl f_succ, ← mul_sum,
      pow_succ' y, mul_assoc, ← mul_add y, ih]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
succ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) * (x + y) ^ n
succ₁ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₂ : (f (n + 1) n + ∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₃ : f (n + 1) n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₄ : (x + y) ^ n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₅ : (x + y) ^ n * x + ((∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1)) = x * (x + y) ^ n + y * (x + y) ^ n
succ₆ : (x + y) ^ n * x + ((∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1)) = (x + y) ^ n * x + y * (x + y) ^ n
succ₇ : (x + y) ^ n * x + ((∑ x ∈ range n, y * f n x) * x + y ^ (n + 1)) = (x + y) ^ n * x + y * (x + y) ^ n
succ₈ : (x + y) ^ n * x + ((y * ∑ i ∈ range n, f n i) * x + y ^ (n + 1)) = (x + y) ^ n * x + y * (x + y) ^ n
succ₉ : (x + y) ^ n * x + ((y * ∑ i ∈ range n, f n i) * x + y * y ^ n) = (x + y) ^ n * x + y * (x + y) ^ n
⊢ (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) ^ (n + 1)
have succ₁₀ : (x + y) ^ n * x + (y * ((∑ i ∈ range n, f n i) * x) + y * y ^ n) = (x + y) ^ n * x + y * (x + y) ^ n
Tactic: rw [pow_succ' (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc,
      (((Commute.refl x).add_right h).pow_right n).eq, sum_congr rfl f_succ, ← mul_sum,
      pow_succ' y, mul_assoc, ← mul_add y, ih]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
succ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) * (x + y) ^ n
succ₁ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₂ : (f (n + 1) n + ∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₃ : f (n + 1) n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₄ : (x + y) ^ n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₅ : (x + y) ^ n * x + ((∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1)) = x * (x + y) ^ n + y * (x + y) ^ n
succ₆ : (x + y) ^ n * x + ((∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1)) = (x + y) ^ n * x + y * (x + y) ^ n
succ₇ : (x + y) ^ n * x + ((∑ x ∈ range n, y * f n x) * x + y ^ (n + 1)) = (x + y) ^ n * x + y * (x + y) ^ n
succ₈ : (x + y) ^ n * x + ((y * ∑ i ∈ range n, f n i) * x + y ^ (n + 1)) = (x + y) ^ n * x + y * (x + y) ^ n
succ₉ : (x + y) ^ n * x + ((y * ∑ i ∈ range n, f n i) * x + y * y ^ n) = (x + y) ^ n * x + y * (x + y) ^ n
succ₁₀ : (x + y) ^ n * x + (y * ((∑ i ∈ range n, f n i) * x) + y * y ^ n) = (x + y) ^ n * x + y * (x + y) ^ n
⊢ (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) ^ (n + 1)
have succ₁₁ : (x + y) ^ n * x + y * ((∑ i ∈ range n, f n i) * x + y ^ n) = (x + y) ^ n * x + y * (x + y) ^ n
Tactic: rw [pow_succ' (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc,
      (((Commute.refl x).add_right h).pow_right n).eq, sum_congr rfl f_succ, ← mul_sum,
      pow_succ' y, mul_assoc, ← mul_add y, ih]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
succ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) * (x + y) ^ n
succ₁ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₂ : (f (n + 1) n + ∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₃ : f (n + 1) n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₄ : (x + y) ^ n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₅ : (x + y) ^ n * x + ((∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1)) = x * (x + y) ^ n + y * (x + y) ^ n
succ₆ : (x + y) ^ n * x + ((∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1)) = (x + y) ^ n * x + y * (x + y) ^ n
succ₇ : (x + y) ^ n * x + ((∑ x ∈ range n, y * f n x) * x + y ^ (n + 1)) = (x + y) ^ n * x + y * (x + y) ^ n
succ₈ : (x + y) ^ n * x + ((y * ∑ i ∈ range n, f n i) * x + y ^ (n + 1)) = (x + y) ^ n * x + y * (x + y) ^ n
succ₉ : (x + y) ^ n * x + ((y * ∑ i ∈ range n, f n i) * x + y * y ^ n) = (x + y) ^ n * x + y * (x + y) ^ n
succ₁₀ : (x + y) ^ n * x + (y * ((∑ i ∈ range n, f n i) * x) + y * y ^ n) = (x + y) ^ n * x + y * (x + y) ^ n
succ₁₁ : (x + y) ^ n * x + y * ((∑ i ∈ range n, f n i) * x + y ^ n) = (x + y) ^ n * x + y * (x + y) ^ n
⊢ (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) ^ (n + 1)
have succ₁₂ : (x + y) ^ n * x + y * (x + y) ^ n = (x + y) ^ n * x + y * (x + y) ^ n
Tactic: rw [pow_succ' (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc,
      (((Commute.refl x).add_right h).pow_right n).eq, sum_congr rfl f_succ, ← mul_sum,
      pow_succ' y, mul_assoc, ← mul_add y, ih]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n : ℕ
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
⊢ (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
have zero : (∑ i ∈ range 0, f 0 i) * x + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
Tactic: induction n with
  | zero => rw [range_zero, sum_empty, zero_mul, zero_add, pow_zero, pow_zero]
  | succ n ih =>
    have f_last : f (n + 1) n = (x + y) ^ n := by
      dsimp only [f]
      rw [← tsub_add_eq_tsub_tsub, Nat.add_comm, tsub_self, pow_zero, mul_one]
    have f_succ : ∀ i, i ∈ range n → f (n + 1) i = y * f n i := fun i hi => by
      dsimp only [f]
      have : Commute y ((x + y) ^ i) := (h.symm.add_right (Commute.refl y)).pow_right i
      rw [← mul_assoc, this.eq, mul_assoc, ← pow_succ' y (n - 1 - i), add_tsub_cancel_right,
        ← tsub_add_eq_tsub_tsub, add_comm 1 i]
      have : i + 1 + (n - (i + 1)) = n := add_tsub_cancel_of_le (mem_range.mp hi)
      rw [add_comm (i + 1)] at this
      rw [← this, add_tsub_cancel_right, add_comm i 1, ← add_assoc, add_tsub_cancel_right]
    rw [pow_succ' (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc,
      (((Commute.refl x).add_right h).pow_right n).eq, sum_congr rfl f_succ, ← mul_sum,
      pow_succ' y, mul_assoc, ← mul_add y, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n : ℕ
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
zero : (∑ i ∈ range 0, f 0 i) * x + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
⊢ (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
have succ : ∀ (n : ℕ) (ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n),
  (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) ^ (n + 1)
Tactic: induction n with
  | zero => rw [range_zero, sum_empty, zero_mul, zero_add, pow_zero, pow_zero]
  | succ n ih =>
    have f_last : f (n + 1) n = (x + y) ^ n := by
      dsimp only [f]
      rw [← tsub_add_eq_tsub_tsub, Nat.add_comm, tsub_self, pow_zero, mul_one]
    have f_succ : ∀ i, i ∈ range n → f (n + 1) i = y * f n i := fun i hi => by
      dsimp only [f]
      have : Commute y ((x + y) ^ i) := (h.symm.add_right (Commute.refl y)).pow_right i
      rw [← mul_assoc, this.eq, mul_assoc, ← pow_succ' y (n - 1 - i), add_tsub_cancel_right,
        ← tsub_add_eq_tsub_tsub, add_comm 1 i]
      have : i + 1 + (n - (i + 1)) = n := add_tsub_cancel_of_le (mem_range.mp hi)
      rw [add_comm (i + 1)] at this
      rw [← this, add_tsub_cancel_right, add_comm i 1, ← add_assoc, add_tsub_cancel_right]
    rw [pow_succ' (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc,
      (((Commute.refl x).add_right h).pow_right n).eq, sum_congr rfl f_succ, ← mul_sum,
      pow_succ' y, mul_assoc, ← mul_add y, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R
n : ℕ
⊢ #(range n) • x ^ (n - 1) = (↑n : R) * x ^ (n - 1)
have rw : n • x ^ (n - 1) = (↑n : R) * x ^ (n - 1)
Tactic: rw [Finset.card_range, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R
n : ℕ
rw : n • x ^ (n - 1) = (↑n : R) * x ^ (n - 1)
⊢ #(range n) • x ^ (n - 1) = (↑n : R) * x ^ (n - 1)
have rw₁ : (↑n : R) * x ^ (n - 1) = (↑n : R) * x ^ (n - 1)
Tactic: rw [Finset.card_range, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
x : R
n : ℕ
⊢ (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
have this : (∑ i ∈ range n, (x + 1) ^ i * HPow.hPow (α := R) 1 (n - 1 - i)) * x + HPow.hPow (α := R) 1 n = (x + 1) ^ n
Tactic: have := (Commute.one_right x).geom_sum₂_mul_add n