∀ {α : Type u_3} [h : TopologicalSpace α],
  (∃ b, b.Countable ∧ h = TopologicalSpace.generateFrom b) →
    (∃ m, PseudoMetricSpace.toUniformSpace.toTopologicalSpace = h ∧ CompleteSpace α) → PolishSpace α