case a0
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
hi : i ∈ s
⊢ X - ↑C (v i) ≠ 0
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 (Finset.erase s i) v = nodal s v / (X - ↑C (v i))
rw [nodal_eq_mul_nodal_erase hi, EuclideanDomain.mul_div_cancel_left]
no goals
case a0
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
hi : i ∈ s
⊢ X - ↑C (v i) ≠ 0
exact X_sub_C_ne_zero _