diff --git a/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean b/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean
index b86887c2..6ebbb627 100644
--- a/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean
+++ b/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean
@@ -151,7 +151,7 @@ theorem zeta_sub_one_dvb_p [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {η : R} (hη :
     rw [hP] at ph
     contradiction
   have h := RingOfIntegers.dvd_norm ℚ (η - 1 : R)
-  have h2 := IsPrimitiveRoot.sub_one_norm_prime this (cyclotomic.irreducible_rat p.2) h0
+  have h2 := IsPrimitiveRoot.norm_sub_one_of_prime_ne_two' this (cyclotomic.irreducible_rat p.2) h0
   convert h
   ext
   rw [show (η : CyclotomicField p ℚ) - 1 = (η - 1 : _) by simp] at h2
diff --git a/lake-manifest.json b/lake-manifest.json
index 7e01501b..371bd6c3 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "56d2e4ee226603eb6b90b05f6b944bde42672cd5",
+   "rev": "14f258593e8c261d8834f13c6edc7b970c253ee8",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "2225b0e4a3528da20499e2304b521e0c4c2a4563",
+   "rev": "f617e0673845925e612b62141ff54c4b7980dc63",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "c46d22bbe4f8363c0829ce0eb48a95012cdc0d79",
+   "rev": "35e38eb320982cfd2fcc864e0e0467ca223c8cdb",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "89b4b590b4938e14211b6296f8ecf0c1940cc999",
+   "rev": "3b462daa45f893202693b13e3965a7b4e1e7b631",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,