case h
σ : Type ?u.4308129
R : Type u_1
inst✝ : CommSemiring R
φ ψ : R[X]
n✝ : ℕ
⊢ ↑(PowerSeries.coeff R n✝) ↑(φ + ψ) = ↑(PowerSeries.coeff R n✝) (↑φ + ↑ψ)
σ : Type ?u.4308129
R : Type u_1
inst✝ : CommSemiring R
φ ψ : R[X]
⊢ ↑(φ + ψ) = ↑φ + ↑ψ
ext
no goals
case h
σ : Type ?u.4308129
R : Type u_1
inst✝ : CommSemiring R
φ ψ : R[X]
n✝ : ℕ
⊢ ↑(PowerSeries.coeff R n✝) ↑(φ + ψ) = ↑(PowerSeries.coeff R n✝) (↑φ + ↑ψ)
simp