no goals
R✝ : Type ?u.213757
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
r s : R
⊢ ↑(taylor r) (↑(taylor s) f) = ↑(taylor (r + s)) f
simp only [taylor_apply, comp_assoc, map_add, add_comp, X_comp, C_comp, C_add, add_assoc]