feat: add missing instance StarAlgEquivClass.toAlgEquivClass (#5160)

Mathlib/Algebra/Star/StarAlgHom.lean

@@ -8,9 +8,10 @@ Authors: Jireh Loreaux
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
+import Mathlib.Algebra.Algebra.Equiv
+import Mathlib.Algebra.Algebra.Prod
 import Mathlib.Algebra.Hom.NonUnitalAlg
 import Mathlib.Algebra.Star.Prod
-import Mathlib.Algebra.Algebra.Prod
 
 /-!
 # Morphisms of star algebras
@@ -743,6 +744,15 @@ instance (priority := 100) (F R A B : Type _) [CommSemiring R] [Semiring A]
     map_zero := map_zero
     commutes := fun f r => by simp only [Algebra.algebraMap_eq_smul_one, map_smul, map_one] }
 
+-- See note [lower instance priority]
+instance (priority := 100) toAlgEquivClass {F R A B : Type _} [CommSemiring R]
+    [Ring A] [Ring B] [Algebra R A] [Algebra R B] [Star A] [Star B] [StarAlgEquivClass F R A B] :
+    AlgEquivClass F R A B :=
+  { StarAlgEquivClass.toRingEquivClass,
+    StarAlgEquivClass.instStarAlgHomClass F R A B with
+    coe := fun f => f
+    inv := fun f => EquivLike.inv f }
+
 end StarAlgEquivClass
 
 namespace StarAlgEquiv