[Merged by Bors] - chore(Algebra/Star): clean up simp lemmas about bundled star equivalences

Mathlib/Algebra/Star/Basic.lean

@@ -93,9 +93,15 @@ theorem star_inj [InvolutiveStar R] {x y : R} : star x = star y ↔ x = y :=
   star_injective.eq_iff
 
 /-- `star` as an equivalence when it is involutive. -/
+@[simps! apply]
 protected def Equiv.Perm.star [InvolutiveStar R] : Equiv.Perm R :=
   star_involutive.toPerm _
 
+@[simp]
+theorem Equiv.Perm.symm_star [InvolutiveStar R] :
+    (Equiv.Perm.star : R ≃ R).symm = Equiv.Perm.star :=
+  rfl
+
 theorem eq_star_of_eq_star [InvolutiveStar R] {r s : R} (h : r = star s) : s = star r := by
   simp [h]
 
@@ -232,11 +238,20 @@ export StarAddMonoid (star_add)
 attribute [simp] star_add
 
 /-- `star` as an `AddEquiv` -/
-@[simps apply]
-def starAddEquiv [AddMonoid R] [StarAddMonoid R] : R ≃+ R :=
-  { InvolutiveStar.star_involutive.toPerm star with
-    toFun := star
-    map_add' := star_add }
+@[simps! apply]
+def starAddEquiv [AddMonoid R] [StarAddMonoid R] : R ≃+ R where
+  toEquiv := Equiv.Perm.star
+  map_add' := star_add
+
+@[simp]
+theorem toEquiv_starAddEquiv [AddMonoid R] [StarAddMonoid R] :
+    (starAddEquiv : R ≃+ R) = (Equiv.Perm.star : R ≃ R) :=
+  rfl
+
+@[simp]
+theorem symm_starAddEquiv [AddMonoid R] [StarAddMonoid R] :
+    (starAddEquiv : R ≃+ R).symm = starAddEquiv :=
+  rfl
 
 variable (R) in
 @[simp]

Mathlib/Algebra/Star/Module.lean

@@ -103,14 +103,34 @@ instance StarAddMonoid.toStarModuleRat [AddCommGroup R] [Module ℚ R] [StarAddM
 
 end SMulLemmas
 
+section starLinearEquiv
+
+variable (R : Type*) {A : Type*}
+  [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A]
+
 /-- If `A` is a module over a commutative `R` with compatible actions,
 then `star` is a semilinear equivalence. -/
-@[simps]
-def starLinearEquiv (R : Type*) {A : Type*} [CommSemiring R] [StarRing R] [AddCommMonoid A]
-    [StarAddMonoid A] [Module R A] [StarModule R A] : A ≃ₗ⋆[R] A :=
-  { starAddEquiv with
-    toFun := star
-    map_smul' := star_smul }
+@[simps! apply]
+def starLinearEquiv : A ≃ₗ⋆[R] A where
+  __ := starAddEquiv
+  map_smul' := star_smul
+
+@[simp]
+theorem toAddEquiv_starLinearEquiv :
+    (starLinearEquiv R : A ≃ₗ⋆[R] A).toAddEquiv = starAddEquiv :=
+  rfl
+
+@[simp]
+theorem symm_starLinearEquiv : (starLinearEquiv R : A ≃ₗ⋆[R] A).symm = starLinearEquiv R :=
+  rfl
+
+@[deprecated "Use `symm_starLinearEquiv` and `starLinearEquiv_apply` instead"
+  (since := "2026-06-03")]
+theorem starLinearEquiv_symm_apply (x : A) :
+    (starLinearEquiv R).symm x = starAddEquiv.invFun x := by
+  simp
+
+end starLinearEquiv
 
 section SelfSkewAdjoint
 

Mathlib/Analysis/CStarAlgebra/Basic.lean

@@ -287,11 +287,19 @@ theorem coe_starₗᵢ : (starₗᵢ 𝕜 : E → E) = star :=
 theorem starₗᵢ_apply {x : E} : starₗᵢ 𝕜 x = star x :=
   rfl
 
+@[simp]
+theorem symm_starₗᵢ : (starₗᵢ 𝕜 : E ≃ₗᵢ⋆[𝕜] E).symm = starₗᵢ 𝕜 :=
+  rfl
+
 @[simp]
 theorem starₗᵢ_toContinuousLinearEquiv :
     (starₗᵢ 𝕜 : E ≃ₗᵢ⋆[𝕜] E).toContinuousLinearEquiv = (starL 𝕜 : E ≃L⋆[𝕜] E) :=
   ContinuousLinearEquiv.ext rfl
 
+@[simp]
+theorem toLinearEquiv_starₗᵢ : (starₗᵢ 𝕜 : E ≃ₗᵢ⋆[𝕜] E).toLinearEquiv = starLinearEquiv 𝕜 :=
+  rfl
+
 end starₗᵢ
 
 namespace StarSubalgebra

Mathlib/Topology/Algebra/Module/Star.lean

@@ -23,32 +23,56 @@ notation:25 M " →L⋆[" R "] " M₂ => ContinuousLinearMap (starRingEnd R) M M
 @[inherit_doc]
 notation:50 M " ≃L⋆[" R "] " M₂ => ContinuousLinearEquiv (starRingEnd R) M M₂
 
+section starL
+
+variable (R : Type*) {A : Type*} [CommSemiring R] [StarRing R] [AddCommMonoid A]
+    [StarAddMonoid A] [Module R A] [StarModule R A] [TopologicalSpace A] [ContinuousStar A]
+
+set_option backward.defeqAttrib.useBackward true in
 /-- If `A` is a topological module over a commutative `R` with compatible actions,
 then `star` is a continuous semilinear equivalence. -/
-@[simps!]
-def starL (R : Type*) {A : Type*} [CommSemiring R] [StarRing R] [AddCommMonoid A]
-    [StarAddMonoid A] [Module R A] [StarModule R A] [TopologicalSpace A] [ContinuousStar A] :
-    A ≃L⋆[R] A where
+@[simps! apply]
+def starL : A ≃L⋆[R] A where
   toLinearEquiv := starLinearEquiv R
-  continuous_toFun := continuous_star
-  continuous_invFun := continuous_star
+
+@[simp]
+theorem toLinearEquiv_starL : (starL R : A ≃L⋆[R] A).toLinearEquiv = starLinearEquiv R :=
+  rfl
+
+@[simp]
+theorem symm_starL : (starL R : A ≃L⋆[R] A).symm = starL R :=
+  rfl
+
+@[deprecated "Use `symm_starL` and `starL_apply` instead" (since := "2026-06-03")]
+theorem starL_symm_apply (x : A) : (starL R).symm x = starAddEquiv.symm x := by
+  simp
+
+variable [TrivialStar R]
 
 -- TODO: this could be replaced with something like `(starL R).restrict_scalarsₛₗ h` if we
 -- implemented the idea in
 -- https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Star-semilinear.20maps.20are.20semilinear.20when.20star.20is.20trivial/near/359557835
 /-- If `A` is a topological module over a commutative `R` with trivial star and compatible actions,
 then `star` is a continuous linear equivalence. -/
-@[simps!]
-def starL' (R : Type*) {A : Type*} [CommSemiring R] [StarRing R] [TrivialStar R] [AddCommMonoid A]
-    [StarAddMonoid A] [Module R A] [StarModule R A] [TopologicalSpace A] [ContinuousStar A] :
-    A ≃L[R] A :=
+@[simps! apply]
+def starL' : A ≃L[R] A :=
   (starL R : A ≃L⋆[R] A).trans
     ({ AddEquiv.refl A with
         map_smul' := fun r a => by simp
         continuous_toFun := continuous_id
         continuous_invFun := continuous_id } :
       A ≃L⋆[R] A)
 
+@[simp]
+theorem symm_starL' : (starL' R : A ≃L[R] A).symm = starL' R :=
+  rfl
+
+@[deprecated "Use `symm_starL'` and `starL'_apply` instead" (since := "2026-06-03")]
+theorem starL'_symm_apply (x : A) : (starL' R).symm x = starAddEquiv.symm x := by
+  simp
+
+end starL
+
 variable (R : Type*) (A : Type*) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A]
   [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible (2 : R)] [TopologicalSpace A]