no goals
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
⊢ nodalWeight s v i = (eval (v i) (nodal (Finset.erase s i) v))⁻¹
rw [eval_nodal, nodalWeight, prod_inv_distrib]