From 3be98461001b50db55585ecd97f8113e87e9d2c3 Mon Sep 17 00:00:00 2001 From: Justin Palumbo Date: Fri, 14 Aug 2026 06:51:59 -0400 Subject: [PATCH] fix(Topology/Metrizable): make instances anonymous to avoid name collisions --- Mathlib/Topology/Metrizable/CompletelyMetrizable.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Topology/Metrizable/CompletelyMetrizable.lean b/Mathlib/Topology/Metrizable/CompletelyMetrizable.lean index ed439f58a69f46..a09f9b3b228345 100644 --- a/Mathlib/Topology/Metrizable/CompletelyMetrizable.lean +++ b/Mathlib/Topology/Metrizable/CompletelyMetrizable.lean @@ -100,7 +100,7 @@ namespace IsCompletelyPseudoMetrizableSpace /-- Note: the priority is set to 90 to ensure that this instance is only applied after `PseudoEMetricSpace.pseudoMetrizableSpace`. This prevents unnecessary attempts to infer completeness. -/ -instance (priority := 90) PseudoMetrizableSpace [TopologicalSpace X] +instance (priority := 90) [TopologicalSpace X] [IsCompletelyPseudoMetrizableSpace X] : PseudoMetrizableSpace X := by let := upgradeIsCompletelyPseudoMetrizable X infer_instance @@ -211,7 +211,7 @@ namespace IsCompletelyMetrizableSpace /-- Note: the priority is set to 90 to ensure that this instance is only applied after `EMetricSpace.metrizableSpace`. This prevents unnecessary attempts to infer completeness. -/ -instance (priority := 90) MetrizableSpace [TopologicalSpace X] [IsCompletelyMetrizableSpace X] : +instance (priority := 90) [TopologicalSpace X] [IsCompletelyMetrizableSpace X] : MetrizableSpace X := by let := upgradeIsCompletelyMetrizable X infer_instance