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
H : ∀ (j : ι), j ∈ Finset.erase s i → basisDivisor (v i) (v j) ≠ 0
⊢ natDegree (Lagrange.basis s v i) = card s - 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
⊢ natDegree (Lagrange.basis s v i) = card s - 1
have H : ∀ j, j ∈ s.erase i → basisDivisor (v i) (v j) ≠ 0 := by
  simp_rw [Ne.def, mem_erase, basisDivisor_eq_zero_iff]
  exact fun j ⟨hij₁, hj⟩ hij₂ => hij₁ (hvs hj hi hij₂.symm)
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
H : ∀ (j : ι), j ∈ Finset.erase s i → basisDivisor (v i) (v j) ≠ 0
⊢ natDegree (Lagrange.basis s v i) = ∑ x in Finset.erase s i, 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
H : ∀ (j : ι), j ∈ Finset.erase s i → basisDivisor (v i) (v j) ≠ 0
⊢ natDegree (Lagrange.basis s v i) = card s - 1
rw [← card_erase_of_mem hi, card_eq_sum_ones]
case h.e'_3
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
H : ∀ (j : ι), j ∈ Finset.erase s i → basisDivisor (v i) (v j) ≠ 0
⊢ ∑ x in Finset.erase s i, 1 = ∑ i_1 in Finset.erase s i, natDegree (basisDivisor (v i) (v i_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
H : ∀ (j : ι), j ∈ Finset.erase s i → basisDivisor (v i) (v j) ≠ 0
⊢ natDegree (Lagrange.basis s v i) = ∑ x in Finset.erase s i, 1
convert natDegree_prod _ _ H using 1
case h.e'_3
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
H : ∀ (j : ι), j ∈ Finset.erase s i → basisDivisor (v i) (v j) ≠ 0
j : ι
hj : j ∈ Finset.erase s i
⊢ v i ≠ v j
case h.e'_3
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
H : ∀ (j : ι), j ∈ Finset.erase s i → basisDivisor (v i) (v j) ≠ 0
⊢ ∑ x in Finset.erase s i, 1 = ∑ i_1 in Finset.erase s i, natDegree (basisDivisor (v i) (v i_1))
refine' sum_congr rfl fun j hj => (natDegree_basisDivisor_of_ne _).symm
case h.e'_3
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
H : ∀ (j : ι), j ∈ Finset.erase s i → basisDivisor (v i) (v j) ≠ 0
j : ι
hj : j ∈ Finset.erase s i
⊢ ¬basisDivisor (v i) (v j) = 0
case h.e'_3
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
H : ∀ (j : ι), j ∈ Finset.erase s i → basisDivisor (v i) (v j) ≠ 0
j : ι
hj : j ∈ Finset.erase s i
⊢ v i ≠ v j
rw [Ne.def, ← basisDivisor_eq_zero_iff]
no goals
case h.e'_3
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
H : ∀ (j : ι), j ∈ Finset.erase s i → basisDivisor (v i) (v j) ≠ 0
j : ι
hj : j ∈ Finset.erase s i
⊢ ¬basisDivisor (v i) (v j) = 0
exact H _ hj
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 : ι), j ≠ i ∧ 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 : ι), j ∈ Finset.erase s i → basisDivisor (v i) (v j) ≠ 0
simp_rw [Ne.def, mem_erase, basisDivisor_eq_zero_iff]
no goals
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 : ι), j ≠ i ∧ j ∈ s → ¬v i = v j
exact fun j ⟨hij₁, hj⟩ hij₂ => hij₁ (hvs hj hi hij₂.symm)