simp only [toFinsupp_mul, AddMonoidAlgebra.mul'_def]
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ (a * b * c).toFinsupp = (a * (b * c)).toFinsupp
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ (sum (sum a.toFinsupp fun a₁ b₁ => sum b.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) fun a₁ b₁ =>
      sum c.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) =
    sum a.toFinsupp fun a₁ b₁ =>
      sum (sum b.toFinsupp fun a₁ b₁ => sum c.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) fun a₂ b₂ =>
        single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)