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.

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,

src/topology/category/Profinite/basic.lean

@@ -43,6 +43,7 @@ profinite
 universe u
 
 open category_theory
+open_locale topology
 
 /-- The type of profinite topological spaces. -/
 structure Profinite :=
@@ -134,11 +135,14 @@ lemma CompHaus.to_Profinite_obj' (X : CompHaus) :
   ↥(CompHaus.to_Profinite.obj X) = connected_components X := rfl
 
 /-- Finite types are given the discrete topology. -/
-def Fintype.discrete_topology (A : Fintype) : topological_space A := ⊥
+def Fintype.bot_topology (A : Fintype) : topological_space A := ⊥
 
 section discrete_topology
 
-local attribute [instance] Fintype.discrete_topology
+local attribute [instance] Fintype.bot_topology
+
+local attribute [instance]
+lemma Fintype.discrete_topology (A : Fintype) : discrete_topology A := ⟨rfl⟩
 
 /-- The natural functor from `Fintype` to `Profinite`, endowing a finite type with the
 discrete topology. -/
@@ -254,17 +258,15 @@ lemma epi_iff_surjective {X Y : Profinite.{u}} (f : X ⟶ Y) : epi f ↔ functio
 begin
   split,
   { contrapose!,
-    rintros ⟨y, hy⟩ hf,
+    rintros ⟨y, hy⟩ hf, resetI,
     let C := set.range f,
     have hC : is_closed C := (is_compact_range f.continuous).is_closed,
     let U := Cᶜ,
-    have hU : is_open U := is_open_compl_iff.mpr hC,
     have hyU : y ∈ U,
     { refine set.mem_compl _, rintro ⟨y', hy'⟩, exact hy y' hy' },
-    have hUy : U ∈ nhds y := hU.mem_nhds hyU,
+    have hUy : U ∈ 𝓝 y := hC.compl_mem_nhds hyU,
     obtain ⟨V, hV, hyV, hVU⟩ := is_topological_basis_clopen.mem_nhds_iff.mp hUy,
     classical,
-    letI : topological_space (ulift.{u} $ fin 2) := ⊥,
     let Z := of (ulift.{u} $ fin 2),
     let g : Y ⟶ Z := ⟨(locally_constant.of_clopen hV).map ulift.up, locally_constant.continuous _⟩,
     let h : Y ⟶ Z := ⟨λ _, ⟨1⟩, continuous_const⟩,

src/topology/category/Top/basic.lean

@@ -55,6 +55,8 @@ def discrete : Type u ⥤ Top.{u} :=
 { obj := λ X, ⟨X, ⊥⟩,
   map := λ X Y f, { to_fun := f, continuous_to_fun := continuous_bot } }
 
+instance {X : Type u} : discrete_topology (discrete.obj X) := ⟨rfl⟩
+
 /-- The trivial topology on any type. -/
 def trivial : Type u ⥤ Top.{u} :=
 { obj := λ X, ⟨X, ⊤⟩,

src/topology/category/Top/limits.lean

@@ -1056,6 +1056,7 @@ lemma nonempty_sections_of_fintype_cofiltered_system.init
   F.sections.nonempty :=
 begin
   let F' : J ⥤ Top := F ⋙ Top.discrete,
+  haveI : ∀ j, discrete_topology (F'.obj j) := λ _, ⟨rfl⟩,
   haveI : Π (j : J), fintype (F'.obj j) := hf,
   haveI : Π (j : J), nonempty (F'.obj j) := hne,
   obtain ⟨⟨u, hu⟩⟩ := Top.nonempty_limit_cone_of_compact_t2_cofiltered_system F',

src/topology/compact_open.lean

@@ -182,7 +182,7 @@ lemma compact_open_le_induced (s : set α) :
   ≤ topological_space.induced (continuous_map.restrict s) continuous_map.compact_open :=
 begin
   simp only [induced_generate_from_eq, continuous_map.compact_open],
-  apply generate_from_mono,
+  apply topological_space.generate_from_anti,
   rintros b ⟨a, ⟨c, hc, u, hu, rfl⟩, rfl⟩,
   refine ⟨coe '' c, hc.image continuous_subtype_coe, u, hu, _⟩,
   ext f,
@@ -202,7 +202,7 @@ begin
   { refine le_infi₂ _,
     exact λ s hs, compact_open_le_induced s },
   simp only [← generate_from_Union, induced_generate_from_eq, continuous_map.compact_open],
-  apply generate_from_mono,
+  apply topological_space.generate_from_anti,
   rintros _ ⟨s, hs, u, hu, rfl⟩,
   rw mem_Union₂,
   refine ⟨s, hs, _, ⟨univ, is_compact_iff_is_compact_univ.mp hs, u, hu, rfl⟩, _⟩,

src/topology/constructions.lean

@@ -466,8 +466,8 @@ lemma filter.has_basis.prod_nhds' {ιa ιb : Type*} {pa : ιa → Prop} {pb : ι
 by { cases ab, exact ha.prod_nhds hb }
 
 instance [discrete_topology α] [discrete_topology β] : discrete_topology (α × β) :=
-⟨eq_of_nhds_eq_nhds $ assume ⟨a, b⟩,
-  by rw [nhds_prod_eq, nhds_discrete α, nhds_discrete β, nhds_bot, filter.prod_pure_pure]⟩
+discrete_topology_iff_nhds.2 $ λ ⟨a, b⟩,
+  by rw [nhds_prod_eq, nhds_discrete α, nhds_discrete β, filter.prod_pure_pure]
 
 lemma prod_mem_nhds_iff {s : set α} {t : set β} {a : α} {b : β} :
   s ×ˢ t ∈ 𝓝 (a, b) ↔ s ∈ 𝓝 a ∧ t ∈ 𝓝 b :=
@@ -925,6 +925,16 @@ lemma embedding.cod_restrict {e : α → β} (he : embedding e) (s : set β) (hs
   embedding (cod_restrict e s hs) :=
 embedding_of_embedding_compose (he.continuous.cod_restrict hs) continuous_subtype_coe he
 
+lemma embedding_inclusion {s t : set α} (h : s ⊆ t) : embedding (set.inclusion h) :=
+embedding_subtype_coe.cod_restrict _ _
+
+/-- Let `s, t ⊆ X` be two subsets of a topological space `X`.  If `t ⊆ s` and the topology induced
+by `X`on `s` is discrete, then also the topology induces on `t` is discrete.  -/
+lemma discrete_topology.of_subset {X : Type*} [topological_space X] {s t : set X}
+  (ds : discrete_topology s) (ts : t ⊆ s) :
+  discrete_topology t :=
+(embedding_inclusion ts).discrete_topology
+
 end subtype
 
 section quotient
@@ -1089,7 +1099,7 @@ lemma pi_generate_from_eq {π : ι → Type*} {g : Πa, set (set (π a))} :
 let G := {t | ∃(s:Πa, set (π a)) (i : finset ι), (∀a∈i, s a ∈ g a) ∧ t = pi ↑i s} in
 begin
   rw [pi_eq_generate_from],
-  refine le_antisymm (generate_from_mono _) (le_generate_from _),
+  refine le_antisymm (generate_from_anti _) (le_generate_from _),
   exact assume s ⟨t, i, ht, eq⟩, ⟨t, i, assume a ha, generate_open.basic _ (ht a ha), eq⟩,
   { rintros s ⟨t, i, hi, rfl⟩,
     rw [pi_def],
@@ -1106,8 +1116,8 @@ lemma pi_generate_from_eq_finite {π : ι → Type*} {g : Πa, set (set (π a))}
 begin
   casesI nonempty_fintype ι,
   rw [pi_generate_from_eq],
-  refine le_antisymm (generate_from_mono _) (le_generate_from _),
-  exact assume s ⟨t, ht, eq⟩, ⟨t, finset.univ, by simp [ht, eq]⟩,
+  refine le_antisymm (generate_from_anti _) (le_generate_from _),
+  { rintro s ⟨t, ht, rfl⟩, exact ⟨t, finset.univ, by simp [ht]⟩ },
   { rintros s ⟨t, i, ht, rfl⟩,
     apply is_open_iff_forall_mem_open.2 _,
     assume f hf,
@@ -1272,4 +1282,11 @@ continuous_induced_dom
   continuous (ulift.up : α → ulift.{v u} α) :=
 continuous_induced_rng.2 continuous_id
 
+lemma embedding_ulift_down [topological_space α] :
+  embedding (ulift.down : ulift.{v u} α → α) :=
+⟨⟨rfl⟩, ulift.down_injective⟩
+
+instance [topological_space α] [discrete_topology α] : discrete_topology (ulift α) :=
+embedding_ulift_down.discrete_topology
+
 end ulift