∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R) (x y : R),
  Polynomial.eval (x + y) f =
    Polynomial.eval x f + Polynomial.eval x (Polynomial.derivative f) * y +
      (f.sum fun e a => a * ↑(Polynomial.polyBinomAux1✝ x y e a)) * y ^ 2