refactor(topology/discrete_quotient): review API (#18401)
Backport various changes I made to the API while porting to Lean 4 in leanprover-community/mathlib4#2157.
* extend `setoid X`;
* require only that the fibers are open in the definition, prove that they are clopen;
* golf proofs, reuse lattice structure on `setoid`s;
* use bundled continuous maps for `comap`;
* swap LHS and RHS in some `simp` lemmas;
* generalize the `order_bot` instance from a discrete space to a locally connected space;
* prove that a discrete topological space is locally connected.
