refactor: redefine metrizable and Polish spaces

New definitions:

class PseudoMetrizableSpace (X : Type*) [t : TopologicalSpace X] : Prop where
  exists_countably_generated_uniformity : ∃ U : UniformSpace X,
    IsCountablyGenerated (𝓤[U]) ∧ U.toTopologicalSpace = t

class MetrizableSpace (X : Type*) [TopologicalSpace X]
    extends T0Space X, PseudoMetrizableSpace X : Prop where

class PolishSpace (X : Type*) [t : TopologicalSpace X] extends T0Space X, SeparableSpace X : Prop where
  exists_complete_uniformity : ∃ U : UniformSpace X, IsCountablyGenerated (𝓤[U]) ∧
    @CompleteSpace X U ∧ U.toTopologicalSpace = t

Start by locating the existing definitions of metrizable and Polish spaces and the code that uses them. Compare those definitions with the proposed classes in the issue, then verify that the updated definitions and their dependents compile without breaking existing topology results.