no goals
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_1
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : degree f < ↑(card s)
eval_f : ∀ (i : ι), i ∈ s → eval (v i) f = 0
⊢ f = 0
classical
  rw [← card_image_of_injOn hvs] at degree_f_lt
  refine' eq_zero_of_degree_lt_of_eval_finset_eq_zero _ degree_f_lt _
  intro x hx
  rcases mem_image.mp hx with ⟨_, hj, rfl⟩
  exact eval_f _ hj
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_1
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : degree f < ↑(card (image v s))
eval_f : ∀ (i : ι), i ∈ s → eval (v i) f = 0
⊢ f = 0
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_1
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : degree f < ↑(card s)
eval_f : ∀ (i : ι), i ∈ s → eval (v i) f = 0
⊢ f = 0
rw [← card_image_of_injOn hvs] at degree_f_lt
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_1
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : degree f < ↑(card (image v s))
eval_f : ∀ (i : ι), i ∈ s → eval (v i) f = 0
⊢ ∀ (x : R), x ∈ image v s → eval x f = 0
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_1
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : degree f < ↑(card (image v s))
eval_f : ∀ (i : ι), i ∈ s → eval (v i) f = 0
⊢ f = 0
refine' eq_zero_of_degree_lt_of_eval_finset_eq_zero _ degree_f_lt _
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_1
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : degree f < ↑(card (image v s))
eval_f : ∀ (i : ι), i ∈ s → eval (v i) f = 0
x : R
hx : x ∈ image v s
⊢ eval x f = 0
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_1
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : degree f < ↑(card (image v s))
eval_f : ∀ (i : ι), i ∈ s → eval (v i) f = 0
⊢ ∀ (x : R), x ∈ image v s → eval x f = 0
intro x hx
case intro.intro
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_1
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : degree f < ↑(card (image v s))
eval_f : ∀ (i : ι), i ∈ s → eval (v i) f = 0
w✝ : ι
hj : w✝ ∈ s
hx : v w✝ ∈ image v s
⊢ eval (v w✝) f = 0
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_1
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : degree f < ↑(card (image v s))
eval_f : ∀ (i : ι), i ∈ s → eval (v i) f = 0
x : R
hx : x ∈ image v s
⊢ eval x f = 0
rcases mem_image.mp hx with ⟨_, hj, rfl⟩
no goals
case intro.intro
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_1
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : degree f < ↑(card (image v s))
eval_f : ∀ (i : ι), i ∈ s → eval (v i) f = 0
w✝ : ι
hj : w✝ ∈ s
hx : v w✝ ∈ image v s
⊢ eval (v w✝) f = 0
exact eval_f _ hj