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
hi : i ∈ s
⊢ degree (↑(interpolate (Finset.erase s i) v) r) < ↑(card (Finset.erase s i))
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
hi : i ∈ s
⊢ degree (↑(interpolate (Finset.erase s i) v) r) < ↑(card s - 1)
rw [← Finset.card_erase_of_mem hi]
no goals
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
hi : i ∈ s
⊢ degree (↑(interpolate (Finset.erase s i) v) r) < ↑(card (Finset.erase s i))
exact degree_interpolate_lt _ (Set.InjOn.mono (coe_subset.mpr (erase_subset _ _)) hvs)