case h
R : Type u
inst✝ : Semiring R
n✝ : ℕ
⊢ ↑(PowerSeries.coeff R n✝) (powerSeriesPart 0) = ↑(PowerSeries.coeff R n✝) 0
R : Type u
inst✝ : Semiring R
⊢ powerSeriesPart 0 = 0
ext
no goals
case h
R : Type u
inst✝ : Semiring R
n✝ : ℕ
⊢ ↑(PowerSeries.coeff R n✝) (powerSeriesPart 0) = ↑(PowerSeries.coeff R n✝) 0
simp