case refine'_1
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
⊢ (sup s fun b => degree (Lagrange.basis s v b)) < ↑(card s)

case refine'_2
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
⊢ degree 1 < ↑(card s)

case refine'_3
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
⊢ ∀ (i : ι), i ∈ s → eval (v i) (∑ j in s, Lagrange.basis s v j) = eval (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
hs : Finset.Nonempty s
⊢ ∑ j in s, Lagrange.basis s v j = 1
refine' eq_of_degrees_lt_of_eval_index_eq s hvs (lt_of_le_of_lt (degree_sum_le _ _) _) _ _
case refine'_1
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
⊢ ∀ (b : ι), b ∈ s → degree (Lagrange.basis s v b) < ↑(card s)
case refine'_1
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
⊢ (sup s fun b => degree (Lagrange.basis s v b)) < ↑(card s)
rw [Nat.cast_withBot, Finset.sup_lt_iff (WithBot.bot_lt_coe s.card)]
case refine'_1
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i✝ j : ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
i : ι
hi : i ∈ s
⊢ degree (Lagrange.basis s v i) < ↑(card s)
case refine'_1
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
⊢ ∀ (b : ι), b ∈ s → degree (Lagrange.basis s v b) < ↑(card s)
intro i hi
case refine'_1
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i✝ j : ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
i : ι
hi : i ∈ s
⊢ card s - 1 < card s
case refine'_1
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i✝ j : ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
i : ι
hi : i ∈ s
⊢ degree (Lagrange.basis s v i) < ↑(card s)
rw [degree_basis hvs hi, Nat.cast_withBot, WithBot.coe_lt_coe]
no goals
case refine'_1
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i✝ j : ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
i : ι
hi : i ∈ s
⊢ card s - 1 < card s
exact Nat.pred_lt (card_ne_zero_of_mem hi)
case refine'_2
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
⊢ 0 < card s
case refine'_2
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
⊢ degree 1 < ↑(card s)
rw [degree_one, ← WithBot.coe_zero, Nat.cast_withBot, WithBot.coe_lt_coe]
no goals
case refine'_2
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
⊢ 0 < card s
exact Nonempty.card_pos hs
case refine'_3
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i✝ j : ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
i : ι
hi : i ∈ s
⊢ eval (v i) (∑ j in s, Lagrange.basis s v j) = eval (v i) 1
case refine'_3
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
⊢ ∀ (i : ι), i ∈ s → eval (v i) (∑ j in s, Lagrange.basis s v j) = eval (v i) 1
intro i hi
case refine'_3
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i✝ j : ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
i : ι
hi : i ∈ s
⊢ ∑ x in Finset.erase s i, eval (v i) (Lagrange.basis s v x) = 0
case refine'_3
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i✝ j : ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
i : ι
hi : i ∈ s
⊢ eval (v i) (∑ j in s, Lagrange.basis s v j) = eval (v i) 1
rw [eval_finset_sum, eval_one, ← add_sum_erase _ _ hi, eval_basis_self hvs hi,
  add_right_eq_self]
case refine'_3
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i✝ j✝ : ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ Finset.erase s i
⊢ eval (v i) (Lagrange.basis s v j) = 0
case refine'_3
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i✝ j : ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
i : ι
hi : i ∈ s
⊢ ∑ x in Finset.erase s i, eval (v i) (Lagrange.basis s v x) = 0
refine' sum_eq_zero fun j hj => _
case refine'_3.intro
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i✝ j✝ : ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ Finset.erase s i
hij : j ≠ i
right✝ : j ∈ s
⊢ eval (v i) (Lagrange.basis s v j) = 0
case refine'_3
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i✝ j✝ : ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ Finset.erase s i
⊢ eval (v i) (Lagrange.basis s v j) = 0
rcases mem_erase.mp hj with ⟨hij, _⟩
no goals
case refine'_3.intro
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i✝ j✝ : ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ Finset.erase s i
hij : j ≠ i
right✝ : j ∈ s
⊢ eval (v i) (Lagrange.basis s v j) = 0
rw [eval_basis_of_ne hij hi]