Merge branch 'master' of https://github.com/leanprover-community/flt-…

…regular

.github/workflows/push.yml

@@ -46,7 +46,7 @@ jobs:
         run: ~/.elan/bin/lake -Kenv=dev exe cache get
 
       - name: Build project
-        run: ~/.elan/bin/lake -Kenv=dev build FltRegular
+        run: ~/.elan/bin/lake -R -Kenv=dev build FltRegular
 
       - uses: actions/cache@v3
         name: Mathlib doc Cache
@@ -57,7 +57,7 @@ jobs:
             DocGen4-
 
       - name: Build documentation
-        run: ~/.elan/bin/lake -Kenv=dev build FltRegular:docs
+        run: ~/.elan/bin/lake -R -Kenv=dev build FltRegular:docs
 
       - name: Install Python
         uses: actions/setup-python@v4

FltRegular.lean

@@ -1,3 +1,31 @@
--- This module serves as the root of the `FltRegular` library.
--- Import modules here that should be built as part of the library.
-import «FltRegular».FltRegular
+import FltRegular.CaseI.AuxLemmas
+import FltRegular.CaseI.Statement
+import FltRegular.CaseII.AuxLemmas
+import FltRegular.CaseII.InductionStep
+import FltRegular.CaseII.Statement
+import FltRegular.FLT5
+import FltRegular.FltRegular
+import FltRegular.MayAssume.Lemmas
+import FltRegular.NumberTheory.AuxLemmas
+import FltRegular.NumberTheory.Cyclotomic.CaseI
+import FltRegular.NumberTheory.Cyclotomic.CyclRat
+import FltRegular.NumberTheory.Cyclotomic.CyclotomicUnits
+import FltRegular.NumberTheory.Cyclotomic.Factoring
+import FltRegular.NumberTheory.Cyclotomic.GaloisActionOnCyclo
+import FltRegular.NumberTheory.Cyclotomic.MoreLemmas
+import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
+import FltRegular.NumberTheory.CyclotomicRing
+import FltRegular.NumberTheory.Different
+import FltRegular.NumberTheory.Finrank
+import FltRegular.NumberTheory.GaloisPrime
+import FltRegular.NumberTheory.Hilbert90
+import FltRegular.NumberTheory.Hilbert92
+import FltRegular.NumberTheory.Hilbert94
+import FltRegular.NumberTheory.IdealNorm
+import FltRegular.NumberTheory.KummersLemma.Field
+import FltRegular.NumberTheory.KummersLemma.KummersLemma
+import FltRegular.NumberTheory.QuotientTrace
+import FltRegular.NumberTheory.RegularPrimes
+import FltRegular.NumberTheory.SystemOfUnits
+import FltRegular.NumberTheory.Unramified
+import FltRegular.ReadyForMathlib.Homogenization

FltRegular/CaseI/AuxLemmas.lean

@@ -1,7 +1,5 @@
-import FltRegular.MayAssume.Lemmas
-import FltRegular.NumberTheory.Cyclotomic.Factoring
 import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
-import FltRegular.NumberTheory.Cyclotomic.CaseI
+import FltRegular.NumberTheory.Cyclotomic.CyclRat
 
 open Finset Nat IsCyclotomicExtension Ideal Polynomial Int Basis
 
@@ -27,7 +25,7 @@ section Zerok₁
 
 theorem aux_cong0k₁ {k : Fin p} (hcong : k ≡ -1 [ZMOD p]) :
   k = ⟨p.pred, pred_lt hpri.ne_zero⟩ := by
-  refine' Fin.ext _
+  refine Fin.ext ?_
   rw [Fin.val_mk, ← ZMod.val_cast_of_lt (Fin.is_lt k)]
   suffices ((k : ℤ) : ZMod p).val = p.pred by simpa
   rw [← ZMod.intCast_eq_intCast_iff] at hcong
@@ -41,7 +39,7 @@ theorem aux_cong0k₁ {k : Fin p} (hcong : k ≡ -1 [ZMOD p]) :
 def f0k₁ (b : ℤ) (p : ℕ) : ℕ → ℤ := fun x => if x = 1 then b else if x = p.pred then -b else 0
 
 theorem auxf0k₁ (hp5 : 5 ≤ p) (b : ℤ) : ∃ i : Fin P, f0k₁ b p (i : ℕ) = 0 := by
-  refine' ⟨⟨2, two_lt hp5⟩, _⟩
+  refine ⟨⟨2, two_lt hp5⟩, ?_⟩
   have hpred : ((⟨2, two_lt hp5⟩ : Fin p) : ℕ) ≠ p.pred := by
     intro h
     simp only [Fin.ext_iff, Fin.val_mk] at h
@@ -69,7 +67,7 @@ theorem aux0k₁ {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot 
       Finset.range_filter_eq]
     simp [hpri.one_lt, Nat.sub_lt hpri.pos, sub_eq_add_neg]
   rw [sum_range] at key
-  refine' caseI (Dvd.dvd.mul_right (Dvd.dvd.mul_left _ _) _)
+  refine caseI (Dvd.dvd.mul_right (Dvd.dvd.mul_left ?_ _) _)
   replace hpri : (P : ℕ).Prime := hpri
   simpa [f0k₁] using dvd_coeff_cycl_integer hpri hζ (auxf0k₁ hpri hp5 b) key ⟨1, hpri.one_lt⟩
 
@@ -81,7 +79,7 @@ section Zerok₂
 def f0k₂ (a b : ℤ) : ℕ → ℤ := fun x => if x = 0 then a - b else if x = 1 then b - a else 0
 
 theorem aux_cong0k₂ {k : Fin p} (hcong : k ≡ 1 [ZMOD p]) : k = ⟨1, hpri.one_lt⟩ := by
-  refine' Fin.ext _
+  refine Fin.ext ?_
   rw [Fin.val_mk, ← ZMod.val_cast_of_lt (Fin.is_lt k)]
   suffices ((k : ℤ) : ZMod p).val = 1 by simpa
   rw [← ZMod.intCast_eq_intCast_iff] at hcong
@@ -90,7 +88,7 @@ theorem aux_cong0k₂ {k : Fin p} (hcong : k ≡ 1 [ZMOD p]) : k = ⟨1, hpri.on
   simp [ZMod.val_one]
 
 theorem auxf0k₂ (hp5 : 5 ≤ p) (a b : ℤ) : ∃ i : Fin P, f0k₂ a b (i : ℕ) = 0 := by
-  refine' ⟨⟨2, two_lt hp5⟩, _⟩
+  refine ⟨⟨2, two_lt hp5⟩, ?_⟩
   have h1 : ((⟨2, two_lt hp5⟩ : Fin p) : ℕ) ≠ 1 := by
     intro h
     simp only [Fin.ext_iff, Fin.val_mk] at h; contradiction
@@ -117,7 +115,7 @@ theorem aux0k₂ {a b : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ
     simp only [hpri.pos, hpri.one_lt, if_true, zsmul_eq_mul, Int.cast_sub, sum_singleton,
       _root_.pow_zero, mul_one, pow_one, Ne, zero_smul, sum_const_zero, add_zero, Fin.val_mk]
   rw [sum_range] at key
-  refine' hab _
+  refine hab ?_
   symm
   rw [← ZMod.intCast_eq_intCast_iff, ZMod.intCast_eq_intCast_iff_dvd_sub]
   have hpri₁ : (P : ℕ).Prime := hpri
@@ -128,7 +126,7 @@ end Zerok₂
 section OnekOne
 
 theorem aux_cong1k₁ {k : Fin p} (hcong : k ≡ 0 [ZMOD p]) : k = ⟨0, hpri.pos⟩ := by
-  refine' Fin.ext _
+  refine Fin.ext ?_
   rw [Fin.val_mk, ← ZMod.val_cast_of_lt (Fin.is_lt k)]
   suffices ((k : ℤ) : ZMod p).val = 0 by simpa
   rw [← ZMod.intCast_eq_intCast_iff] at hcong
@@ -155,7 +153,7 @@ def f1k₂ (a : ℤ) : ℕ → ℤ := fun x => if x = 0 then a else if x = 2 the
 
 theorem aux_cong1k₂ {k : Fin p} (hpri : p.Prime) (hp5 : 5 ≤ p) (hcong : k ≡ 1 + 1 [ZMOD p]) :
     k = ⟨2, two_lt hp5⟩ := by
-  refine' Fin.ext _
+  refine Fin.ext ?_
   rw [Fin.val_mk, ← ZMod.val_cast_of_lt (Fin.is_lt k)]
   suffices ((k : ℤ) : ZMod p).val = 2 by simpa
   rw [← ZMod.intCast_eq_intCast_iff] at hcong
@@ -169,15 +167,9 @@ theorem aux_cong1k₂ {k : Fin p} (hpri : p.Prime) (hp5 : 5 ≤ p) (hcong : k 
   linarith
 
 theorem auxf1k₂ (a : ℤ) : ∃ i : Fin P, f1k₂ a (i : ℕ) = 0 := by
-  refine' ⟨⟨1, hpri.one_lt⟩, _⟩
-  have h2 : ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) ≠ 2 :=
-    by
-    intro h
-    simp only [Fin.ext_iff, Fin.val_mk] at h; contradiction
-  have hzero : ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) ≠ 0 :=
-    by
-    intro h
-    simp only [Fin.ext_iff, Fin.val_mk] at h
+  refine ⟨⟨1, hpri.one_lt⟩, ?_⟩
+  have h2 : ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) ≠ 2 := fun h ↦ by simp at h
+  have hzero : ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) ≠ 0 := fun h ↦ by simp at h
   simp only [f1k₂, h2, if_false, hzero, one_lt_two.ne]
 
 theorem aux1k₂ {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ p)
@@ -200,7 +192,7 @@ theorem aux1k₂ {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot 
   sum_neg_distrib, ne_eq, mem_range, not_and, not_not, zero_smul, sum_const_zero, add_zero]
     ring
   rw [sum_range] at key
-  refine' caseI (Dvd.dvd.mul_right (Dvd.dvd.mul_right _ _) _)
+  refine caseI (Dvd.dvd.mul_right (Dvd.dvd.mul_right ?_ _) _)
   have hpri₁ : (P : ℕ).Prime := hpri
   simpa [f1k₂] using dvd_coeff_cycl_integer hpri₁ hζ (auxf1k₂ hpri a) key ⟨0, hpri.pos⟩
 

FltRegular/CaseI/Statement.lean

@@ -1,4 +1,8 @@
+import FltRegular.MayAssume.Lemmas
+import FltRegular.NumberTheory.Cyclotomic.Factoring
+import FltRegular.NumberTheory.Cyclotomic.CaseI
 import FltRegular.CaseI.AuxLemmas
+import FltRegular.NumberTheory.RegularPrimes
 
 open Finset Nat IsCyclotomicExtension Ideal Polynomial Int Basis FltRegular.CaseI
 
@@ -32,8 +36,7 @@ theorem may_assume : SlightlyEasier → Statement := by
   have hodd : p ≠ 2 := by
     intro h
     rw [h] at H hI
-    refine' hI _
-    refine' Dvd.dvd.mul_left _ _
+    refine hI <| Dvd.dvd.mul_left ?_ _
     simp only [Nat.cast_ofNat] at hI ⊢
     rw [← even_iff_two_dvd, ← Int.odd_iff_not_even] at hI
     rw [← even_iff_two_dvd, ← Int.even_pow' (show 2 ≠ 0 by norm_num), ← H]
@@ -49,7 +52,7 @@ theorem may_assume : SlightlyEasier → Statement := by
     fin_cases this
     · exact MayAssume.p_ne_three hprod H rfl
     · rw [show 2 + 1 + 1 = 2 * 2 from rfl] at hpri
-      refine' Nat.not_prime_mul one_lt_two.ne' one_lt_two.ne' hpri.out
+      exact Nat.not_prime_mul one_lt_two.ne' one_lt_two.ne' hpri.out
   rcases MayAssume.coprime H hprod with ⟨Hxyz, hunit, hprodxyx⟩
   let d := ({a, b, c} : Finset ℤ).gcd id
   have hdiv : ¬↑p ∣ a / d * (b / d) * (c / d) :=
@@ -86,7 +89,7 @@ theorem ab_coprime {a b c : ℤ} (H : a ^ p + b ^ p = c ^ p) (hpzero : p ≠ 0)
     rw [← H]
     exact dvd_add (dvd_pow haq hpzero) (dvd_pow hbq hpzero)
   have Hq : ↑q ∣ ({a, b, c} : Finset ℤ).gcd id := by
-    refine' dvd_gcd fun x hx => _
+    refine dvd_gcd fun x hx ↦ ?_
     simp only [mem_insert, mem_singleton] at hx
     rcases hx with (H | H | H) <;> simpa [H]
   rw [hgcd] at Hq
@@ -104,8 +107,8 @@ theorem exists_ideal {a b c : ℤ} (h5p : 5 ≤ p) (H : a ^ p + b ^ p = c ^ p)
     (hpri.out.eq_two_or_odd.resolve_left fun h => by simp [h] at h5p) hζ'] at H₁
   replace H₁ := congr_arg (fun x => span ({ x } : Set R)) H₁
   simp only [← prod_span_singleton, ← span_singleton_pow] at H₁
-  refine' Finset.exists_eq_pow_of_mul_eq_pow_of_coprime (fun η₁ hη₁ η₂ hη₂ hη => ?_) H₁ ζ hζ
-  refine' fltIdeals_coprime _ _ H (ab_coprime H hpri.out.ne_zero hgcd) hη₁ hη₂ hη caseI
+  refine exists_eq_pow_of_mul_eq_pow_of_coprime (fun η₁ hη₁ η₂ hη₂ hη => ?_) H₁ ζ hζ
+  refine fltIdeals_coprime ?_ ?_ H (ab_coprime H hpri.out.ne_zero hgcd) hη₁ hη₂ hη caseI
   · exact hpri.out
   · exact h5p
 
@@ -123,7 +126,7 @@ theorem is_principal_aux (K' : Type*) [Field K'] [CharZero K'] [IsCyclotomicExte
   replace hα := congr_arg (fun (J : Submodule _ _) => J ^ p) hα
   simp only [← hI, submodule_span_eq, span_singleton_pow, span_singleton_eq_span_singleton] at hα
   obtain ⟨u, hu⟩ := hα
-  refine' ⟨u⁻¹, α, _⟩
+  refine ⟨u⁻¹, α, ?_⟩
   rw [← hu, mul_comm ((_ + ζ * _)), ← mul_assoc]
   simp only [Units.inv_mul, one_mul]
 
@@ -157,10 +160,10 @@ theorem ex_fin_div {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hreg : IsRegularPrime
   obtain ⟨k, hk⟩ := FltRegular.CaseI.exists_int_sum_eq_zero hζ' hP hpri.out a b 1 hu.symm
   simp only [zpow_one, zpow_neg, PNat.mk_coe, mem_span_singleton, ← h] at hk
   have hpcoe : (p : ℤ) ≠ 0 := by simp [hpri.out.ne_zero]
-  refine' ⟨⟨(2 * k % p).natAbs, _⟩, ⟨((2 * k - 1) % p).natAbs, _⟩, _, _⟩
+  refine ⟨⟨(2 * k % p).natAbs, ?_⟩, ⟨((2 * k - 1) % p).natAbs, ?_⟩, ?_, ?_⟩
   repeat'
     rw [← natAbs_ofNat p]
-    refine' natAbs_lt_natAbs_of_nonneg_of_lt (emod_nonneg _ hpcoe) _
+    refine natAbs_lt_natAbs_of_nonneg_of_lt (emod_nonneg _ hpcoe) ?_
     rw [natAbs_ofNat]
     exact emod_lt_of_pos _ (by simp [hpri.out.pos])
   · simp only [natAbs_of_nonneg (emod_nonneg _ hpcoe), ← ZMod.intCast_eq_intCast_iff,
@@ -170,14 +173,13 @@ theorem ex_fin_div {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hreg : IsRegularPrime
   rw [mul_add, mul_comm (↑a : R), ← mul_assoc _ (↑b : R), mul_comm _ (↑b : R), mul_assoc (↑b : R)]
   congr 2
   · ext
-    simp only [Fin.val_mk, map_pow, NumberField.Units.coe_zpow, IsPrimitiveRoot.coe_unit'_coe]
+    simp only [Fin.val_mk, map_pow, NumberField.Units.coe_zpow, ← h]
     refine eq_of_div_eq_one ?_
     rw [← zpow_natCast, ← zpow_sub₀ (hζ'.ne_zero hpri.out.ne_zero), hζ'.zpow_eq_one_iff_dvd]
     simp only [natAbs_of_nonneg (emod_nonneg _ hpcoe), ← ZMod.intCast_zmod_eq_zero_iff_dvd,
       Int.cast_sub, ZMod.intCast_mod, Int.cast_mul, Int.cast_natCast, sub_self]
   · ext
-    simp only [Fin.val_mk, map_pow, _root_.map_mul, NumberField.Units.coe_zpow,
-      IsPrimitiveRoot.coe_unit'_coe, IsPrimitiveRoot.coe_inv_unit'_coe]
+    simp only [Fin.val_mk, map_pow, _root_.map_mul, NumberField.Units.coe_zpow, map_units_inv, ← h]
     refine eq_of_div_eq_one ?_
     rw [← zpow_natCast, ← zpow_sub_one₀ (hζ'.ne_zero hpri.out.ne_zero), ←
       zpow_sub₀ (hζ'.ne_zero hpri.out.ne_zero), hζ'.zpow_eq_one_iff_dvd]
@@ -194,7 +196,7 @@ theorem auxf' (hp5 : 5 ≤ p) (a b : ℤ) (k₁ k₂ : Fin p) :
   have h1 : 1 < p := by linarith
   let s := ({0, 1, k₁.1, k₂.1} : Finset ℕ)
   have : s.card ≤ 4 := by
-    repeat refine' le_trans (card_insert_le _ _) (succ_le_succ _)
+    repeat refine le_trans (card_insert_le _ _) (succ_le_succ ?_)
     exact rfl.ge
   replace this : s.card < 5 := lt_of_le_of_lt this (by norm_num)
   have hs : s ⊆ range p := insert_subset_iff.2 ⟨mem_range.2 h0, insert_subset_iff.2
@@ -205,7 +207,7 @@ theorem auxf' (hp5 : 5 ≤ p) (a b : ℤ) (k₁ k₂ : Fin p) :
     rw [← Finset.card_pos, hcard, card_range]
     exact Nat.sub_pos_of_lt (lt_of_lt_of_le this hp5)
   obtain ⟨i, hi⟩ := hcard
-  refine' ⟨i, sdiff_subset hi, _⟩
+  refine ⟨i, sdiff_subset hi, ?_⟩
   have hi0 : i ≠ 0 := fun h => by simp [h, s] at hi
   have hi1 : i ≠ 1 := fun h => by simp [h, s] at hi
   have hik₁ : i ≠ k₁ := fun h => by simp [h, s] at hi
@@ -243,7 +245,7 @@ theorem caseI_easier {a b c : ℤ} (hreg : IsRegularPrime p) (hp5 : 5 ≤ p)
       add_zero]
     ring
   rw [sum_range] at key
-  refine' caseI (Dvd.dvd.mul_right (Dvd.dvd.mul_right _ _) _)
+  refine caseI (Dvd.dvd.mul_right (Dvd.dvd.mul_right ?_ _) _)
   simpa [f] using dvd_coeff_cycl_integer (by exact hpri.out) hζ (auxf hp5 a b k₁ k₂) key
     ⟨0, hpri.out.pos⟩
 

FltRegular/CaseII/AuxLemmas.lean

@@ -1,12 +1,7 @@
-import Mathlib.NumberTheory.Cyclotomic.Rat
-import FltRegular.NumberTheory.Cyclotomic.Factoring
-import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
-import Mathlib.RingTheory.Ideal.Norm
 import Mathlib.RingTheory.ClassGroup
-import FltRegular.NumberTheory.Cyclotomic.MoreLemmas
-import FltRegular.ReadyForMathlib.PowerBasis
+import Mathlib.NumberTheory.NumberField.Basic
 
-variable {K : Type*} {p : ℕ+} [hpri : Fact p.Prime] [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K]
+variable {K : Type*} {p : ℕ+} [Field K] [CharZero K]
 
 variable {ζ : K} (hζ : IsPrimitiveRoot ζ p)
 
@@ -49,11 +44,6 @@ lemma WfDvdMonoid.multiplicity_finite_iff {M : Type*} [CancelCommMonoidWithZero
   · intro ⟨hx, hy⟩
     exact WfDvdMonoid.multiplicity_finite hx hy
 
-lemma WfDvdMonoid.multiplicity_eq_top_iff {M : Type*} [CancelCommMonoidWithZero M] [WfDvdMonoid M]
-    [DecidableRel (fun a b : M ↦ a ∣ b)] {x y : M} :
-    multiplicity x y = ⊤ ↔ IsUnit x ∨ y = 0 := by
-  rw [multiplicity.eq_top_iff_not_finite, WfDvdMonoid.multiplicity_finite_iff, or_iff_not_and_not]
-
 lemma dvd_iff_multiplicity_le {M : Type*}
     [CancelCommMonoidWithZero M] [DecidableRel (fun a b : M ↦ a ∣ b)] [UniqueFactorizationMonoid M]
     {a b : M} (ha : a ≠ 0) : a ∣ b ↔ ∀ p : M, Prime p → multiplicity p a ≤ multiplicity p b := by
@@ -69,7 +59,7 @@ lemma dvd_iff_multiplicity_le {M : Type*}
     · simp only [ne_eq, mul_eq_zero, not_or] at ha
       rw [UniqueFactorizationMonoid.irreducible_iff_prime] at hq
       obtain ⟨c, rfl⟩ : a ∣ b := by
-        refine' IH ha.2 (fun p hp ↦ (le_trans ?_ (H p hp)))
+        refine IH ha.2 (fun p hp ↦ (le_trans ?_ (H p hp)))
         rw [multiplicity.mul hp]
         exact le_add_self
       rw [mul_comm]

FltRegular/CaseII/InductionStep.lean

@@ -1,5 +1,6 @@
 import FltRegular.CaseII.AuxLemmas
 import FltRegular.NumberTheory.KummersLemma.KummersLemma
+import FltRegular.NumberTheory.Cyclotomic.Factoring
 
 open scoped BigOperators nonZeroDivisors NumberField
 open Polynomial
@@ -47,8 +48,8 @@ lemma one_sub_zeta_dvd_zeta_pow_sub : π ∣ x + y * η := by
   letI : Fact (Nat.Prime p) := hpri
   letI := IsCyclotomicExtension.numberField {p} ℚ K
   have h := zeta_sub_one_dvd hζ e
-  replace h : ∏ _η in nthRootsFinset p (𝓞 K), Ideal.Quotient.mk 𝔭 (x + y * η : 𝓞 K) = 0
-  · rw [pow_add_pow_eq_prod_add_zeta_runity_mul (hpri.out.eq_two_or_odd.resolve_left
+  replace h : ∏ _η in nthRootsFinset p (𝓞 K), Ideal.Quotient.mk 𝔭 (x + y * η : 𝓞 K) = 0 := by
+    rw [pow_add_pow_eq_prod_add_zeta_runity_mul (hpri.out.eq_two_or_odd.resolve_left
       (PNat.coe_injective.ne hp)) hζ.unit'_coe, ← Ideal.Quotient.eq_zero_iff_dvd, map_prod] at h
     convert h using 2 with η' hη'
     rw [map_add, map_add, map_mul, map_mul, IsPrimitiveRoot.eq_one_mod_one_sub' hζ.unit'_coe hη',
@@ -60,8 +61,8 @@ lemma one_sub_zeta_dvd_zeta_pow_sub : π ∣ x + y * η := by
 lemma div_one_sub_zeta_mem : IsIntegral ℤ ((x + y * η : 𝓞 K) / (ζ - 1)) := by
   obtain ⟨⟨a, ha⟩, e⟩ := one_sub_zeta_dvd_zeta_pow_sub hp hζ e η
   rw [e, mul_comm]
-  simp only [map_mul, NumberField.RingOfIntegers.map_mk, map_sub, IsPrimitiveRoot.coe_unit'_coe,
-    map_one]
+  simp only [map_mul, NumberField.RingOfIntegers.map_mk, map_sub,
+    map_one, show hζ.unit'.1 = ζ from rfl]
   rwa [mul_div_cancel_right₀ _ (hζ.sub_one_ne_zero hpri.out.one_lt)]
 
 /- Make (x+yη)/(ζ-1) into an element of O_K -/
@@ -72,7 +73,8 @@ fun η ↦ ⟨(x + y * η.1) / (ζ - 1), div_one_sub_zeta_mem hp hζ e η⟩
 lemma div_zeta_sub_one_mul_zeta_sub_one (η) :
     div_zeta_sub_one hp hζ e η * (π) = x + y * η := by
   ext
-  simp [div_zeta_sub_one, div_mul_cancel₀ _ (hζ.sub_one_ne_zero hpri.out.one_lt)]
+  simp [show hζ.unit'.1 = ζ from rfl,
+    div_zeta_sub_one, div_mul_cancel₀ _ (hζ.sub_one_ne_zero hpri.out.one_lt)]
 
 /- y is associated to (x+yη₁)/(ζ-1) - (x+yη₂)/(ζ-1) for η₁ ≠ η₂. -/
 lemma div_zeta_sub_one_sub (η₁ η₂) (hη : η₁ ≠ η₂) :
@@ -116,18 +118,10 @@ lemma div_zeta_sub_one_Bijective :
   rw [Fintype.bijective_iff_injective_and_card]
   use div_zeta_sub_one_Injective hp hζ e hy
   simp only [PNat.pos, mem_nthRootsFinset, Fintype.card_coe]
-  rw [hζ.unit'_coe.card_nthRootsFinset, ← Submodule.cardQuot_apply, ← Ideal.absNorm_apply,
-    Ideal.absNorm_span_singleton, norm_Int_zeta_sub_one hζ hp]
+  rw [hζ.unit'_coe.card_nthRootsFinset, ← Nat.card_eq_fintype_card, ← Submodule.cardQuot_apply,
+    ← Ideal.absNorm_apply, Ideal.absNorm_span_singleton, norm_Int_zeta_sub_one hζ hp]
   rfl
 
-/- if the image of one of the elements is zero then the corresponding x+yη is divisible by π^2-/
-lemma div_zeta_sub_one_eq_zero_iff (η) :
-    Ideal.Quotient.mk 𝔭 (div_zeta_sub_one hp hζ e η) = 0 ↔ π ^ 2 ∣ x + y * η := by
-  letI := IsCyclotomicExtension.numberField {p} ℚ K
-  rw [Ideal.Quotient.eq_zero_iff_dvd, pow_two,
-    ← div_zeta_sub_one_mul_zeta_sub_one hp hζ e,
-      mul_dvd_mul_iff_right (hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt)]
-
 /- the gcd of x y called 𝔪 is coprime to 𝔭-/
 lemma gcd_zeta_sub_one_eq_one : gcd 𝔪 𝔭 = 1 := by
   have : Fact (Nat.Prime p) := hpri

FltRegular/CaseII/Statement.lean

@@ -10,11 +10,6 @@ variable {ζ : K} (hζ : IsPrimitiveRoot ζ p)
 
 namespace FltRegular
 
-/-- Statement of case II. -/
-def CaseII.Statement : Prop :=
-  ∀ ⦃a b c : ℤ⦄ ⦃p : ℕ⦄ [hp : Fact p.Prime] (_ : @IsRegularPrime p hp) (_ : p ≠ 2)
-    (_ : a * b * c ≠ 0) (_ : ↑p ∣ a * b * c), a ^ p + b ^ p ≠ c ^ p
-
 lemma not_exists_solution (hm : 1 ≤ m) :
   ¬∃ (x' y' z' : 𝓞 K) (ε₃ : (𝓞 K)ˣ),
     ¬((hζ.unit' : 𝓞 K) - 1 ∣ y') ∧ ¬((hζ.unit' : 𝓞 K) - 1 ∣ z') ∧

FltRegular/FLT5.lean

@@ -1,10 +1,10 @@
-import Mathlib
-import FltRegular
+import FltRegular.FltRegular
+import Mathlib.NumberTheory.Cyclotomic.PID
 
 open Nat NumberField IsCyclotomicExtension
 
 theorem fermatLastTheoremFive : FermatLastTheoremFor 5 := by
-  have : Fact (Nat.Prime 5) := ⟨by norm_num⟩
+  have : Fact (Nat.Prime 5) := ⟨Nat.prime_five⟩
 
   refine flt_regular ?_ (by omega)
   rw [IsRegularPrime, IsRegularNumber]