feat(group_theory/subgroup/basic): add some trivial lemmas (#16915)
feat(group_theory/subgroup/basic): add some trivial lemmas (#16915)

* add `subgroup.subtype_injective`, `subgroup.le_closure_to_submonoid`, `subgroup.closure_eq_top_of_mclosure_eq_top`;
* golf `subgroup.closure_inv`, `subgroup.map_le_map_iff_of_injective`, and `subgroup.map_injective`.





leanprover-community/mathlib,leanprover-community/mathlib