no goals
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
hvs : Set.InjOn v ↑s
hx : ∀ (i : ι), i ∈ s → x ≠ v i
hs : Finset.Nonempty s
⊢ eval x (nodal s v) * ∑ i in s, nodalWeight s v i * (x - v i)⁻¹ = 1
simpa only [Pi.one_apply, interpolate_one hvs hs, eval_one, mul_one] using
  (eval_interpolate_not_at_node 1 hx).symm