merge lean-pr-testing-6125

leanprover-community · Nov 23, 2024 · bbe817e · bbe817e
2 parents d340f5a + d2f2a6b
commit bbe817e
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git 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
@@ -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
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "220f518842372e0ee5747482f9d13cf3fa499e96",
+   "rev": "4a0cc9424af7acd48ce2e156e1257b718ccb79cf",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",