no goals
R✝ : Type ?u.211470
inst✝¹ : Semiring R✝
r✝ : R✝
f : R✝[X]
R : Type u_1
inst✝ : CommSemiring R
r : R
p q : R[X]
⊢ ↑(taylor r) (p * q) = ↑(taylor r) p * ↑(taylor r) q
simp only [taylor_apply, mul_comp]