## 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.

Forward-ported from leanprover-community/mathlib3#18312

Also use `{}` arguments in `continuous_def` because otherwise Lean 4
can't use it in `simp` with non-standard instances.