chore: implement porting notes about Polish spaces (#6991)

Make the following changes which were intentionally left till after the port:

- Move several instances of `PolishSpace` from MeasureTheory.Constructions.Polish to Topology.MetricSpace.Polish

- Remove instance of `PolishSpace` for `nat -> nat`, since lean4 can find this automatically

- Change `PolishSpace` to extend `SecondCountableTopology`, since lean4 now allows loops in TC inference.

Mathlib/MeasureTheory/Constructions/Polish.lean

@@ -544,7 +544,6 @@ instance QuotientGroup.borelSpace {G : Type*} [TopologicalSpace G] [PolishSpace
     [IsClosed (N : Set G)] : BorelSpace (G ⧸ N) :=
   -- porting note: 1st and 3rd `haveI`s were not needed in Lean 3
   haveI := Subgroup.t3_quotient_of_isClosed N
-  haveI := @PolishSpace.secondCountableTopology G
   haveI := QuotientGroup.secondCountableTopology (Γ := N)
   Quotient.borelSpace
 #align quotient_group.borel_space QuotientGroup.borelSpace
@@ -845,28 +844,8 @@ end MeasureTheory
 
 /-! ### The Borel Isomorphism Theorem -/
 
--- Porting note: Move to topology/metric_space/polish when porting.
-instance (priority := 50) polish_of_countable [h : Countable α] [DiscreteTopology α] :
-    PolishSpace α := by
-  obtain ⟨f, hf⟩ := h.exists_injective_nat
-  have : ClosedEmbedding f := by
-    apply closedEmbedding_of_continuous_injective_closed continuous_of_discreteTopology hf
-    exact fun t _ => isClosed_discrete _
-  exact this.polishSpace
-#align polish_of_countable polish_of_countable
-
 namespace PolishSpace
 
-/- Porting note: This is to avoid a loop in TC inference. When ported to Lean 4, this will not
-be necessary, and `secondCountable_of_polish` should probably
-just be added as an instance soon after the definition of `PolishSpace`.-/
-private theorem secondCountable_of_polish [h : PolishSpace α] : SecondCountableTopology α :=
-  h.secondCountableTopology
-
-attribute [-instance] polishSpace_of_complete_second_countable
-
-attribute [local instance] secondCountable_of_polish
-
 variable {β : Type*} [TopologicalSpace β] [PolishSpace α] [PolishSpace β]
 
 variable [MeasurableSpace α] [MeasurableSpace β] [BorelSpace α] [BorelSpace β]
@@ -907,11 +886,6 @@ end PolishSpace
 
 namespace MeasureTheory
 
--- Porting note: todo after the port: move to topology/metric_space/polish
-instance instPolishSpaceUniv [PolishSpace α] : PolishSpace (univ : Set α) :=
-  isClosed_univ.polishSpace
-#align measure_theory.set.univ.polish_space MeasureTheory.instPolishSpaceUniv
-
 variable (α)
 variable [MeasurableSpace α] [PolishSpace α] [BorelSpace α]
 

Mathlib/Topology/MetricSpace/Polish.lean

@@ -62,8 +62,8 @@ other way around as this is the most common use case.
 
 To endow a Polish space with a complete metric space structure, do `letI := upgradePolishSpace α`.
 -/
-class PolishSpace (α : Type*) [h : TopologicalSpace α] : Prop where
-  secondCountableTopology : SecondCountableTopology α
+class PolishSpace (α : Type*) [h : TopologicalSpace α]
+    extends SecondCountableTopology α : Prop where
   complete : ∃ m : MetricSpace α, m.toUniformSpace.toTopologicalSpace = h ∧
     @CompleteSpace α m.toUniformSpace
 #align polish_space PolishSpace
@@ -76,8 +76,7 @@ class UpgradedPolishSpace (α : Type*) extends MetricSpace α, SecondCountableTo
 #align upgraded_polish_space UpgradedPolishSpace
 
 instance (priority := 100) polishSpace_of_complete_second_countable [m : MetricSpace α]
-    [h : SecondCountableTopology α] [h' : CompleteSpace α] : PolishSpace α where
-  secondCountableTopology := h
+    [SecondCountableTopology α] [h' : CompleteSpace α] : PolishSpace α where
   complete := ⟨m, rfl, h'⟩
 #align polish_space_of_complete_second_countable polishSpace_of_complete_second_countable
 
@@ -97,7 +96,7 @@ theorem complete_polishSpaceMetric (α : Type*) [ht : TopologicalSpace α] [h :
 def upgradePolishSpace (α : Type*) [TopologicalSpace α] [PolishSpace α] :
     UpgradedPolishSpace α :=
   letI := polishSpaceMetric α
-  { complete_polishSpaceMetric α, PolishSpace.secondCountableTopology with }
+  { complete_polishSpaceMetric α with }
 #align upgrade_polish_space upgradePolishSpace
 
 namespace PolishSpace
@@ -117,11 +116,6 @@ instance pi_countable {ι : Type*} [Countable ι] {E : ι → Type*} [∀ i, Top
   infer_instance
 #align polish_space.pi_countable PolishSpace.pi_countable
 
-/-- Without this instance, Lean 3 was unable to find `PolishSpace (ℕ → ℕ)` by typeclass inference.
-Porting note: TODO: test with Lean 4. -/
-instance nat_fun [TopologicalSpace α] [PolishSpace α] : PolishSpace (ℕ → α) := inferInstance
-#align polish_space.nat_fun PolishSpace.nat_fun
-
 /-- A countable disjoint union of Polish spaces is Polish. -/
 instance sigma {ι : Type*} [Countable ι] {E : ι → Type*} [∀ n, TopologicalSpace (E n)]
     [∀ n, PolishSpace (E n)] : PolishSpace (Σn, E n) :=
@@ -159,6 +153,16 @@ theorem _root_.ClosedEmbedding.polishSpace [TopologicalSpace α] [TopologicalSpa
   infer_instance
 #align closed_embedding.polish_space ClosedEmbedding.polishSpace
 
+/-- Any countable discrete space is Polish. -/
+instance (priority := 50) polish_of_countable [TopologicalSpace α]
+    [h : Countable α] [DiscreteTopology α] : PolishSpace α := by
+  obtain ⟨f, hf⟩ := h.exists_injective_nat
+  have : ClosedEmbedding f := by
+    apply closedEmbedding_of_continuous_injective_closed continuous_of_discreteTopology hf
+    exact fun t _ => isClosed_discrete _
+  exact this.polishSpace
+#align polish_of_countable PolishSpace.polish_of_countable
+
 /-- Pulling back a Polish topology under an equiv gives again a Polish topology. -/
 theorem _root_.Equiv.polishSpace_induced [t : TopologicalSpace β] [PolishSpace β] (f : α ≃ β) :
     @PolishSpace α (t.induced f) :=
@@ -167,11 +171,16 @@ theorem _root_.Equiv.polishSpace_induced [t : TopologicalSpace β] [PolishSpace
 #align equiv.polish_space_induced Equiv.polishSpace_induced
 
 /-- A closed subset of a Polish space is also Polish. -/
-theorem _root_.IsClosed.polishSpace {α : Type*} [TopologicalSpace α] [PolishSpace α] {s : Set α}
+theorem _root_.IsClosed.polishSpace [TopologicalSpace α] [PolishSpace α] {s : Set α}
     (hs : IsClosed s) : PolishSpace s :=
   (IsClosed.closedEmbedding_subtype_val hs).polishSpace
 #align is_closed.polish_space IsClosed.polishSpace
 
+instance instPolishSpaceUniv [TopologicalSpace α] [PolishSpace α] :
+    PolishSpace (univ : Set α) :=
+  isClosed_univ.polishSpace
+#align measure_theory.set.univ.polish_space PolishSpace.instPolishSpaceUniv
+
 /-- A sequence of type synonyms of a given type `α`, useful in the proof of
 `exists_polishSpace_forall_le` to endow each copy with a different topology. -/
 @[nolint unusedArguments]