refactor(group_theory/commutator): Golf proof of `commutator_mem_comm…

…utator` (#12584)

This PR golfs the proof of `commutator_mem_commutator`, and moves it earlier in the file so that it can be used earlier.

src/group_theory/commutator.lean

@@ -41,6 +41,10 @@ instance commutator : has_bracket (subgroup G) (subgroup G) :=
 lemma commutator_def (H₁ H₂ : subgroup G) :
   ⁅H₁, H₂⁆ = closure {g | ∃ (g₁ ∈ H₁) (g₂ ∈ H₂), ⁅g₁, g₂⁆ = g} := rfl
 
+lemma commutator_mem_commutator {H₁ H₂ : subgroup G} {g₁ g₂ : G} (h₁ : g₁ ∈ H₁) (h₂ : g₂ ∈ H₂) :
+  ⁅g₁, g₂⁆ ∈ ⁅H₁, H₂⁆ :=
+subset_closure ⟨g₁, h₁, g₂, h₂, rfl⟩
+
 instance commutator_normal (H₁ H₂ : subgroup G) [h₁ : H₁.normal]
   [h₂ : H₂.normal] : normal ⁅H₁, H₂⁆ :=
 begin
@@ -78,10 +82,6 @@ begin
     exact h p hp q hq, }
 end
 
-lemma commutator_mem_commutator {H₁ H₂ : subgroup G} {p q : G} (hp : p ∈ H₁) (hq : q ∈ H₂) :
-  ⁅p, q⁆ ∈ ⁅H₁, H₂⁆ :=
-(commutator_le H₁ H₂ ⁅H₁, H₂⁆).mp (le_refl ⁅H₁, H₂⁆) p hp q hq
-
 lemma commutator_comm (H₁ H₂ : subgroup G) : ⁅H₁, H₂⁆ = ⁅H₂, H₁⁆ :=
 begin
   suffices : ∀ H₁ H₂ : subgroup G, ⁅H₁, H₂⁆ ≤ ⁅H₂, H₁⁆, { exact le_antisymm (this _ _) (this _ _) },