Commit 2022-11-30 13:42 d57133e4

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.