diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
index 5c87be9ceb0bc..df614fe6a7795 100644
--- a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
+++ b/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
@@ -92,7 +92,7 @@ that the `U i`'s are open subspaces of the glued space.
 -/
 -- Porting note (https://github.com/leanprover-community/mathlib4/issues/5171): this linter isn't ported yet.
 -- @[nolint has_nonempty_instance]
-structure GlueData extends GlueData (PresheafedSpace.{u, v, v} C) where
+structure GlueData extends CategoryTheory.GlueData (PresheafedSpace.{u, v, v} C) where
   f_open : ∀ i j, IsOpenImmersion (f i j)
 
 attribute [instance] GlueData.f_open
diff --git a/Mathlib/Topology/Gluing.lean b/Mathlib/Topology/Gluing.lean
index c5385f98801ee..6c4f75721330d 100644
--- a/Mathlib/Topology/Gluing.lean
+++ b/Mathlib/Topology/Gluing.lean
@@ -83,7 +83,7 @@ Most of the times it would be easier to use the constructor `TopCat.GlueData.mk'
 conditions are stated in a less categorical way.
 -/
 -- Porting note (https://github.com/leanprover-community/mathlib4/issues/5171): removed @[nolint has_nonempty_instance]
-structure GlueData extends GlueData TopCat where
+structure GlueData extends CategoryTheory.GlueData TopCat where
   f_open : ∀ i j, IsOpenEmbedding (f i j)
   f_mono i j := (TopCat.mono_iff_injective _).mpr (f_open i j).isEmbedding.injective
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 57b517f646e3f..c079482804514 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "220f518842372e0ee5747482f9d13cf3fa499e96",
+   "rev": "4a0cc9424af7acd48ce2e156e1257b718ccb79cf",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",