no goals
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
hi : ¬i ∈ s
⊢ nodal (insert i s) v = (X - ↑C (v i)) * nodal s v
simp_rw [nodal, prod_insert hi]