no goals
R✝ : Type ?u.222958
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_1
inst✝ : CommSemiring R
r : R
f : R[X]
s : R
⊢ eval s (↑(taylor r) f) = eval (s + r) f
simp only [taylor_apply, eval_comp, eval_C, eval_X, eval_add]