refactor: split NormalSpace into NormalSpace and T4Space (#7072)

urkud · urkud · commit bf815bd5bd5a · 2023-09-12T17:41:29.000Z
* Rename `NormalSpace` to `T4Space`. * Add `NormalSpace`, a version without the `T1Space` assumption. * Adjust some theorems. * Supersedes thus closes #6892. * Add some instance cycles, see #2030
diff --git a/Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean b/Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean
@@ -54,11 +54,9 @@ theorem continuous_im : Continuous im :=
 instance : TopologicalSpace.SecondCountableTopology ℍ :=
   TopologicalSpace.Subtype.secondCountableTopology _
 
-instance : T3Space ℍ :=
-  Subtype.t3Space
+instance : T3Space ℍ := Subtype.t3Space
 
-instance : NormalSpace ℍ :=
-  normalSpaceOfT3SecondCountable ℍ
+instance : T4Space ℍ := inferInstance
 
 instance : ContractibleSpace ℍ :=
   (convex_halfspace_im_gt 0).contractibleSpace ⟨I, one_pos.trans_eq I_im.symm⟩
diff --git a/Mathlib/Geometry/Manifold/Metrizable.lean b/Mathlib/Geometry/Manifold/Metrizable.lean
@@ -26,7 +26,6 @@ theorem ManifoldWithCorners.metrizableSpace {E : Type*} [NormedAddCommGroup E] [
     (M : Type*) [TopologicalSpace M] [ChartedSpace H M] [SigmaCompactSpace M] [T2Space M] :
     MetrizableSpace M := by
   haveI := I.locallyCompactSpace; haveI := ChartedSpace.locallyCompactSpace H M
-  haveI : NormalSpace M := normal_of_paracompact_t2
   haveI := I.secondCountableTopology
   haveI := ChartedSpace.secondCountable_of_sigma_compact H M
   exact metrizableSpace_of_t3_second_countable M
diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean
@@ -343,7 +343,6 @@ theorem exists_isSubordinate [T2Space M] [SigmaCompactSpace M] (hs : IsClosed s)
   -- First we deduce some missing instances
   haveI : LocallyCompactSpace H := I.locallyCompactSpace
   haveI : LocallyCompactSpace M := ChartedSpace.locallyCompactSpace H M
-  haveI : NormalSpace M := normal_of_paracompact_t2
   -- Next we choose a covering by supports of smooth bump functions
   have hB := fun x hx => SmoothBumpFunction.nhds_basis_support I (hU x hx)
   rcases refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set hs hB with
@@ -523,7 +522,6 @@ theorem exists_isSubordinate {s : Set M} (hs : IsClosed s) (U : ι → Set M) (h
     (hU : s ⊆ ⋃ i, U i) : ∃ f : SmoothPartitionOfUnity ι I M s, f.IsSubordinate U := by
   haveI : LocallyCompactSpace H := I.locallyCompactSpace
   haveI : LocallyCompactSpace M := ChartedSpace.locallyCompactSpace H M
-  haveI : NormalSpace M := normal_of_paracompact_t2
   -- porting note(https://github.com/leanprover/std4/issues/116):
   -- split `rcases` into `have` + `rcases`
   have := BumpCovering.exists_isSubordinate_of_prop (Smooth I 𝓘(ℝ)) ?_ hs U ho hU
diff --git a/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean b/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean
@@ -63,7 +63,7 @@ open scoped ENNReal NNReal Topology BoundedContinuousFunction
 
 open MeasureTheory TopologicalSpace ContinuousMap Set
 
-variable {α : Type*} [MeasurableSpace α] [TopologicalSpace α] [NormalSpace α] [BorelSpace α]
+variable {α : Type*} [MeasurableSpace α] [TopologicalSpace α] [T4Space α] [BorelSpace α]
 
 variable {E : Type*} [NormedAddCommGroup E] {μ : Measure α} {p : ℝ≥0∞}
 
diff --git a/Mathlib/Topology/Category/CompHaus/Basic.lean b/Mathlib/Topology/Category/CompHaus/Basic.lean
@@ -340,8 +340,6 @@ theorem epi_iff_surjective {X Y : CompHaus.{u}} (f : X ⟶ Y) : Epi f ↔ Functi
       rw [Set.disjoint_singleton_right]
       rintro ⟨y', hy'⟩
       exact hy y' hy'
-    --haveI : NormalSpace Y.toTop := normalOfCompactT2
-    haveI : NormalSpace ((forget CompHaus).obj Y) := normalOfCompactT2
     obtain ⟨φ, hφ0, hφ1, hφ01⟩ := exists_continuous_zero_one_of_closed hC hD hCD
     haveI : CompactSpace (ULift.{u} <| Set.Icc (0 : ℝ) 1) := Homeomorph.ulift.symm.compactSpace
     haveI : T2Space (ULift.{u} <| Set.Icc (0 : ℝ) 1) := Homeomorph.ulift.symm.t2Space
diff --git a/Mathlib/Topology/Compactification/OnePoint.lean b/Mathlib/Topology/Compactification/OnePoint.lean
@@ -457,14 +457,14 @@ instance [T1Space X] : T1Space (OnePoint X) where
     · rw [← image_singleton, isClosed_image_coe]
       exact ⟨isClosed_singleton, isCompact_singleton⟩
 
-/-- The one point compactification of a locally compact Hausdorff space is a normal (hence,
-Hausdorff and regular) topological space. -/
-instance [LocallyCompactSpace X] [T2Space X] : NormalSpace (OnePoint X) := by
+/-- The one point compactification of a weakly locally compact Hausdorff space is a T₄
+(hence, Hausdorff and regular) topological space. -/
+instance [WeaklyLocallyCompactSpace X] [T2Space X] : T4Space (OnePoint X) := by
   have key : ∀ z : X, Disjoint (𝓝 (some z)) (𝓝 ∞) := fun z => by
     rw [nhds_infty_eq, disjoint_sup_right, nhds_coe_eq, coclosedCompact_eq_cocompact,
       disjoint_map coe_injective, ← principal_singleton, disjoint_principal_right, compl_infty]
     exact ⟨disjoint_nhds_cocompact z, range_mem_map⟩
-  suffices : T2Space (OnePoint X); exact normalOfCompactT2
+  suffices : T2Space (OnePoint X); infer_instance
   refine t2Space_iff_disjoint_nhds.2 fun x y hxy => ?_
   induction x using OnePoint.rec <;> induction y using OnePoint.rec
   · exact (hxy rfl).elim
diff --git a/Mathlib/Topology/ContinuousFunction/Ideals.lean b/Mathlib/Topology/ContinuousFunction/Ideals.lean
@@ -321,7 +321,6 @@ theorem setOfIdeal_ofSet_eq_interior (s : Set X) : setOfIdeal (idealOfSet 𝕜 s
   -- If `x ∉ closure sᶜ`, we must produce `f : C(X, 𝕜)` which is zero on `sᶜ` and `f x ≠ 0`.
   rw [← compl_compl (interior s), ← closure_compl] at hx
   simp_rw [mem_setOfIdeal, mem_idealOfSet]
-  haveI : NormalSpace X := normalOfCompactT2
   /- Apply Urysohn's lemma to get `g : C(X, ℝ)` which is zero on `sᶜ` and `g x ≠ 0`, then compose
     with the natural embedding `ℝ ↪ 𝕜` to produce the desired `f`. -/
   obtain ⟨g, hgs, hgx : Set.EqOn g 1 {x}, -⟩ :=
@@ -436,7 +435,6 @@ variable [CompactSpace X] [T2Space X] [IsROrC 𝕜]
 theorem continuousMapEval_bijective : Bijective (continuousMapEval X 𝕜) := by
   refine' ⟨fun x y hxy => _, fun φ => _⟩
   · contrapose! hxy
-    haveI := @normalOfCompactT2 X _ _ _
     rcases exists_continuous_zero_one_of_closed (isClosed_singleton : _root_.IsClosed {x})
         (isClosed_singleton : _root_.IsClosed {y}) (Set.disjoint_singleton.mpr hxy) with
       ⟨f, fx, fy, -⟩
diff --git a/Mathlib/Topology/EMetricSpace/Paracompact.lean b/Mathlib/Topology/EMetricSpace/Paracompact.lean
@@ -35,8 +35,8 @@ open ENNReal Topology Set
 namespace EMetric
 
 -- See note [lower instance priority]
-/-- A `PseudoEMetricSpace` is always a paracompact space. Formalization is based
-on [MR0236876]. -/
+/-- A `PseudoEMetricSpace` is always a paracompact space.
+Formalization is based on [MR0236876]. -/
 instance (priority := 100) instParacompactSpace [PseudoEMetricSpace α] : ParacompactSpace α := by
   /- We start with trivial observations about `1 / 2 ^ k`. Here and below we use `1 / 2 ^ k` in
     the comments and `2⁻¹ ^ k` in the code. -/
@@ -166,9 +166,8 @@ instance (priority := 100) instParacompactSpace [PseudoEMetricSpace α] : Paraco
     exact not_lt.1 fun hlt => (Hgt I.1 hlt I.2).le_bot hI.choose_spec
 #align emetric.paracompact_space EMetric.instParacompactSpace
 
--- see Note [lower instance priority]
-instance (priority := 100) instNormalSpace [EMetricSpace α] : NormalSpace α :=
-  normal_of_paracompact_t2
-#align emetric.normal_of_emetric EMetric.instNormalSpace
+-- porting note: no longer an instance because `inferInstance` can find it
+theorem t4Space [EMetricSpace α] : T4Space α := inferInstance
+#align emetric.normal_of_emetric EMetric.t4Space
 
 end EMetric
diff --git a/Mathlib/Topology/Homeomorph.lean b/Mathlib/Topology/Homeomorph.lean
@@ -360,7 +360,10 @@ protected theorem closedEmbedding (h : α ≃ₜ β) : ClosedEmbedding h :=
 
 protected theorem normalSpace [NormalSpace α] (h : α ≃ₜ β) : NormalSpace β :=
   h.symm.closedEmbedding.normalSpace
-#align homeomorph.normal_space Homeomorph.normalSpace
+
+protected theorem t4Space [T4Space α] (h : α ≃ₜ β) : T4Space β :=
+  h.symm.closedEmbedding.t4Space
+#align homeomorph.normal_space Homeomorph.t4Space
 
 theorem preimage_closure (h : α ≃ₜ β) (s : Set β) : h ⁻¹' closure s = closure (h ⁻¹' s) :=
   h.isOpenMap.preimage_closure_eq_closure_preimage h.continuous _
diff --git a/Mathlib/Topology/Instances/AddCircle.lean b/Mathlib/Topology/Instances/AddCircle.lean
@@ -525,9 +525,8 @@ instance : ProperlyDiscontinuousVAdd (AddSubgroup.opposite (zmultiples p)) ℝ :
 instance : T2Space (AddCircle p) :=
   t2Space_of_properlyDiscontinuousVAdd_of_t2Space
 
-/-- The "additive circle" `ℝ ⧸ (ℤ ∙ p)` is normal. -/
-instance [Fact (0 < p)] : NormalSpace (AddCircle p) :=
-  normalOfCompactT2
+/-- The "additive circle" `ℝ ⧸ (ℤ ∙ p)` is T₄. -/
+instance [Fact (0 < p)] : T4Space (AddCircle p) := inferInstance
 
 /-- The "additive circle" `ℝ ⧸ (ℤ ∙ p)` is second-countable. -/
 instance : SecondCountableTopology (AddCircle p) :=
diff --git a/Mathlib/Topology/Instances/ENNReal.lean b/Mathlib/Topology/Instances/ENNReal.lean
@@ -42,7 +42,7 @@ instance : OrderTopology ℝ≥0∞ := ⟨rfl⟩
 -- short-circuit type class inference
 instance : T2Space ℝ≥0∞ := inferInstance
 instance : T5Space ℝ≥0∞ := inferInstance
-instance : NormalSpace ℝ≥0∞ := inferInstance
+instance : T4Space ℝ≥0∞ := inferInstance
 
 instance : SecondCountableTopology ℝ≥0∞ :=
   orderIsoUnitIntervalBirational.toHomeomorph.embedding.secondCountableTopology
diff --git a/Mathlib/Topology/MetricSpace/Metrizable.lean b/Mathlib/Topology/MetricSpace/Metrizable.lean
@@ -150,7 +150,6 @@ variable [T3Space X] [SecondCountableTopology X]
 
 /-- A T₃ topological space with second countable topology can be embedded into `l^∞ = ℕ →ᵇ ℝ`. -/
 theorem exists_embedding_l_infty : ∃ f : X → ℕ →ᵇ ℝ, Embedding f := by
-  haveI : NormalSpace X := normalSpaceOfT3SecondCountable X
   -- Choose a countable basis, and consider the set `s` of pairs of set `(U, V)` such that `U ∈ B`,
   -- `V ∈ B`, and `closure U ⊆ V`.
   rcases exists_countable_basis X with ⟨B, hBc, -, hB⟩
diff --git a/Mathlib/Topology/Paracompact.lean b/Mathlib/Topology/Paracompact.lean
@@ -287,17 +287,18 @@ instance (priority := 100) paracompact_of_locallyCompact_sigmaCompact [WeaklyLoc
   exact ⟨β, t, fun x ↦ (hto x).1.2, htc, htf, fun b ↦ ⟨i <| c b, (hto b).2⟩⟩
 #align paracompact_of_locally_compact_sigma_compact paracompact_of_locallyCompact_sigmaCompact
 
-/- Dieudonné's theorem: a paracompact Hausdorff space is normal. Formalization is based on the proof
+/- **Dieudonné's theorem**: a paracompact Hausdorff space is normal.
+Formalization is based on the proof
 at [ncatlab](https://ncatlab.org/nlab/show/paracompact+Hausdorff+spaces+are+normal). -/
-theorem normal_of_paracompact_t2 [T2Space X] [ParacompactSpace X] : NormalSpace X := by
+instance (priority := 100) T4Space.of_paracompactSpace_t2Space [T2Space X] [ParacompactSpace X] :
+    T4Space X := by
   -- First we show how to go from points to a set on one side.
-  have : ∀ s t : Set X, IsClosed s → IsClosed t →
+  have : ∀ s t : Set X, IsClosed s →
       (∀ x ∈ s, ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v) →
-      ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v := by
+      ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v := fun s t hs H ↦ by
     /- For each `x ∈ s` we choose open disjoint `u x ∋ x` and `v x ⊇ t`. The sets `u x` form an
         open covering of `s`. We choose a locally finite refinement `u' : s → Set X`, then
         `⋃ i, u' i` and `(closure (⋃ i, u' i))ᶜ` are disjoint open neighborhoods of `s` and `t`. -/
-    intro s t hs _ H
     choose u v hu hv hxu htv huv using SetCoe.forall'.1 H
     rcases precise_refinement_set hs u hu fun x hx ↦ mem_iUnion.2 ⟨⟨x, hx⟩, hxu _⟩ with
       ⟨u', hu'o, hcov', hu'fin, hsub⟩
@@ -308,10 +309,10 @@ theorem normal_of_paracompact_t2 [T2Space X] [ParacompactSpace X] : NormalSpace
       absurd (htv i hxt) (closure_minimal _ (isClosed_compl_iff.2 <| hv _) hxu)
     exact fun y hyu hyv ↦ (huv i).le_bot ⟨hsub _ hyu, hyv⟩
   -- Now we apply the lemma twice: first to `s` and `t`, then to `t` and each point of `s`.
-  refine' ⟨fun s t hs ht hst ↦ this s t hs ht fun x hx ↦ _⟩
-  rcases this t {x} ht isClosed_singleton fun y hy ↦ (by
+  refine { normal := fun s t hs ht hst ↦ this s t hs fun x hx ↦ ?_ }
+  rcases this t {x} ht fun y hy ↦ (by
     simp_rw [singleton_subset_iff]
     exact t2_separation (hst.symm.ne_of_mem hy hx))
     with ⟨v, u, hv, hu, htv, hxu, huv⟩
   exact ⟨u, v, hu, hv, singleton_subset_iff.1 hxu, htv, huv.symm⟩
-#align normal_of_paracompact_t2 normal_of_paracompact_t2
+#align normal_of_paracompact_t2 T4Space.of_paracompactSpace_t2Space
diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean
diff --git a/Mathlib/Topology/StoneCech.lean b/Mathlib/Topology/StoneCech.lean
diff --git a/Mathlib/Topology/SubsetProperties.lean b/Mathlib/Topology/SubsetProperties.lean
diff --git a/Mathlib/Topology/UniformSpace/Compact.lean b/Mathlib/Topology/UniformSpace/Compact.lean
