case h
R : Type u_1
inst✝ : CommSemiring R
f : ℕ → R
a : R
n✝ : ℕ
⊢ ↑(coeff R n✝) (↑(rescale a) (mk f)) = ↑(coeff R n✝) (mk fun n => a ^ n * f n)
R : Type u_1
inst✝ : CommSemiring R
f : ℕ → R
a : R
⊢ ↑(rescale a) (mk f) = mk fun n => a ^ n * f n
ext
no goals
case h
R : Type u_1
inst✝ : CommSemiring R
f : ℕ → R
a : R
n✝ : ℕ
⊢ ↑(coeff R n✝) (↑(rescale a) (mk f)) = ↑(coeff R n✝) (mk fun n => a ^ n * f n)
rw [coeff_rescale, coeff_mk, coeff_mk]