no goals
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
n : σ →₀ ℕ
⊢ ↑(MvPowerSeries.coeff R n) ↑(φ * ψ) = ↑(MvPowerSeries.coeff R n) (↑φ * ↑ψ)
simp only [coeff_coe, MvPowerSeries.coeff_mul, coeff_mul]