[Merged by Bors] - chore: standardise names for coercions from morphism classes to morphisms

Mathlib/Algebra/Algebra/Spectrum/Quasispectrum.lean

@@ -316,7 +316,7 @@ lemma AlgEquiv.quasispectrum_eq {F R A B : Type*} [CommSemiring R] [NonUnitalRin
   let : Star A := ⟨id⟩
   let : Star B := ⟨id⟩
   have : StarHomClass F A B := ⟨fun _ _ ↦ rfl⟩
-  let e := StarAlgEquivClass.toStarAlgEquiv f
+  let e := StarAlgEquiv.ofClass f
   apply subset_antisymm
   · exact NonUnitalAlgHom.quasispectrum_apply_subset' R e a
   · simpa using! NonUnitalAlgHom.quasispectrum_apply_subset' R e.symm (e a)

Mathlib/Algebra/Star/StarAlgHom.lean

@@ -77,12 +77,14 @@ variable [FunLike F A B] [NonUnitalAlgHomClass F R A B]
 into an actual `NonUnitalStarAlgHom`. This is declared as the default coercion from `F` to
 `A →⋆ₙₐ[R] B`. -/
 @[coe]
-def toNonUnitalStarAlgHom [StarHomClass F A B] (f : F) : A →⋆ₙₐ[R] B :=
+def _root_.NonUnitalStarAlgHom.ofClass [StarHomClass F A B] (f : F) : A →⋆ₙₐ[R] B :=
   { (f : A →ₙₐ[R] B) with
     map_star' := map_star f }
 
+@[deprecated (since := "2026-09-02")] alias toNonUnitalStarAlgHom := NonUnitalStarAlgHom.ofClass
+
 instance [StarHomClass F A B] : CoeTC F (A →⋆ₙₐ[R] B) :=
-  ⟨toNonUnitalStarAlgHom⟩
+  ⟨.ofClass⟩
 
 instance [StarHomClass F A B] : NonUnitalStarRingHomClass F A B :=
   NonUnitalStarRingHomClass.mk
@@ -307,12 +309,14 @@ variable [StarHomClass F A 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 :=
+def _root_.StarAlgHom.ofClass (f : F) : A →⋆ₐ[R] B :=
   { (AlgHomClass.toAlgHom f) with
     map_star' := map_star f }
 
+@[deprecated (since := "2026-09-02")] alias toStarAlgHom := StarAlgHom.ofClass
+
 instance : CoeTC F (A →⋆ₐ[R] B) :=
-  ⟨toStarAlgHom⟩
+  ⟨.ofClass⟩
 
 end StarAlgHomClass
 
@@ -661,26 +665,25 @@ instance (priority := 100) (F R A B : Type*) [CommSemiring R] [Semiring A]
     AlgEquivClass F R A B :=
   { commutes := fun f r => by simp only [Algebra.algebraMap_eq_smul_one, map_smul, map_one] }
 
-namespace StarAlgEquivClass
-
 /-- 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] [StarHomClass F A B]
-    (f : F) : A ≃⋆ₐ[R] B :=
+def StarAlgEquiv.ofClass {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] [StarHomClass F A B] (f : F) : A ≃⋆ₐ[R] B :=
   { (RingEquivClass.toRingEquiv f : A ≃+* B) with
     map_star' := map_star f
     map_smul' := map_smul f }
 
+@[deprecated (since := "2026-09-02")] alias StarAlgEquivClass.toStarAlgEquiv := StarAlgEquiv.ofClass
+
 /-- 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] [StarHomClass F A B] :
+instance StarAlgEquivClass.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] [StarHomClass F A B] :
     CoeHead F (A ≃⋆ₐ[R] B) :=
-  ⟨toStarAlgEquiv⟩
-
-end StarAlgEquivClass
+  ⟨.ofClass⟩
 
 namespace StarAlgEquiv
 

Mathlib/Algebra/Star/StarRingHom.lean

@@ -71,12 +71,14 @@ variable [FunLike F A B] [NonUnitalRingHomClass F A B]
 /-- Turn an element of a type `F` satisfying `NonUnitalStarRingHomClass F A B` into an actual
 `NonUnitalStarRingHom`. This is declared as the default coercion from `F` to `A →⋆ₙ+ B`. -/
 @[coe]
-def toNonUnitalStarRingHom [NonUnitalStarRingHomClass F A B] (f : F) : A →⋆ₙ+* B :=
+def _root_.NonUnitalStarRingHom.ofClass [NonUnitalStarRingHomClass F A B] (f : F) : A →⋆ₙ+* B :=
   { (f : A →ₙ+* B) with
     map_star' := map_star f }
 
+@[deprecated (since := "2026-09-03")] alias toNonUnitalStarRingHom := NonUnitalStarRingHom.ofClass
+
 instance [NonUnitalStarRingHomClass F A B] : CoeHead F (A →⋆ₙ+* B) :=
-  ⟨toNonUnitalStarRingHom⟩
+  ⟨.ofClass⟩
 
 end NonUnitalStarRingHomClass
 
@@ -271,16 +273,18 @@ instance (priority := 100) {F A B : Type*} [NonUnitalNonAssocSemiring A] [Star A
 /-- Turn an element of a type `F` satisfying `StarRingEquivClass F A B` into an actual
 `StarRingEquiv`. This is declared as the default coercion from `F` to `A ≃⋆+* B`. -/
 @[coe]
-def toStarRingEquiv {F A B : Type*} [Add A] [Mul A] [Star A] [Add B] [Mul B] [Star B]
+def _root_.StarRingEquiv.ofClass {F A B : Type*} [Add A] [Mul A] [Star A] [Add B] [Mul B] [Star B]
     [EquivLike F A B] [StarRingEquivClass F A B] (f : F) : A ≃⋆+* B :=
   { (RingEquivClass.toRingEquiv f : A ≃+* B) with
     map_star' := map_star f }
 
+@[deprecated (since := "2026-09-03")] alias toStarRingEquiv := StarRingEquiv.ofClass
+
 /-- Any type satisfying `StarRingEquivClass` can be cast into `StarRingEquiv` via
 `StarRingEquivClass.toStarRingEquiv`. -/
 instance instCoeHead {F A B : Type*} [Add A] [Mul A] [Star A] [Add B] [Mul B] [Star B]
     [EquivLike F A B] [StarRingEquivClass F A B] : CoeHead F (A ≃⋆+* B) :=
-  ⟨toStarRingEquiv⟩
+  ⟨.ofClass⟩
 
 end StarRingEquivClass
 

Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.lean

@@ -235,7 +235,7 @@ public instance (priority := 100) {F : Type*} [EquivLike F (V →L[𝕜] V) (W 
     OrderIsoClass F _ _ where
   map_le_map_iff f x y := by
     obtain ⟨U, hU⟩ := StarAlgEquiv.eq_linearIsometryEquivConjStarAlgEquiv
-      (StarAlgEquivClass.toStarAlgEquiv f : _ ≃⋆ₐ[𝕜] _) (map_continuous f)
+      (StarAlgEquiv.ofClass f : _ ≃⋆ₐ[𝕜] _) (map_continuous f)
     have this a : f a = U.conjStarAlgEquiv a := by simpa using! congr($hU a)
     simp_rw [le_def, ← _root_.map_sub, ← isPositive_toLinearMap_iff, this]
     exact LinearMap.isPositive_linearIsometryEquiv_conj_iff U

Mathlib/CategoryTheory/Limits/Preserves/Lattice.lean

@@ -36,15 +36,15 @@ section
 variable [SemilatticeInf α] [OrderTop α] [SemilatticeInf β] [OrderTop β] [InfTopHomClass F α β]
 
 instance preservesLimit_finite_toFunctor {J : Type w} [SmallCategory J]
-    [FinCategory J] (K : J ⥤ α) : PreservesLimit K (toOrderHom f).toFunctor :=
+    [FinCategory J] (K : J ⥤ α) : PreservesLimit K (OrderHom.ofClass f).toFunctor :=
   preservesLimit_of_preserves_limit_cone (finiteLimitCone K).isLimit <|
     (finiteLimitCone _).isLimit.ofIsoLimit
       (Cone.ext (eqToIso (show Finset.univ.inf _ = f _ by aesop)) (by subsingleton))
 
 instance preservesLimitsOfShape_finite_toFunctor {J : Type w} [SmallCategory J] [FinCategory J] :
-    PreservesLimitsOfShape J (toOrderHom f).toFunctor where
+    PreservesLimitsOfShape J (OrderHom.ofClass f).toFunctor where
 
-instance : PreservesFiniteLimits (toOrderHom f).toFunctor where
+instance : PreservesFiniteLimits (OrderHom.ofClass f).toFunctor where
   preservesFiniteLimits _ _ _ := inferInstance
 
 end
@@ -54,15 +54,15 @@ section
 variable [SemilatticeSup α] [OrderBot α] [SemilatticeSup β] [OrderBot β] [SupBotHomClass F α β]
 
 instance preservesColimit_finite_toFunctor {J : Type w} [SmallCategory J]
-    [FinCategory J] (K : J ⥤ α) : PreservesColimit K (toOrderHom f).toFunctor :=
+    [FinCategory J] (K : J ⥤ α) : PreservesColimit K (OrderHom.ofClass f).toFunctor :=
   preservesColimit_of_preserves_colimit_cocone (finiteColimitCocone K).isColimit <|
     (finiteColimitCocone _).isColimit.ofIsoColimit
       (Cocone.ext (eqToIso (show Finset.univ.sup _ = f _ by aesop)) (by subsingleton))
 
 instance preservesColimitsOfShape_finite_toFunctor {J : Type w} [SmallCategory J]
-    [FinCategory J] : PreservesColimitsOfShape J (toOrderHom f).toFunctor where
+    [FinCategory J] : PreservesColimitsOfShape J (OrderHom.ofClass f).toFunctor where
 
-instance : PreservesFiniteColimits (toOrderHom f).toFunctor where
+instance : PreservesFiniteColimits (OrderHom.ofClass f).toFunctor where
   preservesFiniteColimits _ _ _ := inferInstance
 
 end
@@ -72,32 +72,32 @@ section
 variable [CompleteLattice α] [CompleteLattice β]
 
 instance preservesLimit_toFunctor [sInfHomClass F α β] {J : Type w} [Category.{w'} J]
-    (K : J ⥤ α) : PreservesLimit K (toOrderHom f).toFunctor :=
+    (K : J ⥤ α) : PreservesLimit K (OrderHom.ofClass f).toFunctor :=
   preservesLimit_of_preserves_limit_cone (limitCone K).isLimit <|
     (limitCone _).isLimit.ofIsoLimit (Cone.ext (eqToIso (by aesop)) (by subsingleton))
 
 instance preservesLimitsOfShape_toFunctor [sInfHomClass F α β] {J : Type w} [Category.{w'} J] :
-    PreservesLimitsOfShape J (toOrderHom f).toFunctor where
+    PreservesLimitsOfShape J (OrderHom.ofClass f).toFunctor where
 
 instance preservesLimitsOfSize_toFunctor [sInfHomClass F α β] :
-    PreservesLimitsOfSize.{w', w} (toOrderHom f).toFunctor where
+    PreservesLimitsOfSize.{w', w} (OrderHom.ofClass f).toFunctor where
 
 instance preservesLimits_toFunctor [sInfHomClass F α β] :
-    PreservesLimits (toOrderHom f).toFunctor where
+    PreservesLimits (OrderHom.ofClass f).toFunctor where
 
 instance preservesColimit_toFunctor [sSupHomClass F α β] {J : Type w} [Category.{w'} J]
-    (K : J ⥤ α) : PreservesColimit K (toOrderHom f).toFunctor :=
+    (K : J ⥤ α) : PreservesColimit K (OrderHom.ofClass f).toFunctor :=
   preservesColimit_of_preserves_colimit_cocone (colimitCocone K).isColimit <|
     (colimitCocone _).isColimit.ofIsoColimit (Cocone.ext (eqToIso (by aesop)) (by subsingleton))
 
 instance preservesColimitsOfShape_toFunctor [sSupHomClass F α β] {J : Type w} [Category.{w'} J] :
-    PreservesColimitsOfShape J (toOrderHom f).toFunctor where
+    PreservesColimitsOfShape J (OrderHom.ofClass f).toFunctor where
 
 instance preservesColimitsOfSize_toFunctor [sSupHomClass F α β] :
-    PreservesColimitsOfSize.{w', w} (toOrderHom f).toFunctor where
+    PreservesColimitsOfSize.{w', w} (OrderHom.ofClass f).toFunctor where
 
 instance preservesColimits_toFunctor [sSupHomClass F α β] :
-    PreservesColimits (toOrderHom f).toFunctor where
+    PreservesColimits (OrderHom.ofClass f).toFunctor where
 
 end
 

Mathlib/Order/Category/FinBddDistLat.lean

@@ -164,7 +164,7 @@ instance hasForgetToBddDistLat : HasForget₂ FinBddDistLat BddDistLat where
 
 instance hasForgetToFinPartOrd : HasForget₂ FinBddDistLat FinPartOrd where
   forget₂.obj X := ↧X
-  forget₂.map f := ConcreteCategory.ofHom (OrderHomClass.toOrderHom f.hom)
+  forget₂.map f := ConcreteCategory.ofHom (.ofClass f.hom)
 
 /-- Constructs an equivalence between finite distributive lattices from an order isomorphism
 between them. -/

Mathlib/Order/Hom/Basic.lean

@@ -143,14 +143,15 @@ attribute [simp] map_le_map_iff
 /-- Turn an element of a type `F` satisfying `OrderIsoClass F α β` into an actual
 `OrderIso`. This is declared as the default coercion from `F` to `α ≃o β`. -/
 @[coe]
-def OrderIsoClass.toOrderIso [LE α] [LE β] [EquivLike F α β] [OrderIsoClass F α β] (f : F) :
+def OrderIso.ofClass [LE α] [LE β] [EquivLike F α β] [OrderIsoClass F α β] (f : F) :
     α ≃o β :=
   { EquivLike.toEquiv f with map_rel_iff' := map_le_map_iff f }
 
-/-- Any type satisfying `OrderIsoClass` can be cast into `OrderIso` via
-`OrderIsoClass.toOrderIso`. -/
+@[deprecated (since := "2026-09-02")] alias OrderIsoClass.toOrderIso := OrderIso.ofClass
+
+/-- Any type satisfying `OrderIsoClass` can be cast into `OrderIso` via `OrderIso.ofClass`. -/
 instance [LE α] [LE β] [EquivLike F α β] [OrderIsoClass F α β] : CoeTC F (α ≃o β) :=
-  ⟨OrderIsoClass.toOrderIso⟩
+  ⟨.ofClass⟩
 
 -- See note [lower instance priority]
 instance (priority := 100) OrderIsoClass.toOrderHomClass [LE α] [LE β]
@@ -170,14 +171,15 @@ protected theorem mono (f : F) : Monotone f := fun _ _ => map_rel f
 /-- Turn an element of a type `F` satisfying `OrderHomClass F α β` into an actual
 `OrderHom`. This is declared as the default coercion from `F` to `α →o β`. -/
 @[coe]
-def toOrderHom (f : F) : α →o β where
+def _root_.OrderHom.ofClass (f : F) : α →o β where
   toFun := f
   monotone' := OrderHomClass.monotone f
 
-/-- Any type satisfying `OrderHomClass` can be cast into `OrderHom` via
-`OrderHomClass.toOrderHom`. -/
+/-- Any type satisfying `OrderHomClass` can be cast into `OrderHom` via `OrderHom.ofClass`. -/
 instance : CoeTC F (α →o β) :=
-  ⟨toOrderHom⟩
+  ⟨.ofClass⟩
+
+@[deprecated (since := "2026-09-02")] alias toOrderHom := OrderHom.ofClass
 
 end OrderHomClass
 
@@ -251,7 +253,7 @@ initialize_simps_projections OrderHom (toFun → coe)
 theorem ext (f g : α →o β) (h : (f : α → β) = g) : f = g :=
   DFunLike.coe_injective h
 
-@[simp] theorem coe_eq (f : α →o β) : OrderHomClass.toOrderHom f = f := rfl
+@[simp] theorem coe_eq (f : α →o β) : .ofClass f = f := rfl
 
 @[simp] theorem _root_.OrderHomClass.coe_coe {F} [FunLike F α β] [OrderHomClass F α β] (f : F) :
     ⇑(f : α →o β) = f :=

Mathlib/Topology/Category/TopCat/Opens.lean

@@ -158,7 +158,7 @@ def _root_.TopCat.Hom.frameHom (f : X ⟶ Y) : FrameHom (Opens Y) (Opens X) wher
 /-- `Opens.map f` gives the functor from open sets in Y to open set in X,
 given by taking preimages under f. -/
 def map (f : X ⟶ Y) : Opens Y ⥤ Opens X :=
-  (OrderHomClass.toOrderHom f.frameHom).toFunctor
+  (OrderHom.ofClass f.frameHom).toFunctor
 
 lemma map_def (f : X ⟶ Y) : map f =
   { obj U := ⟨f ⁻¹' (U : Set Y), U.isOpen.preimage f.hom.continuous⟩
@@ -312,7 +312,7 @@ lemma mapMapIso_counitIso {X Y : TopCat.{u}} (H : X ≅ Y) :
 
 instance (f : X ⟶ Y) {J : Type w} [SmallCategory J] [FinCategory J] (K : J ⥤ (Opens Y)) :
     Limits.PreservesLimit K (map f) :=
-  inferInstanceAs <| Limits.PreservesLimit K (OrderHomClass.toOrderHom f.frameHom).toFunctor
+  inferInstanceAs <| Limits.PreservesLimit K (OrderHom.ofClass f.frameHom).toFunctor
 
 instance (f : X ⟶ Y) {J : Type w} [SmallCategory J] [FinCategory J] :
     Limits.PreservesLimitsOfShape J (map f) where
@@ -322,7 +322,7 @@ instance (f : X ⟶ Y) : Limits.PreservesFiniteLimits (map f) where
 
 instance (f : X ⟶ Y) {J : Type w} [Category.{w'} J] (K : J ⥤ (Opens Y)) :
     Limits.PreservesColimit K (map f) :=
-  inferInstanceAs <| Limits.PreservesColimit K (OrderHomClass.toOrderHom f.frameHom).toFunctor
+  inferInstanceAs <| Limits.PreservesColimit K (OrderHom.ofClass f.frameHom).toFunctor
 
 instance (f : X ⟶ Y) {J : Type w} [Category.{w'} J] :
     Limits.PreservesColimitsOfShape J (map f) where