∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F},
  Set.InjOn v ↑s →
    ∀ {P : Polynomial F},
      ↑s.card = P.degree + 1 → P.leadingCoeff = ∑ i ∈ s, Polynomial.eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)