case h
σ : Type ?u.4303706
R : Type u_1
inst✝ : CommSemiring R
φ ψ : R[X]
n : ℕ
a : R
n✝ : ℕ
⊢ ↑(PowerSeries.coeff R n✝) ↑(↑(monomial n) a) = ↑(PowerSeries.coeff R n✝) (↑(PowerSeries.monomial R n) a)
σ : Type ?u.4303706
R : Type u_1
inst✝ : CommSemiring R
φ ψ : R[X]
n : ℕ
a : R
⊢ ↑(↑(monomial n) a) = ↑(PowerSeries.monomial R n) a
ext
no goals
case h
σ : Type ?u.4303706
R : Type u_1
inst✝ : CommSemiring R
φ ψ : R[X]
n : ℕ
a : R
n✝ : ℕ
⊢ ↑(PowerSeries.coeff R n✝) ↑(↑(monomial n) a) = ↑(PowerSeries.coeff R n✝) (↑(PowerSeries.monomial R n) a)
simp [coeff_coe, PowerSeries.coeff_monomial, Polynomial.coeff_monomial, eq_comm]