no goals
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ↑(coeff R n) ((φ₁ + φ₂) * φ₃) = ↑(coeff R n) (φ₁ * φ₃ + φ₂ * φ₃)
simp only [coeff_mul, add_mul, Finset.sum_add_distrib, LinearMap.map_add]