chore(*): golf (#18111)
### Sets
* Add `set.maps_to_prod_map_diagonal`, `set.diagonal_nonempty`, and `set.diagonal_subset_iff`.
### Filters
* Generalize and rename `nhds_eq_comap_uniformity_aux` to `filter.mem_comap_prod_mk`.
* Add `set.nonempty.principal_ne_bot` and `filter.comap_id'`.
* Rename `filter.has_basis.comp_of_surjective` to `filter.has_basis.comp_surjective`.
### Uniform spaces
* Rename `monotone_comp_rel` to `monotone.comp_rel` to enable dot notation.
* Add `nhds_eq_comap_uniformity'`.
* Use `𝓝ˢ (diagonal γ)` instead of `⨆ x, 𝓝 (x, x)` in `uniform_space_of_compact_t2`.
* Golf here and there.
### Mathlib 4 port
Relevant parts are forward-ported in leanprover-community/mathlib4#1438
