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
⊢ Lagrange.basis s v i = ↑C (nodalWeight s v i) * (nodal s v / (X - ↑C (v i)))
simp_rw [Lagrange.basis, basisDivisor, nodalWeight, prod_mul_distrib, map_prod, ←
  nodal_erase_eq_nodal_div hi, nodal]