F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
⊢ (sup s fun b => degree (↑C (r b) * Lagrange.basis s v b)) ≤ ↑(card s - 1)
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
⊢ degree (↑(interpolate s v) r) ≤ ↑(card s - 1)
refine' (degree_sum_le _ _).trans _
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
⊢ ∀ (b : ι), b ∈ s → degree (↑C (r b) * Lagrange.basis s v b) ≤ ↑(card s - 1)
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
⊢ (sup s fun b => degree (↑C (r b) * Lagrange.basis s v b)) ≤ ↑(card s - 1)
rw [Finset.sup_le_iff]
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i✝ j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
i : ι
hi : i ∈ s
⊢ degree (↑C (r i) * Lagrange.basis s v i) ≤ ↑(card s - 1)
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
⊢ ∀ (b : ι), b ∈ s → degree (↑C (r b) * Lagrange.basis s v b) ≤ ↑(card s - 1)
intro i hi
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i✝ j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
i : ι
hi : i ∈ s
⊢ degree (↑C (r i)) + ↑(card s - 1) ≤ ↑(card s - 1)
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i✝ j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
i : ι
hi : i ∈ s
⊢ degree (↑C (r i) * Lagrange.basis s v i) ≤ ↑(card s - 1)
rw [degree_mul, degree_basis hvs hi]
case pos
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i✝ j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
i : ι
hi : i ∈ s
hr : r i = 0
⊢ degree (↑C (r i)) + ↑(card s - 1) ≤ ↑(card s - 1)

case neg
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i✝ j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
i : ι
hi : i ∈ s
hr : ¬r i = 0
⊢ degree (↑C (r i)) + ↑(card s - 1) ≤ ↑(card s - 1)
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i✝ j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
i : ι
hi : i ∈ s
⊢ degree (↑C (r i)) + ↑(card s - 1) ≤ ↑(card s - 1)
by_cases hr : r i = 0
no goals
case pos
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i✝ j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
i : ι
hi : i ∈ s
hr : r i = 0
⊢ degree (↑C (r i)) + ↑(card s - 1) ≤ ↑(card s - 1)
simpa only [hr, map_zero, degree_zero, WithBot.bot_add] using bot_le
no goals
case neg
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i✝ j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
i : ι
hi : i ∈ s
hr : ¬r i = 0
⊢ degree (↑C (r i)) + ↑(card s - 1) ≤ ↑(card s - 1)
rw [degree_C hr, zero_add]