From c3aa2450225e628d3af91561649018494c14b1c3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 15 Jan 2025 08:13:40 +0000
Subject: [PATCH] more

---
 Mathlib.lean                               |  2 +-
 Mathlib/GroupTheory/Commutator/Basic.lean  | 34 -----------
 Mathlib/GroupTheory/Commutator/Finite.lean | 35 -----------
 Mathlib/GroupTheory/Commutator/Lemmas.lean | 68 ++++++++++++++++++++++
 Mathlib/GroupTheory/Index.lean             |  1 +
 Mathlib/GroupTheory/Nilpotent.lean         |  2 +-
 6 files changed, 71 insertions(+), 71 deletions(-)
 delete mode 100644 Mathlib/GroupTheory/Commutator/Finite.lean
 create mode 100644 Mathlib/GroupTheory/Commutator/Lemmas.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 885a2c7635a91f..dedcc1de77b82f 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3234,7 +3234,7 @@ import Mathlib.GroupTheory.ArchimedeanDensely
 import Mathlib.GroupTheory.ClassEquation
 import Mathlib.GroupTheory.Commensurable
 import Mathlib.GroupTheory.Commutator.Basic
-import Mathlib.GroupTheory.Commutator.Finite
+import Mathlib.GroupTheory.Commutator.Lemmas
 import Mathlib.GroupTheory.CommutingProbability
 import Mathlib.GroupTheory.Complement
 import Mathlib.GroupTheory.Congruence.Basic
diff --git a/Mathlib/GroupTheory/Commutator/Basic.lean b/Mathlib/GroupTheory/Commutator/Basic.lean
index 3e9b2f49f4583d..38ed41f97f06e4 100644
--- a/Mathlib/GroupTheory/Commutator/Basic.lean
+++ b/Mathlib/GroupTheory/Commutator/Basic.lean
@@ -3,7 +3,6 @@ Copyright (c) 2021 Jordan Brown, Thomas Browning, Patrick Lutz. All rights reser
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jordan Brown, Thomas Browning, Patrick Lutz
 -/
-import Mathlib.GroupTheory.GroupAction.Quotient
 import Mathlib.GroupTheory.Subgroup.Centralizer
 import Mathlib.Tactic.Group
 
@@ -211,36 +210,3 @@ theorem mem_commutatorSet_iff : g ∈ commutatorSet G ↔ ∃ g₁ g₂ : G, ⁅
 
 theorem commutator_mem_commutatorSet : ⁅g₁, g₂⁆ ∈ commutatorSet G :=
   ⟨g₁, g₂, rfl⟩
-
-namespace Subgroup
-
-open QuotientGroup
-
-/-- Cosets of the centralizer of an element embed into the set of commutators. -/
-noncomputable def quotientCentralizerEmbedding (g : G) :
-    G ⧸ centralizer (zpowers (g : G)) ↪ commutatorSet G :=
-  ((MulAction.orbitEquivQuotientStabilizer (ConjAct G) g).trans
-            (quotientEquivOfEq (ConjAct.stabilizer_eq_centralizer g))).symm.toEmbedding.trans
-    ⟨fun x =>
-      ⟨x * g⁻¹,
-        let ⟨_, x, rfl⟩ := x
-        ⟨x, g, rfl⟩⟩,
-      fun _ _ => Subtype.ext ∘ mul_right_cancel ∘ Subtype.ext_iff.mp⟩
-
-theorem quotientCentralizerEmbedding_apply (g : G) (x : G) :
-    quotientCentralizerEmbedding g x = ⟨⁅x, g⁆, x, g, rfl⟩ :=
-  rfl
-
-/-- If `G` is generated by `S`, then the quotient by the center embeds into `S`-indexed sequences
-of commutators. -/
-noncomputable def quotientCenterEmbedding {S : Set G} (hS : closure S = ⊤) :
-    G ⧸ center G ↪ S → commutatorSet G :=
-  (quotientEquivOfEq (center_eq_infi' S hS)).toEmbedding.trans
-    ((quotientiInfEmbedding _).trans
-      (Function.Embedding.piCongrRight fun g => quotientCentralizerEmbedding (g : G)))
-
-theorem quotientCenterEmbedding_apply {S : Set G} (hS : closure S = ⊤) (g : G) (s : S) :
-    quotientCenterEmbedding hS g s = ⟨⁅g, s⁆, g, s, rfl⟩ :=
-  rfl
-
-end Subgroup
diff --git a/Mathlib/GroupTheory/Commutator/Finite.lean b/Mathlib/GroupTheory/Commutator/Finite.lean
deleted file mode 100644
index 0109ea7274cb1c..00000000000000
--- a/Mathlib/GroupTheory/Commutator/Finite.lean
+++ /dev/null
@@ -1,35 +0,0 @@
-/-
-Copyright (c) 2021 Jordan Brown, Thomas Browning, Patrick Lutz. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jordan Brown, Thomas Browning, Patrick Lutz
--/
-import Mathlib.Algebra.Group.Subgroup.Finite
-import Mathlib.GroupTheory.Commutator.Basic
-
-/-!
-The commutator of a finite direct product is contained in the direct product of the commutators.
--/
-
-
-namespace Subgroup
-
-/-- The commutator of a finite direct product is contained in the direct product of the commutators.
--/
-theorem commutator_pi_pi_of_finite {η : Type*} [Finite η] {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 fun i => ⁅H i, K i⁆ := by
-  classical
-    apply le_antisymm (commutator_pi_pi_le H K)
-    rw [pi_le_iff]
-    intro i hi
-    rw [map_commutator]
-    apply commutator_mono <;>
-      · rw [le_pi_iff]
-        intro j _hj
-        rintro _ ⟨_, ⟨x, hx, rfl⟩, rfl⟩
-        by_cases h : j = i
-        · subst h
-          simpa using hx
-        · simp [h, one_mem]
-
-end Subgroup
diff --git a/Mathlib/GroupTheory/Commutator/Lemmas.lean b/Mathlib/GroupTheory/Commutator/Lemmas.lean
new file mode 100644
index 00000000000000..06a5f8a43b0a36
--- /dev/null
+++ b/Mathlib/GroupTheory/Commutator/Lemmas.lean
@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2021 Jordan Brown, Thomas Browning, Patrick Lutz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jordan Brown, Thomas Browning, Patrick Lutz
+-/
+import Mathlib.Algebra.Group.Subgroup.Finite
+import Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
+import Mathlib.GroupTheory.Commutator.Basic
+import Mathlib.GroupTheory.GroupAction.Quotient
+
+/-!
+# Extra lemmas about commutators
+
+The commutator of a finite direct product is contained in the direct product of the commutators.
+-/
+
+open QuotientGroup
+
+namespace Subgroup
+variable {G : Type*} [Group G]
+
+/-- The commutator of a finite direct product is contained in the direct product of the commutators.
+-/
+theorem commutator_pi_pi_of_finite {η : Type*} [Finite η] {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 fun i => ⁅H i, K i⁆ := by
+  classical
+    apply le_antisymm (commutator_pi_pi_le H K)
+    rw [pi_le_iff]
+    intro i hi
+    rw [map_commutator]
+    apply commutator_mono <;>
+      · rw [le_pi_iff]
+        intro j _hj
+        rintro _ ⟨_, ⟨x, hx, rfl⟩, rfl⟩
+        by_cases h : j = i
+        · subst h
+          simpa using hx
+        · simp [h, one_mem]
+
+/-- Cosets of the centralizer of an element embed into the set of commutators. -/
+noncomputable def quotientCentralizerEmbedding (g : G) :
+    G ⧸ centralizer (zpowers (g : G)) ↪ commutatorSet G :=
+  ((MulAction.orbitEquivQuotientStabilizer (ConjAct G) g).trans
+            (quotientEquivOfEq (ConjAct.stabilizer_eq_centralizer g))).symm.toEmbedding.trans
+    ⟨fun x =>
+      ⟨x * g⁻¹,
+        let ⟨_, x, rfl⟩ := x
+        ⟨x, g, rfl⟩⟩,
+      fun _ _ => Subtype.ext ∘ mul_right_cancel ∘ Subtype.ext_iff.mp⟩
+
+theorem quotientCentralizerEmbedding_apply (g : G) (x : G) :
+    quotientCentralizerEmbedding g x = ⟨⁅x, g⁆, x, g, rfl⟩ :=
+  rfl
+
+/-- If `G` is generated by `S`, then the quotient by the center embeds into `S`-indexed sequences
+of commutators. -/
+noncomputable def quotientCenterEmbedding {S : Set G} (hS : closure S = ⊤) :
+    G ⧸ center G ↪ S → commutatorSet G :=
+  (quotientEquivOfEq (center_eq_infi' S hS)).toEmbedding.trans
+    ((quotientiInfEmbedding _).trans
+      (Function.Embedding.piCongrRight fun g => quotientCentralizerEmbedding (g : G)))
+
+theorem quotientCenterEmbedding_apply {S : Set G} (hS : closure S = ⊤) (g : G) (s : S) :
+    quotientCenterEmbedding hS g s = ⟨⁅g, s⁆, g, s, rfl⟩ :=
+  rfl
+
+end Subgroup
diff --git a/Mathlib/GroupTheory/Index.lean b/Mathlib/GroupTheory/Index.lean
index f8e36f80728c3f..631bb7bf3728c8 100644
--- a/Mathlib/GroupTheory/Index.lean
+++ b/Mathlib/GroupTheory/Index.lean
@@ -6,6 +6,7 @@ Authors: Thomas Browning
 import Mathlib.Algebra.BigOperators.GroupWithZero.Finset
 import Mathlib.Data.Finite.Card
 import Mathlib.Data.Set.Card
+import Mathlib.GroupTheory.Commutator.Lemmas
 import Mathlib.GroupTheory.Coset.Card
 import Mathlib.GroupTheory.Finiteness
 import Mathlib.GroupTheory.GroupAction.Quotient
diff --git a/Mathlib/GroupTheory/Nilpotent.lean b/Mathlib/GroupTheory/Nilpotent.lean
index 2b1d6262d8668a..7c21d2dc70564b 100644
--- a/Mathlib/GroupTheory/Nilpotent.lean
+++ b/Mathlib/GroupTheory/Nilpotent.lean
@@ -6,7 +6,7 @@ Authors: Kevin Buzzard, Ines Wright, Joachim Breitner
 import Mathlib.GroupTheory.Solvable
 import Mathlib.GroupTheory.Sylow
 import Mathlib.Algebra.Group.Subgroup.Order
-import Mathlib.GroupTheory.Commutator.Finite
+import Mathlib.GroupTheory.Commutator.Lemmas
 
 /-!