case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ MulOpposite.op ((∑ i in Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y)) = MulOpposite.op (x ^ n - y ^ (n - m) * x ^ m)
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ (∑ i in Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ (n - m) * x ^ m
apply op_injective
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ (MulOpposite.op x - MulOpposite.op y) * ∑ x_1 in Ico m n, MulOpposite.op y ^ (n - 1 - x_1) * MulOpposite.op x ^ x_1 =
    MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ MulOpposite.op ((∑ i in Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y)) = MulOpposite.op (x ^ n - y ^ (n - m) * x ^ m)
simp only [op_sub, op_mul, op_pow, op_sum]
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this :
  ∑ k in Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k =
    ∑ k in Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
⊢ (MulOpposite.op x - MulOpposite.op y) * ∑ x_1 in Ico m n, MulOpposite.op y ^ (n - 1 - x_1) * MulOpposite.op x ^ x_1 =
    MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ (MulOpposite.op x - MulOpposite.op y) * ∑ x_1 in Ico m n, MulOpposite.op y ^ (n - 1 - x_1) * MulOpposite.op x ^ x_1 =
    MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)
have : (∑ k in Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k) =
    ∑ k in Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k) := by
  refine' sum_congr rfl fun k _ => _
  simp only [ge_iff_le, tsub_le_iff_right]
  have hp := Commute.pow_pow (Commute.op h.symm) (n - 1 - k) k
  simpa [Commute, SemiconjBy] using hp
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this :
  ∑ k in Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k =
    ∑ k in Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
⊢ (MulOpposite.op x - MulOpposite.op y) * ∑ k in Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k) =
    MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this :
  ∑ k in Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k =
    ∑ k in Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
⊢ (MulOpposite.op x - MulOpposite.op y) * ∑ x_1 in Ico m n, MulOpposite.op y ^ (n - 1 - x_1) * MulOpposite.op x ^ x_1 =
    MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)
simp only [this]
no goals
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this :
  ∑ k in Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k =
    ∑ k in Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
⊢ (MulOpposite.op x - MulOpposite.op y) * ∑ k in Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k) =
    MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)
convert (Commute.op h).mul_geom_sum₂_Ico hmn
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
k : ℕ
x✝ : k ∈ Ico m n
⊢ MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k = MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ ∑ k in Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k =
    ∑ k in Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
refine' sum_congr rfl fun k _ => _
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
k : ℕ
x✝ : k ∈ Ico m n
⊢ MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k = MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
k : ℕ
x✝ : k ∈ Ico m n
⊢ MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k = MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
simp only [ge_iff_le, tsub_le_iff_right]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
k : ℕ
x✝ : k ∈ Ico m n
hp : Commute (MulOpposite.op y ^ (n - 1 - k)) (MulOpposite.op x ^ k)
⊢ MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k = MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
k : ℕ
x✝ : k ∈ Ico m n
⊢ MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k = MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
have hp := Commute.pow_pow (Commute.op h.symm) (n - 1 - k) k
no goals
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
k : ℕ
x✝ : k ∈ Ico m n
hp : Commute (MulOpposite.op y ^ (n - 1 - k)) (MulOpposite.op x ^ k)
⊢ MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k = MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
simpa [Commute, SemiconjBy] using hp