refactor(topology/{order,*}): review API (#18312)

## Main changes

* Switch from `@[class] structure topological_space` to `class`.
* Introduce notation `is_open[t]`/`is_closed[t]`/`𝓤[u]` and use it instead of `t.is_open`/`@is_closed _ t`/`u.uniformity`
* Don't introduce a temporary order on `topological_space`, use `galois_coinsertion` to the order-dual of `set (set α)` instead.
* Drop `discrete_topology_bot`. It seems that this instance doesn't work well in Lean 4 (in fact, I failed to define it without using `@DiscreteTopology.mk`).

## Other changes

### Topological spaces
* Add `is_open_mk`.
* Rename `generate_from_mono` to `generate_from_anti`, move it to the `topological_space` namespace.
* Add `embedding_inclusion`, `embedding_ulift_down`, and `ulift.discrete_topology`.
* Move `discrete_topology.of_subset` from `topology.separation` to `topology.constructions`.
* Move `embedding.discrete_topology` from `topology.separation` to `topology.maps`.
* Use explicit arguments in an argument of `nhds_mk_of_nhds`.
* Move some definitions and lemmas like `mk_of_closure`, `gi_generate_from` (renamed to `gci_generate_from`), `left_inverse_generate_from` to the `topological_space` namespace. These lemmas are very specific and use generic names.
* Add `topological_space` and `discrete_topology` instances for `fin n`.
* Drop `is_open_induced_iff'`, use non-primed version instead.
* Prove `set_of_is_open_sup` by `rfl`.
* Drop `nhds_bot`, use `nhds_discrete` instead.
* Drop `induced_bot` and `discrete_topology_induced`

### Uniform spaces

* Drop `infi_uniformity'` and `inf_uniformity'`.
* Use `@uniformity α (uniform_space.comap _ _)` instead of `(h : ‹uniform_space α› = uniform_space.comap f ‹uniform_space β›)` in `uniformity_comap`.

### Locally constant functions and discrete quotients

* Use quotient space topology for the coercion of a `discrete_quotient` to `Type*`, then prove `[discrete_topology]`. This way we avoid surprising diamonds in the future (especially if Lean 4 will unfold the coercion).
* Merge `locally_constant.lift` and `locally_constant.locally_constant_lift` into 1 def, rename `factors` to `lift_comp_proj`.
* Protect `locally_constant.is_locally_constant`.
* Drop `locally_constant.iff_continuous_bot`

### Categories

* Add an instance for `discrete_topology (discrete.obj X)`.
* Rename `Fintype.discrete_topology` to `Fintype.bot_topology `, add lemma `Fintype.discrete_topology` sating that this is a `[discrete_topology]`.

### Topological rings

* Fix&golf a proof that failed because of API changes.

Author: urkud

src/analysis/locally_convex/polar.lean

@@ -37,6 +37,7 @@ polar
 
 
 variables {𝕜 E F : Type*}
+open_locale topology
 
 namespace linear_map
 
@@ -101,7 +102,7 @@ end
 
 /-- The polar set is closed in the weak topology induced by `B.flip`. -/
 lemma polar_weak_closed (s : set E) :
-  @is_closed _ (weak_bilin.topological_space B.flip) (B.polar s) :=
+  is_closed[weak_bilin.topological_space B.flip] (B.polar s) :=
 begin
   rw polar_eq_Inter,
   refine is_closed_Inter (λ x, is_closed_Inter (λ _, _)),

src/analysis/normed_space/pi_Lp.lean

@@ -368,7 +368,7 @@ begin
 end
 
 lemma aux_uniformity_eq :
-  𝓤 (pi_Lp p β) = @uniformity _ (Pi.uniform_space _) :=
+  𝓤 (pi_Lp p β) = 𝓤[Pi.uniform_space _] :=
 begin
   have A : uniform_inducing (pi_Lp.equiv p β) :=
     (antilipschitz_with_equiv_aux p β).uniform_inducing

src/geometry/manifold/charted_space.lean

@@ -708,7 +708,7 @@ protected def to_topological_space : topological_space M :=
 topological_space.generate_from $ ⋃ (e : local_equiv M H) (he : e ∈ c.atlas)
   (s : set H) (s_open : is_open s), {e ⁻¹' s ∩ e.source}
 
-lemma open_source' (he : e ∈ c.atlas) : @is_open M c.to_topological_space e.source :=
+lemma open_source' (he : e ∈ c.atlas) : is_open[c.to_topological_space] e.source :=
 begin
   apply topological_space.generate_open.basic,
   simp only [exists_prop, mem_Union, mem_singleton_iff],

src/measure_theory/constructions/polish.lean

@@ -231,8 +231,8 @@ begin
   topology `t'`. It is analytic for this topology. As the identity from `t'` to `t` is continuous
   and the image of an analytic set is analytic, it follows that `s` is also analytic for `t`. -/
   obtain ⟨t', t't, t'_polish, s_closed, s_open⟩ :
-    ∃ (t' : topological_space α), t' ≤ t ∧ @polish_space α t' ∧ @is_closed α t' s ∧
-      @is_open α t' s := hs.is_clopenable,
+    ∃ t' : topological_space α, t' ≤ t ∧ @polish_space α t' ∧ is_closed[t'] s ∧ is_open[t'] s :=
+    hs.is_clopenable,
   have A := @is_closed.analytic_set α t' t'_polish s s_closed,
   convert @analytic_set.image_of_continuous α t' α t s A id (continuous_id_of_le t't),
   simp only [id.def, image_id'],
@@ -593,8 +593,8 @@ theorem _root_.measurable_set.image_of_continuous_on_inj_on
   measurable_set (f '' s) :=
 begin
   obtain ⟨t', t't, t'_polish, s_closed, s_open⟩ :
-    ∃ (t' : topological_space γ), t' ≤ tγ ∧ @polish_space γ t' ∧ @is_closed γ t' s ∧
-      @is_open γ t' s := hs.is_clopenable,
+    ∃ (t' : topological_space γ), t' ≤ tγ ∧ @polish_space γ t' ∧ is_closed[t'] s ∧
+      is_open[t'] s := hs.is_clopenable,
   exact @is_closed.measurable_set_image_of_continuous_on_inj_on γ t' t'_polish β _ _ _ _ s
     s_closed f (f_cont.mono_dom t't) f_inj,
 end
@@ -665,8 +665,8 @@ begin
   refine ⟨λ hs, _, λ hs, hs.is_clopenable⟩,
   -- consider a finer topology `t'` in which `s` is open and closed.
   obtain ⟨t', t't, t'_polish, s_closed, s_open⟩ :
-    ∃ (t' : topological_space γ), t' ≤ tγ ∧ @polish_space γ t' ∧ @is_closed γ t' s ∧
-      @is_open γ t' s := hs,
+    ∃ (t' : topological_space γ), t' ≤ tγ ∧ @polish_space γ t' ∧ is_closed[t'] s ∧
+      is_open[t'] s := hs,
   -- the identity is continuous from `t'` to `tγ`.
   have C : @continuous γ γ t' tγ id := continuous_id_of_le t't,
   -- therefore, it is also a measurable embedding, by the Lusin-Souslin theorem

src/topology/algebra/group/basic.lean

@@ -1466,7 +1466,8 @@ instance : has_top (group_topology α) :=
 @[to_additive]
 instance : has_bot (group_topology α) :=
 ⟨{to_topological_space := ⊥,
-  continuous_mul       := by continuity,
+  continuous_mul       := by
+  { letI : topological_space α := ⊥, haveI := discrete_topology_bot α, continuity },
   continuous_inv       := continuous_bot}⟩
 
 @[simp, to_additive] lemma to_topological_space_bot :

src/topology/algebra/ring.lean

@@ -369,7 +369,7 @@ instance inhabited {α : Type u} [ring α] : inhabited (ring_topology α) :=
 
 @[ext]
 lemma ext' {f g : ring_topology α} (h : f.is_open = g.is_open) : f = g :=
-by { ext, rw h }
+by { ext : 2, exact h }
 
 /-- The ordering on ring topologies on the ring `α`.
   `t ≤ s` if every set open in `s` is also open in `t` (`t` is finer than `s`). -/
@@ -452,24 +452,7 @@ def to_add_group_topology (t : ring_topology α) : add_group_topology α :=
 /-- The order embedding from ring topologies on `a` to additive group topologies on `a`. -/
 def to_add_group_topology.order_embedding : order_embedding (ring_topology α)
   (add_group_topology α) :=
-{ to_fun       := λ t, t.to_add_group_topology,
-  inj'         :=
-  begin
-    intros t₁ t₂ h_eq,
-    dsimp only at h_eq,
-    ext,
-    have h_t₁ : t₁.to_topological_space = t₁.to_add_group_topology.to_topological_space := rfl,
-    rw [h_t₁, h_eq],
-    refl,
-  end,
-  map_rel_iff' :=
-  begin
-    intros t₁ t₂,
-    rw [embedding.coe_fn_mk],
-    have h_le : t₁ ≤ t₂ ↔ t₁.to_topological_space ≤ t₂.to_topological_space := by refl,
-    rw h_le,
-    refl,
-  end }
+order_embedding.of_map_le_iff to_add_group_topology $ λ _ _, iff.rfl
 
 end ring_topology
 

src/topology/algebra/uniform_group.lean

@@ -213,11 +213,8 @@ by { rw [← comap_swap_uniformity, uniformity_eq_comap_nhds_one, comap_comap, (
   (hu : @uniform_group G u _) (hv : @uniform_group G v _)
   (h : @nhds _ u.to_topological_space 1 = @nhds _ v.to_topological_space 1) :
   u = v :=
-begin
-  refine uniform_space_eq _,
-  change @uniformity _ u = @uniformity _ v,
-  rw [@uniformity_eq_comap_nhds_one _ u _ hu, @uniformity_eq_comap_nhds_one _ v _ hv, h]
-end
+uniform_space_eq $
+  by rw [@uniformity_eq_comap_nhds_one _ u _ hu, @uniformity_eq_comap_nhds_one _ v _ hv, h]
 
 @[to_additive] lemma uniform_group.ext_iff {G : Type*} [group G] {u v : uniform_space G}
   (hu : @uniform_group G u _) (hv : @uniform_group G v _) :
@@ -579,7 +576,6 @@ end
   [group G] [uniform_group G] : topological_group.to_uniform_space G = u :=
 begin
   ext : 1,
-  show @uniformity G (topological_group.to_uniform_space G) = 𝓤 G,
   rw [uniformity_eq_comap_nhds_one' G, uniformity_eq_comap_nhds_one G]
 end
 

src/topology/bases.lean

@@ -71,7 +71,7 @@ begin
     obtain ⟨t₃, h₃, hs⟩ := h.exists_subset_inter _ h₁ _ h₂ x ⟨hx₁, hx₂⟩,
     exact ⟨t₃, or.inr h₃, hs⟩ },
   { rw h.eq_generate_from,
-    refine le_antisymm (le_generate_from $ λ t, _) (generate_from_mono $ subset_insert ∅ s),
+    refine le_antisymm (le_generate_from $ λ t, _) (generate_from_anti $ subset_insert ∅ s),
     rintro (rfl|ht), { convert is_open_empty }, { exact generate_open.basic t ht } },
 end
 
@@ -83,7 +83,7 @@ begin
     obtain ⟨t₃, h₃, hs⟩ := h.exists_subset_inter _ h₁ _ h₂ x hx,
     exact ⟨t₃, ⟨h₃, nonempty.ne_empty ⟨x, hs.1⟩⟩, hs⟩ },
   { rw h.eq_generate_from,
-    refine le_antisymm (generate_from_mono $ diff_subset s _) (le_generate_from $ λ t ht, _),
+    refine le_antisymm (generate_from_anti $ diff_subset s _) (le_generate_from $ λ t ht, _),
     obtain rfl|he := eq_or_ne t ∅, { convert is_open_empty },
     exact generate_open.basic t ⟨ht, he⟩ },
 end
@@ -93,7 +93,7 @@ subcollections of `s` form a topological basis. -/
 lemma is_topological_basis_of_subbasis {s : set (set α)} (hs : t = generate_from s) :
   is_topological_basis ((λ f, ⋂₀ f) '' {f : set (set α) | f.finite ∧ f ⊆ s}) :=
 begin
-  refine ⟨_, _, hs.trans (le_antisymm (le_generate_from _) $ generate_from_mono $ λ t ht, _)⟩,
+  refine ⟨_, _, hs.trans (le_antisymm (le_generate_from _) $ generate_from_anti $ λ t ht, _)⟩,
   { rintro _ ⟨t₁, ⟨hft₁, ht₁b⟩, rfl⟩ _ ⟨t₂, ⟨hft₂, ht₂b⟩, rfl⟩ x h,
     exact ⟨_, ⟨_, ⟨hft₁.union hft₂, union_subset ht₁b ht₂b⟩, sInter_union t₁ t₂⟩, h, subset.rfl⟩ },
   { rw [sUnion_image, Union₂_eq_univ_iff],

src/topology/basic.lean

@@ -62,14 +62,12 @@ universes u v w
 -/
 
 /-- A topology on `α`. -/
-@[protect_proj] structure topological_space (α : Type u) :=
+@[protect_proj] class topological_space (α : Type u) :=
 (is_open        : set α → Prop)
 (is_open_univ   : is_open univ)
 (is_open_inter  : ∀s t, is_open s → is_open t → is_open (s ∩ t))
 (is_open_sUnion : ∀s, (∀t∈s, is_open t) → is_open (⋃₀ s))
 
-attribute [class] topological_space
-
 /-- A constructor for topologies by specifying the closed sets,
 and showing that they satisfy the appropriate conditions. -/
 def topological_space.of_closed {α : Type u} (T : set (set α))
@@ -86,32 +84,36 @@ section topological_space
 
 variables {α : Type u} {β : Type v} {ι : Sort w} {a : α} {s s₁ s₂ t : set α} {p p₁ p₂ : α → Prop}
 
+/-- `is_open s` means that `s` is open in the ambient topological space on `α` -/
+def is_open [topological_space α] (s : set α) : Prop := @topological_space.is_open _ ‹_› s
+
+localized "notation (name := is_open_of) `is_open[` t `]` := @is_open hole! t" in topology
+
+lemma is_open_mk {p h₁ h₂ h₃} {s : set α} : is_open[⟨p, h₁, h₂, h₃⟩] s ↔ p s := iff.rfl
+
 @[ext]
-lemma topological_space_eq : ∀ {f g : topological_space α}, f.is_open = g.is_open → f = g
-| ⟨a, _, _, _⟩ ⟨b, _, _, _⟩ rfl := rfl
+lemma topological_space_eq {f g : topological_space α} (h : is_open[f] = is_open[g]) : f = g :=
+by unfreezingI { cases f, cases g, congr, exact h }
 
 section
 variables [topological_space α]
 
-/-- `is_open s` means that `s` is open in the ambient topological space on `α` -/
-def is_open (s : set α) : Prop := topological_space.is_open ‹_› s
-
 @[simp]
-lemma is_open_univ : is_open (univ : set α) := topological_space.is_open_univ _
+lemma is_open_univ : is_open (univ : set α) := topological_space.is_open_univ
 
 lemma is_open.inter (h₁ : is_open s₁) (h₂ : is_open s₂) : is_open (s₁ ∩ s₂) :=
-topological_space.is_open_inter _ s₁ s₂ h₁ h₂
+topological_space.is_open_inter s₁ s₂ h₁ h₂
 
 lemma is_open_sUnion {s : set (set α)} (h : ∀t ∈ s, is_open t) : is_open (⋃₀ s) :=
-topological_space.is_open_sUnion _ s h
+topological_space.is_open_sUnion s h
 
 end
 
 lemma topological_space_eq_iff {t t' : topological_space α} :
-  t = t' ↔ ∀ s, @is_open α t s ↔ @is_open α t' s :=
+  t = t' ↔ ∀ s, is_open[t] s ↔ is_open[t'] s :=
 ⟨λ h s, h ▸ iff.rfl, λ h, by { ext, exact h _ }⟩
 
-lemma is_open_fold {s : set α} {t : topological_space α} : t.is_open s = @is_open α t s :=
+lemma is_open_fold {s : set α} {t : topological_space α} : t.is_open s = is_open[t] s :=
 rfl
 
 variables [topological_space α]
@@ -165,6 +167,8 @@ is_open.inter
 class is_closed (s : set α) : Prop :=
 (is_open_compl : is_open sᶜ)
 
+localized "notation (name := is_closed_of) `is_closed[` t `]` := @is_closed hole! t" in topology
+
 @[simp] lemma is_open_compl_iff {s : set α} : is_open sᶜ ↔ is_closed s :=
 ⟨λ h, ⟨h⟩, λ h, h.is_open_compl⟩
 

src/topology/category/CompHaus/basic.lean

@@ -235,8 +235,8 @@ lemma mono_iff_injective {X Y : CompHaus.{u}} (f : X ⟶ Y) : mono f ↔ functio
 begin
   split,
   { introsI hf x₁ x₂ h,
-    let g₁ : of punit ⟶ X := ⟨λ _, x₁, continuous_of_discrete_topology⟩,
-    let g₂ : of punit ⟶ X := ⟨λ _, x₂, continuous_of_discrete_topology⟩,
+    let g₁ : of punit ⟶ X := ⟨λ _, x₁, continuous_const⟩,
+    let g₂ : of punit ⟶ X := ⟨λ _, x₂, continuous_const⟩,
     have : g₁ ≫ f = g₂ ≫ f, by { ext, exact h },
     rw cancel_mono at this,
     apply_fun (λ e, e punit.star) at this,