feat: custom simp sets for translating between Equiv and algebraic notation

Mathlib/Algebra/Group/End.lean

@@ -12,6 +12,8 @@ public import Mathlib.Algebra.Group.Units.Equiv
 public import Mathlib.Data.Set.Basic
 public import Mathlib.Tactic.Common
 
+public import Mathlib.Tactic.Attr.Register
+
 /-!
 # Monoids of endomorphisms, groups of automorphisms
 
@@ -104,12 +106,15 @@ theorem mul_apply (f g : Perm α) (x) : (f * g) x = f (g x) :=
 theorem one_apply (x) : (1 : Perm α) x = x :=
   rfl
 
+@[equiv_simps, unequiv_simps← ]
 theorem one_def : (1 : Perm α) = Equiv.refl α :=
   rfl
 
+@[equiv_simps, unequiv_simps← ]
 theorem mul_def (f g : Perm α) : f * g = g.trans f :=
   rfl
 
+@[equiv_simps, unequiv_simps← ]
 theorem inv_def (f : Perm α) : f⁻¹ = f.symm :=
   rfl
 
@@ -121,7 +126,8 @@ theorem inv_def (f : Perm α) : f⁻¹ = f.symm :=
 
 @[norm_cast] lemma coe_pow (f : Perm α) (n : ℕ) : ⇑(f ^ n) = f^[n] := rfl
 
-@[simp] lemma iterate_eq_pow (f : Perm α) (n : ℕ) : f^[n] = ⇑(f ^ n) := rfl
+@[equiv_simps← , unequiv_simps]
+lemma iterate_eq_pow (f : Perm α) (n : ℕ) : f^[n] = ⇑(f ^ n) := rfl
 
 theorem eq_inv_iff_eq {f : Perm α} {x y : α} : x = f⁻¹ y ↔ f x = y :=
   f.eq_symm_apply
@@ -138,44 +144,43 @@ theorem zpow_apply_comm {α : Type*} (σ : Perm α) (m n : ℤ) {x : α} :
 The assumption made here is that if you're using the group structure, you want to preserve it after
 simp. -/
 
-
-@[simp]
+@[deprecated "use `equiv_simps` simpset instead" (since := "2026-04-27")]
 theorem trans_one {α : Sort*} {β : Type*} (e : α ≃ β) : e.trans (1 : Perm β) = e :=
   Equiv.trans_refl e
 
-@[simp]
+@[deprecated "use `equiv_simps` simpset instead" (since := "2026-04-27")]
 theorem mul_refl (e : Perm α) : e * Equiv.refl α = e :=
   Equiv.trans_refl e
 
-@[simp]
+@[deprecated "use `equiv_simps` simpset instead" (since := "2026-04-27")]
 theorem one_symm : (1 : Perm α).symm = 1 :=
   rfl
 
-@[simp]
+@[deprecated "use `equiv_simps` simpset instead" (since := "2026-04-27")]
 theorem refl_inv : (Equiv.refl α : Perm α)⁻¹ = 1 :=
   rfl
 
-@[simp]
+@[deprecated "use `equiv_simps` simpset instead" (since := "2026-04-27")]
 theorem one_trans {α : Type*} {β : Sort*} (e : α ≃ β) : (1 : Perm α).trans e = e :=
   rfl
 
-@[simp]
+@[deprecated "use `equiv_simps` simpset instead" (since := "2026-04-27")]
 theorem refl_mul (e : Perm α) : Equiv.refl α * e = e :=
   rfl
 
-@[simp]
+@[deprecated "use `equiv_simps` simpset instead" (since := "2026-04-27")]
 theorem inv_trans_self (e : Perm α) : e⁻¹.trans e = 1 :=
   Equiv.symm_trans_self e
 
-@[simp]
+@[deprecated "use `equiv_simps` simpset instead" (since := "2026-04-27")]
 theorem mul_symm (e : Perm α) : e * e.symm = 1 :=
   Equiv.symm_trans_self e
 
-@[simp]
+@[deprecated "use `equiv_simps` simpset instead" (since := "2026-04-27")]
 theorem self_trans_inv (e : Perm α) : e.trans e⁻¹ = 1 :=
   Equiv.self_trans_symm e
 
-@[simp]
+@[deprecated "use `equiv_simps` simpset instead" (since := "2026-04-27")]
 theorem symm_mul (e : Perm α) : e.symm * e = 1 :=
   Equiv.self_trans_symm e
 

Mathlib/GroupTheory/Perm/Cycle/Concrete.lean

@@ -215,7 +215,7 @@ theorem length_toList_pos_of_mem_support (h : x ∈ p.support) : 0 < length (toL
   zero_lt_two.trans_le (two_le_length_toList_iff_mem_support.mpr h)
 
 theorem getElem_toList (n : ℕ) (hn : n < length (toList p x)) :
-    (toList p x)[n] = (p ^ n) x := by simp [toList]
+    (toList p x)[n] = (p ^ n) x := by simp [toList, equiv_simps]
 
 theorem toList_getElem_zero (h : x ∈ p.support) :
     (toList p x)[0]'(length_toList_pos_of_mem_support _ _ h) = x := by simp [toList]

Mathlib/GroupTheory/Perm/Fin.lean

@@ -29,7 +29,7 @@ def Equiv.Perm.decomposeFin {n : ℕ} : Perm (Fin n.succ) ≃ Fin n.succ × Perm
 @[simp]
 theorem Equiv.Perm.decomposeFin_symm_of_refl {n : ℕ} (p : Fin (n + 1)) :
     Equiv.Perm.decomposeFin.symm (p, Equiv.refl _) = swap 0 p := by
-  simp [Equiv.Perm.decomposeFin, Equiv.permCongr_def]
+  simp [Equiv.Perm.decomposeFin, Equiv.permCongr_def, equiv_simps]
 
 @[simp]
 theorem Equiv.Perm.decomposeFin_symm_of_one {n : ℕ} (p : Fin (n + 1)) :

Mathlib/GroupTheory/Perm/Support.lean

@@ -481,7 +481,7 @@ theorem support_swap_mul_ge_support_diff (f : Perm α) (x y : α) :
 theorem support_swap_mul_eq (f : Perm α) (x : α) (h : f (f x) ≠ x) :
     (swap x (f x) * f).support = f.support \ {x} := by
   by_cases hx : f x = x
-  · simp [hx, sdiff_singleton_eq_erase, notMem_support.mpr hx, erase_eq_of_notMem]
+  · simp [hx, sdiff_singleton_eq_erase, notMem_support.mpr hx, erase_eq_of_notMem, equiv_simps]
   ext z
   by_cases hzx : z = x
   · simp [hzx]

Mathlib/Tactic/Attr/Register.lean

@@ -53,6 +53,24 @@ register_simp_attr qify_simps
 which gives a well-behaved subtraction. -/
 register_simp_attr zify_simps
 
+/--
+The simpset `equiv_simps` translates algebraic formulations of equivalence relations into the
+standard equivalence definitions, so for example `1 : Equiv α α` becomes `Equiv.refl α` and
+`a * b` becomes `b.trans a`.
+
+The dual simpset is `unequiv_simps`.
+-/
+register_simp_attr equiv_simps
+
+/--
+The simpset `unequiv_simps` translates the standard formulations of equivalence relations to
+algebraic, so for example `Equiv.refl α` becomes `1 : Equiv α α` and
+`b.trans a` becomes `a * b`.
+
+The dual simpset is `equiv_simps`.
+-/
+register_simp_attr unequiv_simps
+
 /--
 The simpset `mfld_simps` records several simp lemmas that are
 especially useful in manifolds. It is a subset of the whole set of simp lemmas, but it makes it