case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ MulOpposite.op ((y - x) * ∑ i in range n, x ^ i * y ^ (n - 1 - i)) = MulOpposite.op (y ^ n - x ^ n)
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ (y - x) * ∑ i in range n, x ^ i * y ^ (n - 1 - i) = y ^ n - x ^ n
apply op_injective
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ MulOpposite.op (∑ i in range n, x ^ i * y ^ (n - 1 - i)) * (MulOpposite.op y - MulOpposite.op x) =
    MulOpposite.op y ^ n - MulOpposite.op x ^ n
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ MulOpposite.op ((y - x) * ∑ i in range n, x ^ i * y ^ (n - 1 - i)) = MulOpposite.op (y ^ n - x ^ n)
simp only [op_mul, op_sub, op_geom_sum₂, op_pow]
no goals
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ MulOpposite.op (∑ i in range n, x ^ i * y ^ (n - 1 - i)) * (MulOpposite.op y - MulOpposite.op x) =
    MulOpposite.op y ^ n - MulOpposite.op x ^ n
simp [(Commute.op h.symm).geom_sum₂_mul n]