∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} (r r' : ι → F),
  Set.InjOn v ↑s → ((Lagrange.interpolate s v) r = (Lagrange.interpolate s v) r' ↔ ∀ i ∈ s, r i = r' i)