chore(topology/algebra/weak_dual_topology): review (#11141)
* Fix universes in `pi.has_continuous_smul`.
* Add `function.injective.embedding_induced` and
`weak_dual.coe_fn_embedding`.
* Golf some proofs.
* Review `weak_dual.module` etc instances to ensure, e.g.,
`module ℝ (weak_dual ℂ E)`.
