∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [inst_1 : IsDomain R] [inst_2 : DecidableEq R],
  f.Splits →
    ∀ (x : R),
      Polynomial.eval x (Polynomial.derivative f) =
        f.leadingCoeff *
          (Multiset.map (fun a => (Multiset.map (fun x_1 => x - x_1) (f.roots.erase a)).prod) f.roots).sum