∀ {S : Type u_1} [inst : CommRing S] {f : Polynomial S} (y : Polynomial S) (S' : Type u_1) (w : CommRing S')
  (w_1 : Algebra S S') (m : Multiset S')
  (motive :
    Polynomial.map (algebraMap S S') f ∣
        Polynomial.map (algebraMap S S') (Polynomial.derivative f * y) -
          (Multiset.map
              (fun x =>
                (Multiset.map (fun x => Polynomial.X - Polynomial.C x) (m.erase x)).prod *
                  Polynomial.C ((Polynomial.aeval x) y))
              m).sum →
      Prop)
  (x :
    Polynomial.map (algebraMap S S') f ∣
      Polynomial.map (algebraMap S S') (Polynomial.derivative f * y) -
        (Multiset.map
            (fun x =>
              (Multiset.map (fun x => Polynomial.X - Polynomial.C x) (m.erase x)).prod *
                Polynomial.C ((Polynomial.aeval x) y))
            m).sum),
  (∀ (g : Polynomial S')
      (hg :
        Polynomial.map (algebraMap S S') (Polynomial.derivative f * y) -
            (Multiset.map
                (fun x =>
                  (Multiset.map (fun x => Polynomial.X - Polynomial.C x) (m.erase x)).prod *
                    Polynomial.C ((Polynomial.aeval x) y))
                m).sum =
          Polynomial.map (algebraMap S S') f * g),
      motive ⋯) →
    motive x