mathlib3

ef25c4ca - refactor(group_theory/commutator): Rename `commutator_containment` to `commutator_mem_commutator` (#12553)

refactor(group_theory/commutator): Rename `commutator_containment` to `commutator_mem_commutator` (#12553) This PR renames `commutator_containment` to `commutator_mem_commutator`, uses the new commutator notation, and makes the subgroups implicit.