refactor: @[simp] for e.conj f x = e (f (e.symm x)) (#34183)

This came up while reviewing PR #33615.

Not only `LinearMap` & `LinearEquiv` but also other bundled maps often simplify when applied. So it's natural to have a simp lemma for `e.conj f x`.

This simp lemma has lower priority, because it should rewrite after unapplied `conj` lemmas for performance reason (e.g. `e.conj LinearMap.id x => LinearMap.id x` => `x` rather than `e.conj LinearMap.id x => e (LinearMap.id (e.symm x)) => e (e.symm x) => x`)

Co-authored-by: Komyyy <pol_tta@outlook.jp>

Author: Komyyy

Mathlib/Algebra/Algebra/Equiv.lean

@@ -551,15 +551,15 @@ theorem trans_toLinearMap (f : A₁ ≃ₐ[R] A₂) (g : A₂ ≃ₐ[R] A₃) :
 
 @[simp] theorem linearEquivConj_mulLeft (f : A₁ ≃ₐ[R] A₂) (x : A₁) :
     f.toLinearEquiv.conj (.mulLeft R x) = .mulLeft R (f x) := by
-  ext; simp [LinearEquiv.conj_apply]
+  ext; simp
 
 @[simp] theorem linearEquivConj_mulRight (f : A₁ ≃ₐ[R] A₂) (x : A₁) :
     f.toLinearEquiv.conj (.mulRight R x) = .mulRight R (f x) := by
-  ext; simp [LinearEquiv.conj_apply]
+  ext; simp
 
 @[simp] theorem linearEquivConj_mulLeftRight (f : A₁ ≃ₐ[R] A₂) (x : A₁ × A₁) :
     f.toLinearEquiv.conj (.mulLeftRight R x) = .mulLeftRight R (Prod.map f f x) := by
-  cases x; ext; simp [LinearEquiv.conj_apply]
+  cases x; ext; simp
 
 /-- Promotes a bijective algebra homomorphism to an algebra equivalence. -/
 noncomputable def ofBijective (f : A₁ →ₐ[R] A₂) (hf : Function.Bijective f) : A₁ ≃ₐ[R] A₂ :=

Mathlib/Algebra/Module/Equiv/Basic.lean

@@ -683,6 +683,10 @@ theorem conj_apply (e : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : Module.End R₁'
     e.conj f = ((↑e : M₁' →ₛₗ[σ₁'₂'] M₂').comp f).comp (e.symm : M₂' →ₛₗ[σ₂'₁'] M₁') :=
   rfl
 
+-- Note this has lower `simp` priority for performance reasons, so that we rewrite as
+-- `e.conj LinearMap.id x => LinearMap.id x` => `x` rather than
+-- `e.conj LinearMap.id x => e (LinearMap.id (e.symm x)) => e (e.symm x) => x`.
+@[simp 900]
 theorem conj_apply_apply (e : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : Module.End R₁' M₁') (x : M₂') :
     e.conj f x = e (f (e.symm x)) :=
   rfl
@@ -700,14 +704,13 @@ theorem conj_trans (e₁ : M₁' ≃ₛₗ[σ₁'₂'] M₂') (e₂ : M₂' ≃
   rfl
 
 @[simp] lemma conj_conj_symm (e : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : Module.End R₂' M₂') :
-    e.conj (e.symm.conj f) = f := by ext; simp [conj_apply]
+    e.conj (e.symm.conj f) = f := by ext; simp
 
 @[simp] lemma conj_symm_conj (e : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : Module.End R₁' M₁') :
-    e.symm.conj (e.conj f) = f := by ext; simp [conj_apply]
+    e.symm.conj (e.conj f) = f := by ext; simp
 
 @[simp]
-theorem conj_id (e : M₁' ≃ₛₗ[σ₁'₂'] M₂') : e.conj LinearMap.id = LinearMap.id := by
-  simp [conj_apply]
+theorem conj_id (e : M₁' ≃ₛₗ[σ₁'₂'] M₂') : e.conj LinearMap.id = LinearMap.id := by ext; simp
 
 @[simp]
 theorem conj_refl (f : Module.End R M) : (refl R M).conj f = f := rfl

Mathlib/LinearAlgebra/Charpoly/ToMatrix.lean

@@ -79,7 +79,7 @@ lemma LinearEquiv.charpoly_conj (e : M₁ ≃ₗ[R] M₂) (φ : Module.End R M
   rw [← LinearMap.charpoly_toMatrix φ b, ← LinearMap.charpoly_toMatrix (e.conj φ) (b.map e)]
   congr 1
   ext i j : 1
-  simp [LinearMap.toMatrix, LinearEquiv.conj_apply]
+  simp [LinearMap.toMatrix]
 
 namespace Matrix
 

Mathlib/LinearAlgebra/RootSystem/Defs.lean

@@ -379,7 +379,7 @@ lemma pairing_reflectionPerm (i j k : ι) :
 lemma toPerfPair_conj_reflection :
     P.toPerfPair.conj (P.reflection i) = (P.coreflection i).toLinearMap.dualMap := by
   ext f n
-  simp [LinearEquiv.conj_apply, reflection_apply, coreflection_apply, mul_comm (f <| P.coroot i)]
+  simp [reflection_apply, coreflection_apply, mul_comm (f <| P.coroot i)]
 
 @[simp]
 lemma toPerfPair_flip_conj_coreflection :

Mathlib/RingTheory/Trace/Basic.lean

@@ -175,7 +175,7 @@ lemma Algebra.trace_eq_of_algEquiv {A B C : Type*} [CommRing A] [CommRing B] [Co
     [Algebra A B] [Algebra A C] (e : B ≃ₐ[A] C) (x) :
     Algebra.trace A C (e x) = Algebra.trace A B x := by
   simp_rw [Algebra.trace_apply, ← LinearMap.trace_conj' _ e.toLinearEquiv]
-  congr; ext; simp [LinearEquiv.conj_apply]
+  congr; ext; simp
 
 lemma Algebra.trace_eq_of_ringEquiv {A B C : Type*} [CommRing A] [CommRing B] [CommRing C]
     [Algebra A C] [Algebra B C] (e : A ≃+* B) (he : (algebraMap B C).comp e = algebraMap A C) (x) :