∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {f g : Polynomial R} (s : Finset R),
  f.degree ≤ ↑s.card →
    f.degree = g.degree → f.leadingCoeff = g.leadingCoeff → (∀ x ∈ s, Polynomial.eval x f = Polynomial.eval x g) → f = g