refactor: deprecate StarAlgHomClass and similar as they just duplic…

…ate `StarHomClass` (#16591)

When `FunLike` (and `EquivLike`) was unbundled from all the hom classes, it was necessary to make `StarAlgHomClass` (and similarly `NonUnitalStarAlgHomClass` and `StarAlgEquivClass`) and its un-starred counterparts an argument instead of extending that class. The net effect of this was that these classes became duplicates of `StarHomClass` with stricter type class assumptions.

This PR deprecates all of these classes in favor of `StarHomClass` alone.

Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

@@ -97,7 +97,7 @@ variable [CommSemiring R]
 variable [NonUnitalNonAssocSemiring A] [Module R A] [Star A]
 variable [NonUnitalNonAssocSemiring B] [Module R B] [Star B]
 variable [NonUnitalNonAssocSemiring C] [Module R C] [Star C]
-variable [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B]
+variable [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B]
 
 instance instSetLike : SetLike (NonUnitalStarSubalgebra R A) A where
   coe {s} := s.carrier
@@ -398,7 +398,7 @@ variable [CommSemiring R]
 variable [NonUnitalNonAssocSemiring A] [Module R A] [Star A]
 variable [NonUnitalNonAssocSemiring B] [Module R B] [Star B]
 variable [NonUnitalNonAssocSemiring C] [Module R C] [Star C]
-variable [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B]
+variable [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B]
 
 /-- Range of an `NonUnitalAlgHom` as a `NonUnitalStarSubalgebra`. -/
 protected def range (φ : F) : NonUnitalStarSubalgebra R B where
@@ -471,7 +471,7 @@ variable [CommSemiring R]
 variable [NonUnitalSemiring A] [Module R A] [Star A]
 variable [NonUnitalSemiring B] [Module R B] [Star B]
 variable [NonUnitalSemiring C] [Module R C] [Star C]
-variable [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B]
+variable [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B]
 
 /-- Restrict a non-unital star algebra homomorphism with a left inverse to an algebra isomorphism
 to its range.
@@ -600,7 +600,7 @@ namespace NonUnitalStarAlgebra
 variable [CommSemiring R] [StarRing R]
 variable [NonUnitalSemiring A] [StarRing A] [Module R A]
 variable [NonUnitalSemiring B] [StarRing B] [Module R B]
-variable [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B]
+variable [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B]
 
 section StarSubAlgebraA
 
@@ -831,7 +831,7 @@ open NonUnitalStarAlgebra
 variable [CommSemiring R]
 variable [NonUnitalSemiring A] [StarRing A] [Module R A]
 variable [NonUnitalSemiring B] [StarRing B] [Module R B]
-variable [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B]
+variable [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B]
 variable (S : NonUnitalStarSubalgebra R A)
 
 section StarSubalgebra

Mathlib/Algebra/Star/StarAlgHom.lean

@@ -64,6 +64,7 @@ add_decl_doc NonUnitalStarAlgHom.toNonUnitalAlgHom
 
 /-- `NonUnitalStarAlgHomClass F R A B` asserts `F` is a type of bundled non-unital ⋆-algebra
 homomorphisms from `A` to `B`. -/
+@[deprecated StarHomClass (since := "2024-09-08")]
 class NonUnitalStarAlgHomClass (F : Type*) (R A B : outParam Type*)
   [Monoid R] [Star A] [Star B] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B]
   [DistribMulAction R A] [DistribMulAction R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B]
@@ -76,17 +77,18 @@ variable [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A]
 variable [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B]
 variable [FunLike F A B] [NonUnitalAlgHomClass F R A B]
 
-/-- Turn an element of a type `F` satisfying `NonUnitalStarAlgHomClass F R A B` into an actual
-`NonUnitalStarAlgHom`. This is declared as the default coercion from `F` to `A →⋆ₙₐ[R] B`. -/
+/-- Turn an element of a type `F` satisfying `NonUnitalAlgHomClass F R A B` and `StarHomClass F A B`
+into an actual `NonUnitalStarAlgHom`. This is declared as the default coercion from `F` to
+`A →⋆ₙₐ[R] B`. -/
 @[coe]
-def toNonUnitalStarAlgHom [NonUnitalStarAlgHomClass F R A B] (f : F) : A →⋆ₙₐ[R] B :=
+def toNonUnitalStarAlgHom [StarHomClass F A B] (f : F) : A →⋆ₙₐ[R] B :=
   { (f : A →ₙₐ[R] B) with
     map_star' := map_star f }
 
-instance [NonUnitalStarAlgHomClass F R A B] : CoeTC F (A →⋆ₙₐ[R] B) :=
+instance [StarHomClass F A B] : CoeTC F (A →⋆ₙₐ[R] B) :=
   ⟨toNonUnitalStarAlgHom⟩
 
-instance [NonUnitalStarAlgHomClass F R A B] : NonUnitalStarRingHomClass F A B :=
+instance [StarHomClass F A B] : NonUnitalStarRingHomClass F A B :=
   NonUnitalStarRingHomClass.mk
 
 end NonUnitalStarAlgHomClass
@@ -111,7 +113,7 @@ instance : NonUnitalAlgHomClass (A →⋆ₙₐ[R] B) R A B where
   map_zero f := f.map_zero'
   map_mul f := f.map_mul'
 
-instance : NonUnitalStarAlgHomClass (A →⋆ₙₐ[R] B) R A B where
+instance : StarHomClass (A →⋆ₙₐ[R] B) A B where
   map_star f := f.map_star'
 
 -- Porting note: in mathlib3 we didn't need the `Simps.apply` hint.
@@ -123,7 +125,7 @@ initialize_simps_projections NonUnitalStarAlgHom
 
 @[simp]
 protected theorem coe_coe {F : Type*} [FunLike F A B] [NonUnitalAlgHomClass F R A B]
-    [NonUnitalStarAlgHomClass F R A B] (f : F) :
+    [StarHomClass F A B] (f : F) :
     ⇑(f : A →⋆ₙₐ[R] B) = f := rfl
 
 @[simp]
@@ -304,34 +306,21 @@ by forgetting the interaction with the star operation. -/
 add_decl_doc StarAlgHom.toAlgHom
 
 /-- `StarAlgHomClass F R A B` states that `F` is a type of ⋆-algebra homomorphisms.
-
 You should also extend this typeclass when you extend `StarAlgHom`. -/
+@[deprecated StarHomClass (since := "2024-09-08")]
 class StarAlgHomClass (F : Type*) (R A B : outParam Type*)
     [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B]
     [FunLike F A B] [AlgHomClass F R A B] extends StarHomClass F A B : Prop
-
--- Porting note: no longer needed
----- `R` becomes a metavariable but that's fine because it's an `outParam`
---attribute [nolint dangerousInstance] StarAlgHomClass.toStarHomClass
-
 namespace StarAlgHomClass
 
-variable (F R A B : Type*)
-
--- See note [lower instance priority]
-instance (priority := 100) toNonUnitalStarAlgHomClass [CommSemiring R] [Semiring A] [Algebra R A]
-  [Star A] [Semiring B] [Algebra R B] [Star B] [FunLike F A B] [AlgHomClass F R A B]
-  [StarAlgHomClass F R A B] :
-  NonUnitalStarAlgHomClass F R A B :=
-  { }
+variable {F R A B : Type*}
 
 variable [CommSemiring R] [Semiring A] [Algebra R A] [Star A]
 variable [Semiring B] [Algebra R B] [Star B] [FunLike F A B] [AlgHomClass F R A B]
-variable [StarAlgHomClass F R A B]
+variable [StarHomClass F A B]
 
-variable {F R A B} in
-/-- Turn an element of a type `F` satisfying `StarAlgHomClass F R A B` into an actual
-`StarAlgHom`. This is declared as the default coercion from `F` to `A →⋆ₐ[R] B`. -/
+/-- Turn an element of a type `F` satisfying `AlgHomClass F R A B` and `StarHomClass F A B` into an
+actual `StarAlgHom`. This is declared as the default coercion from `F` to `A →⋆ₐ[R] B`. -/
 @[coe]
 def toStarAlgHom (f : F) : A →⋆ₐ[R] B :=
   { (f : A →ₐ[R] B) with
@@ -358,12 +347,12 @@ instance : AlgHomClass (A →⋆ₐ[R] B) R A B where
   map_zero f := f.map_zero'
   commutes f := f.commutes'
 
-instance : StarAlgHomClass (A →⋆ₐ[R] B) R A B where
+instance : StarHomClass (A →⋆ₐ[R] B) A B where
   map_star f := f.map_star'
 
 @[simp]
 protected theorem coe_coe {F : Type*} [FunLike F A B] [AlgHomClass F R A B]
-    [StarAlgHomClass F R A B] (f : F) :
+    [StarHomClass F A B] (f : F) :
     ⇑(f : A →⋆ₐ[R] B) = f :=
   rfl
 
@@ -660,69 +649,44 @@ class NonUnitalAlgEquivClass (F : Type*) (R A B : outParam Type*)
 
 /-- `StarAlgEquivClass F R A B` asserts `F` is a type of bundled ⋆-algebra equivalences between
 `A` and `B`.
-
 You should also extend this typeclass when you extend `StarAlgEquiv`. -/
+@[deprecated StarHomClass (since := "2024-09-08")]
 class StarAlgEquivClass (F : Type*) (R A B : outParam Type*)
   [Add A] [Mul A] [SMul R A] [Star A] [Add B] [Mul B] [SMul R B]
   [Star B] [EquivLike F A B] [NonUnitalAlgEquivClass F R A B] : Prop where
   /-- By definition, a ⋆-algebra equivalence preserves the `star` operation. -/
-  map_star : ∀ (f : F) (a : A), f (star a) = star (f a)
-
--- Porting note: no longer needed
----- `R` becomes a metavariable but that's fine because it's an `outParam`
--- attribute [nolint dangerousInstance] StarAlgEquivClass.toRingEquivClass
+  protected map_star : ∀ (f : F) (a : A), f (star a) = star (f a)
 
 namespace StarAlgEquivClass
 
--- See note [lower instance priority]
-instance (priority := 50) {F R A B : Type*} [Add A] [Mul A] [SMul R A] [Star A] [Add B] [Mul B]
-    [SMul R B] [Star B] [EquivLike F A B] [NonUnitalAlgEquivClass F R A B]
-    [hF : StarAlgEquivClass F R A B] :
-    StarHomClass F A B :=
-  { hF with }
-
 -- See note [lower instance priority]
 instance (priority := 100) {F R A B : Type*} [Monoid R] [NonUnitalNonAssocSemiring A]
     [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [EquivLike F A B]
     [NonUnitalAlgEquivClass F R A B] :
     NonUnitalAlgHomClass F R A B :=
   { }
 
--- See note [lower instance priority]
-instance (priority := 100) {F R A B : Type*} [Monoid R] [NonUnitalNonAssocSemiring A]
-    [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B]
-    [EquivLike F A B] [NonUnitalAlgEquivClass F R A B] [StarAlgEquivClass F R A B] :
-    NonUnitalStarAlgHomClass F R A B :=
-  { }
-
 -- See note [lower instance priority]
 instance (priority := 100) instAlgHomClass (F R A B : Type*) [CommSemiring R] [Semiring A]
     [Algebra R A] [Semiring B] [Algebra R B] [EquivLike F A B] [NonUnitalAlgEquivClass F R A B] :
     AlgEquivClass F R A B :=
   { commutes := fun f r => by simp only [Algebra.algebraMap_eq_smul_one, map_smul, map_one] }
 
--- See note [lower instance priority]
-instance (priority := 100) instStarAlgHomClass (F R A B : Type*) [CommSemiring R] [Semiring A]
-    [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [EquivLike F A B]
-    [NonUnitalAlgEquivClass F R A B] [StarAlgEquivClass F R A B] :
-    StarAlgHomClass F R A B :=
-  { }
-
-/-- Turn an element of a type `F` satisfying `StarAlgEquivClass F R A B` into an actual
-`StarAlgEquiv`. This is declared as the default coercion from `F` to `A ≃⋆ₐ[R] B`. -/
+/-- Turn an element of a type `F` satisfying `AlgEquivClass F R A B` and `StarHomClass F A B` into
+an actual `StarAlgEquiv`. This is declared as the default coercion from `F` to `A ≃⋆ₐ[R] B`. -/
 @[coe]
 def toStarAlgEquiv {F R A B : Type*} [Add A] [Mul A] [SMul R A] [Star A] [Add B] [Mul B] [SMul R B]
-    [Star B] [EquivLike F A B] [NonUnitalAlgEquivClass F R A B] [StarAlgEquivClass F R A B]
+    [Star B] [EquivLike F A B] [NonUnitalAlgEquivClass F R A B] [StarHomClass F A B]
     (f : F) : A ≃⋆ₐ[R] B :=
   { (f : A ≃+* B) with
     map_star' := map_star f
     map_smul' := map_smul f}
 
-/-- Any type satisfying `StarAlgEquivClass` can be cast into `StarAlgEquiv` via
+/-- Any type satisfying `AlgEquivClass` and `StarHomClass` can be cast into `StarAlgEquiv` via
 `StarAlgEquivClass.toStarAlgEquiv`. -/
 instance instCoeHead {F R A B : Type*} [Add A] [Mul A] [SMul R A] [Star A] [Add B] [Mul B]
-    [SMul R B] [Star B] [EquivLike F A B] [NonUnitalAlgEquivClass F R A B]
-    [StarAlgEquivClass F R A B] : CoeHead F (A ≃⋆ₐ[R] B) :=
+    [SMul R B] [Star B] [EquivLike F A B] [NonUnitalAlgEquivClass F R A B] [StarHomClass F A B] :
+    CoeHead F (A ≃⋆ₐ[R] B) :=
   ⟨toStarAlgEquiv⟩
 
 end StarAlgEquivClass
@@ -749,7 +713,7 @@ instance : NonUnitalAlgEquivClass (A ≃⋆ₐ[R] B) R A B where
   map_add f := f.map_add'
   map_smulₛₗ := map_smul'
 
-instance : StarAlgEquivClass (A ≃⋆ₐ[R] B) R A B where
+instance : StarHomClass (A ≃⋆ₐ[R] B) A B where
   map_star := map_star'
 
 /-- Helper instance for cases where the inference via `EquivLike` is too hard. -/
@@ -889,8 +853,8 @@ section Bijective
 variable {F G R A B : Type*} [Monoid R]
 variable [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A]
 variable [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B]
-variable [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B]
-variable [FunLike G B A] [NonUnitalAlgHomClass G R B A] [NonUnitalStarAlgHomClass G R B A]
+variable [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B]
+variable [FunLike G B A] [NonUnitalAlgHomClass G R B A] [StarHomClass G B A]
 
 /-- If a (unital or non-unital) star algebra morphism has an inverse, it is an isomorphism of
 star algebras. -/

Mathlib/Algebra/Star/Subalgebra.lean

@@ -657,7 +657,7 @@ section
 variable [StarModule R A]
 
 theorem ext_adjoin {s : Set A} [FunLike F (adjoin R s) B]
-    [AlgHomClass F R (adjoin R s) B] [StarAlgHomClass F R (adjoin R s) B] {f g : F}
+    [AlgHomClass F R (adjoin R s) B] [StarHomClass F (adjoin R s) B] {f g : F}
     (h : ∀ x : adjoin R s, (x : A) ∈ s → f x = g x) : f = g := by
   refine DFunLike.ext f g fun a =>
     adjoin_induction' (p := fun y => f y = g y) a (fun x hx => ?_) (fun r => ?_)
@@ -669,15 +669,15 @@ theorem ext_adjoin {s : Set A} [FunLike F (adjoin R s) B]
   · simp only [map_star, hx]
 
 theorem ext_adjoin_singleton {a : A} [FunLike F (adjoin R ({a} : Set A)) B]
-    [AlgHomClass F R (adjoin R ({a} : Set A)) B] [StarAlgHomClass F R (adjoin R ({a} : Set A)) B]
+    [AlgHomClass F R (adjoin R ({a} : Set A)) B] [StarHomClass F (adjoin R ({a} : Set A)) B]
     {f g : F} (h : f ⟨a, self_mem_adjoin_singleton R a⟩ = g ⟨a, self_mem_adjoin_singleton R a⟩) :
     f = g :=
   ext_adjoin fun x hx =>
     (show x = ⟨a, self_mem_adjoin_singleton R a⟩ from
           Subtype.ext <| Set.mem_singleton_iff.mp hx).symm ▸
       h
 
-variable [FunLike F A B] [AlgHomClass F R A B] [StarAlgHomClass F R A B] (f g : F)
+variable [FunLike F A B] [AlgHomClass F R A B] [StarHomClass F A B] (f g : F)
 
 /-- The equalizer of two star `R`-algebra homomorphisms. -/
 def equalizer : StarSubalgebra R A :=

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean

@@ -435,7 +435,7 @@ variable {F R S A B : Type*} {p : A → Prop} {q : B → Prop}
   [Module S A] [Module S B] [IsScalarTower R S A] [IsScalarTower R S B]
   [NonUnitalContinuousFunctionalCalculus R p] [NonUnitalContinuousFunctionalCalculus R q]
   [UniqueNonUnitalContinuousFunctionalCalculus R B] [FunLike F A B] [NonUnitalAlgHomClass F S A B]
-  [NonUnitalStarAlgHomClass F S A B]
+  [StarHomClass F A B]
 
 include S in
 /-- Non-unital star algebra homomorphisms commute with the non-unital continuous functional
@@ -484,7 +484,7 @@ variable {F R S A B : Type*} {p : A → Prop} {q : B → Prop}
   [CommSemiring S] [Algebra R S] [Algebra S A] [Algebra S B] [IsScalarTower R S A]
   [IsScalarTower R S B] [ContinuousFunctionalCalculus R p] [ContinuousFunctionalCalculus R q]
   [UniqueContinuousFunctionalCalculus R B] [FunLike F A B] [AlgHomClass F S A B]
-  [StarAlgHomClass F S A B]
+  [StarHomClass F A B]
 
 include S in
 /-- Star algebra homomorphisms commute with the continuous functional calculus. -/

Mathlib/Analysis/CStarAlgebra/Spectrum.lean

@@ -226,7 +226,7 @@ variable [NonUnitalNormedRing A] [CompleteSpace A] [StarRing A] [CStarRing A]
 variable [NormedSpace ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A]
 variable [NonUnitalNormedRing B] [CompleteSpace B] [StarRing B] [CStarRing B]
 variable [NormedSpace ℂ B] [IsScalarTower ℂ B B] [SMulCommClass ℂ B B] [StarModule ℂ B]
-variable [FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [NonUnitalStarAlgHomClass F ℂ A B]
+variable [FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B]
 
 open Unitization
 
@@ -267,7 +267,7 @@ variable {F A B : Type*} [NormedRing A] [NormedSpace ℂ A] [SMulCommClass ℂ A
 variable [IsScalarTower ℂ A A] [CompleteSpace A] [StarRing A] [CStarRing A] [StarModule ℂ A]
 variable [NormedRing B] [NormedSpace ℂ B] [SMulCommClass ℂ B B] [IsScalarTower ℂ B B]
 variable [CompleteSpace B] [StarRing B] [CStarRing B] [StarModule ℂ B] [EquivLike F A B]
-variable [NonUnitalAlgEquivClass F ℂ A B] [StarAlgEquivClass F ℂ A B]
+variable [NonUnitalAlgEquivClass F ℂ A B] [StarHomClass F A B]
 
 lemma nnnorm_map (φ : F) (a : A) : ‖φ a‖₊ = ‖a‖₊ :=
   le_antisymm (NonUnitalStarAlgHom.nnnorm_apply_le φ a) <| by
@@ -292,7 +292,7 @@ open scoped ComplexStarModule
 variable {F A : Type*} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A]
   [CStarRing A] [StarModule ℂ A] [FunLike F A ℂ] [hF : AlgHomClass F ℂ A ℂ]
 
-/-- This instance is provided instead of `StarAlgHomClass` to avoid type class inference loops.
+/-- This instance is provided instead of `StarHomClass` to avoid type class inference loops.
 See note [lower instance priority] -/
 noncomputable instance (priority := 100) Complex.instStarHomClass : StarHomClass F A ℂ where
   map_star φ a := by
@@ -309,13 +309,13 @@ noncomputable instance (priority := 100) Complex.instStarHomClass : StarHomClass
 
 /-- This is not an instance to avoid type class inference loops. See
 `WeakDual.Complex.instStarHomClass`. -/
-lemma _root_.AlgHomClass.instStarAlgHomClass : StarAlgHomClass F ℂ A ℂ :=
+lemma _root_.AlgHomClass.instStarHomClass : StarHomClass F A ℂ :=
   { WeakDual.Complex.instStarHomClass, hF with }
 
 namespace CharacterSpace
 
-noncomputable instance instStarAlgHomClass : StarAlgHomClass (characterSpace ℂ A) ℂ A ℂ :=
-  { AlgHomClass.instStarAlgHomClass with }
+noncomputable instance instStarHomClass : StarHomClass (characterSpace ℂ A) A ℂ :=
+  { AlgHomClass.instStarHomClass with }
 
 end CharacterSpace
 

Mathlib/Topology/Algebra/StarSubalgebra.lean

@@ -146,7 +146,7 @@ theorem _root_.StarAlgHom.ext_topologicalClosure [T2Space B] {S : StarSubalgebra
 
 theorem _root_.StarAlgHomClass.ext_topologicalClosure [T2Space B] {F : Type*}
     {S : StarSubalgebra R A} [FunLike F S.topologicalClosure B]
-    [AlgHomClass F R S.topologicalClosure B] [StarAlgHomClass F R S.topologicalClosure B] {φ ψ : F}
+    [AlgHomClass F R S.topologicalClosure B] [StarHomClass F S.topologicalClosure B] {φ ψ : F}
     (hφ : Continuous φ) (hψ : Continuous ψ) (h : ∀ x : S,
         φ (inclusion (le_topologicalClosure S) x) = ψ ((inclusion (le_topologicalClosure S)) x)) :
     φ = ψ := by
@@ -242,12 +242,12 @@ theorem induction_on {x y : A}
     exact mul u (subset_closure hu_mem) v (subset_closure hv_mem) (hu hu_mem) (hv hv_mem)
 
 theorem starAlgHomClass_ext [T2Space B] {F : Type*} {a : A}
-    [FunLike F (elementalStarAlgebra R a) B] [AlgHomClass F R _ B] [StarAlgHomClass F R _ B]
+    [FunLike F (elementalStarAlgebra R a) B] [AlgHomClass F R _ B] [StarHomClass F _ B]
     {φ ψ : F} (hφ : Continuous φ)
     (hψ : Continuous ψ) (h : φ ⟨a, self_mem R a⟩ = ψ ⟨a, self_mem R a⟩) : φ = ψ := by
   -- Note: help with unfolding `elementalStarAlgebra`
-  have : StarAlgHomClass F R (↥(topologicalClosure (adjoin R {a}))) B :=
-    inferInstanceAs (StarAlgHomClass F R (elementalStarAlgebra R a) B)
+  have : StarHomClass F (↥(topologicalClosure (adjoin R {a}))) B :=
+    inferInstanceAs (StarHomClass F (elementalStarAlgebra R a) B)
   refine StarAlgHomClass.ext_topologicalClosure hφ hψ fun x => ?_
   refine adjoin_induction' x ?_ ?_ ?_ ?_ ?_
   exacts [fun y hy => by simpa only [Set.mem_singleton_iff.mp hy] using h, fun r => by