chore(topology/algebra): cleanup (#15301)
* Drop instances about `sub*.topological_closure`. Normal `sub*` instances apply.
* Add `units.inducing_embed_product` and `units.embedding_embed_product`.
* Add `inducing.has_continuous_mul`, `inducing.has_continuous_inv`, and `inducing.topological_group`.
* Use new lemmas to golf some instances.
* Don't use `section .. variables` for assumptions that are used only once.
* Reuse `topological_group_inf`, `topological_group_Inf` in `group_topology.has_inf`, `group_topology.has_Inf`.
