bump

FltRegular/FLT5.lean

@@ -5,31 +5,9 @@ open Nat NumberField Polynomial IsPrimitiveRoot IsCyclotomicExtension Real Compl
 open scoped nonZeroDivisors
 
 theorem fermatLastTheoremFive : FermatLastTheoremFor 5 := by
-  classical
-  have five_pos : 0 < 5 := by norm_num
-  let p := (⟨5, five_pos⟩ : ℕ+)
-  have hφ : φ 5 = 4 := rfl
   have : Fact (Nat.Prime 5) := ⟨by norm_num⟩
-  have hodd : 5 ≠ 2 := by omega
-  have hp : Fact (Nat.Prime (↑p : ℕ)) := this
-  let K := CyclotomicField p ℚ
 
-  refine flt_regular ?_ hodd
+  refine flt_regular ?_ (by omega)
   rw [IsRegularPrime, IsRegularNumber]
   convert coprime_one_right _
-  refine classNumber_eq_one_iff.2 (RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt ?_)
-  suffices : discr K = 125
-  rw [IsCyclotomicExtension.finrank (n := 5) K (cyclotomic.irreducible_rat five_pos), this]
-  · suffices InfinitePlace.NrComplexPlaces K = 2 by
-      · rw [this, show ((5 : ℕ+) : ℕ) = 5 by rfl, hφ, show ((4! : ℕ) : ℝ) = 24 by rfl,
-          abs_of_pos (by norm_num)]
-        norm_num
-        suffices (2 * (3 ^ 2 / 16) * (32 / 3)) ^ 2 < (2 * ((π : ℝ) ^ 2 / 16) * (32 / 3)) ^ 2 by
-          · refine lt_trans ?_ this
-            norm_num
-        gcongr
-        exact pi_gt_three
-    rw [Rat.nrComplexPlaces_eq_totient_div_two (n := 5)]
-    rfl
-  · convert IsCyclotomicExtension.Rat.absdiscr_prime p K
-    assumption
+  exact classNumber_eq_one_iff.2 (Rat.five_pid (CyclotomicField _ ℚ))

lake-manifest.json

@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "86b7828a1e4debe4984e5051220a6026c8d4c6a1",
+   "rev": "1095e9af4d1f75960ab5485a6c5b3a851f48b5f4",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,