mathlib

d57133e4 - refactor(subgroup/basic): use `subgroup.subgroup_of` as the normal form (#17744)

refactor(subgroup/basic): use `subgroup.subgroup_of` as the normal form (#17744) Update or drop lemmas/defs that used `subgroup.comap (subgroup.subtype _) _`. * Golf some proofs. * Drop `inf_relindex_eq_relindex_sup`, `comap_subtype_self_eq_top`, `comap_subtype_inf_left`, `comap_subtype_inf_right`, `subgroup.normal_inf`. * Swap LHS and RHS of `relindex_eq_relindex_sup`, rename to `relindex_sup_right`, add `relindex_sup_left`. * Use `subgroup_of` instead of `comap (subtype _) _` in - `quotient_inf_equiv_prod_normal_quotient`, - `comap_subtype_equiv_of_le`, rename it to `subgroup_of_equiv_of_le` - `normal_in_normalizer` - `le_normalizer_of_normal` - `comap_subtype_normalizer_eq`, rename to `subgroup_of_normalizer_eq` * Simplify `subgroup.comap (subgroup.subtype _) _` to `subgroup.subgroup_of _ _`. * Add `comap_inclusion_subgroup_of`, `subgroup_of_inj`, `inf_subgroup_of_left`, `inf_subgroup_of_right`, `codisjoint_subgroup_of_sup`, `normal.subgroup_of`, `normal_subgroup_of`. * Mark `subgroup_of_map_subtype` as `simp`.