F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ {i, j} ⊆ s
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ ↑(interpolate s v) r =
    ↑(interpolate (Finset.erase s j) v) r * basisDivisor (v i) (v j) +
      ↑(interpolate (Finset.erase s i) v) r * basisDivisor (v j) (v i)
rw [interpolate_eq_sum_interpolate_insert_sdiff _ hvs ⟨i, mem_insert_self i {j}⟩ _,
  sum_insert (not_mem_singleton.mpr hij), sum_singleton, basis_pair_left hij,
  basis_pair_right hij, sdiff_insert_insert_of_mem_of_not_mem hi (not_mem_singleton.mpr hij),
  sdiff_singleton_eq_erase, pair_comm,
  sdiff_insert_insert_of_mem_of_not_mem hj (not_mem_singleton.mpr hij.symm),
  sdiff_singleton_eq_erase]
no goals
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ {i, j} ⊆ s
exact insert_subset.mpr ⟨hi, singleton_subset_iff.mpr hj⟩