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)
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)
rw [Nat.cast_withBot]
case inl
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑∅
⊢ degree (↑(interpolate ∅ v) r) < ↑(card ∅)

case inr
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
h : Finset.Nonempty s
⊢ degree (↑(interpolate s v) r) < ↑(card s)
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)
rcases eq_empty_or_nonempty s with (rfl | h)
case inl
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑∅
⊢ ⊥ < ↑0
case inl
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑∅
⊢ degree (↑(interpolate ∅ v) r) < ↑(card ∅)
rw [interpolate_empty, degree_zero, card_empty]
no goals
case inl
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑∅
⊢ ⊥ < ↑0
exact WithBot.bot_lt_coe _
case inr
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
h : Finset.Nonempty s
⊢ ↑(card s - 1) < ↑(card s)
case inr
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
h : Finset.Nonempty s
⊢ degree (↑(interpolate s v) r) < ↑(card s)
refine' lt_of_le_of_lt (degree_interpolate_le _ hvs) _
case inr
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
h : Finset.Nonempty s
⊢ card s - 1 < card s
case inr
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
h : Finset.Nonempty s
⊢ ↑(card s - 1) < ↑(card s)
rw [Nat.cast_withBot, WithBot.coe_lt_coe]
no goals
case inr
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
h : Finset.Nonempty s
⊢ card s - 1 < card s
exact Nat.sub_lt (Nonempty.card_pos h) zero_lt_one