case a.h
R : Type u_1
inst✝ : CommSemiring R
x✝ : PowerSeries R
n✝ : ℕ
⊢ ↑(coeff R n✝) (↑(rescale 1) x✝) = ↑(coeff R n✝) (↑(RingHom.id (PowerSeries R)) x✝)
R : Type u_1
inst✝ : CommSemiring R
⊢ rescale 1 = RingHom.id (PowerSeries R)
ext
no goals
case a.h
R : Type u_1
inst✝ : CommSemiring R
x✝ : PowerSeries R
n✝ : ℕ
⊢ ↑(coeff R n✝) (↑(rescale 1) x✝) = ↑(coeff R n✝) (↑(RingHom.id (PowerSeries R)) x✝)
simp only [coeff_rescale, one_pow, one_mul, RingHom.id_apply]