rw [← ofFinsupp_mul]
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝¹ } * { toFinsupp := toFinsupp✝ }).toFinsupp =
    AddMonoidAlgebra.mul' φ { toFinsupp := toFinsupp✝¹ }.toFinsupp { toFinsupp := toFinsupp✝ }.toFinsupp
no goals