chore(topology/*): golf some proofs (#4528)
* move `exists_nhds_split` to `topology/algebra/monoid`, rename to `exists_nhds_one_split`;
* add a version `exists_open_nhds_one_split`;
* move `exists_nhds_split4` to `topology/algebra/monoid`, rename to `exists_nhds_one_split4`;
* move `one_open_separated_mul` to `topology/algebra/monoid`, rename to `exists_open_nhds_one_mul_subset`;
* add `mem_prod_nhds_iff`;
* golf some proofs.
