diff --git a/FltRegular/NumberTheory/GaloisPrime.lean b/FltRegular/NumberTheory/GaloisPrime.lean
index 4421ece9..b87fba9f 100644
--- a/FltRegular/NumberTheory/GaloisPrime.lean
+++ b/FltRegular/NumberTheory/GaloisPrime.lean
@@ -5,7 +5,7 @@ import Mathlib.Order.CompletePartialOrder
 import Mathlib.RingTheory.DedekindDomain.Dvr
 import Mathlib.Algebra.Order.Star.Basic
 import Mathlib.RingTheory.SimpleRing.Basic
-import Mathlib.NumberTheory.RamificationInertia
+import Mathlib.NumberTheory.RamificationInertia.Basic
 import Mathlib.Algebra.Lie.OfAssociative
 
 /-!
diff --git a/lake-manifest.json b/lake-manifest.json
index 03a8117c..b22788c6 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "3805203e1e80948a62f00d3c3923bd8b31f16533",
+   "rev": "6d297a4172e6c37d3bf82e68924c45d72621ac5d",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -135,7 +135,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5777dc79236057c79665f4eca0a2b08cbbf40ebb",
+   "rev": "7b6a56e8e4fcf54d3834b225b9814a7c9e4d4bda",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",