case a.h
R : Type u_1
inst✝ : CommSemiring R
a b : R
x✝ : PowerSeries R
n✝ : ℕ
⊢ ↑(coeff R n✝) (↑(rescale (a * b)) x✝) = ↑(coeff R n✝) (↑(RingHom.comp (rescale b) (rescale a)) x✝)
R : Type u_1
inst✝ : CommSemiring R
a b : R
⊢ rescale (a * b) = RingHom.comp (rescale b) (rescale a)
ext
no goals
case a.h
R : Type u_1
inst✝ : CommSemiring R
a b : R
x✝ : PowerSeries R
n✝ : ℕ
⊢ ↑(coeff R n✝) (↑(rescale (a * b)) x✝) = ↑(coeff R n✝) (↑(RingHom.comp (rescale b) (rescale a)) x✝)
simp [← rescale_rescale]