diff --git a/FltRegular/NumberTheory/Finrank.lean b/FltRegular/NumberTheory/Finrank.lean
index 0b1990ed..c3b139ff 100644
--- a/FltRegular/NumberTheory/Finrank.lean
+++ b/FltRegular/NumberTheory/Finrank.lean
@@ -48,7 +48,7 @@ lemma FiniteDimensional.finrank_add_finrank_quotient_le (N : Submodule R M) :
       ← Finsupp.range_linearCombination]
     rintro _ ⟨h, l, rfl⟩
     rw [SetLike.mem_coe, ← Submodule.Quotient.mk_eq_zero, ← Submodule.mkQ_apply,
-      Finsupp.apply_linearCombination, ← Function.comp.assoc,
+      Finsupp.apply_linearCombination, ← Function.comp_assoc,
       show N.mkQ ∘ f = id from funext hf] at h
     rw [linearIndependent_iff.mp ht' l h, map_zero]
     exact zero_mem _
diff --git a/FltRegular/NumberTheory/IdealNorm.lean b/FltRegular/NumberTheory/IdealNorm.lean
index 82fe8ef0..3e8071f0 100644
--- a/FltRegular/NumberTheory/IdealNorm.lean
+++ b/FltRegular/NumberTheory/IdealNorm.lean
@@ -3,7 +3,7 @@ import Mathlib.RingTheory.DedekindDomain.Dvr
 import Mathlib.RingTheory.Localization.NormTrace
 import Mathlib.RingTheory.Localization.LocalizationLocalization
 import Mathlib.RingTheory.Nakayama
-import Mathlib.RingTheory.LocalProperties
+import Mathlib.RingTheory.LocalProperties.IntegrallyClosed
 import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 import Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
 import Mathlib.NumberTheory.RamificationInertia
diff --git a/lake-manifest.json b/lake-manifest.json
index 3e381c3c..3c98b1a2 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "46fed98b5cac2b1ea64e363b420c382ed1af0d85",
+   "rev": "c57ab80c8dd20b345b29c81c446c78a6b3677d20",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2c39748d927749624f480b641f1d2d77b8632b92",
+   "rev": "a895713f7701e295a015b1087f3113fd3d615272",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "70883b92b66c911b8666c98ae4cb2425e591a958",
+   "rev": "2ba60fa2c384a94735454db11a2d523612eaabff",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e4699dfe66fd5a01a8a0f85b8cde6c555f25c3a1",
+   "rev": "d942826fbe921454e3ae9942d00b06526e310812",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,