-- Mathlib/Algebra/Polynomial/Roots.lean
lemma eq_zero_of_natDegree_lt_card_of_eval_eq_zero {R} [CommRing R] [IsDomain R]
    (p : R[X]) {ι} [Fintype ι] {f : ι → R} (hf : Function.Injective f)
    (heval : ∀ i, p.eval (f i) = 0) (hcard : natDegree p < Fintype.card ι) : p = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
a✝ : R
⊢ ∀ (x : ι), f x = a✝ → eval a✝ p = 0

Tactic:
rintro x rfl

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
x : ι
⊢ eval (f x) p = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
⊢ False

Tactic:
refine lt_irrefl #p.roots.toFinset ?_

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
⊢ #p.roots.toFinset < #p.roots.toFinset

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
⊢ image f univ ≤ p.roots.toFinset

Tactic:
intro _

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
a✝ : R
⊢ a✝ ∈ image f univ → a✝ ∈ p.roots.toFinset

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
⊢ Fintype.card ↑(Set.range f) = #(image f univ)

Tactic:
rw [← Set.toFinset_card, Set.toFinset_range]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
x : ι
⊢ eval (f x) p = 0

Tactic:
exact heval _

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
⊢ p = 0

Tactic:
by_contra hp

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
⊢ False

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
⊢ #p.roots.toFinset < #p.roots.toFinset

Tactic:
calc
  #p.roots.toFinset ≤ Multiset.card p.roots := Multiset.toFinset_card_le _
  _ ≤ natDegree p := Polynomial.card_roots' p
  _ < Fintype.card ι := hcard
  _ = Fintype.card (Set.range f) := (Set.card_range_of_injective hf).symm
  _ = #(Finset.univ.image f) := by rw [← Set.toFinset_card, Set.toFinset_range]
  _ ≤ #p.roots.toFinset := Finset.card_mono ?_

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
⊢ image f univ ≤ p.roots.toFinset

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
⊢ p = 0

Tactic:
classical
by_contra hp
refine lt_irrefl #p.roots.toFinset ?_
calc
  #p.roots.toFinset ≤ Multiset.card p.roots := Multiset.toFinset_card_le _
  _ ≤ natDegree p := Polynomial.card_roots' p
  _ < Fintype.card ι := hcard
  _ = Fintype.card (Set.range f) := (Set.card_range_of_injective hf).symm
  _ = #(Finset.univ.image f) := by rw [← Set.toFinset_card, Set.toFinset_range]
  _ ≤ #p.roots.toFinset := Finset.card_mono ?_
intro _
simp only [Finset.mem_image, Finset.mem_univ, true_and, Multiset.mem_toFinset, mem_roots', ne_eq,
  IsRoot.def, forall_exists_index, hp, not_false_eq_true]
rintro x rfl
exact heval _

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
a✝ : R
⊢ a✝ ∈ image f univ → a✝ ∈ p.roots.toFinset

Tactic:
simp only [Finset.mem_image, Finset.mem_univ, true_and, Multiset.mem_toFinset, mem_roots', ne_eq,
  IsRoot.def, forall_exists_index, hp, not_false_eq_true]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
a✝ : R
⊢ ∀ (x : ι), f x = a✝ → eval a✝ p = 0