Theorem: SkewPolynomial.toFinsupp_neg (SkewPolynomials.lean)

State before:
R : Type u
a✝ b : R
m n : ℕ
inst✝¹ : Semiring R
φ✝ : R →+* R
p q : R[X;φ✝]
S : Type u
inst✝ : Ring S
φ : S →+* S
a : S[X;φ]
⊢ (-a).toFinsupp = -a.toFinsupp
Tactic:
cases a
State after:
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
φ✝ : R →+* R
p q : R[X;φ✝]
S : Type u
inst✝ : Ring S
φ : S →+* S
toFinsupp✝ : AddMonoidAlgebra S ℕ
⊢ (-{ toFinsupp := toFinsupp✝ }).toFinsupp = -{ toFinsupp := toFinsupp✝ }.toFinsupp

State before:
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
φ✝ : R →+* R
p q : R[X;φ✝]
S : Type u
inst✝ : Ring S
φ : S →+* S
toFinsupp✝ : AddMonoidAlgebra S ℕ
⊢ (-{ toFinsupp := toFinsupp✝ }).toFinsupp = -{ toFinsupp := toFinsupp✝ }.toFinsupp
Tactic:
rw [← ofFinsupp_neg]
State after:
no goals