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
hi : i ∈ s
⊢ ∀ (a : ι), a ∈ Finset.erase s i → (v i - v a)⁻¹ ≠ 0
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
hi : i ∈ s
⊢ nodalWeight s v i ≠ 0
rw [nodalWeight, prod_ne_zero_iff]
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
hi : i ∈ s
j : ι
hj : j ∈ Finset.erase s i
⊢ (v i - v j)⁻¹ ≠ 0
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
hi : i ∈ s
⊢ ∀ (a : ι), a ∈ Finset.erase s i → (v i - v a)⁻¹ ≠ 0
intro j hj
case intro
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
hi : i ∈ s
j : ι
hj✝ : j ∈ Finset.erase s i
hij : j ≠ i
hj : j ∈ s
⊢ (v i - v j)⁻¹ ≠ 0
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
hi : i ∈ s
j : ι
hj : j ∈ Finset.erase s i
⊢ (v i - v j)⁻¹ ≠ 0
rcases mem_erase.mp hj with ⟨hij, hj⟩
no goals
case intro
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
hi : i ∈ s
j : ι
hj✝ : j ∈ Finset.erase s i
hij : j ≠ i
hj : j ∈ s
⊢ (v i - v j)⁻¹ ≠ 0
refine' inv_ne_zero (sub_ne_zero_of_ne (mt (hvs.eq_iff hi hj).mp hij.symm))