case mp
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
h : degree f < ↑(card s) ∧ ∀ (i : ι), i ∈ s → eval (v i) f = r i
⊢ f = ↑(interpolate s v) r

case mpr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
h : f = ↑(interpolate s v) r
⊢ degree f < ↑(card s) ∧ ∀ (i : ι), i ∈ s → eval (v i) f = r i
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
⊢ (degree f < ↑(card s) ∧ ∀ (i : ι), i ∈ s → eval (v i) f = r i) ↔ f = ↑(interpolate s v) r
constructor <;> intro h
no goals
case mp
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
h : degree f < ↑(card s) ∧ ∀ (i : ι), i ∈ s → eval (v i) f = r i
⊢ f = ↑(interpolate s v) r
exact eq_interpolate_of_eval_eq _ hvs h.1 h.2
case mpr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
h : f = ↑(interpolate s v) r
⊢ degree (↑(interpolate s v) r) < ↑(card s) ∧ ∀ (i : ι), i ∈ s → eval (v i) (↑(interpolate s v) r) = r i
case mpr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
h : f = ↑(interpolate s v) r
⊢ degree f < ↑(card s) ∧ ∀ (i : ι), i ∈ s → eval (v i) f = r i
rw [h]
no goals
case mpr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
h : f = ↑(interpolate s v) r
⊢ degree (↑(interpolate s v) r) < ↑(card s) ∧ ∀ (i : ι), i ∈ s → eval (v i) (↑(interpolate s v) r) = r i
exact ⟨degree_interpolate_lt _ hvs, fun _ hi => eval_interpolate_at_node _ hvs hi⟩