address review comments

- Rename Aₙ_far → A_not_adjacent, Aₙ_adjacent → A_adjacent (use CoxeterMatrix.A)
- Add @[simp] to mul_apply, one_apply, pow_add_one_apply
- Add @[to_additive] to normalClosure_singleton_one
- Remove ofList section (per eric-wieser's suggestion to use FreeMonoid API instead)

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: kim-em

Mathlib/Algebra/Group/End.lean

@@ -98,15 +98,15 @@ 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 =]
+@[simp, grind =]
 theorem mul_apply (f g : Perm α) (x) : (f * g) x = f (g x) :=
   rfl
 
-@[grind =]
+@[simp, grind =]
 theorem one_apply (x) : (1 : Perm α) x = x :=
   rfl
 
-@[grind =]
+@[simp, grind =]
 theorem pow_add_one_apply (f : Perm α) (n : ℕ) (x : α) :
     (f ^ (n + 1)) x = (f^n) (f x) := by
   rfl

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -550,7 +550,7 @@ 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]
+@[to_additive (attr := simp)]
 theorem normalClosure_singleton_one : normalClosure ({1} : Set G) = ⊥ :=
   le_antisymm (normalClosure_le_normal (by simp)) bot_le
 

Mathlib/GroupTheory/Coxeter/Matrix.lean

@@ -114,14 +114,14 @@ 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]
+theorem A_adjacent (n : ℕ) (i j : Fin n) (h : (i : ℕ) + 1 = j ∨ (j : ℕ) + 1 = i) :
+    (CoxeterMatrix.A n) i j = 3 := by
+  simp only [CoxeterMatrix.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]
+theorem A_not_adjacent (n : ℕ) (i j : Fin n) (h1 : i ≠ j) (h2 : (i : ℕ) + 1 ≠ j)
+    (h3 : (j : ℕ) + 1 ≠ i) : (CoxeterMatrix.A n) i j = 2 := by
+  simp only [CoxeterMatrix.A, Matrix.of_apply]
   grind
 
 /-- The Coxeter matrix of type Bₙ.

Mathlib/GroupTheory/FreeGroup/Basic.lean

@@ -908,35 +908,6 @@ 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,