mathlib3

cc6e2eb1 - feat(group_theory/commutator): The three subgroups lemma (#12634)

feat(group_theory/commutator): The three subgroups lemma (#12634) This PR proves the three subgroups lemma: If `⁅⁅H₂, H₃⁆, H₁⁆ = ⊥` and `⁅⁅H₃, H₁⁆, H₂⁆ = ⊥`, then `⁅⁅H₁, H₂⁆, H₃⁆ = ⊥`.