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, mul_add, Finset.sum_add_distrib, LinearMap.map_add]