no goals
R✝ : Type ?u.229785
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
f : R[X]
r : R
⊢ (sum (↑(taylor r) f) fun i a => ↑C a * (X - ↑C r) ^ i) = f
rw [← comp_eq_sum_left, sub_eq_add_neg, ← C_neg, ← taylor_apply, taylor_taylor, neg_add_self,
  taylor_zero]