From 30681aa169cb0b7538a07c071353bb486ab3b46e Mon Sep 17 00:00:00 2001
From: morrison-daniel <39346894+morrison-daniel@users.noreply.github.com>
Date: Tue, 1 Oct 2024 21:32:46 -0700
Subject: [PATCH 01/10] create M_spec_map

---
 FLT/MathlibExperiments/FrobeniusRiou.lean | 31 +++--------------------
 1 file changed, 4 insertions(+), 27 deletions(-)

diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean
index befb716c6..bdba18a21 100644
--- a/FLT/MathlibExperiments/FrobeniusRiou.lean
+++ b/FLT/MathlibExperiments/FrobeniusRiou.lean
@@ -271,36 +271,13 @@ theorem M_spec (b : B) : ((M hFull b : A[X]) : B[X]) = F G b := by
   simp_rw [finset_sum_coeff, ← lcoeff_apply, lcoeff_apply, coeff_monomial]
   aesop
 
-/-
-private theorem F_descent_monic
-  (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a) (b : B) :
-    ∃ M : A[X], (M : B[X]) = F G b ∧ Monic M := by
-  have : F G b ∈ Polynomial.lifts (algebraMap A B) := by
-    choose M hM using F_descent hFull b
-    use M; exact hM
-  choose M hM using lifts_and_degree_eq_and_monic this (F_monic b)
-  use M
-  exact ⟨hM.1, hM.2.2⟩
-
-variable (G) in
-noncomputable def M [Finite G] (b : B) : A[X] := (F_descent_monic hFull b).choose
-
-theorem M_spec (b : B) : ((M G hFull b : A[X]) : B[X]) = F G b :=
-  (F_descent_monic hFull b).choose_spec.1
-
-theorem M_spec' (b : B) : (map (algebraMap A B) (M G hFull b)) = F G b :=
-  (F_descent_monic hFull b).choose_spec.1
-
-theorem M_monic (b : B) : (M G hFull b).Monic := (F_descent_monic hFull b).choose_spec.2
--/
-
 omit [Nontrivial B] in
-theorem coe_poly_as_map (p : A[X]) : (p : B[X]) = map (algebraMap A B) p := rfl
-
+theorem M_spec_map (b : B) : (map (algebraMap A B) (M hFull b)) = F G b := by
+  rw [← M_spec hFull b]; rfl
 
 omit [Nontrivial B] in
 theorem M_eval_eq_zero (b : B) : (M hFull b).eval₂ (algebraMap A B) b = 0 := by
-  rw [eval₂_eq_eval_map, ← coe_poly_as_map, M_spec, F_eval_eq_zero]
+  rw [eval₂_eq_eval_map, M_spec_map, F_eval_eq_zero]
 
 include hFull in
 theorem isIntegral : Algebra.IsIntegral A B where
@@ -730,7 +707,7 @@ theorem algebraic {A : Type*} [CommRing A] {B : Type*} [Nontrivial B] [CommRing
     exact M_monic hFull b
   . rw [← hb, algebraMap_cast, map_map, ← IsScalarTower.algebraMap_eq]
     rw [algebraMap_algebraMap, aeval_def, eval₂_eq_eval_map, map_map, ← IsScalarTower.algebraMap_eq]
-    rw [IsScalarTower.algebraMap_eq A B L, ← map_map, ← coe_poly_as_map (M hFull b), M_spec]
+    rw [IsScalarTower.algebraMap_eq A B L, ← map_map, M_spec_map]
     rw [eval_map, eval₂_hom, F_eval_eq_zero]
     exact algebraMap.coe_zero
 

From f96596eadd8e5e0eef5053174a64547c7f78cb25 Mon Sep 17 00:00:00 2001
From: morrison-daniel <39346894+morrison-daniel@users.noreply.github.com>
Date: Wed, 2 Oct 2024 19:44:02 -0700
Subject: [PATCH 02/10] Algebra.exists_dvd_nonzero_if_isIntegral

---
 FLT/MathlibExperiments/FrobeniusRiou.lean | 119 +++++++++++++++++++++-
 1 file changed, 116 insertions(+), 3 deletions(-)

diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean
index bdba18a21..4cd0e0fea 100644
--- a/FLT/MathlibExperiments/FrobeniusRiou.lean
+++ b/FLT/MathlibExperiments/FrobeniusRiou.lean
@@ -486,10 +486,123 @@ theorem reduction_isIntegral : Algebra.IsIntegral (A ⧸ P) (B ⧸ Q) := by
 
 end MulSemiringAction
 
-theorem Algebra.exists_dvd_nonzero_if_isIntegral (R S : Type) [CommRing R] [CommRing S]
-    [Algebra R S] [Algebra.IsIntegral R S] [IsDomain S] (s : S) (hs : s ≠ 0) :
+theorem Polynomial.monic_nonzero_const_if_isIntegral (R S : Type) [CommRing R] [Nontrivial R]
+    [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] [IsDomain S] (s : S) (hs : s ≠ 0) :
+    ∃ (q : Polynomial R), Monic q ∧ q.coeff 0 ≠ 0 ∧ q.eval₂ (algebraMap R S) s = 0 := by
+    obtain ⟨p, p_monic, p_eval⟩ := (@Algebra.isIntegral_def R S).mp inferInstance s
+    have p_neq_zero := ne_zero_of_ne_zero_of_monic X_ne_zero p_monic
+    let d := p.natTrailingDegree
+    use ∑ n ∈ p.support, monomial (n - d) (p.coeff n)
+    have : (∑ n ∈ p.support, monomial (n - d) (p.coeff n)).degree ≤ p.natDegree - d := by
+      have := Polynomial.degree_sum_le p.support (fun x ↦ monomial (x - d) (p.coeff x))
+      refine le_trans this ?_
+      rw [Finset.sup_le_iff]
+      intro n hn
+      apply le_trans (degree_monomial_le (n - d) _) ?_
+      rw [Nat.cast_le]
+      apply Nat.sub_le_sub_right _ d
+      exact le_natDegree_of_mem_supp n hn
+    constructor
+    . apply monic_of_degree_le_of_coeff_eq_one (p.natDegree - d) this
+      rw [finset_sum_coeff]
+      rw [Finset.sum_eq_single_of_mem p.natDegree]
+      . simp
+        exact Monic.leadingCoeff p_monic
+      . exact natDegree_mem_support_of_nonzero p_neq_zero
+      . intro b b_support b_ne_natDegree
+        rw [coeff_monomial_of_ne]
+        by_contra h
+        apply b_ne_natDegree
+        have this1 : p.natTrailingDegree ≤ b := by
+          rw [natTrailingDegree_eq_support_min' p_neq_zero]
+          exact Finset.min'_le p.support b b_support
+        have this2 : d ≤ p.natDegree := by
+          exact Polynomial.natTrailingDegree_le_natDegree p
+        rw [Nat.sub_eq_iff_eq_add this1] at h
+        simp [h, this1, this2]
+    . constructor
+      . rw [finset_sum_coeff]
+        rw [Finset.sum_eq_single_of_mem d]
+        . rw [coeff_monomial]
+          simp [d, p_neq_zero]
+        . exact natTrailingDegree_mem_support_of_nonzero p_neq_zero
+        . intro n n_support n_neq_d
+          rw [coeff_monomial_of_ne]
+          have : d ≤ n := by
+            apply natTrailingDegree_le_of_mem_supp
+            exact n_support
+          by_contra h
+          apply n_neq_d
+          rw [Nat.sub_eq_iff_eq_add this] at h
+          simp [h, this]
+      . rw [eval₂_finset_sum]
+        simp
+        have : ∑ n ∈ p.support, (algebraMap R S) (p.coeff n) * s ^ n = 0 := by
+          rw [← p_eval]
+          nth_rw 3 [as_sum_support p]
+          rw [eval₂_finset_sum]
+          simp
+        have : (s ^ d) * ∑ n ∈ p.support, (algebraMap R S) (p.coeff n) * (s ^ (n - d)) = 0 := by
+          rw [← this]
+          rw [Finset.mul_sum]
+          congr
+          ext n
+          rcases Classical.em (n ∈ p.support) with n_support | n_nsupport
+          . have : d ≤ n := natTrailingDegree_le_of_mem_supp n n_support
+            rw [mul_comm, mul_assoc]
+            congr
+            rw [mul_comm]
+            exact pow_mul_pow_sub s this
+          . rw [not_mem_support_iff.mp n_nsupport]
+            simp
+        let zero_or_zero := NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero this
+        rcases zero_or_zero with s_pow_zero | h
+        . by_contra
+          apply hs
+          exact pow_eq_zero s_pow_zero
+        . exact h
+
+theorem Algebra.exists_dvd_nonzero_if_isIntegral (R S : Type) [CommRing R] [Nontrivial R]
+    [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] [IsDomain S] (s : S) (hs : s ≠ 0) :
     ∃ r : R, r ≠ 0 ∧ s ∣ (r : S) := by
-  sorry
+  obtain ⟨q, _, q_zero_coeff, q_eval_zero⟩ :=
+      Polynomial.monic_nonzero_const_if_isIntegral R S s hs
+  have zero_support : 0 ∈ q.support := by
+    exact Polynomial.mem_support_iff.mpr q_zero_coeff
+  have q_eval_zero : ∑ n ∈ q.support, (algebraMap R S) (q.coeff n) * s ^ n = 0 := by
+          rw [← q_eval_zero]
+          nth_rw 3 [Polynomial.as_sum_support q]
+          rw [Polynomial.eval₂_finset_sum]
+          simp
+  use q.coeff 0
+  constructor
+  . exact q_zero_coeff
+  . have : (q.coeff 0 : S) = ((algebraMap R S) (q.coeff 0)) * s ^ 0 := by
+      simp
+    have : q.coeff 0 = - ∑ n ∈ q.support.erase 0, (algebraMap R S) (q.coeff n) * s ^ n := by
+      rw [← sub_add_cancel_left (q.coeff 0 : S)
+        (∑ n ∈ q.support.erase 0, (algebraMap R S) (q.coeff n) * s ^ n)]
+      nth_rw 3 [this]
+      rw [add_comm, Finset.sum_erase_add _ _ zero_support, q_eval_zero]
+      simp
+    rw [this]
+    simp
+    use ∑ n ∈ q.support.erase 0, (algebraMap R S) (q.coeff n) * s ^ (n - 1)
+    rw [Finset.mul_sum]
+    apply Finset.sum_equiv (Equiv.refl ℕ)
+    . intro i; rfl
+    . intro i hi
+      rw [Finset.mem_erase] at hi
+      obtain ⟨i_nzero, _⟩ := hi
+      simp
+      rw [← mul_assoc]
+      nth_rw 3 [mul_comm]
+      rw [mul_assoc]
+      congr
+      symm
+      nth_rw 1 [← pow_one s]
+      apply pow_mul_pow_sub s
+      exact Nat.one_le_iff_ne_zero.mpr i_nzero
 
 end B_mod_Q_over_A_mod_P_stuff
 

From a21949c91ab31f1c75b187346f870ce6f47f5ea5 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 10 Oct 2024 16:31:04 +0200
Subject: [PATCH 03/10]  Remove `import Mathlib`

---
 FLT/MathlibExperiments/FrobeniusRiou.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean
index 43a4f3db4..a8abbcabb 100644
--- a/FLT/MathlibExperiments/FrobeniusRiou.lean
+++ b/FLT/MathlibExperiments/FrobeniusRiou.lean
@@ -11,7 +11,7 @@ import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 import Mathlib.RingTheory.Ideal.Pointwise
 import Mathlib.RingTheory.Ideal.Over
 import Mathlib.FieldTheory.Normal
-import Mathlib
+import Mathlib.FieldTheory.SeparableClosure
 import Mathlib.RingTheory.OreLocalization.Ring
 
 /-!

From 403327d7bf6b924d0a74ddaa5451ea3363a72e3c Mon Sep 17 00:00:00 2001
From: morrison-daniel <39346894+morrison-daniel@users.noreply.github.com>
Date: Thu, 10 Oct 2024 12:51:15 -0700
Subject: [PATCH 04/10] Update FLT/MathlibExperiments/FrobeniusRiou.lean

Co-authored-by: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
---
 FLT/MathlibExperiments/FrobeniusRiou.lean | 63 ++++++++++-------------
 1 file changed, 27 insertions(+), 36 deletions(-)

diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean
index a8abbcabb..e39994619 100644
--- a/FLT/MathlibExperiments/FrobeniusRiou.lean
+++ b/FLT/MathlibExperiments/FrobeniusRiou.lean
@@ -601,44 +601,35 @@ theorem Polynomial.monic_nonzero_const_if_isIntegral (R S : Type) [CommRing R] [
 theorem Algebra.exists_dvd_nonzero_if_isIntegral (R S : Type) [CommRing R] [Nontrivial R]
     [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] [IsDomain S] (s : S) (hs : s ≠ 0) :
     ∃ r : R, r ≠ 0 ∧ s ∣ (r : S) := by
-  obtain ⟨q, _, q_zero_coeff, q_eval_zero⟩ :=
-      Polynomial.monic_nonzero_const_if_isIntegral R S s hs
-  have zero_support : 0 ∈ q.support := by
-    exact Polynomial.mem_support_iff.mpr q_zero_coeff
+  obtain ⟨q, _, q_zero_coeff, q_eval_zero⟩ := Polynomial.monic_nonzero_const_if_isIntegral R S s hs
+  have zero_support : 0 ∈ q.support := Polynomial.mem_support_iff.mpr q_zero_coeff
   have q_eval_zero : ∑ n ∈ q.support, (algebraMap R S) (q.coeff n) * s ^ n = 0 := by
-          rw [← q_eval_zero]
-          nth_rw 3 [Polynomial.as_sum_support q]
-          rw [Polynomial.eval₂_finset_sum]
-          simp
-  use q.coeff 0
-  constructor
-  . exact q_zero_coeff
-  . have : (q.coeff 0 : S) = ((algebraMap R S) (q.coeff 0)) * s ^ 0 := by
-      simp
-    have : q.coeff 0 = - ∑ n ∈ q.support.erase 0, (algebraMap R S) (q.coeff n) * s ^ n := by
-      rw [← sub_add_cancel_left (q.coeff 0 : S)
-        (∑ n ∈ q.support.erase 0, (algebraMap R S) (q.coeff n) * s ^ n)]
-      nth_rw 3 [this]
-      rw [add_comm, Finset.sum_erase_add _ _ zero_support, q_eval_zero]
-      simp
-    rw [this]
+    rw [← q_eval_zero]
+    nth_rw 3 [Polynomial.as_sum_support q]
+    rw [Polynomial.eval₂_finset_sum]
+    simp
+  refine ⟨q.coeff 0, q_zero_coeff, ?_⟩
+  have : (q.coeff 0 : S) = ((algebraMap R S) (q.coeff 0)) * s ^ 0 := by rw [pow_zero, mul_one]
+  have : q.coeff 0 = - ∑ n ∈ q.support.erase 0, (algebraMap R S) (q.coeff n) * s ^ n := by
+    rw [← sub_add_cancel_left (q.coeff 0 : S)
+      (∑ n ∈ q.support.erase 0, (algebraMap R S) (q.coeff n) * s ^ n)]
+    nth_rw 3 [this]
+    rw [add_comm, Finset.sum_erase_add _ _ zero_support, q_eval_zero]
     simp
-    use ∑ n ∈ q.support.erase 0, (algebraMap R S) (q.coeff n) * s ^ (n - 1)
-    rw [Finset.mul_sum]
-    apply Finset.sum_equiv (Equiv.refl ℕ)
-    . intro i; rfl
-    . intro i hi
-      rw [Finset.mem_erase] at hi
-      obtain ⟨i_nzero, _⟩ := hi
-      simp
-      rw [← mul_assoc]
-      nth_rw 3 [mul_comm]
-      rw [mul_assoc]
-      congr
-      symm
-      nth_rw 1 [← pow_one s]
-      apply pow_mul_pow_sub s
-      exact Nat.one_le_iff_ne_zero.mpr i_nzero
+  rw [this, dvd_neg]
+  refine ⟨∑ n ∈ q.support.erase 0, (algebraMap R S) (q.coeff n) * s ^ (n - 1), ?_⟩
+  rw [Finset.mul_sum]
+  refine Finset.sum_equiv (Equiv.refl ℕ) (fun _ ↦ Iff.symm (Eq.to_iff rfl)) ?_
+  . intro i hi
+    rw [Finset.mem_erase] at hi
+    obtain ⟨i_nzero, _⟩ := hi
+    rw [Equiv.refl_apply, ← mul_assoc]
+    nth_rw 3 [mul_comm]
+    rw [mul_assoc]
+    congr
+    symm
+    nth_rw 1 [← pow_one s]
+    exact pow_mul_pow_sub s (Nat.one_le_iff_ne_zero.mpr i_nzero)
 
 end B_mod_Q_over_A_mod_P_stuff
 

From 1528c72f96dba216fd4847e14df6faede7665261 Mon Sep 17 00:00:00 2001
From: morrison-daniel <39346894+morrison-daniel@users.noreply.github.com>
Date: Thu, 10 Oct 2024 12:51:27 -0700
Subject: [PATCH 05/10] Update FLT/MathlibExperiments/FrobeniusRiou.lean

Co-authored-by: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
---
 FLT/MathlibExperiments/FrobeniusRiou.lean | 59 ++++++++++-------------
 1 file changed, 25 insertions(+), 34 deletions(-)

diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean
index e39994619..d66765d12 100644
--- a/FLT/MathlibExperiments/FrobeniusRiou.lean
+++ b/FLT/MathlibExperiments/FrobeniusRiou.lean
@@ -526,47 +526,41 @@ theorem Polynomial.monic_nonzero_const_if_isIntegral (R S : Type) [CommRing R] [
     [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] [IsDomain S] (s : S) (hs : s ≠ 0) :
     ∃ (q : Polynomial R), Monic q ∧ q.coeff 0 ≠ 0 ∧ q.eval₂ (algebraMap R S) s = 0 := by
     obtain ⟨p, p_monic, p_eval⟩ := (@Algebra.isIntegral_def R S).mp inferInstance s
-    have p_neq_zero := ne_zero_of_ne_zero_of_monic X_ne_zero p_monic
-    let d := p.natTrailingDegree
-    use ∑ n ∈ p.support, monomial (n - d) (p.coeff n)
-    have : (∑ n ∈ p.support, monomial (n - d) (p.coeff n)).degree ≤ p.natDegree - d := by
-      have := Polynomial.degree_sum_le p.support (fun x ↦ monomial (x - d) (p.coeff x))
-      refine le_trans this ?_
+    use ∑ n ∈ p.support, monomial (n - p.natTrailingDegree) (p.coeff n)
+    have : (∑ n ∈ p.support, monomial (n - p.natTrailingDegree) (p.coeff n)).degree
+        ≤ p.natDegree - p.natTrailingDegree := by
+      refine le_trans (Polynomial.degree_sum_le p.support (fun x ↦ monomial (x - p.natTrailingDegree) (p.coeff x))) ?_
       rw [Finset.sup_le_iff]
-      intro n hn
-      apply le_trans (degree_monomial_le (n - d) _) ?_
+      refine fun n hn ↦ le_trans (degree_monomial_le (n - p.natTrailingDegree) _) (?_)
       rw [Nat.cast_le]
-      apply Nat.sub_le_sub_right _ d
-      exact le_natDegree_of_mem_supp n hn
+      exact Nat.sub_le_sub_right (le_natDegree_of_mem_supp n hn) p.natTrailingDegree
     constructor
-    . apply monic_of_degree_le_of_coeff_eq_one (p.natDegree - d) this
-      rw [finset_sum_coeff]
-      rw [Finset.sum_eq_single_of_mem p.natDegree]
-      . simp
+    . apply monic_of_degree_le_of_coeff_eq_one (p.natDegree - p.natTrailingDegree) this
+      rw [finset_sum_coeff, Finset.sum_eq_single_of_mem p.natDegree]
+      . rw [coeff_natDegree, coeff_monomial_same]
         exact Monic.leadingCoeff p_monic
-      . exact natDegree_mem_support_of_nonzero p_neq_zero
+      . exact natDegree_mem_support_of_nonzero (ne_zero_of_ne_zero_of_monic X_ne_zero p_monic)
       . intro b b_support b_ne_natDegree
         rw [coeff_monomial_of_ne]
         by_contra h
         apply b_ne_natDegree
         have this1 : p.natTrailingDegree ≤ b := by
-          rw [natTrailingDegree_eq_support_min' p_neq_zero]
+          rw [natTrailingDegree_eq_support_min' (ne_zero_of_ne_zero_of_monic X_ne_zero p_monic)]
           exact Finset.min'_le p.support b b_support
-        have this2 : d ≤ p.natDegree := by
-          exact Polynomial.natTrailingDegree_le_natDegree p
+        have this2 : p.natTrailingDegree ≤ p.natDegree := Polynomial.natTrailingDegree_le_natDegree p
         rw [Nat.sub_eq_iff_eq_add this1] at h
         simp [h, this1, this2]
     . constructor
-      . rw [finset_sum_coeff]
-        rw [Finset.sum_eq_single_of_mem d]
+      . rw [finset_sum_coeff, Finset.sum_eq_single_of_mem p.natTrailingDegree]
         . rw [coeff_monomial]
-          simp [d, p_neq_zero]
-        . exact natTrailingDegree_mem_support_of_nonzero p_neq_zero
+          simp only [le_refl, tsub_eq_zero_of_le, ↓reduceIte, ne_eq,
+            coeff_natTrailingDegree_eq_zero, ne_zero_of_ne_zero_of_monic X_ne_zero p_monic,
+            not_false_eq_true]
+        . exact natTrailingDegree_mem_support_of_nonzero
+            (ne_zero_of_ne_zero_of_monic X_ne_zero p_monic)
         . intro n n_support n_neq_d
           rw [coeff_monomial_of_ne]
-          have : d ≤ n := by
-            apply natTrailingDegree_le_of_mem_supp
-            exact n_support
+          have : p.natTrailingDegree ≤ n := natTrailingDegree_le_of_mem_supp _ n_support
           by_contra h
           apply n_neq_d
           rw [Nat.sub_eq_iff_eq_add this] at h
@@ -578,13 +572,12 @@ theorem Polynomial.monic_nonzero_const_if_isIntegral (R S : Type) [CommRing R] [
           nth_rw 3 [as_sum_support p]
           rw [eval₂_finset_sum]
           simp
-        have : (s ^ d) * ∑ n ∈ p.support, (algebraMap R S) (p.coeff n) * (s ^ (n - d)) = 0 := by
-          rw [← this]
-          rw [Finset.mul_sum]
-          congr
-          ext n
+        have : (s ^ p.natTrailingDegree) * ∑ n ∈ p.support, (algebraMap R S) (p.coeff n)
+            * (s ^ (n - p.natTrailingDegree)) = 0 := by
+          rw [← this, Finset.mul_sum]
+          congr with n
           rcases Classical.em (n ∈ p.support) with n_support | n_nsupport
-          . have : d ≤ n := natTrailingDegree_le_of_mem_supp n n_support
+          . have : p.natTrailingDegree ≤ n := natTrailingDegree_le_of_mem_supp n n_support
             rw [mul_comm, mul_assoc]
             congr
             rw [mul_comm]
@@ -593,9 +586,7 @@ theorem Polynomial.monic_nonzero_const_if_isIntegral (R S : Type) [CommRing R] [
             simp
         let zero_or_zero := NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero this
         rcases zero_or_zero with s_pow_zero | h
-        . by_contra
-          apply hs
-          exact pow_eq_zero s_pow_zero
+        . by_contra; exact hs (pow_eq_zero s_pow_zero)
         . exact h
 
 theorem Algebra.exists_dvd_nonzero_if_isIntegral (R S : Type) [CommRing R] [Nontrivial R]

From bed8a228dcb2c7bf172c88fa874eae20a2b430e6 Mon Sep 17 00:00:00 2001
From: morrison-daniel <39346894+morrison-daniel@users.noreply.github.com>
Date: Thu, 10 Oct 2024 15:51:34 -0700
Subject: [PATCH 06/10] Golfing lemmas

---
 FLT/MathlibExperiments/FrobeniusRiou.lean | 33 +++++++++++++++++++++++
 1 file changed, 33 insertions(+)

diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean
index d8fb5e2cb..0d8e8de11 100644
--- a/FLT/MathlibExperiments/FrobeniusRiou.lean
+++ b/FLT/MathlibExperiments/FrobeniusRiou.lean
@@ -627,6 +627,39 @@ theorem Algebra.exists_dvd_nonzero_if_isIntegral (R S : Type) [CommRing R] [Nont
     nth_rw 1 [← pow_one s]
     exact pow_mul_pow_sub s (Nat.one_le_iff_ne_zero.mpr i_nzero)
 
+theorem Polynomial.monic_nonzero_const_if_isIntegral' (R S : Type) [CommRing R] [Nontrivial R]
+    [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] [IsDomain S] (s : S) (hs : s ≠ 0) :
+    ∃ (q : Polynomial R), q.coeff 0 ≠ 0 ∧ q.eval₂ (algebraMap R S) s = 0 := by
+  obtain ⟨p, p_monic, p_eval⟩ := (@Algebra.isIntegral_def R S).mp inferInstance s
+  have p_nzero := ne_zero_of_ne_zero_of_monic X_ne_zero p_monic
+  obtain ⟨q, p_eq, q_ndvd⟩ := Polynomial.exists_eq_pow_rootMultiplicity_mul_and_not_dvd p p_nzero 0
+  rw [C_0, sub_zero] at p_eq
+  rw [C_0, sub_zero] at q_ndvd
+  use q
+  constructor
+  . intro q_coeff_0
+    exact q_ndvd <| X_dvd_iff.mpr q_coeff_0
+  . rw [p_eq, eval₂_mul] at p_eval
+    rcases NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero p_eval with Xpow_eval | q_eval
+    . by_contra
+      apply hs
+      rw [eval₂_X_pow] at Xpow_eval
+      exact pow_eq_zero Xpow_eval
+    . exact q_eval
+
+theorem Algebra.exists_dvd_nonzero_if_isIntegral' (R S : Type) [CommRing R] [Nontrivial R]
+    [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] [IsDomain S] (s : S) (hs : s ≠ 0) :
+    ∃ r : R, r ≠ 0 ∧ s ∣ (algebraMap R S) r := by
+  obtain ⟨q, q_zero_coeff, q_eval_zero⟩ := Polynomial.monic_nonzero_const_if_isIntegral' R S s hs
+  use q.coeff 0
+  refine ⟨q_zero_coeff, ?_⟩
+  rw [← dvd_neg]
+  rw [← Polynomial.eval₂_C (algebraMap R S) s]
+  nth_rw 1 [← Polynomial.eval₂_X (algebraMap R S) s]
+  rw [← zero_add (-_), Mathlib.Tactic.RingNF.add_neg, ← q_eval_zero, ← Polynomial.eval₂_sub]
+  apply Polynomial.eval₂_dvd
+  exact Polynomial.X_dvd_sub_C
+
 end B_mod_Q_over_A_mod_P_stuff
 
 /-

From a6a1e95e0137389fae6543cd16e0f17d8f4f33e3 Mon Sep 17 00:00:00 2001
From: morrison-daniel <39346894+morrison-daniel@users.noreply.github.com>
Date: Thu, 10 Oct 2024 15:52:48 -0700
Subject: [PATCH 07/10] Golfing lemmas

---
 FLT/MathlibExperiments/FrobeniusRiou.lean | 104 +---------------------
 1 file changed, 2 insertions(+), 102 deletions(-)

diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean
index 0d8e8de11..64f891e56 100644
--- a/FLT/MathlibExperiments/FrobeniusRiou.lean
+++ b/FLT/MathlibExperiments/FrobeniusRiou.lean
@@ -528,106 +528,6 @@ theorem reduction_isIntegral
 end MulSemiringAction
 
 theorem Polynomial.monic_nonzero_const_if_isIntegral (R S : Type) [CommRing R] [Nontrivial R]
-    [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] [IsDomain S] (s : S) (hs : s ≠ 0) :
-    ∃ (q : Polynomial R), Monic q ∧ q.coeff 0 ≠ 0 ∧ q.eval₂ (algebraMap R S) s = 0 := by
-    obtain ⟨p, p_monic, p_eval⟩ := (@Algebra.isIntegral_def R S).mp inferInstance s
-    use ∑ n ∈ p.support, monomial (n - p.natTrailingDegree) (p.coeff n)
-    have : (∑ n ∈ p.support, monomial (n - p.natTrailingDegree) (p.coeff n)).degree
-        ≤ p.natDegree - p.natTrailingDegree := by
-      refine le_trans (Polynomial.degree_sum_le p.support (fun x ↦ monomial (x - p.natTrailingDegree) (p.coeff x))) ?_
-      rw [Finset.sup_le_iff]
-      refine fun n hn ↦ le_trans (degree_monomial_le (n - p.natTrailingDegree) _) (?_)
-      rw [Nat.cast_le]
-      exact Nat.sub_le_sub_right (le_natDegree_of_mem_supp n hn) p.natTrailingDegree
-    constructor
-    . apply monic_of_degree_le_of_coeff_eq_one (p.natDegree - p.natTrailingDegree) this
-      rw [finset_sum_coeff, Finset.sum_eq_single_of_mem p.natDegree]
-      . rw [coeff_natDegree, coeff_monomial_same]
-        exact Monic.leadingCoeff p_monic
-      . exact natDegree_mem_support_of_nonzero (ne_zero_of_ne_zero_of_monic X_ne_zero p_monic)
-      . intro b b_support b_ne_natDegree
-        rw [coeff_monomial_of_ne]
-        by_contra h
-        apply b_ne_natDegree
-        have this1 : p.natTrailingDegree ≤ b := by
-          rw [natTrailingDegree_eq_support_min' (ne_zero_of_ne_zero_of_monic X_ne_zero p_monic)]
-          exact Finset.min'_le p.support b b_support
-        have this2 : p.natTrailingDegree ≤ p.natDegree := Polynomial.natTrailingDegree_le_natDegree p
-        rw [Nat.sub_eq_iff_eq_add this1] at h
-        simp [h, this1, this2]
-    . constructor
-      . rw [finset_sum_coeff, Finset.sum_eq_single_of_mem p.natTrailingDegree]
-        . rw [coeff_monomial]
-          simp only [le_refl, tsub_eq_zero_of_le, ↓reduceIte, ne_eq,
-            coeff_natTrailingDegree_eq_zero, ne_zero_of_ne_zero_of_monic X_ne_zero p_monic,
-            not_false_eq_true]
-        . exact natTrailingDegree_mem_support_of_nonzero
-            (ne_zero_of_ne_zero_of_monic X_ne_zero p_monic)
-        . intro n n_support n_neq_d
-          rw [coeff_monomial_of_ne]
-          have : p.natTrailingDegree ≤ n := natTrailingDegree_le_of_mem_supp _ n_support
-          by_contra h
-          apply n_neq_d
-          rw [Nat.sub_eq_iff_eq_add this] at h
-          simp [h, this]
-      . rw [eval₂_finset_sum]
-        simp
-        have : ∑ n ∈ p.support, (algebraMap R S) (p.coeff n) * s ^ n = 0 := by
-          rw [← p_eval]
-          nth_rw 3 [as_sum_support p]
-          rw [eval₂_finset_sum]
-          simp
-        have : (s ^ p.natTrailingDegree) * ∑ n ∈ p.support, (algebraMap R S) (p.coeff n)
-            * (s ^ (n - p.natTrailingDegree)) = 0 := by
-          rw [← this, Finset.mul_sum]
-          congr with n
-          rcases Classical.em (n ∈ p.support) with n_support | n_nsupport
-          . have : p.natTrailingDegree ≤ n := natTrailingDegree_le_of_mem_supp n n_support
-            rw [mul_comm, mul_assoc]
-            congr
-            rw [mul_comm]
-            exact pow_mul_pow_sub s this
-          . rw [not_mem_support_iff.mp n_nsupport]
-            simp
-        let zero_or_zero := NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero this
-        rcases zero_or_zero with s_pow_zero | h
-        . by_contra; exact hs (pow_eq_zero s_pow_zero)
-        . exact h
-
-theorem Algebra.exists_dvd_nonzero_if_isIntegral (R S : Type) [CommRing R] [Nontrivial R]
-    [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] [IsDomain S] (s : S) (hs : s ≠ 0) :
-    ∃ r : R, r ≠ 0 ∧ s ∣ (r : S) := by
-  obtain ⟨q, _, q_zero_coeff, q_eval_zero⟩ := Polynomial.monic_nonzero_const_if_isIntegral R S s hs
-  have zero_support : 0 ∈ q.support := Polynomial.mem_support_iff.mpr q_zero_coeff
-  have q_eval_zero : ∑ n ∈ q.support, (algebraMap R S) (q.coeff n) * s ^ n = 0 := by
-    rw [← q_eval_zero]
-    nth_rw 3 [Polynomial.as_sum_support q]
-    rw [Polynomial.eval₂_finset_sum]
-    simp
-  refine ⟨q.coeff 0, q_zero_coeff, ?_⟩
-  have : (q.coeff 0 : S) = ((algebraMap R S) (q.coeff 0)) * s ^ 0 := by rw [pow_zero, mul_one]
-  have : q.coeff 0 = - ∑ n ∈ q.support.erase 0, (algebraMap R S) (q.coeff n) * s ^ n := by
-    rw [← sub_add_cancel_left (q.coeff 0 : S)
-      (∑ n ∈ q.support.erase 0, (algebraMap R S) (q.coeff n) * s ^ n)]
-    nth_rw 3 [this]
-    rw [add_comm, Finset.sum_erase_add _ _ zero_support, q_eval_zero]
-    simp
-  rw [this, dvd_neg]
-  refine ⟨∑ n ∈ q.support.erase 0, (algebraMap R S) (q.coeff n) * s ^ (n - 1), ?_⟩
-  rw [Finset.mul_sum]
-  refine Finset.sum_equiv (Equiv.refl ℕ) (fun _ ↦ Iff.symm (Eq.to_iff rfl)) ?_
-  . intro i hi
-    rw [Finset.mem_erase] at hi
-    obtain ⟨i_nzero, _⟩ := hi
-    rw [Equiv.refl_apply, ← mul_assoc]
-    nth_rw 3 [mul_comm]
-    rw [mul_assoc]
-    congr
-    symm
-    nth_rw 1 [← pow_one s]
-    exact pow_mul_pow_sub s (Nat.one_le_iff_ne_zero.mpr i_nzero)
-
-theorem Polynomial.monic_nonzero_const_if_isIntegral' (R S : Type) [CommRing R] [Nontrivial R]
     [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] [IsDomain S] (s : S) (hs : s ≠ 0) :
     ∃ (q : Polynomial R), q.coeff 0 ≠ 0 ∧ q.eval₂ (algebraMap R S) s = 0 := by
   obtain ⟨p, p_monic, p_eval⟩ := (@Algebra.isIntegral_def R S).mp inferInstance s
@@ -647,10 +547,10 @@ theorem Polynomial.monic_nonzero_const_if_isIntegral' (R S : Type) [CommRing R]
       exact pow_eq_zero Xpow_eval
     . exact q_eval
 
-theorem Algebra.exists_dvd_nonzero_if_isIntegral' (R S : Type) [CommRing R] [Nontrivial R]
+theorem Algebra.exists_dvd_nonzero_if_isIntegral (R S : Type) [CommRing R] [Nontrivial R]
     [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] [IsDomain S] (s : S) (hs : s ≠ 0) :
     ∃ r : R, r ≠ 0 ∧ s ∣ (algebraMap R S) r := by
-  obtain ⟨q, q_zero_coeff, q_eval_zero⟩ := Polynomial.monic_nonzero_const_if_isIntegral' R S s hs
+  obtain ⟨q, q_zero_coeff, q_eval_zero⟩ := Polynomial.monic_nonzero_const_if_isIntegral R S s hs
   use q.coeff 0
   refine ⟨q_zero_coeff, ?_⟩
   rw [← dvd_neg]

From 0da260f1d4b9679fcb4f849d0a31dd045c2da98b Mon Sep 17 00:00:00 2001
From: morrison-daniel <39346894+morrison-daniel@users.noreply.github.com>
Date: Thu, 10 Oct 2024 15:55:48 -0700
Subject: [PATCH 08/10] cleanup

---
 FLT/MathlibExperiments/FrobeniusRiou.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean
index 64f891e56..5c4942076 100644
--- a/FLT/MathlibExperiments/FrobeniusRiou.lean
+++ b/FLT/MathlibExperiments/FrobeniusRiou.lean
@@ -553,9 +553,7 @@ theorem Algebra.exists_dvd_nonzero_if_isIntegral (R S : Type) [CommRing R] [Nont
   obtain ⟨q, q_zero_coeff, q_eval_zero⟩ := Polynomial.monic_nonzero_const_if_isIntegral R S s hs
   use q.coeff 0
   refine ⟨q_zero_coeff, ?_⟩
-  rw [← dvd_neg]
-  rw [← Polynomial.eval₂_C (algebraMap R S) s]
-  nth_rw 1 [← Polynomial.eval₂_X (algebraMap R S) s]
+  rw [← Polynomial.eval₂_X (algebraMap R S) s, ← dvd_neg, ← Polynomial.eval₂_C (algebraMap R S) s]
   rw [← zero_add (-_), Mathlib.Tactic.RingNF.add_neg, ← q_eval_zero, ← Polynomial.eval₂_sub]
   apply Polynomial.eval₂_dvd
   exact Polynomial.X_dvd_sub_C

From 5c8554d2961c097211d4fb7fb23dc522f5537f7d Mon Sep 17 00:00:00 2001
From: morrison-daniel <39346894+morrison-daniel@users.noreply.github.com>
Date: Thu, 10 Oct 2024 15:57:37 -0700
Subject: [PATCH 09/10] Rename theorem for refactor

---
 FLT/MathlibExperiments/FrobeniusRiou.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean
index 5c4942076..218e4b33e 100644
--- a/FLT/MathlibExperiments/FrobeniusRiou.lean
+++ b/FLT/MathlibExperiments/FrobeniusRiou.lean
@@ -527,7 +527,7 @@ theorem reduction_isIntegral
 
 end MulSemiringAction
 
-theorem Polynomial.monic_nonzero_const_if_isIntegral (R S : Type) [CommRing R] [Nontrivial R]
+theorem Polynomial.nonzero_const_if_isIntegral (R S : Type) [CommRing R] [Nontrivial R]
     [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] [IsDomain S] (s : S) (hs : s ≠ 0) :
     ∃ (q : Polynomial R), q.coeff 0 ≠ 0 ∧ q.eval₂ (algebraMap R S) s = 0 := by
   obtain ⟨p, p_monic, p_eval⟩ := (@Algebra.isIntegral_def R S).mp inferInstance s
@@ -550,7 +550,7 @@ theorem Polynomial.monic_nonzero_const_if_isIntegral (R S : Type) [CommRing R] [
 theorem Algebra.exists_dvd_nonzero_if_isIntegral (R S : Type) [CommRing R] [Nontrivial R]
     [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] [IsDomain S] (s : S) (hs : s ≠ 0) :
     ∃ r : R, r ≠ 0 ∧ s ∣ (algebraMap R S) r := by
-  obtain ⟨q, q_zero_coeff, q_eval_zero⟩ := Polynomial.monic_nonzero_const_if_isIntegral R S s hs
+  obtain ⟨q, q_zero_coeff, q_eval_zero⟩ := Polynomial.nonzero_const_if_isIntegral R S s hs
   use q.coeff 0
   refine ⟨q_zero_coeff, ?_⟩
   rw [← Polynomial.eval₂_X (algebraMap R S) s, ← dvd_neg, ← Polynomial.eval₂_C (algebraMap R S) s]

From 01ddfd0dcb2661e9be209ee5ccd760eee380d514 Mon Sep 17 00:00:00 2001
From: kbuzzard <31867827+kbuzzard@users.noreply.github.com>
Date: Wed, 16 Oct 2024 08:18:45 +0000
Subject: [PATCH 10/10] [create-pull-request] automated change

---
 lake-manifest.json | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index db55fa254..95381d490 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "daf1ed91789811cf6bbb7bf2f4dad6b3bad8fbf4",
+   "rev": "b731e84cb99d738b8d9710a0ba02bf8ec8d7fd26",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2b2f6d7fbe9d917fc010e9054c1ce11774c9088b",
+   "rev": "fa3d73a2cf077f4b14c7840352ac7b08aeb6eb41",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,10 +35,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
+   "rev": "cd20dae87c48495f0220663014dff11671597fcf",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.42",
+   "inputRev": "v0.0.43-pre",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7376ac07aa2b0492372c056b7a2c3163b3026d1e",
+   "rev": "9b4088ccf0f44ddd7b1132bb1348aef8cf481e12",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8a434b09e83db1785dbd4476134981712c606746",
+   "rev": "765ccc9135f3ebeec047798d6c715dc3224c0c73",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,