refactor(Topology): use WithTopology to define WithConstructibleTopology (leanprover-community#39621)

We replace the type synonym `WithConstructibleTopology` by `WithTopology _ (constructibleTopology X)`. This breaks the def-eq `X = WithConstructibleTopology X`, which was luckily not abused much yet.

Author: chrisflav

Mathlib/Topology/Compactness/Compact.lean

@@ -961,6 +961,12 @@ theorem disjoint_map_cocompact {g : X → Y} {f : Filter X} (hg : Continuous g)
 theorem isCompact_range [CompactSpace X] {f : X → Y} (hf : Continuous f) : IsCompact (range f) := by
   rw [← image_univ]; exact isCompact_univ.image hf
 
+lemma Function.Surjective.compactSpace {f : X → Y} (hf : Continuous f) [CompactSpace X]
+    (hf' : f.Surjective) : CompactSpace Y where
+  isCompact_univ := by
+    rw [← hf'.range_eq]
+    exact isCompact_range hf
+
 theorem isCompact_diagonal [CompactSpace X] : IsCompact (diagonal X) :=
   @range_diag X ▸ isCompact_range (continuous_id.prodMk continuous_id)
 

Mathlib/Topology/Spectral/ConstructibleTopology.lean

@@ -6,6 +6,7 @@ Authors: Johan Commelin, Jiedong Jiang, Christian Merten
 module
 
 public import Mathlib.Topology.Spectral.Basic
+public import Mathlib.Topology.WithTopology
 public import Mathlib.Topology.JacobsonSpace
 public import Mathlib.Data.Set.Card
 
@@ -43,14 +44,19 @@ def constructibleTopology (X : Type*) [TopologicalSpace X] : TopologicalSpace X
 
 /-- A type synonym for `X` that is equipped with the constructible topology of `X`. -/
 @[nolint unusedArguments]
-def WithConstructibleTopology (X : Type*) [TopologicalSpace X] : Type _ :=
-  X
-
-instance : TopologicalSpace (WithConstructibleTopology X) :=
-  fast_instance% constructibleTopology X
+abbrev WithConstructibleTopology (X : Type*) [TopologicalSpace X] : Type _ :=
+  WithTopology X (constructibleTopology X)
 
 open Topology
 
+lemma WithConstructibleTopology.isOpen_iff {s : Set (WithConstructibleTopology X)} :
+    IsOpen s ↔ IsOpen[constructibleTopology X] (WithTopology.toTopology _ ⁻¹' s) :=
+  WithTopology.isOpen_iff _
+
+lemma WithConstructibleTopology.isClosed_iff {s : Set (WithConstructibleTopology X)} :
+    IsClosed s ↔ IsClosed[constructibleTopology X] (WithTopology.toTopology _ ⁻¹' s) :=
+  WithTopology.isClosed_iff _
+
 lemma IsCompact.isOpen_constructibleTopology_of_isOpen {s : Set X}
     (hs : IsCompact s) (ho : IsOpen s) : IsOpen[constructibleTopology X] s := by
   apply TopologicalSpace.isOpen_generateFrom_of_mem
@@ -86,6 +92,9 @@ spaces. -/
 instance compactSpace_withConstructibleTopology [CompactSpace X] [QuasiSober X]
     [PrespectralSpace X] [QuasiSeparatedSpace X] :
     CompactSpace (WithConstructibleTopology X) := by
+  suffices h : @CompactSpace X (constructibleTopology X) from
+    @Function.Surjective.compactSpace _ _ (constructibleTopology X) _ _
+      (WithTopology.continuous_toTopology _) _ (WithTopology.toTopology_surjective _)
   let 𝔅 := constructibleTopologySubbasis X
   /- It suffices to check that any subset of `𝔅` for which every finite subset has non-empty
   intersection, has non-empty intersection. We argue by contradiction and by Zorn's

Mathlib/Topology/WithTopology.lean

@@ -63,6 +63,24 @@ lemma toTopology_inj {x y : X} : toTopology t x = toTopology t y ↔ x = y :=
 @[simp] lemma ofTopology_inj {x y : WithTopology X t} : ofTopology x = ofTopology y ↔ x = y :=
   (ofTopology_injective t).eq_iff
 
+open Topology
+
+lemma isOpen_iff {s : Set (WithTopology X t)} :
+    IsOpen s ↔ IsOpen[t] (toTopology t ⁻¹' s) :=
+  .rfl
+
+lemma isClosed_iff {s : Set (WithTopology X t)} :
+    IsClosed s ↔ IsClosed[t] (toTopology t ⁻¹' s) := by
+  simp [← isOpen_compl_iff, isOpen_iff]
+
+/-- If `X` is equipped with topology `t`, the map `X → WithTopology X t` is continuous. -/
+lemma continuous_toTopology : Continuous[t, _] (toTopology t) :=
+  ⟨fun _ ↦ (·)⟩
+
+/-- If `X` is equipped with topology `t`, the map `WithTopology X t → X` is continuous. -/
+lemma continuous_ofTopology : Continuous[_, t] (ofTopology (t := t)) :=
+  ⟨fun _ ↦ (·)⟩
+
 /-! ### Set-theoretic lemmas -/
 
 open Set