-- Mathlib/Algebra/GeomSum.lean
theorem Commute.mul_geom_sum₂_Ico [Ring α] {x y : α} (h : Commute x y) {m n : ℕ}
    (hmn : m ≤ n) :
    ((x - y) * ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i)) = x ^ n - x ^ m * y ^ (n - m)

Proof state:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) = ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - ∑ x_1 ∈ range m, x ^ x_1 * y ^ (m - 1 - x_1) * y ^ (n - m)) =
    x ^ n - x ^ m * y ^ (n - m)

Tactic:
rw [← sum_mul, mul_sub, h.mul_geom_sum₂, ← mul_assoc, h.mul_geom_sum₂, sub_mul, ← pow_add,
  add_tsub_cancel_of_le hmn, sub_sub_sub_cancel_right (x ^ n) (x ^ m * y ^ (n - m)) (y ^ n)]

Result:
no goals

Proof state:
case e_a.e_a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j ∈ range m
⊢ n - 1 - j = n - m + (m - 1 - j)

Tactic:
rw [mem_range] at j_in

Result:
case e_a.e_a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j < m
⊢ n - 1 - j = n - m + (m - 1 - j)

Proof state:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j ∈ range m
⊢ x ^ j * y ^ (n - 1 - j) = x ^ j * y ^ (n - m + (m - 1 - j))

Tactic:
congr

Result:
case e_a.e_a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j ∈ range m
⊢ n - 1 - j = n - m + (m - 1 - j)

Proof state:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) = ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k)) =
    x ^ n - x ^ m * y ^ (n - m)

Tactic:
rw [this]

Result:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) = ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))) =
    x ^ n - x ^ m * y ^ (n - m)

Proof state:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j ∈ range m
⊢ x ^ j * y ^ (n - 1 - j) = x ^ j * (y ^ (n - m) * y ^ (m - 1 - j))

Tactic:
rw [← pow_add]

Result:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j ∈ range m
⊢ x ^ j * y ^ (n - 1 - j) = x ^ j * y ^ (n - m + (m - 1 - j))

Proof state:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) = ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - ∑ x_1 ∈ range m, x ^ x_1 * (y ^ (m - 1 - x_1) * y ^ (n - m))) =
    x ^ n - x ^ m * y ^ (n - m)

Tactic:
simp_rw [← mul_assoc]

Result:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) = ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - ∑ x_1 ∈ range m, x ^ x_1 * y ^ (m - 1 - x_1) * y ^ (n - m)) =
    x ^ n - x ^ m * y ^ (n - m)

Proof state:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ (x - y) * ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = x ^ n - x ^ m * y ^ (n - m)

Tactic:
rw [sum_Ico_eq_sub _ hmn]

Result:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k)) =
    x ^ n - x ^ m * y ^ (n - m)

Proof state:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) = ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))) =
    x ^ n - x ^ m * y ^ (n - m)

Tactic:
simp_rw [pow_mul_comm y (n - m) _]

Result:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) = ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - ∑ x_1 ∈ range m, x ^ x_1 * (y ^ (m - 1 - x_1) * y ^ (n - m))) =
    x ^ n - x ^ m * y ^ (n - m)

Proof state:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k)) =
    x ^ n - x ^ m * y ^ (n - m)

Tactic:
have :
  ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) =
    ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k)) := by
  refine sum_congr rfl fun j j_in => ?_
  rw [← pow_add]
  congr
  rw [mem_range] at j_in
  omega

Result:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) = ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k)) =
    x ^ n - x ^ m * y ^ (n - m)

Proof state:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) = ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))

Tactic:
refine sum_congr rfl fun j j_in => ?_

Result:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j ∈ range m
⊢ x ^ j * y ^ (n - 1 - j) = x ^ j * (y ^ (n - m) * y ^ (m - 1 - j))

Proof state:
case e_a.e_a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j < m
⊢ n - 1 - j = n - m + (m - 1 - j)

Tactic:
omega

Result:
no goals