feat: add TendstoCofinite lemma for polynomial functions (#40807)

Add `Polynomial.tendstoCofinite_of_natDegree_ne_zero`, which states that a non-constant (univariate) polynomial over a domain has finite fibres.

Co-authored-by: Bhavik Mehta
Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>

Author: Xmask19

Mathlib/Algebra/Polynomial/Degree/Defs.lean

@@ -73,11 +73,11 @@ theorem Monic.leadingCoeff {p : R[X]} (hp : p.Monic) : leadingCoeff p = 1 :=
 theorem Monic.coeff_natDegree {p : R[X]} (hp : p.Monic) : p.coeff p.natDegree = 1 :=
   hp
 
-@[simp]
+@[simp, grind =]
 theorem degree_zero : degree (0 : R[X]) = ⊥ :=
   rfl
 
-@[simp]
+@[simp, grind =]
 theorem natDegree_zero : natDegree (0 : R[X]) = 0 :=
   rfl
 
@@ -161,18 +161,18 @@ theorem degree_C_lt : degree (C a) < 1 :=
 
 theorem degree_one_le : degree (1 : R[X]) ≤ (0 : WithBot ℕ) := by rw [← C_1]; exact degree_C_le
 
-@[simp]
+@[simp, grind =]
 theorem natDegree_C (a : R) : natDegree (C a) = 0 := by
   by_cases ha : a = 0
   · have : C a = 0 := by rw [ha, C_0]
     rw [natDegree, degree_eq_bot.2 this, WithBot.unbotD_bot]
   · rw [natDegree, degree_C ha, WithBot.unbotD_zero]
 
-@[simp]
+@[simp, grind =]
 theorem natDegree_one : natDegree (1 : R[X]) = 0 :=
   natDegree_C 1
 
-@[simp]
+@[simp, grind =]
 theorem natDegree_natCast (n : ℕ) : natDegree (n : R[X]) = 0 := by
   simp only [← C_eq_natCast, natDegree_C]
 

Mathlib/Algebra/Polynomial/Roots.lean

@@ -12,6 +12,7 @@ public import Mathlib.Data.Set.Finite.Lemmas
 public import Mathlib.RingTheory.Coprime.Lemmas
 public import Mathlib.RingTheory.Localization.FractionRing
 public import Mathlib.SetTheory.Cardinal.Order
+public import Mathlib.Order.Filter.TendstoCofinite
 
 /-!
 # Theory of univariate polynomials
@@ -157,6 +158,15 @@ theorem eq_of_infinite_eval_eq (p q : R[X]) (h : Set.Infinite { x | eval x p = e
   apply eq_zero_of_infinite_isRoot
   simpa only [IsRoot, eval_sub, sub_eq_zero]
 
+/-- Non-constant polynomials have finite fibres, provided the coefficients are a domain. -/
+lemma tendstoCofinite_of_natDegree_ne_zero {R : Type} [CommRing R] [IsDomain R] (p : R[X])
+    (hp : p.natDegree ≠ 0) : Filter.TendstoCofinite p.eval := by
+  rw [Filter.tendstoCofinite_iff_finite_preimage_singleton]
+  intro x
+  by_contra! hx
+  obtain ⟨rfl⟩ : p = C x := p.eq_of_infinite_eval_eq (C x) (by simpa)
+  simp at hp
+
 theorem roots_mul {p q : R[X]} (hpq : p * q ≠ 0) : (p * q).roots = p.roots + q.roots := by
   classical
   exact Multiset.ext.mpr fun r => by

Mathlib/RingTheory/PowerBasis.lean

@@ -115,7 +115,7 @@ theorem mem_span_pow {x y : S} {d : ℕ} (hd : d ≠ 0) :
   · rintro ⟨f, h, hy⟩
     refine ⟨f, ?_, hy⟩
     by_cases hf : f = 0
-    · simp only [hf, natDegree_zero, degree_zero] at h ⊢
+    · simp only [hf, natDegree_zero, Polynomial.degree_zero] at h ⊢
       first | exact lt_of_le_of_ne (Nat.zero_le d) hd.symm | exact WithBot.bot_lt_coe d
     simpa [degree_eq_natDegree hf] using h