∀ (X : Type u_2) [inst : TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X]
  [TopologicalSpace.SeparableSpace X] [inst_3 : MeasurableSpace X] [inst_4 : BorelSpace X],
  TopologicalSpace.MetrizableSpace (MeasureTheory.ProbabilityMeasure X)