From 74e4adca921c5d7bad65f639ef1f1d3b7c07d854 Mon Sep 17 00:00:00 2001 From: Moritz Doll Date: Wed, 22 Apr 2026 17:03:51 +1000 Subject: [PATCH 1/5] initial test --- Mathlib/Algebra/Group/End.lean | 11 ++++++++--- Mathlib/GroupTheory/Perm/Support.lean | 2 +- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Group/End.lean b/Mathlib/Algebra/Group/End.lean index bdc0c224765663..243c37f9189417 100644 --- a/Mathlib/Algebra/Group/End.lean +++ b/Mathlib/Algebra/Group/End.lean @@ -12,6 +12,7 @@ public import Mathlib.Algebra.Group.Units.Equiv public import Mathlib.Data.Set.Basic public import Mathlib.Tactic.Common +public import Mathlib.Logic.Equiv.Equivify /-! # Monoids of endomorphisms, groups of automorphisms @@ -104,12 +105,15 @@ theorem mul_apply (f g : Perm α) (x) : (f * g) x = f (g x) := theorem one_apply (x) : (1 : Perm α) x = x := rfl +@[equivify, unequivify← ] theorem one_def : (1 : Perm α) = Equiv.refl α := rfl +@[equivify, unequivify← ] theorem mul_def (f g : Perm α) : f * g = g.trans f := rfl +@[equivify, unequivify← ] theorem inv_def (f : Perm α) : f⁻¹ = f.symm := rfl @@ -121,7 +125,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 +@[simp, equivify← , unequivify] +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 @@ -139,7 +144,7 @@ The assumption made here is that if you're using the group structure, you want t simp. -/ -@[simp] +/-@[simp] theorem trans_one {α : Sort*} {β : Type*} (e : α ≃ β) : e.trans (1 : Perm β) = e := Equiv.trans_refl e @@ -177,7 +182,7 @@ theorem self_trans_inv (e : Perm α) : e.trans e⁻¹ = 1 := @[simp] theorem symm_mul (e : Perm α) : e.symm * e = 1 := - Equiv.self_trans_symm e + Equiv.self_trans_symm e-/ /-! Lemmas about `Equiv.Perm.sumCongr` re-expressed via the group structure. -/ diff --git a/Mathlib/GroupTheory/Perm/Support.lean b/Mathlib/GroupTheory/Perm/Support.lean index 9c2f9763b2828c..215dcd2c1f251d 100644 --- a/Mathlib/GroupTheory/Perm/Support.lean +++ b/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, equivify] ext z by_cases hzx : z = x · simp [hzx] From 97436c684b4cf78a86ef1501a99018cccb82dc01 Mon Sep 17 00:00:00 2001 From: Moritz Doll Date: Wed, 22 Apr 2026 17:24:30 +1000 Subject: [PATCH 2/5] rename and put in attr --- Mathlib/Algebra/Group/End.lean | 11 ++++++----- Mathlib/GroupTheory/Perm/Support.lean | 2 +- Mathlib/Tactic/Attr/Register.lean | 18 ++++++++++++++++++ 3 files changed, 25 insertions(+), 6 deletions(-) diff --git a/Mathlib/Algebra/Group/End.lean b/Mathlib/Algebra/Group/End.lean index 243c37f9189417..288a70649bcec5 100644 --- a/Mathlib/Algebra/Group/End.lean +++ b/Mathlib/Algebra/Group/End.lean @@ -12,7 +12,8 @@ public import Mathlib.Algebra.Group.Units.Equiv public import Mathlib.Data.Set.Basic public import Mathlib.Tactic.Common -public import Mathlib.Logic.Equiv.Equivify +public import Mathlib.Tactic.Attr.Register + /-! # Monoids of endomorphisms, groups of automorphisms @@ -105,15 +106,15 @@ theorem mul_apply (f g : Perm α) (x) : (f * g) x = f (g x) := theorem one_apply (x) : (1 : Perm α) x = x := rfl -@[equivify, unequivify← ] +@[equiv_simps, unequiv_simps← ] theorem one_def : (1 : Perm α) = Equiv.refl α := rfl -@[equivify, unequivify← ] +@[equiv_simps, unequiv_simps← ] theorem mul_def (f g : Perm α) : f * g = g.trans f := rfl -@[equivify, unequivify← ] +@[equiv_simps, unequiv_simps← ] theorem inv_def (f : Perm α) : f⁻¹ = f.symm := rfl @@ -125,7 +126,7 @@ theorem inv_def (f : Perm α) : f⁻¹ = f.symm := @[norm_cast] lemma coe_pow (f : Perm α) (n : ℕ) : ⇑(f ^ n) = f^[n] := rfl -@[simp, equivify← , unequivify] +@[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 := diff --git a/Mathlib/GroupTheory/Perm/Support.lean b/Mathlib/GroupTheory/Perm/Support.lean index 215dcd2c1f251d..b8cfc39735c389 100644 --- a/Mathlib/GroupTheory/Perm/Support.lean +++ b/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, equivify] + · 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] diff --git a/Mathlib/Tactic/Attr/Register.lean b/Mathlib/Tactic/Attr/Register.lean index 9ffe1f41361fa6..4ff44ed36d15e1 100644 --- a/Mathlib/Tactic/Attr/Register.lean +++ b/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 From 8f25acf38d168c637ffa382fcae16cc19a05d738 Mon Sep 17 00:00:00 2001 From: Moritz Doll Date: Thu, 23 Apr 2026 00:43:55 +1000 Subject: [PATCH 3/5] fix --- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean b/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean index 4c1eedbadd05e4..5e79b4f9bec8e5 100644 --- a/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean +++ b/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] From 437195c9741fb95387b8460b6e99d3d0186a1d69 Mon Sep 17 00:00:00 2001 From: Moritz Doll Date: Thu, 23 Apr 2026 01:14:05 +1000 Subject: [PATCH 4/5] fix --- Mathlib/GroupTheory/Perm/Fin.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/GroupTheory/Perm/Fin.lean b/Mathlib/GroupTheory/Perm/Fin.lean index a217d26f12542d..503e8db32b687d 100644 --- a/Mathlib/GroupTheory/Perm/Fin.lean +++ b/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)) : From 035f8165ee97079731ab00fbfc8ece010bc7d98c Mon Sep 17 00:00:00 2001 From: Moritz Doll Date: Mon, 27 Apr 2026 08:41:34 +1000 Subject: [PATCH 5/5] deprecations --- Mathlib/Algebra/Group/End.lean | 23 +++++++++++------------ 1 file changed, 11 insertions(+), 12 deletions(-) diff --git a/Mathlib/Algebra/Group/End.lean b/Mathlib/Algebra/Group/End.lean index 288a70649bcec5..9e31de199b5151 100644 --- a/Mathlib/Algebra/Group/End.lean +++ b/Mathlib/Algebra/Group/End.lean @@ -144,46 +144,45 @@ 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-/ + Equiv.self_trans_symm e /-! Lemmas about `Equiv.Perm.sumCongr` re-expressed via the group structure. -/