-- Mathlib/Algebra/GeomSum.lean
theorem Commute.geom_sum₂_mul_add {x y : α} (h : Commute x y) (n : ℕ) :
    (∑ i ∈ range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n

Proof state:
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n : ℕ
⊢ (∑ i ∈ range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n

Tactic:
let f :  ℕ → ℕ → α := fun m i : ℕ => (x + y) ^ i * y ^ (m - 1 - i)

Result:
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n : ℕ
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
⊢ (∑ i ∈ range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n

Proof state:
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := 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 (n + 1) n = (x + y) ^ n

Tactic:
dsimp only [f]

Result:
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
⊢ (x + y) ^ n * y ^ (n + 1 - 1 - n) = (x + y) ^ n

Proof state:
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := 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
⊢ f (n + 1) i = y * f n i

Tactic:
dsimp only [f]

Result:
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := 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
⊢ (x + y) ^ i * y ^ (n + 1 - 1 - i) = y * ((x + y) ^ i * y ^ (n - 1 - i))

Proof state:
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := 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)

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]

Result:
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := 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)

Proof state:
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := 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 : Commute y ((x + y) ^ i)
⊢ (x + y) ^ i * y ^ (n + 1 - 1 - i) = y * ((x + y) ^ i * y ^ (n - 1 - i))

Tactic:
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]

Result:
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := 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 : Commute y ((x + y) ^ i)
⊢ (x + y) ^ i * y ^ (n - i) = (x + y) ^ i * y ^ (n - (i + 1) + 1)

Proof state:
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := 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
⊢ (x + y) ^ i * y ^ (n + 1 - 1 - i) = y * ((x + y) ^ i * y ^ (n - 1 - i))

Tactic:
have : Commute y ((x + y) ^ i) := (h.symm.add_right (Commute.refl y)).pow_right i

Result:
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := 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 : Commute y ((x + y) ^ i)
⊢ (x + y) ^ i * y ^ (n + 1 - 1 - i) = y * ((x + y) ^ i * y ^ (n - 1 - i))

Proof state:
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n : ℕ
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
⊢ (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n

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]

Result:
no goals

Proof state:
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n : ℕ
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
⊢ (∑ i ∈ range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n

Tactic:
change (∑ i ∈ range n, (f n) i) * x + y ^ n = (x + y) ^ n

Result:
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n : ℕ
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
⊢ (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n

Proof state:
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
⊢ (x + y) ^ n * y ^ (n + 1 - 1 - n) = (x + y) ^ n

Tactic:
rw [← tsub_add_eq_tsub_tsub, Nat.add_comm, tsub_self, pow_zero, mul_one]

Result:
no goals

Proof state:
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := 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 : Commute y ((x + y) ^ i)
⊢ (x + y) ^ i * y ^ (n - i) = (x + y) ^ i * y ^ (n - (i + 1) + 1)

Tactic:
have : i + 1 + (n - (i + 1)) = n := add_tsub_cancel_of_le (mem_range.mp hi)

Result:
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := 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✝ : Commute y ((x + y) ^ i)
this : i + 1 + (n - (i + 1)) = n
⊢ (x + y) ^ i * y ^ (n - i) = (x + y) ^ i * y ^ (n - (i + 1) + 1)

Proof state:
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
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:
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]

Result:
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := 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)