α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ (x - y) * (∑ k in range n, x ^ k * y ^ (n - 1 - k) - ∑ k in range m, x ^ k * y ^ (n - 1 - k)) =
    x ^ n - x ^ m * y ^ (n - m)
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ (x - y) * ∑ i in Ico m n, x ^ i * y ^ (n - 1 - i) = x ^ n - x ^ m * y ^ (n - m)
rw [sum_Ico_eq_sub _ hmn]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k in range m, x ^ k * y ^ (n - 1 - k) = ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k in range n, x ^ k * y ^ (n - 1 - k) - ∑ k in range m, x ^ k * y ^ (n - 1 - k)) =
    x ^ n - x ^ m * y ^ (n - m)
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ (x - y) * (∑ k in range n, x ^ k * y ^ (n - 1 - k) - ∑ k in range m, x ^ k * y ^ (n - 1 - k)) =
    x ^ n - x ^ m * y ^ (n - m)
have :
  (∑ k in range m, x ^ k * y ^ (n - 1 - k)) =
    ∑ k in 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, Nat.lt_iff_add_one_le, add_comm] at j_in
  have h' : n - m + (m - (1 + j)) = n - (1 + j) := tsub_add_tsub_cancel hmn j_in
  rw [← tsub_add_eq_tsub_tsub m, h', ← tsub_add_eq_tsub_tsub]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k in range m, x ^ k * y ^ (n - 1 - k) = ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k in range n, x ^ k * y ^ (n - 1 - k) - ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))) =
    x ^ n - x ^ m * y ^ (n - m)
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k in range m, x ^ k * y ^ (n - 1 - k) = ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k in range n, x ^ k * y ^ (n - 1 - k) - ∑ k in range m, x ^ k * y ^ (n - 1 - k)) =
    x ^ n - x ^ m * y ^ (n - m)
rw [this]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k in range m, x ^ k * y ^ (n - 1 - k) = ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k in range n, x ^ k * y ^ (n - 1 - k) - ∑ x_1 in range m, x ^ x_1 * (y ^ (m - 1 - x_1) * y ^ (n - m))) =
    x ^ n - x ^ m * y ^ (n - m)
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k in range m, x ^ k * y ^ (n - 1 - k) = ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k in range n, x ^ k * y ^ (n - 1 - k) - ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))) =
    x ^ n - x ^ m * y ^ (n - m)
simp_rw [pow_mul_comm y (n - m) _]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k in range m, x ^ k * y ^ (n - 1 - k) = ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k in range n, x ^ k * y ^ (n - 1 - k) - ∑ x_1 in range m, x ^ x_1 * y ^ (m - 1 - x_1) * y ^ (n - m)) =
    x ^ n - x ^ m * y ^ (n - m)
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k in range m, x ^ k * y ^ (n - 1 - k) = ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k in range n, x ^ k * y ^ (n - 1 - k) - ∑ x_1 in range m, x ^ x_1 * (y ^ (m - 1 - x_1) * y ^ (n - m))) =
    x ^ n - x ^ m * y ^ (n - m)
simp_rw [← mul_assoc]
no goals
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k in range m, x ^ k * y ^ (n - 1 - k) = ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k in range n, x ^ k * y ^ (n - 1 - k) - ∑ x_1 in range m, x ^ x_1 * y ^ (m - 1 - x_1) * y ^ (n - m)) =
    x ^ n - x ^ m * y ^ (n - m)
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)]
α : 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))
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ ∑ k in range m, x ^ k * y ^ (n - 1 - k) = ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
refine' sum_congr rfl fun j j_in => _
α : 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))
α : 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))
rw [← pow_add]
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)
α : 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))
congr
case e_a.e_a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : 1 + j ≤ m
⊢ n - 1 - j = n - m + (m - 1 - j)
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)
rw [mem_range, Nat.lt_iff_add_one_le, add_comm] at j_in
case e_a.e_a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : 1 + j ≤ m
h' : n - m + (m - (1 + j)) = n - (1 + j)
⊢ n - 1 - j = n - m + (m - 1 - j)
case e_a.e_a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : 1 + j ≤ m
⊢ n - 1 - j = n - m + (m - 1 - j)
have h' : n - m + (m - (1 + j)) = n - (1 + j) := tsub_add_tsub_cancel hmn j_in
no goals
case e_a.e_a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : 1 + j ≤ m
h' : n - m + (m - (1 + j)) = n - (1 + j)
⊢ n - 1 - j = n - m + (m - 1 - j)
rw [← tsub_add_eq_tsub_tsub m, h', ← tsub_add_eq_tsub_tsub]