chore: rename CoAlg{Hom,Equiv}Class.toCoAlg{Hom,Equiv} as CoAlg{Hom,Equiv}.ofClass

Mathlib/Algebra/Algebra/Equiv.lean

@@ -65,10 +65,12 @@ instance (priority := 100) toLinearEquivClass (F R A B : Type*) [CommSemiring R]
 /-- Turn an element of a type `F` satisfying `AlgEquivClass F R A B` into an actual `AlgEquiv`.
 This is declared as the default coercion from `F` to `A ≃ₐ[R] B`. -/
 @[coe]
-def toAlgEquiv {F R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A]
-    [Algebra R B] [EquivLike F A B] [AlgEquivClass F R A B] (f : F) : A ≃ₐ[R] B :=
+def _root_.AlgEquiv.ofClass {F R A B : Type*} [CommSemiring R]
+    [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [EquivLike F A B] [AlgEquivClass F R A B]
+    (f : F) : A ≃ₐ[R] B :=
   { (f : A ≃ B), (RingEquivClass.toRingEquiv f : A ≃+* B) with commutes' := commutes f }
 
+@[deprecated (since := "2026-09-07")] alias toAlgEquiv := AlgEquiv.ofClass
 end AlgEquivClass
 
 namespace AlgEquiv
@@ -133,9 +135,10 @@ theorem toEquiv_eq_coe : e.toEquiv = e :=
   rfl
 
 @[simp]
-protected theorem coe_coe {F : Type*} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂] (f : F) :
-    ⇑(AlgEquivClass.toAlgEquiv f) = f :=
+protected theorem coe_ofClass {F : Type*} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂] (f : F) :
+    ⇑(ofClass f) = f :=
   rfl
+@[deprecated (since := "2026-09-07")] alias coe_coe := AlgEquiv.coe_ofClass
 
 theorem coe_fun_injective : @Function.Injective (A₁ ≃ₐ[R] A₂) (A₁ → A₂) fun e => (e : A₁ → A₂) :=
   DFunLike.coe_injective
@@ -256,17 +259,22 @@ theorem invFun_eq_symm {e : A₁ ≃ₐ[R] A₂} : e.invFun = e.symm :=
   rfl
 
 @[simp]
-theorem coe_apply_coe_coe_symm_apply {F : Type*} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂]
+theorem coe_apply_ofClass_symm_apply {F : Type*} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂]
     (f : F) (x : A₂) :
-    f ((AlgEquivClass.toAlgEquiv f).symm x) = x :=
+    f ((ofClass f).symm x) = x :=
   EquivLike.right_inv f x
 
 @[simp]
-theorem coe_coe_symm_apply_coe_apply {F : Type*} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂]
+theorem ofClass_symm_apply_coe_apply {F : Type*} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂]
     (f : F) (x : A₁) :
-    (AlgEquivClass.toAlgEquiv f).symm (f x) = x :=
+    (ofClass f).symm (f x) = x :=
   EquivLike.left_inv f x
 
+@[deprecated (since := "2026-09-07")]
+alias coe_apply_coe_coe_symm_apply := coe_apply_ofClass_symm_apply
+@[deprecated (since := "2026-09-07")]
+alias coe_coe_symm_apply_coe_apply := ofClass_symm_apply_coe_apply
+
 /-- `simp` normal form of `invFun_eq_symm` -/
 @[simp]
 theorem symm_toEquiv_eq_symm {e : A₁ ≃ₐ[R] A₂} : (e : A₁ ≃ A₂).symm = e.symm :=

Mathlib/Algebra/Algebra/Hom.lean

@@ -66,11 +66,14 @@ instance (priority := 100) linearMapClass [AlgHomClass F R A B] : LinearMapClass
 /-- Turn an element of a type `F` satisfying `AlgHomClass F α β` into an actual
 `AlgHom`. This is declared as the default coercion from `F` to `α →+* β`. -/
 @[coe]
-def toAlgHom {F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) : A →ₐ[R] B where
+def _root_.AlgHom.ofClass {F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) :
+    A →ₐ[R] B where
   __ := (f : A →+* B)
   toFun := f
   commutes' := AlgHomClass.commutes f
 
+@[deprecated (since := "2026-09-07")] alias toAlgHom := AlgHom.ofClass
+
 end AlgHomClass
 
 namespace AlgHom
@@ -96,9 +99,11 @@ instance algHomClass : AlgHomClass (A →ₐ[R] B) R A B where
   map_one f := f.map_one'
   commutes f := f.commutes'
 
-@[simp] lemma _root_.AlgHomClass.toLinearMap_toAlgHom {R A B F : Type*} [CommSemiring R]
+@[simp] lemma _root_.AlgHomClass.toLinearMap_ofClass {R A B F : Type*} [CommSemiring R]
     [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [FunLike F A B] [AlgHomClass F R A B]
-    (f : F) : (AlgHomClass.toAlgHom f : A →ₗ[R] B) = f := rfl
+    (f : F) : (ofClass f : A →ₗ[R] B) = f := rfl
+
+@[deprecated (since := "2026-09-07")] alias toLinearMap_toAlgHom := AlgHomClass.toLinearMap_ofClass
 
 /-- See Note [custom simps projection] -/
 def Simps.apply {R : Type u} {α : Type v} {β : Type w} [CommSemiring R]
@@ -107,10 +112,12 @@ def Simps.apply {R : Type u} {α : Type v} {β : Type w} [CommSemiring R]
 initialize_simps_projections AlgHom (toFun → apply)
 
 @[simp]
-protected theorem coe_coe {F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) :
-    ⇑(AlgHomClass.toAlgHom f : A →ₐ[R] B) = f :=
+protected theorem coe_ofClass {F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) :
+    ⇑(ofClass f) = f :=
   rfl
 
+@[deprecated (since := "2026-09-07")] alias coe_coe := AlgHom.coe_ofClass
+
 @[simp]
 theorem toFun_eq_coe (f : A →ₐ[R] B) : f.toFun = f :=
   rfl
@@ -404,7 +411,7 @@ namespace AlgHomClass
 @[simp]
 lemma toRingHom_toAlgHom {R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A]
     [Algebra R B] {F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) :
-    RingHomClass.toRingHom (AlgHomClass.toAlgHom f) = RingHomClass.toRingHom f := rfl
+    RingHomClass.toRingHom (AlgHom.ofClass f) = RingHomClass.toRingHom f := rfl
 
 end AlgHomClass
 

Mathlib/Algebra/Algebra/Spectrum/Basic.lean

@@ -443,8 +443,8 @@ theorem AlgEquiv.spectrum_eq {F R A B : Type*} [CommSemiring R] [Ring A] [Ring B
     [Algebra R B] [EquivLike F A B] [AlgEquivClass F R A B] (f : F) (a : A) :
     spectrum R (f a) = spectrum R a :=
   Set.Subset.antisymm (AlgHom.spectrum_apply_subset _ _) <| by
-    simpa only [AlgEquiv.coe_toAlgHom, AlgEquiv.coe_coe_symm_apply_coe_apply] using
-      AlgHom.spectrum_apply_subset (AlgEquivClass.toAlgEquiv f : A ≃ₐ[R] B).symm (f a)
+    simpa only [AlgEquiv.coe_toAlgHom, AlgEquiv.ofClass_symm_apply_coe_apply] using
+      AlgHom.spectrum_apply_subset (AlgEquiv.ofClass f : A ≃ₐ[R] B).symm (f a)
 
 section ConjugateUnits
 

Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean

@@ -384,7 +384,7 @@ variable {F : Type*} [FunLike F A B] [AlgHomClass F R A B]
 
 theorem eqOn_sup {φ ψ : F} {S T : Subalgebra R A} (hS : Set.EqOn φ ψ S) (hT : Set.EqOn φ ψ T) :
     Set.EqOn φ ψ ↑(S ⊔ T) := by
-  rw [← AlgHom.coe_coe φ, ← AlgHom.coe_coe ψ, ← le_equalizer] at hS hT ⊢
+  rw [← AlgHom.coe_ofClass φ, ← AlgHom.coe_ofClass ψ, ← le_equalizer] at hS hT ⊢
   exact sup_le hS hT
 
 theorem ext_on_codisjoint {φ ψ : F} {S T : Subalgebra R A} (hST : Codisjoint S T)

Mathlib/Algebra/Star/StarAlgHom.lean

@@ -310,7 +310,7 @@ variable [StarHomClass F A B]
 actual `StarAlgHom`. This is declared as the default coercion from `F` to `A →⋆ₐ[R] B`. -/
 @[coe]
 def _root_.StarAlgHom.ofClass (f : F) : A →⋆ₐ[R] B :=
-  { (AlgHomClass.toAlgHom f) with
+  { (AlgHom.ofClass f) with
     map_star' := map_star f }
 
 @[deprecated (since := "2026-09-02")] alias toStarAlgHom := StarAlgHom.ofClass

Mathlib/LinearAlgebra/Determinant.lean

@@ -460,21 +460,21 @@ end LinearEquiv
 @[simp] theorem LinearMap.det_map {K V W : Type*} [Field K] [AddCommGroup V] [Module K V]
     [AddCommGroup W] [Module K W] {F : Type*} [EquivLike F (End K V) (End K W)]
     [AlgEquivClass F K _ _] (f : F) (x : End K V) : (f x).det = x.det :=
-  have ⟨_, h⟩ := (AlgEquivClass.toAlgEquiv f).eq_linearEquivConjAlgEquiv
+  have ⟨_, h⟩ := (AlgEquiv.ofClass f).eq_linearEquivConjAlgEquiv
   (by simpa using congr($h x)) ▸ det_conj _ _
 
 @[simp] theorem Matrix.det_map {K m n : Type*} [Field K] [Fintype m] [Fintype n]
     [DecidableEq m] [DecidableEq n] {F : Type*} [EquivLike F (Matrix m m K) (Matrix n n K)]
     [AlgEquivClass F K _ _] (f : F) (x : Matrix m m K) : (f x).det = x.det := by
   simpa [toMatrixAlgEquiv', Matrix.toLinAlgEquiv'] using
     LinearMap.det_map ((Matrix.toLinAlgEquiv'.symm.trans
-      (AlgEquivClass.toAlgEquiv f)).trans Matrix.toLinAlgEquiv') x.toLin'
+      (AlgEquiv.ofClass f)).trans Matrix.toLinAlgEquiv') x.toLin'
 
 @[simp] theorem Matrix.det_map' {K m F : Type*} [Field K] [Fintype m] [DecidableEq m]
     [FunLike F (Matrix m m K) (Matrix m m K)] [AlgHomClass F K _ _] (f : F) (x : Matrix m m K) :
     (f x).det = x.det := by
   by_cases! Nonempty m
-  · exact det_map (AlgEquiv.ofBijective _ (AlgHomClass.toAlgHom f).bijective) x
+  · exact det_map (AlgEquiv.ofBijective _ (AlgHom.ofClass f).bijective) x
   · simp
 
 /-- The determinants of a `LinearEquiv` and its inverse multiply to 1. -/

Mathlib/LinearAlgebra/Trace.lean

@@ -307,21 +307,21 @@ theorem trace_conj' (f : M →ₗ[R] M) (e : M ≃ₗ[R] N) : trace R N (e.conj
 @[simp] theorem trace_map {K V W : Type*} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W]
     [Module K W] {F : Type*} [EquivLike F (End K V) (End K W)] [AlgEquivClass F K _ _]
     (f : F) (x : End K V) : (f x).trace K W = x.trace K V :=
-  have ⟨_, h⟩ := (AlgEquivClass.toAlgEquiv f).eq_linearEquivConjAlgEquiv
+  have ⟨_, h⟩ := (AlgEquiv.ofClass f).eq_linearEquivConjAlgEquiv
   (by simpa using congr($h x)) ▸ trace_conj' _ _
 
 @[simp] theorem _root_.Matrix.trace_map {K m n : Type*} [Field K] [Fintype m] [Fintype n]
     [DecidableEq m] [DecidableEq n] {F : Type*} [EquivLike F (Matrix m m K) (Matrix n n K)]
     [AlgEquivClass F K _ _] (f : F) (x : Matrix m m K) : (f x).trace = x.trace := by
   simpa [toMatrixAlgEquiv', Matrix.toLinAlgEquiv'] using
     LinearMap.trace_map ((Matrix.toLinAlgEquiv'.symm.trans
-      (AlgEquivClass.toAlgEquiv f)).trans Matrix.toLinAlgEquiv') x.toLin'
+      (AlgEquiv.ofClass f)).trans Matrix.toLinAlgEquiv') x.toLin'
 
 @[simp] theorem _root_.Matrix.trace_map' {K m F : Type*} [Field K] [Fintype m] [DecidableEq m]
     [FunLike F (Matrix m m K) (Matrix m m K)] [AlgHomClass F K _ _] (f : F) (x : Matrix m m K) :
     (f x).trace = x.trace := by
   by_cases! Nonempty m
-  · exact Matrix.trace_map (AlgEquiv.ofBijective _ (AlgHomClass.toAlgHom f).bijective) x
+  · exact Matrix.trace_map (AlgEquiv.ofBijective _ (AlgHom.ofClass f).bijective) x
   · simp
 
 theorem IsProj.trace {p : Submodule R M} {f : M →ₗ[R] M} (h : IsProj p f) [Module.Free R p]

Mathlib/NumberTheory/NumberField/Basic.lean

@@ -223,13 +223,13 @@ def mapAlgHom {k K L F : Type*} [Field k] [Field K] [Field L] [Algebra k K]
     [Algebra k L] [FunLike F K L] [AlgHomClass F k K L] (f : F) : (𝓞 K) →ₐ[𝓞 k] (𝓞 L) where
   toRingHom := mapRingHom f
   commutes' x := SetCoe.ext (AlgHomClass.commutes
-    ((AlgHomClass.toAlgHom f).restrictScalars (𝓞 k)) x)
+    ((AlgHom.ofClass f).restrictScalars (𝓞 k)) x)
 
 /-- The isomorphism of algebras `(𝓞 K) ≃ₐ[𝓞 k] (𝓞 L)` given by restricting
   an isomorphism of algebras `e : K ≃ₐ[k] L` to `𝓞 K`. -/
 def mapAlgEquiv {k K L E : Type*} [Field k] [Field K] [Field L] [Algebra k K]
     [Algebra k L] [EquivLike E K L] [AlgEquivClass E k K L] (e : E) : (𝓞 K) ≃ₐ[𝓞 k] (𝓞 L) :=
-  AlgEquiv.ofAlgHom (mapAlgHom e) (mapAlgHom (AlgEquivClass.toAlgEquiv e : K ≃ₐ[k] L).symm)
+  AlgEquiv.ofAlgHom (mapAlgHom e) (mapAlgHom (AlgEquiv.ofClass e).symm)
     (AlgHom.ext fun x => ext (EquivLike.right_inv e x.1))
       (AlgHom.ext fun x => ext (EquivLike.left_inv e x.1))
 

Mathlib/NumberTheory/RamificationInertia/Ramification.lean

@@ -183,7 +183,7 @@ lemma ramificationIdx'_map_eq {E : Type*} [EquivLike E S S₁] [AlgEquivClass E
     (P : Ideal S) (e : E) :
     ramificationIdx' p (P.map e) = ramificationIdx' p P := by
   rw [show P.map e = _ from P.map_comap_of_equiv (RingEquivClass.toRingEquiv e : S ≃+* S₁)]
-  exact p.ramificationIdx'_comap_eq (AlgEquivClass.toAlgEquiv e).symm P
+  exact p.ramificationIdx'_comap_eq (AlgEquiv.ofClass e).symm P
 
 @[deprecated (since := "2026-07-01")] alias ramificationIdx_map_eq := ramificationIdx'_map_eq
 

Mathlib/RingTheory/Bialgebra/Hom.lean

@@ -77,7 +77,7 @@ instance (priority := 100) toAlgHomClass : AlgHomClass F R A B where
 `BialgHom`. This is declared as the default coercion from `F` to `A →ₐc[R] B`. -/
 @[coe]
 def toBialgHom (f : F) : A →ₐc[R] B :=
-  { CoalgHomClass.toCoalgHom f, AlgHomClass.toAlgHom f with
+  { CoAlgHom.ofClass f, AlgHom.ofClass f with
     toFun := f }
 
 instance instCoeToBialgHom :
@@ -91,13 +91,13 @@ variable [CommSemiring R] [Semiring A] [Bialgebra R A] [Semiring B] [Bialgebra R
 
 @[simp]
 theorem counitAlgHom_comp (f : F) :
-    (counitAlgHom R B).comp (AlgHomClass.toAlgHom f) = counitAlgHom R A :=
+    (counitAlgHom R B).comp (AlgHom.ofClass f) = counitAlgHom R A :=
   AlgHom.toLinearMap_injective (CoalgHomClass.counit_comp f)
 
 @[simp]
 theorem map_comp_comulAlgHom (f : F) :
-    (Algebra.TensorProduct.map (AlgHomClass.toAlgHom f) (AlgHomClass.toAlgHom f)).comp
-      (comulAlgHom R A) = (comulAlgHom R B).comp (AlgHomClass.toAlgHom f) :=
+    (Algebra.TensorProduct.map (AlgHom.ofClass f) (AlgHom.ofClass f)).comp
+      (comulAlgHom R A) = (comulAlgHom R B).comp (AlgHom.ofClass f) :=
   AlgHom.toLinearMap_injective (CoalgHomClass.map_comp_comul f)
 
 end

Mathlib/RingTheory/Bialgebra/TensorProduct.lean

@@ -142,8 +142,8 @@ bialgebra equivalence. -/
 @[expose] protected def rid : A ⊗[R] R ≃ₐc[S] A where
   toCoalgEquiv := Coalgebra.TensorProduct.rid R S A
   map_mul' x y := by
-    simp only [CoalgEquiv.toCoalgHom_eq_coe, CoalgHom.toLinearMap_eq_coe, AddHom.toFun_eq_coe,
-      LinearMap.coe_toAddHom, CoalgHom.coe_toLinearMap, CoalgHom.coe_coe,
+    simp only [CoalgEquiv.toCoalgHom_eq_ofClass, CoalgHom.toLinearMap_eq_coe, AddHom.toFun_eq_coe,
+      LinearMap.coe_toAddHom, CoalgHom.coe_toLinearMap, CoalgHom.coe_ofClass,
       coalgebra_rid_eq_algebra_rid_apply, map_mul]
 
 @[simp]

Mathlib/RingTheory/Coalgebra/Equiv.lean

@@ -55,13 +55,14 @@ variable {F R A B : Type*} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B]
 
 /-- Reinterpret an element of a type of coalgebra equivalences as a coalgebra equivalence. -/
 @[coe]
-def toCoalgEquiv [EquivLike F A B] [CoalgEquivClass F R A B] (f : F) : A ≃ₗc[R] B :=
+def _root_.CoalgEquiv.ofClass [EquivLike F A B] [CoalgEquivClass F R A B] (f : F) : A ≃ₗc[R] B :=
   { (f : A →ₗc[R] B), (SemilinearEquivClass.semilinearEquiv f : A ≃ₗ[R] B) with }
+@[deprecated (since := "2026-09-08")] alias toCoalgEquiv := CoalgEquiv.ofClass
 
 /-- Reinterpret an element of a type of coalgebra equivalences as a coalgebra equivalence. -/
 instance instCoeToCoalgEquiv
     [EquivLike F A B] [CoalgEquivClass F R A B] : CoeHead F (A ≃ₗc[R] B) where
-  coe f := toCoalgEquiv f
+  coe f := .ofClass f
 
 end CoalgEquivClass
 
@@ -126,24 +127,28 @@ variable [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [Module R A] [Mod
 variable (e e' : A ≃ₗc[R] B)
 
 @[simp, norm_cast]
-theorem coe_coe : ⇑(e : A →ₗc[R] B) = e :=
+theorem coe_ofClass : ⇑(ofClass e) = e :=
   rfl
+@[deprecated (since := "2026-09-08")] alias coe_coe := coe_ofClass
 
 @[nolint synTaut, deprecated "Now a syntactic tautology" (since := "2026-04-12")]
 theorem toLinearEquiv_eq_coe (f : A ≃ₗc[R] B) : f.toLinearEquiv = f :=
   rfl
 
 @[simp]
-theorem toCoalgHom_eq_coe (f : A ≃ₗc[R] B) : f.toCoalgHom = f :=
+theorem toCoalgHom_eq_ofClass (f : A ≃ₗc[R] B) : f.toCoalgHom = f :=
   rfl
+@[deprecated (since := "2026-09-08")] alias toCoalgHom_eq_coe := toCoalgHom_eq_ofClass
 
 @[simp]
 theorem coe_toLinearEquiv : ⇑(e : A ≃ₗ[R] B) = e :=
   rfl
 
+-- TODO: is this the right way to name this lemma?
 @[simp]
-theorem coe_toCoalgHom : ⇑(e : A →ₗc[R] B) = e :=
+theorem coe_coAlgHomOfClass : ⇑(CoAlgHom.ofClass e) = e :=
   rfl
+@[deprecated (since := "2026-09-08")] alias coe_toCoalgHom := coe_coAlgHomOfClass
 
 theorem toLinearEquiv_toLinearMap : ((e : A ≃ₗ[R] B) : A →ₗ[R] B) = (e : A →ₗc[R] B) :=
   rfl
@@ -173,7 +178,7 @@ def symm (e : A ≃ₗc[R] B) : B ≃ₗc[R] A :=
       change (TensorProduct.congr (e : A ≃ₗ[R] B) (e : A ≃ₗ[R] B)).symm.toLinearMap ∘ₗ comul
         = comul ∘ₗ (e : A ≃ₗ[R] B).symm
       rw [LinearEquiv.toLinearMap_symm_comp_eq]
-      simp only [TensorProduct.congr, toCoalgHom_eq_coe, CoalgHom.toLinearMap_eq_coe,
+      simp only [TensorProduct.congr, toCoalgHom_eq_ofClass, CoalgHom.toLinearMap_eq_coe,
         LinearEquiv.toLinearMap_ofLinearMap, ← LinearMap.comp_assoc, CoalgHomClass.map_comp_comul]
       rw [← toLinearEquiv_toLinearMap, LinearEquiv.comp_symm_cancel_right] }
 
@@ -311,9 +316,9 @@ structure on `B`. -/
       ← LinearMap.comp_assoc]
     congr 1
     ext x
-    simpa only [toCoalgHom_eq_coe, CoalgHom.toLinearMap_eq_coe, LinearMap.coe_comp,
+    simpa only [toCoalgHom_eq_ofClass, CoalgHom.toLinearMap_eq_coe, LinearMap.coe_comp,
       LinearEquiv.coe_coe, Function.comp_apply, ← (ℛ R _).eq, map_sum, TensorProduct.map_tmul,
-      LinearMap.coe_coe, CoalgHom.coe_coe, LinearMap.rTensor_tmul, coe_symm_toLinearEquiv,
+      LinearMap.coe_coe, CoalgHom.coe_ofClass, LinearMap.rTensor_tmul, coe_symm_toLinearEquiv,
       symm_apply_apply, LinearMap.lTensor_comp_map, TensorProduct.sum_tmul,
       TensorProduct.assoc_tmul, TensorProduct.tmul_sum] using (sum_map_tmul_tmul_eq f f f x).symm
   rTensor_counit_comp_comul := by

Mathlib/RingTheory/Coalgebra/GroupLike.lean

@@ -57,7 +57,7 @@ lemma IsGroupLikeElem.map [FunLike F A B] [CoalgHomClass F R A B] (f : F)
 /-- A coalgebra isomorphism preserves group-like elements. -/
 @[simp] lemma isGroupLikeElem_map_equiv [EquivLike F A B] [CoalgEquivClass F R A B] (f : F) :
     IsGroupLikeElem R (f a) ↔ IsGroupLikeElem R a where
-  mp ha := (CoalgEquivClass.toCoalgEquiv f).symm_apply_apply a ▸ ha.map _
+  mp ha := (CoalgEquiv.ofClass f).symm_apply_apply a ▸ ha.map _
   mpr := .map f
 
 variable (R A) in

Mathlib/RingTheory/Coalgebra/Hom.lean

@@ -68,14 +68,15 @@ variable {R A B F : Type*} [CommSemiring R]
 /-- Turn an element of a type `F` satisfying `CoalgHomClass F R A B` into an actual
 `CoalgHom`. This is declared as the default coercion from `F` to `A →ₗc[R] B`. -/
 @[coe]
-def toCoalgHom (f : F) : A →ₗc[R] B :=
+def _root_.CoAlgHom.ofClass (f : F) : A →ₗc[R] B :=
   { (f : A →ₗ[R] B) with
     toFun := f
     counit_comp := CoalgHomClass.counit_comp f
     map_comp_comul := CoalgHomClass.map_comp_comul f }
+@[deprecated (since := "2026-09-08")] alias toCoAlgHom := CoAlgHom.ofClass
 
 instance instCoeToCoalgHom : CoeHead F (A →ₗc[R] B) :=
-  ⟨CoalgHomClass.toCoalgHom⟩
+  ⟨CoAlgHom.ofClass⟩
 
 @[simp]
 theorem counit_comp_apply (f : F) (x : A) : counit (f x) = counit (R := R) x :=
@@ -120,9 +121,10 @@ def Simps.apply {R α β : Type*} [CommSemiring R]
 initialize_simps_projections CoalgHom (toFun → apply)
 
 @[simp]
-protected theorem coe_coe {F : Type*} [FunLike F A B] [CoalgHomClass F R A B] (f : F) :
-    ⇑(f : A →ₗc[R] B) = f :=
+protected theorem coe_ofClass {F : Type*} [FunLike F A B] [CoalgHomClass F R A B] (f : F) :
+    ⇑(CoAlgHom.ofClass f) = f :=
   rfl
+@[deprecated (since := "2026-09-08")] alias coe_coe := CoalgHom.coe_ofClass
 
 @[simp]
 theorem coe_mk {f : A →ₗ[R] B} (h h₁) : ((⟨f, h, h₁⟩ : A →ₗc[R] B) : A → B) = f :=
@@ -136,10 +138,12 @@ theorem coe_mks {f : A → B} (h₁ h₂ h₃ h₄) : ⇑(⟨⟨⟨f, h₁⟩, h
 theorem coe_linearMap_mk {f : A →ₗ[R] B} (h h₁) : ((⟨f, h, h₁⟩ : A →ₗc[R] B) : A →ₗ[R] B) = f :=
   rfl
 
+-- TODO: rename to toLinearMap_eq_ofClass once the semilinear rename is merged!
 @[simp]
 theorem toLinearMap_eq_coe (f : A →ₗc[R] B) : f.toLinearMap = f :=
   rfl
 
+-- TODO: also rename/revisit name
 @[simp, norm_cast]
 theorem coe_toLinearMap (f : A →ₗc[R] B) : ⇑(f : A →ₗ[R] B) = f :=
   rfl
@@ -154,6 +158,7 @@ theorem coe_fn_injective : @Function.Injective (A →ₗc[R] B) (A → B) (↑)
 theorem coe_fn_inj {φ₁ φ₂ : A →ₗc[R] B} : (φ₁ : A → B) = φ₂ ↔ φ₁ = φ₂ :=
   DFunLike.coe_fn_eq
 
+-- TODO: call `linearMapOfClass` or similarly, after the rename
 theorem coe_linearMap_injective : Function.Injective ((↑) : (A →ₗc[R] B) → A →ₗ[R] B) :=
   fun φ₁ φ₂ H => coe_fn_injective <|
     show ((φ₁ : A →ₗ[R] B) : A → B) = ((φ₂ : A →ₗ[R] B) : A → B) from congr_arg _ H

Mathlib/RingTheory/Coalgebra/Primitive.lean

@@ -80,7 +80,7 @@ end IsSkewPrimitiveElem
 @[simp] lemma isSkewPrimitiveElem_map_equiv [EquivLike F A B] [CoalgEquivClass F R A B] (f : F) :
     IsSkewPrimitiveElem R (f g) (f h) (f a) ↔ IsSkewPrimitiveElem R g h a where
   mp ha :=
-    let e := CoalgEquivClass.toCoalgEquiv f
+    let e := CoalgEquiv.ofClass f
     e.symm_apply_apply g ▸ e.symm_apply_apply h ▸ e.symm_apply_apply a ▸ ha.map _
   mpr := .map f