feat: auxiliary lemmas for Artin and braid groups

Add small lemmas to existing files, in preparation for the Artin groups and braid groups PRs:

- `Commute.mul_pow_eq_one`: for commuting elements with `a ^ m = 1` and `b ^ m = 1`
- `Equiv.Perm.swap_conjugate`: braid relation for adjacent transpositions
- `Equiv.Perm.swap_mul_swap_comm_of_disjoint`: disjoint transpositions commute
- `@[grind =]` attributes on `Perm.mul_apply`, `Perm.one_apply`
- `Perm.pow_add_one_apply`
- `Subgroup.normalClosure_singleton_one`
- `FreeGroup.ofList` and associated lemmas
- `FreeGroup.freeGroupUnitMulEquivInt`
- `PresentedGroup.instUniqueOfIsEmpty`
- `CoxeterMatrix.Aₙ_adjacent`, `CoxeterMatrix.Aₙ_far`

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: kim-em

Mathlib/Algebra/Group/Commute/Defs.lean

@@ -164,6 +164,13 @@ theorem pow_pow_self (a : M) (m n : ℕ) : Commute (a ^ m) (a ^ n) :=
   | 0 => by rw [pow_zero, pow_zero, pow_zero, one_mul]
   | n + 1 => by simp only [pow_succ', h.mul_pow n, ← mul_assoc, (h.pow_left n).right_comm]
 
+/-- For commuting elements satisfying `a ^ m = 1` and `b ^ m = 1`, we have `(a * b) ^ m = 1`. -/
+@[to_additive /-- For commuting elements satisfying `m • a = 0` and `m • b = 0`,
+we have `m • (a + b) = 0`. -/]
+theorem mul_pow_eq_one (h : Commute a b) {m : ℕ} (ha : a ^ m = 1) (hb : b ^ m = 1) :
+    (a * b) ^ m = 1 := by
+  rw [h.mul_pow, ha, hb, one_mul]
+
 end Monoid
 
 section DivisionMonoid

Mathlib/Algebra/Group/End.lean

@@ -98,12 +98,27 @@ def equivUnitsEnd : Perm α ≃* Units (Function.End α) where
 def _root_.MonoidHom.toHomPerm {G : Type*} [Group G] (f : G →* Function.End α) : G →* Perm α :=
   equivUnitsEnd.symm.toMonoidHom.comp f.toHomUnits
 
+@[grind =]
 theorem mul_apply (f g : Perm α) (x) : (f * g) x = f (g x) :=
   rfl
 
+@[grind =]
 theorem one_apply (x) : (1 : Perm α) x = x :=
   rfl
 
+@[grind =]
+theorem pow_add_one_apply (f : Perm α) (n : ℕ) (x : α) :
+    (f ^ (n + 1)) x = (f^n) (f x) := by
+  rfl
+
+@[deprecated symm_apply_apply (since := "2025-08-16")]
+theorem inv_apply_self (f : Perm α) (x) : f⁻¹ (f x) = x :=
+  f.symm_apply_apply x
+
+@[deprecated apply_symm_apply (since := "2025-08-16")]
+theorem apply_inv_self (f : Perm α) (x) : f (f⁻¹ x) = x :=
+  f.apply_symm_apply x
+
 theorem one_def : (1 : Perm α) = Equiv.refl α :=
   rfl
 
@@ -575,6 +590,19 @@ theorem swap_mul_swap_mul_swap {x y z : α} (hxy : x ≠ y) (hxz : x ≠ z) :
   nth_rewrite 3 [← swap_inv]
   rw [← swap_apply_apply, swap_apply_left, swap_apply_of_ne_of_ne hxy hxz, swap_comm]
 
+/-- Conjugating `swap b c` by `swap a b` equals conjugating `swap a b` by `swap b c`.
+This is also known as the braid relation for adjacent transpositions. -/
+theorem swap_conjugate {a b c : α} (hab : a ≠ b) (hbc : b ≠ c) :
+    swap a b * swap b c * swap a b = swap b c * swap a b * swap b c := by
+  grind
+
+/-- Disjoint transpositions commute: if `{a, b}` and `{c, d}` are disjoint,
+then `swap a b` and `swap c d` commute. -/
+theorem swap_mul_swap_comm_of_disjoint {a b c d : α}
+    (hac : a ≠ c) (had : a ≠ d) (hbc : b ≠ c) (hbd : b ≠ d) :
+    swap a b * swap c d = swap c d * swap a b := by
+  grind
+
 end Swap
 
 section Group

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -550,6 +550,10 @@ theorem normalClosure_closure_eq_normalClosure {s : Set G} :
 lemma normalClosure_empty : normalClosure (∅ : Set G) = (⊥ : Subgroup G) := by
   rw [← normalClosure_closure_eq_normalClosure, closure_empty, normalClosure_eq_self]
 
+@[simp]
+theorem normalClosure_singleton_one : normalClosure ({1} : Set G) = ⊥ :=
+  le_antisymm (normalClosure_le_normal (by simp)) bot_le
+
 /-- The normal core of a subgroup `H` is the largest normal subgroup of `G` contained in `H`,
 as shown by `Subgroup.normalCore_eq_iSup`. -/
 @[to_additive /-- The normal core of an additive subgroup `H` is the largest normal additive

Mathlib/GroupTheory/Coxeter/Matrix.lean

@@ -114,6 +114,16 @@ protected def A : CoxeterMatrix (Fin n) where
 
 @[deprecated (since := "2026-03-25")] alias Aₙ := CoxeterMatrix.A
 
+theorem Aₙ_adjacent (n : ℕ) (i j : Fin n) (h : (i : ℕ) + 1 = j ∨ (j : ℕ) + 1 = i) :
+    (Aₙ n) i j = 3 := by
+  simp only [Aₙ, Fin.ext_iff, Matrix.of_apply]
+  grind
+
+theorem Aₙ_far (n : ℕ) (i j : Fin n) (h1 : i ≠ j) (h2 : (i : ℕ) + 1 ≠ j)
+    (h3 : (j : ℕ) + 1 ≠ i) : (Aₙ n) i j = 2 := by
+  simp only [Aₙ, Matrix.of_apply]
+  grind
+
 /-- The Coxeter matrix of type Bₙ.
 
 The corresponding Coxeter-Dynkin diagram is:

Mathlib/GroupTheory/FreeGroup/Basic.lean

@@ -908,6 +908,35 @@ theorem sum.map_inv : sum x⁻¹ = -sum x :=
 
 end Sum
 
+section OfList
+
+variable {α : Type*}
+
+/-- Convert a list of generators to an element of the free group by taking the product of `of`
+applied to each element. -/
+@[to_additive /-- Convert a list of generators to an element of the additive free group by taking
+the sum of `of` applied to each element. -/]
+def ofList (l : List α) : FreeGroup α := (l.map of).prod
+
+@[to_additive (attr := simp)]
+theorem ofList_nil : ofList ([] : List α) = 1 := rfl
+
+@[to_additive (attr := simp)]
+theorem ofList_singleton (x : α) : ofList [x] = of x := by simp [ofList]
+
+@[to_additive]
+theorem ofList_cons (x : α) (l : List α) : ofList (x :: l) = of x * ofList l := by simp [ofList]
+
+@[to_additive]
+theorem ofList_concat (l : List α) (x : α) : ofList (l.concat x) = ofList l * of x := by
+  simp [ofList]
+
+@[to_additive]
+theorem ofList_append (l₁ l₂ : List α) : ofList (l₁ ++ l₂) = ofList l₁ * ofList l₂ := by
+  simp [ofList]
+
+end OfList
+
 /-- The bijection between the free group on the empty type, and a type with one element. -/
 @[to_additive
   (attr := deprecated "Use `Equiv.ofUnique (FreeGroup Empty) Unit` instead,

Mathlib/GroupTheory/PresentedGroup.lean

@@ -163,4 +163,12 @@ end ToGroup
 instance (rels : Set (FreeGroup α)) : Inhabited (PresentedGroup rels) :=
   ⟨1⟩
 
+/-- A presented group with no generators is trivial. -/
+instance instUniqueOfIsEmpty [IsEmpty α] (rels : Set (FreeGroup α)) :
+    Unique (PresentedGroup rels) where
+  default := 1
+  uniq x := by
+    induction x using PresentedGroup.induction_on with
+    | _ z => exact congrArg _ (Unique.eq_default z)
+
 end PresentedGroup