F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ∏ j in Finset.erase s i, eval (v i) (basisDivisor (v i) (v j)) = 1
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ eval (v i) (Lagrange.basis s v i) = 1
rw [Lagrange.basis, eval_prod]
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j✝ : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ Finset.erase s i
⊢ eval (v i) (basisDivisor (v i) (v j)) = 1
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ∏ j in Finset.erase s i, eval (v i) (basisDivisor (v i) (v j)) = 1
refine' prod_eq_one fun j H => _
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j✝ : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ Finset.erase s i
⊢ v i ≠ v j
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j✝ : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ Finset.erase s i
⊢ eval (v i) (basisDivisor (v i) (v j)) = 1
rw [eval_basisDivisor_left_of_ne]
case intro
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j✝ : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ Finset.erase s i
hij : j ≠ i
hj : j ∈ s
⊢ v i ≠ v j
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j✝ : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ Finset.erase s i
⊢ v i ≠ v j
rcases mem_erase.mp H with ⟨hij, hj⟩
no goals
case intro
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j✝ : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ Finset.erase s i
hij : j ≠ i
hj : j ∈ s
⊢ v i ≠ v j
exact mt (hvs hi hj) hij.symm