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
hrr' : ↑(interpolate s v) r = ↑(interpolate s v) r'
x✝ : ι
hi : x✝ ∈ s
⊢ r x✝ = r' x✝
rw [← eval_interpolate_at_node r hvs hi, hrr', eval_interpolate_at_node r' hvs hi]