diff --git a/FLT/ForMathlib/MiscLemmas.lean b/FLT/ForMathlib/MiscLemmas.lean
index a0d3785f..20a22eb2 100644
--- a/FLT/ForMathlib/MiscLemmas.lean
+++ b/FLT/ForMathlib/MiscLemmas.lean
@@ -76,12 +76,12 @@ variable {B : Type*} [SMul S B]
 -- note: use convert not exact to ensure typeclass inference doesn't try to find topology on B
 theorem induced_continuous_smul [τA : TopologicalSpace A] [ContinuousSMul R A] (g : B →ₑ[f] A)
     (hf : Continuous f) : @ContinuousSMul S B _ _ (TopologicalSpace.induced g τA) := by
-  convert Inducing.continuousSMul (inducing_induced g) hf (fun {c} {x} ↦ map_smulₛₗ g c x)
+  convert IsInducing.continuousSMul (IsInducing.induced g) hf (fun {c} {x} ↦ map_smulₛₗ g c x)
 
 theorem induced_continuous_add [AddCommMonoid A] [τA : TopologicalSpace A] [ContinuousAdd A]
     [AddCommMonoid B] (h : B →+ A) :
     @ContinuousAdd B (TopologicalSpace.induced h τA) _ := by
-  convert Inducing.continuousAdd h (inducing_induced h)
+  convert IsInducing.continuousAdd h (IsInducing.induced h)
 
 end induced
 
diff --git a/FLT/GlobalLanglandsConjectures/GLzero.lean b/FLT/GlobalLanglandsConjectures/GLzero.lean
index 8551ccc3..305acf2f 100644
--- a/FLT/GlobalLanglandsConjectures/GLzero.lean
+++ b/FLT/GlobalLanglandsConjectures/GLzero.lean
@@ -5,7 +5,6 @@ Authors: Kevin Buzzard, Jonas Bayer
 -/
 import Mathlib.RingTheory.DedekindDomain.Ideal
 import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
-import Mathlib.RingTheory.Ideal.QuotientOperations
 import Mathlib.FieldTheory.Cardinality
 import FLT.GlobalLanglandsConjectures.GLnDefs
 /-
diff --git a/FLT/MathlibExperiments/Frobenius.lean b/FLT/MathlibExperiments/Frobenius.lean
index 1635bb7e..eafc70a9 100644
--- a/FLT/MathlibExperiments/Frobenius.lean
+++ b/FLT/MathlibExperiments/Frobenius.lean
@@ -5,7 +5,6 @@ Authors: Jou Glasheen
 -/
 import Mathlib.RingTheory.DedekindDomain.Ideal
 import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
-import Mathlib.RingTheory.Ideal.QuotientOperations
 import Mathlib.FieldTheory.Cardinality
 
 
@@ -330,7 +329,7 @@ variable {A K L B Q}
 -- this lemma written by Amelia
 lemma smul_ideal_eq_map (g : L ≃ₐ[K] L) (I : Ideal' A K L B) :
     g • I = Ideal.map (galRestrict A K L B g) I :=
-  Ideal.comap_symm I (galRestrict A K L B g).toRingEquiv
+  Ideal.comap_symm (galRestrict A K L B g).toRingEquiv
 
 lemma mem_smul_ideal_iff (g : L ≃ₐ[K] L) (I : Ideal' A K L B) (x : B) :
   x ∈ g • I ↔ (galRestrict A K L B g).symm x ∈ I := Iff.rfl
diff --git a/FLT/MathlibExperiments/Frobenius2.lean b/FLT/MathlibExperiments/Frobenius2.lean
index 6f0d7d1d..a47350f6 100644
--- a/FLT/MathlibExperiments/Frobenius2.lean
+++ b/FLT/MathlibExperiments/Frobenius2.lean
@@ -6,7 +6,6 @@ Authors: Jou Glasheen, Amelia Livingston, Jujian Zhang, Kevin Buzzard
 import Mathlib.FieldTheory.Cardinality
 import Mathlib.RingTheory.DedekindDomain.Ideal
 import Mathlib.RingTheory.Ideal.Pointwise
-import Mathlib.RingTheory.Ideal.QuotientOperations
 import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 
 /-
diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean
index 601dd607..c20e2415 100644
--- a/FLT/MathlibExperiments/FrobeniusRiou.lean
+++ b/FLT/MathlibExperiments/FrobeniusRiou.lean
@@ -6,7 +6,6 @@ Authors: Jou Glasheen, Amelia Livingston, Jujian Zhang, Kevin Buzzard
 import Mathlib.FieldTheory.Cardinality
 import Mathlib.RingTheory.DedekindDomain.Ideal
 import Mathlib.RingTheory.Ideal.Pointwise
-import Mathlib.RingTheory.Ideal.QuotientOperations
 import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 import Mathlib.RingTheory.Ideal.Pointwise
 import Mathlib.RingTheory.Ideal.Over
diff --git a/FLT/MathlibExperiments/IsFrobenius.lean b/FLT/MathlibExperiments/IsFrobenius.lean
index bbed6c2b..9a254aa2 100644
--- a/FLT/MathlibExperiments/IsFrobenius.lean
+++ b/FLT/MathlibExperiments/IsFrobenius.lean
@@ -50,7 +50,7 @@ its image is itself-/
 def IsInvariant (f : (B ≃ₐ[A] B)) (Q : Ideal B) : Prop := (Q = Q.comap (f.symm : B →+* B))
 
 lemma comap_symm (f : (B ≃ₐ[A] B)) (Q : Ideal B)  : (Q.comap (f.symm : B →+* B) = Q.map f) :=
-  Ideal.comap_symm _ _
+  Ideal.comap_symm _
 
 variable (B)
 
diff --git a/lake-manifest.json b/lake-manifest.json
index db2c2551..66a7d454 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "85f6511d93f9e6a8188ec9985c82f08f65c26cae",
+   "rev": "31a10a332858d6981dbcf55d54ee51680dd75f18",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9ac12945862fa39eab7795c2f79bb9aa0c8e332c",
+   "rev": "5f934891e11d70a1b86e302fdf9cecfc21e8de46",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0ea83a676d288220ba227808568cbb80fe43ace0",
+   "rev": "984d7ee170b75d6b03c0903e0b750ee2c6d1e3fb",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -71,11 +71,21 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "d212dd74414e997653cd3484921f4159c955ccca",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9fc60c1ad982f142d6d0671bef8f4cda3b1590cd",
+   "rev": "80b452d9e5fa9a10381d159790ace5e42ab1bee4",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -105,7 +115,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6d2e06515f1ed1f74208d5a1da3a9cc26c60a7a0",
+   "rev": "107e98b3e7603628d9bfd817b4704488d8a25e96",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -115,7 +125,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "85e1e7143dd4cfa2b551826c27867bada60858e8",
+   "rev": "bdc2fc30b1e834b294759a5d391d83020a90058e",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -125,7 +135,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d36b7fd4c730cae8a3a8edfe98beb34ef0fc6e0a",
+   "rev": "c2156beadb1a4d049ff3b19fe396c5403025aac5",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lean-toolchain b/lean-toolchain
index eff86fd6..4f86f953 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.13.0-rc3
+leanprover/lean4:v4.13.0