From f0f8a2a4b7dacadd87a2f1af23b0d04965ce860b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Attila=20G=C3=A1sp=C3=A1r?=
 <58485900+gasparattila@users.noreply.github.com>
Date: Sat, 23 May 2026 21:44:08 +0200
Subject: [PATCH 1/7] chore(Algebra/Star): clean up `simp` lemmas about bundled
 `star` equivalences

This PR adds `.symm` lemmas for these equivalences, allowing `simp` to reduce applications of their inverses to applications of `star`.
---
 Mathlib/Algebra/Star/Basic.lean           | 19 +++++++++++----
 Mathlib/Algebra/Star/Module.lean          | 21 +++++++++++-----
 Mathlib/Analysis/CStarAlgebra/Basic.lean  |  4 ++++
 Mathlib/Topology/Algebra/Module/Star.lean | 29 ++++++++++++++++-------
 4 files changed, 54 insertions(+), 19 deletions(-)

diff --git a/Mathlib/Algebra/Star/Basic.lean b/Mathlib/Algebra/Star/Basic.lean
index d27cffae63f8f0..6c99469ddd4e4f 100644
--- a/Mathlib/Algebra/Star/Basic.lean
+++ b/Mathlib/Algebra/Star/Basic.lean
@@ -93,9 +93,14 @@ 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.star [InvolutiveStar R] : Equiv.Perm R :=
   star_involutive.toPerm _
 
+@[simp]
+theorem Equiv.star_symm [InvolutiveStar R] : (Equiv.star : R ≃ R).symm = Equiv.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 +237,15 @@ 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.star
+  map_add' := star_add
+
+@[simp]
+theorem starAddEquiv_symm [AddMonoid R] [StarAddMonoid R] :
+    (starAddEquiv : R ≃+ R).symm = starAddEquiv :=
+  rfl
 
 variable (R) in
 @[simp]
diff --git a/Mathlib/Algebra/Star/Module.lean b/Mathlib/Algebra/Star/Module.lean
index 50a3342a3e94de..ef078149edb7f4 100644
--- a/Mathlib/Algebra/Star/Module.lean
+++ b/Mathlib/Algebra/Star/Module.lean
@@ -103,14 +103,23 @@ 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, simps! -isSimp symm_apply]
+def starLinearEquiv : A ≃ₗ⋆[R] A where
+  __ := starAddEquiv
+  map_smul' := star_smul
+
+@[simp]
+theorem starLinearEquiv_symm : (starLinearEquiv R : A ≃ₗ⋆[R] A).symm = starLinearEquiv R :=
+  rfl
+
+end starLinearEquiv
 
 section SelfSkewAdjoint
 
diff --git a/Mathlib/Analysis/CStarAlgebra/Basic.lean b/Mathlib/Analysis/CStarAlgebra/Basic.lean
index e1fc9f013ff005..88549f47044a95 100644
--- a/Mathlib/Analysis/CStarAlgebra/Basic.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Basic.lean
@@ -287,6 +287,10 @@ theorem coe_starₗᵢ : (starₗᵢ 𝕜 : E → E) = star :=
 theorem starₗᵢ_apply {x : E} : starₗᵢ 𝕜 x = star x :=
   rfl
 
+@[simp]
+theorem starₗᵢ_symm : (starₗᵢ 𝕜 : E ≃ₗᵢ⋆[𝕜] E).symm = starₗᵢ 𝕜 :=
+  rfl
+
 @[simp]
 theorem starₗᵢ_toContinuousLinearEquiv :
     (starₗᵢ 𝕜 : E ≃ₗᵢ⋆[𝕜] E).toContinuousLinearEquiv = (starL 𝕜 : E ≃L⋆[𝕜] E) :=
diff --git a/Mathlib/Topology/Algebra/Module/Star.lean b/Mathlib/Topology/Algebra/Module/Star.lean
index cd3fdb6a81bf1c..d71747b183d8d2 100644
--- a/Mathlib/Topology/Algebra/Module/Star.lean
+++ b/Mathlib/Topology/Algebra/Module/Star.lean
@@ -23,25 +23,32 @@ 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]
+
 /-- 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, simps! -isSimp symm_apply]
+def starL : A ≃L⋆[R] A where
   toLinearEquiv := starLinearEquiv R
   continuous_toFun := continuous_star
   continuous_invFun := continuous_star
 
+@[simp]
+theorem starL_symm : (starL R : A ≃L⋆[R] A).symm = starL R :=
+  rfl
+
+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, simps! -isSimp symm_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
@@ -49,6 +56,12 @@ def starL' (R : Type*) {A : Type*} [CommSemiring R] [StarRing R] [TrivialStar R]
         continuous_invFun := continuous_id } :
       A ≃L⋆[R] A)
 
+@[simp]
+theorem starL'_symm : (starL' R : A ≃L[R] A).symm = starL' R :=
+  rfl
+
+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]
 

From d5a81e4fe59afa3b7463736ead4071b32bd76fd2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Attila=20G=C3=A1sp=C3=A1r?=
 <58485900+gasparattila@users.noreply.github.com>
Date: Sun, 24 May 2026 14:00:44 +0200
Subject: [PATCH 2/7] prefix symm

---
 Mathlib/Algebra/Star/Basic.lean           |  4 ++--
 Mathlib/Algebra/Star/Module.lean          |  9 +++++++--
 Mathlib/Analysis/CStarAlgebra/Basic.lean  |  2 +-
 Mathlib/Topology/Algebra/Module/Star.lean | 16 ++++++++++++----
 4 files changed, 22 insertions(+), 9 deletions(-)

diff --git a/Mathlib/Algebra/Star/Basic.lean b/Mathlib/Algebra/Star/Basic.lean
index 6c99469ddd4e4f..9e508090cd4085 100644
--- a/Mathlib/Algebra/Star/Basic.lean
+++ b/Mathlib/Algebra/Star/Basic.lean
@@ -98,7 +98,7 @@ protected def Equiv.star [InvolutiveStar R] : Equiv.Perm R :=
   star_involutive.toPerm _
 
 @[simp]
-theorem Equiv.star_symm [InvolutiveStar R] : (Equiv.star : R ≃ R).symm = Equiv.star :=
+theorem Equiv.symm_star [InvolutiveStar R] : (Equiv.star : R ≃ R).symm = Equiv.star :=
   rfl
 
 theorem eq_star_of_eq_star [InvolutiveStar R] {r s : R} (h : r = star s) : s = star r := by
@@ -243,7 +243,7 @@ def starAddEquiv [AddMonoid R] [StarAddMonoid R] : R ≃+ R where
   map_add' := star_add
 
 @[simp]
-theorem starAddEquiv_symm [AddMonoid R] [StarAddMonoid R] :
+theorem symm_starAddEquiv [AddMonoid R] [StarAddMonoid R] :
     (starAddEquiv : R ≃+ R).symm = starAddEquiv :=
   rfl
 
diff --git a/Mathlib/Algebra/Star/Module.lean b/Mathlib/Algebra/Star/Module.lean
index ef078149edb7f4..76280bbc63323c 100644
--- a/Mathlib/Algebra/Star/Module.lean
+++ b/Mathlib/Algebra/Star/Module.lean
@@ -110,13 +110,18 @@ variable (R : Type*) {A : Type*}
 
 /-- If `A` is a module over a commutative `R` with compatible actions,
 then `star` is a semilinear equivalence. -/
-@[simps! apply, simps! -isSimp symm_apply]
+@[simps! apply]
 def starLinearEquiv : A ≃ₗ⋆[R] A where
   __ := starAddEquiv
   map_smul' := star_smul
 
+@[deprecated "Use `symm_starLinearEquiv` and `starLinearEquiv_apply` instead"
+  (since := "2026-05-24")]
+theorem starLinearEquiv_symm_apply (x : A) : (starLinearEquiv R).symm x = starAddEquiv.invFun x :=
+  rfl
+
 @[simp]
-theorem starLinearEquiv_symm : (starLinearEquiv R : A ≃ₗ⋆[R] A).symm = starLinearEquiv R :=
+theorem symm_starLinearEquiv : (starLinearEquiv R : A ≃ₗ⋆[R] A).symm = starLinearEquiv R :=
   rfl
 
 end starLinearEquiv
diff --git a/Mathlib/Analysis/CStarAlgebra/Basic.lean b/Mathlib/Analysis/CStarAlgebra/Basic.lean
index 88549f47044a95..c375f7934bbad2 100644
--- a/Mathlib/Analysis/CStarAlgebra/Basic.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Basic.lean
@@ -288,7 +288,7 @@ theorem starₗᵢ_apply {x : E} : starₗᵢ 𝕜 x = star x :=
   rfl
 
 @[simp]
-theorem starₗᵢ_symm : (starₗᵢ 𝕜 : E ≃ₗᵢ⋆[𝕜] E).symm = starₗᵢ 𝕜 :=
+theorem symm_starₗᵢ : (starₗᵢ 𝕜 : E ≃ₗᵢ⋆[𝕜] E).symm = starₗᵢ 𝕜 :=
   rfl
 
 @[simp]
diff --git a/Mathlib/Topology/Algebra/Module/Star.lean b/Mathlib/Topology/Algebra/Module/Star.lean
index d71747b183d8d2..4a2a458a3a6437 100644
--- a/Mathlib/Topology/Algebra/Module/Star.lean
+++ b/Mathlib/Topology/Algebra/Module/Star.lean
@@ -30,14 +30,18 @@ variable (R : Type*) {A : Type*} [CommSemiring R] [StarRing R] [AddCommMonoid A]
 
 /-- If `A` is a topological module over a commutative `R` with compatible actions,
 then `star` is a continuous semilinear equivalence. -/
-@[simps! apply, simps! -isSimp symm_apply]
+@[simps! apply]
 def starL : A ≃L⋆[R] A where
   toLinearEquiv := starLinearEquiv R
   continuous_toFun := continuous_star
   continuous_invFun := continuous_star
 
+@[deprecated "Use `symm_starL` and `starL_apply` instead" (since := "2026-05-24")]
+theorem starL_symm_apply (x : A) : (starL R).symm x = starAddEquiv.symm x :=
+  rfl
+
 @[simp]
-theorem starL_symm : (starL R : A ≃L⋆[R] A).symm = starL R :=
+theorem symm_starL : (starL R : A ≃L⋆[R] A).symm = starL R :=
   rfl
 
 variable [TrivialStar R]
@@ -47,7 +51,7 @@ variable [TrivialStar R]
 -- 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! apply, simps! -isSimp symm_apply]
+@[simps! apply]
 def starL' : A ≃L[R] A :=
   (starL R : A ≃L⋆[R] A).trans
     ({ AddEquiv.refl A with
@@ -56,8 +60,12 @@ def starL' : A ≃L[R] A :=
         continuous_invFun := continuous_id } :
       A ≃L⋆[R] A)
 
+@[deprecated "Use `symm_starL'` and `starL'_apply` instead" (since := "2026-05-24")]
+theorem starL'_symm_apply (x : A) : (starL' R).symm x = starAddEquiv.symm x :=
+  rfl
+
 @[simp]
-theorem starL'_symm : (starL' R : A ≃L[R] A).symm = starL' R :=
+theorem symm_starL' : (starL' R : A ≃L[R] A).symm = starL' R :=
   rfl
 
 end starL

From c30a30415068d71c141bf437efe7d01357955a5d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Attila=20G=C3=A1sp=C3=A1r?=
 <58485900+gasparattila@users.noreply.github.com>
Date: Mon, 25 May 2026 21:47:42 +0200
Subject: [PATCH 3/7] Use default tactic

---
 Mathlib/Topology/Algebra/Module/Star.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Mathlib/Topology/Algebra/Module/Star.lean b/Mathlib/Topology/Algebra/Module/Star.lean
index 4a2a458a3a6437..0deea80ba0232a 100644
--- a/Mathlib/Topology/Algebra/Module/Star.lean
+++ b/Mathlib/Topology/Algebra/Module/Star.lean
@@ -33,8 +33,6 @@ then `star` is a continuous semilinear equivalence. -/
 @[simps! apply]
 def starL : A ≃L⋆[R] A where
   toLinearEquiv := starLinearEquiv R
-  continuous_toFun := continuous_star
-  continuous_invFun := continuous_star
 
 @[deprecated "Use `symm_starL` and `starL_apply` instead" (since := "2026-05-24")]
 theorem starL_symm_apply (x : A) : (starL R).symm x = starAddEquiv.symm x :=

From 6b692b4932d8c429ce5b2578b407e5215008294e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Attila=20G=C3=A1sp=C3=A1r?=
 <58485900+gasparattila@users.noreply.github.com>
Date: Wed, 3 Jun 2026 21:45:12 +0200
Subject: [PATCH 4/7] update

---
 Mathlib/Algebra/Star/Basic.lean           |  5 +++++
 Mathlib/Algebra/Star/Module.lean          | 12 +++++++++---
 Mathlib/Analysis/CStarAlgebra/Basic.lean  |  6 ++++++
 Mathlib/Topology/Algebra/Module/Star.lean | 17 +++++++++++------
 4 files changed, 31 insertions(+), 9 deletions(-)

diff --git a/Mathlib/Algebra/Star/Basic.lean b/Mathlib/Algebra/Star/Basic.lean
index 32d7fbd578f8a3..935de2e0d300f2 100644
--- a/Mathlib/Algebra/Star/Basic.lean
+++ b/Mathlib/Algebra/Star/Basic.lean
@@ -243,6 +243,11 @@ 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).toEquiv = Equiv.Perm.star :=
+  rfl
+
 @[simp]
 theorem symm_starAddEquiv [AddMonoid R] [StarAddMonoid R] :
     (starAddEquiv : R ≃+ R).symm = starAddEquiv :=
diff --git a/Mathlib/Algebra/Star/Module.lean b/Mathlib/Algebra/Star/Module.lean
index 7766e1f5aef3c0..2b343fc94591af 100644
--- a/Mathlib/Algebra/Star/Module.lean
+++ b/Mathlib/Algebra/Star/Module.lean
@@ -115,15 +115,21 @@ def starLinearEquiv : A ≃ₗ⋆[R] A where
   __ := starAddEquiv
   map_smul' := star_smul
 
-@[deprecated "Use `symm_starLinearEquiv` and `starLinearEquiv_apply` instead"
-  (since := "2026-05-24")]
-theorem starLinearEquiv_symm_apply (x : A) : (starLinearEquiv R).symm x = starAddEquiv.invFun x :=
+@[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
diff --git a/Mathlib/Analysis/CStarAlgebra/Basic.lean b/Mathlib/Analysis/CStarAlgebra/Basic.lean
index e04c16e0b304c7..d5e1f7a09a2cf0 100644
--- a/Mathlib/Analysis/CStarAlgebra/Basic.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Basic.lean
@@ -296,6 +296,12 @@ theorem starₗᵢ_toContinuousLinearEquiv :
     (starₗᵢ 𝕜 : E ≃ₗᵢ⋆[𝕜] E).toContinuousLinearEquiv = (starL 𝕜 : E ≃L⋆[𝕜] E) :=
   ContinuousLinearEquiv.ext rfl
 
+@[simp]
+theorem toLinearEquiv_starₗᵢ :
+    (starₗᵢ 𝕜 : E ≃ₗᵢ⋆[𝕜] E).toContinuousLinearEquiv = starLinearEquiv :=
+  rfl
+
+
 end starₗᵢ
 
 namespace StarSubalgebra
diff --git a/Mathlib/Topology/Algebra/Module/Star.lean b/Mathlib/Topology/Algebra/Module/Star.lean
index 0deea80ba0232a..9a3b8b14c78854 100644
--- a/Mathlib/Topology/Algebra/Module/Star.lean
+++ b/Mathlib/Topology/Algebra/Module/Star.lean
@@ -28,20 +28,25 @@ 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! apply]
 def starL : A ≃L⋆[R] A where
   toLinearEquiv := starLinearEquiv R
 
-@[deprecated "Use `symm_starL` and `starL_apply` instead" (since := "2026-05-24")]
-theorem starL_symm_apply (x : A) : (starL R).symm x = starAddEquiv.symm x :=
+@[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
@@ -58,14 +63,14 @@ def starL' : A ≃L[R] A :=
         continuous_invFun := continuous_id } :
       A ≃L⋆[R] A)
 
-@[deprecated "Use `symm_starL'` and `starL'_apply` instead" (since := "2026-05-24")]
-theorem starL'_symm_apply (x : A) : (starL' R).symm x = starAddEquiv.symm x :=
-  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
+
 end starL
 
 variable (R : Type*) (A : Type*) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A]

From 057003fc9e73b40593d7c69796cfe493f4573b02 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Attila=20G=C3=A1sp=C3=A1r?=
 <58485900+gasparattila@users.noreply.github.com>
Date: Wed, 3 Jun 2026 22:04:36 +0200
Subject: [PATCH 5/7] fix

---
 Mathlib/Analysis/CStarAlgebra/Basic.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Mathlib/Analysis/CStarAlgebra/Basic.lean b/Mathlib/Analysis/CStarAlgebra/Basic.lean
index d5e1f7a09a2cf0..74f68d6a3f2aaf 100644
--- a/Mathlib/Analysis/CStarAlgebra/Basic.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Basic.lean
@@ -297,11 +297,9 @@ theorem starₗᵢ_toContinuousLinearEquiv :
   ContinuousLinearEquiv.ext rfl
 
 @[simp]
-theorem toLinearEquiv_starₗᵢ :
-    (starₗᵢ 𝕜 : E ≃ₗᵢ⋆[𝕜] E).toContinuousLinearEquiv = starLinearEquiv :=
+theorem toLinearEquiv_starₗᵢ : (starₗᵢ 𝕜 : E ≃ₗᵢ⋆[𝕜] E).toLinearEquiv = starLinearEquiv :=
   rfl
 
-
 end starₗᵢ
 
 namespace StarSubalgebra

From 39a07ce387116cbb4dd68ee4f1a7ce44f7dc483e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Attila=20G=C3=A1sp=C3=A1r?=
 <58485900+gasparattila@users.noreply.github.com>
Date: Wed, 3 Jun 2026 22:11:26 +0200
Subject: [PATCH 6/7] fix

---
 Mathlib/Analysis/CStarAlgebra/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Analysis/CStarAlgebra/Basic.lean b/Mathlib/Analysis/CStarAlgebra/Basic.lean
index 74f68d6a3f2aaf..d8a77466ce59d5 100644
--- a/Mathlib/Analysis/CStarAlgebra/Basic.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Basic.lean
@@ -297,7 +297,7 @@ theorem starₗᵢ_toContinuousLinearEquiv :
   ContinuousLinearEquiv.ext rfl
 
 @[simp]
-theorem toLinearEquiv_starₗᵢ : (starₗᵢ 𝕜 : E ≃ₗᵢ⋆[𝕜] E).toLinearEquiv = starLinearEquiv :=
+theorem toLinearEquiv_starₗᵢ : (starₗᵢ 𝕜 : E ≃ₗᵢ⋆[𝕜] E).toLinearEquiv = starLinearEquiv 𝕜 :=
   rfl
 
 end starₗᵢ

From e648de2d58fb3424897b8f44ca85ef9471ba0c4f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Attila=20G=C3=A1sp=C3=A1r?=
 <58485900+gasparattila@users.noreply.github.com>
Date: Wed, 3 Jun 2026 22:32:23 +0200
Subject: [PATCH 7/7] fix

---
 Mathlib/Algebra/Star/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/Star/Basic.lean b/Mathlib/Algebra/Star/Basic.lean
index 935de2e0d300f2..f37f1dc5d07931 100644
--- a/Mathlib/Algebra/Star/Basic.lean
+++ b/Mathlib/Algebra/Star/Basic.lean
@@ -245,7 +245,7 @@ def starAddEquiv [AddMonoid R] [StarAddMonoid R] : R ≃+ R where
 
 @[simp]
 theorem toEquiv_starAddEquiv [AddMonoid R] [StarAddMonoid R] :
-    (starAddEquiv : R ≃+ R).toEquiv = Equiv.Perm.star :=
+    (starAddEquiv : R ≃+ R) = (Equiv.Perm.star : R ≃ R) :=
   rfl
 
 @[simp]