diff --git a/FLT/AutomorphicRepresentation/Example.lean b/FLT/AutomorphicRepresentation/Example.lean
index 8332b245..db3cd451 100644
--- a/FLT/AutomorphicRepresentation/Example.lean
+++ b/FLT/AutomorphicRepresentation/Example.lean
@@ -895,7 +895,7 @@ lemma exists_near (a : ℍ) : ∃ q : 𝓞, dist a (toQuaternion q) < 1 := by
 
   use fromQuaternion ⟨x,y,z,w⟩
   rw [aux]
-  rw [NormedRing.dist_eq, ← sq_lt_one_iff (_root_.norm_nonneg _), sq,
+  rw [NormedRing.dist_eq, ← sq_lt_one_iff₀ (_root_.norm_nonneg _), sq,
     ← Quaternion.normSq_eq_norm_mul_self, normSq_def']
 
   simp only [sub_re, sub_imI, sub_imJ, sub_imK]
diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean
index 6757b207..a26924a8 100644
--- a/FLT/MathlibExperiments/FrobeniusRiou.lean
+++ b/FLT/MathlibExperiments/FrobeniusRiou.lean
@@ -456,8 +456,7 @@ namespace Ideal
 variable {R : Type*} [CommRing R] {I : Ideal R}
 
 protected noncomputable
-def Quotient.out (x : R ⧸ I) :=
-  Quotient.out' x
+def Quotient.out (x : R ⧸ I) := x.out
 
 theorem Quotient.out_eq (x : R ⧸ I) : Ideal.Quotient.mk I (Ideal.Quotient.out x) = x := by
   simp only [Ideal.Quotient.out, Ideal.Quotient.mk, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
diff --git a/lake-manifest.json b/lake-manifest.json
index 03ca2a28..157887f8 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "01f4969b6e861db6a99261ea5eadd5a9bb63011b",
+   "rev": "0dc51ac7947ff6aa2c16bcffb64c46c7149d1276",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "86d0d0584f5cd165353e2f8a30c455cd0e168ac2",
+   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "955e8f97a6372ceeeb97f4acc87f71ae1fea7d85",
+   "rev": "f28fa7213f2fe9065a3a12f88d256ea7dd006d7e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -125,7 +125,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "bdc2fc30b1e834b294759a5d391d83020a90058e",
+   "rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -135,7 +135,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7b6a56e8e4fcf54d3834b225b9814a7c9e4d4bda",
+   "rev": "059eb7e86f1f5c16780657d14de1a560a9d6784c",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",