feat(GroupTheory/Commutator/Basic): more commutator identities (leanprover-community#39892)

From [Wikipedia](https://en.wikipedia.org/wiki/Commutator#Identities_(group_theory))

Author: SnirBroshi

Mathlib/GroupTheory/Commutator/Basic.lean

@@ -32,6 +32,10 @@ open scoped commutatorElement
 variable {G G' F : Type*} [Group G] [Group G'] [FunLike F G G'] [MonoidHomClass F G G']
 variable (f : F) {g₁ g₂ g₃ g : G}
 
+@[to_additive]
+theorem conj_eq_commutatorElement_mul : MulAut.conj g₁ g₂ = ⁅g₁, g₂⁆ * g₂ := by
+  simp [commutatorElement_def]
+
 @[to_additive]
 theorem commutatorElement_eq_one_iff_mul_comm : ⁅g₁, g₂⁆ = 1 ↔ g₁ * g₂ = g₂ * g₁ := by
   rw [commutatorElement_def, mul_inv_eq_one, mul_inv_eq_iff_eq_mul]
@@ -80,6 +84,46 @@ theorem commutatorElement_mul_right_eq_mul_conj (a b c : G) :
     ⁅a, b * c⁆ = ⁅a, b⁆ * b * ⁅a, c⁆ * b⁻¹ := by
   simp [mul_assoc, commutatorElement_def]
 
+@[to_additive]
+theorem commutatorElement_inv_left (a b : G) : ⁅a⁻¹, b⁆ = a⁻¹ * ⁅b, a⁆ * a := by
+  simp [mul_assoc, commutatorElement_def]
+
+@[to_additive]
+theorem commutatorElement_inv_right (a b : G) : ⁅a, b⁻¹⁆ = b⁻¹ * ⁅b, a⁆ * b := by
+  simp [mul_assoc, commutatorElement_def]
+
+/-- **The Hall-Witt identity** -/
+@[to_additive /-- **The Hall-Witt identity** -/]
+theorem conj_commutatorElement_left_commutatorElement_mul (a b c : G) :
+    a * ⁅⁅a⁻¹, b⁆, c⁆ * a⁻¹ * c * ⁅⁅c⁻¹, a⁆, b⁆ * c⁻¹ * b * ⁅⁅b⁻¹, c⁆, a⁆ * b⁻¹ = 1 := by
+  simp [mul_assoc, commutatorElement_def]
+
+/-- **The Hall-Witt identity** -/
+@[to_additive /-- **The Hall-Witt identity** -/]
+theorem conj_commutatorElement_right_commutatorElement_mul (a b c : G) :
+    b * ⁅a, ⁅b⁻¹, c⁆⁆ * b⁻¹ * c * ⁅b, ⁅c⁻¹, a⁆⁆ * c⁻¹ * a * ⁅c, ⁅a⁻¹, b⁆⁆ * a⁻¹ = 1 := by
+  simp [mul_assoc, commutatorElement_def]
+
+/-- **The Hall-Witt identity** -/
+@[to_additive /-- **The Hall-Witt identity** -/]
+theorem commutatorElement_commutatorElement_conj_mul (a b c : G) :
+    ⁅⁅a, b⁆, b * c * b⁻¹⁆ * ⁅⁅b, c⁆, c * a * c⁻¹⁆ * ⁅⁅c, a⁆, a * b * a⁻¹⁆ = 1 := by
+  simp [mul_assoc, commutatorElement_def]
+
+/-- **The Hall-Witt identity** -/
+@[to_additive /-- **The Hall-Witt identity** -/]
+theorem commutatorElement_conj_commutatorElement_mul (a b c : G) :
+    ⁅a * b * a⁻¹, ⁅c, a⁆⁆ * ⁅c * a * c⁻¹, ⁅b, c⁆⁆ * ⁅b * c * b⁻¹, ⁅a, b⁆⁆ = 1 := by
+  simp [mul_assoc, commutatorElement_def]
+
+@[to_additive]
+theorem commutatorElement_mul_left_mul (a b c : G) : ⁅a * b, c⁆ * ⁅c * a, b⁆ * ⁅b * c, a⁆ = 1 := by
+  simp [mul_assoc, commutatorElement_def]
+
+@[to_additive]
+theorem commutatorElement_mul_right_mul (a b c : G) : ⁅a, b * c⁆ * ⁅b, c * a⁆ * ⁅c, a * b⁆ = 1 := by
+  simp [mul_assoc, commutatorElement_def]
+
 namespace Subgroup
 
 /-- The commutator of two subgroups `H₁` and `H₂`. -/