∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F},
  Set.InjOn v ↑s →
    ∀ {P : Polynomial F},
      P.degree < ↑s.card →
        ∀ {k : ℕ},
          k < s.card →
            ∀ (x : F),
              Polynomial.eval x ((⇑Polynomial.derivative)^[k] P) =
                ↑k.factorial *
                  ∑ i ∈ s,
                    (Polynomial.eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)) *
                      ∑ t ∈ Finset.powersetCard (s.card - (k + 1)) (s.erase i), ∏ a ∈ t, (x - v a)