no goals
σ : Type ?u.4310929
R : Type u_1
inst✝ : CommSemiring R
φ ψ : R[X]
n : ℕ
⊢ ↑(PowerSeries.coeff R n) ↑(φ * ψ) = ↑(PowerSeries.coeff R n) (↑φ * ↑ψ)
simp only [coeff_coe, PowerSeries.coeff_mul, coeff_mul]