Note that we spell it as Metrizable in TopologicalSpace.MetrizableSpace

My guess is that this linter doesn't catch anything, because normally you use data in [MetricSpace X], otherwise this would be an unused argument. The linter should catch theorems that only use the projection to UniformSpace. Another question is how to catch uses of [UniformSpace X] that only use projection to TopologicalSpace X (should be replaced by [TopologicalSpace X] [CompletelyRegularSpace X] once we redefine the latter to avoid dependency on Real) or [UniformSpace X] [Filter.IsCountablyGenerated (uniformity X)] that only use the projection to TopologicalSpace X everywhere else (should be replaced by [PseudoMetrizableSpace X].