refactor(group_theory/commutator): Move and golf commutator_le (#12599

)

This PR golfs `commutator_le` and moves it earlier in the file so that it can be used earlier.

This PR will conflict with #12600, so don't merge them simultaneously (bors d+ might be better).

src/group_theory/commutator.lean

@@ -62,6 +62,10 @@ lemma commutator_mem_commutator {H₁ H₂ : subgroup G} {g₁ g₂ : G} (h₁ :
   ⁅g₁, g₂⁆ ∈ ⁅H₁, H₂⁆ :=
 subset_closure ⟨g₁, h₁, g₂, h₂, rfl⟩
 
+lemma commutator_le {H₁ H₂ H₃ : subgroup G} :
+  ⁅H₁, H₂⁆ ≤ H₃ ↔ ∀ (g₁ ∈ H₁) (g₂ ∈ H₂), ⁅g₁, g₂⁆ ∈ H₃ :=
+H₃.closure_le.trans ⟨λ h a b c d, h ⟨a, b, c, d, rfl⟩, λ h g ⟨a, b, c, d, h_eq⟩, h_eq ▸ h a b c d⟩
+
 instance commutator_normal (H₁ H₂ : subgroup G) [h₁ : H₁.normal]
   [h₂ : H₂.normal] : normal ⁅H₁, H₂⁆ :=
 begin
@@ -88,17 +92,6 @@ lemma commutator_def' (H₁ H₂ : subgroup G) [H₁.normal] [H₂.normal] :
   ⁅H₁, H₂⁆ = normal_closure {g | ∃ (g₁ ∈ H₁) (g₂ ∈ H₂), ⁅g₁, g₂⁆ = g} :=
 le_antisymm closure_le_normal_closure (normal_closure_le_normal subset_closure)
 
-lemma commutator_le (H₁ H₂ : subgroup G) (K : subgroup G) :
-  ⁅H₁, H₂⁆ ≤ K ↔ ∀ (p ∈ H₁) (q ∈ H₂), ⁅p, q⁆ ∈ K :=
-begin
-  rw [subgroup.commutator, closure_le],
-  split,
-  { intros h p hp q hq,
-    exact h ⟨p, hp, q, hq, rfl⟩, },
-  { rintros h x ⟨p, hp, q, hq, rfl⟩,
-    exact h p hp q hq, }
-end
-
 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 _ _) },
@@ -111,7 +104,7 @@ begin
 end
 
 lemma commutator_le_right (H₁ H₂ : subgroup G) [h : normal H₂] : ⁅H₁, H₂⁆ ≤ H₂ :=
-(commutator_le _ _ _).mpr (λ g₁ h₁ g₂ h₂, H₂.mul_mem (h.conj_mem g₂ h₂ g₁) (H₂.inv_mem h₂))
+commutator_le.mpr (λ g₁ h₁ g₂ h₂, H₂.mul_mem (h.conj_mem g₂ h₂ g₁) (H₂.inv_mem h₂))
 
 lemma commutator_le_left (H₁ H₂ : subgroup G) [h : normal H₁] : ⁅H₁, H₂⁆ ≤ H₁ :=
 commutator_comm H₂ H₁ ▸ commutator_le_right H₂ H₁
@@ -159,7 +152,7 @@ See `commutator_pi_pi_of_fintype` for equality given `fintype η`.
 lemma commutator_pi_pi_le {η : Type*} {Gs : η → Type*} [∀ i, group (Gs i)]
   (H K : Π i, subgroup (Gs i)) :
   ⁅subgroup.pi set.univ H, subgroup.pi set.univ K⁆ ≤ subgroup.pi set.univ (λ i, ⁅H i, K i⁆) :=
-(commutator_le _ _ _).mpr $ λ p hp q hq i hi, commutator_mem_commutator (hp i hi) (hq i hi)
+commutator_le.mpr $ λ p hp q hq i hi, commutator_mem_commutator (hp i hi) (hq i hi)
 
 /-- The commutator of a finite direct product is contained in the direct product of the commutators.
 -/

src/group_theory/nilpotent.lean

@@ -319,12 +319,7 @@ end
 lemma descending_central_series_ge_lower (H : ℕ → subgroup G)
   (hH : is_descending_central_series H) : ∀ n : ℕ, lower_central_series G n ≤ H n
 | 0 := hH.1.symm ▸ le_refl ⊤
-| (n + 1) := begin
-  specialize descending_central_series_ge_lower n,
-  apply (commutator_le _ _ _).2,
-  intros x hx q _,
-  exact hH.2 x n (descending_central_series_ge_lower hx) q,
-end
+| (n + 1) := commutator_le.mpr (λ x hx q _, hH.2 x n (descending_central_series_ge_lower n hx) q)
 
 /-- A group is nilpotent if and only if its lower central series eventually reaches
   the trivial subgroup. -/