chore: make sure that some coercions have an attached definition (#6667)

Mathlib/Algebra/Algebra/Equiv.lean

@@ -72,13 +72,16 @@ instance (priority := 100) toLinearEquivClass (F R A B : Type*) [CommSemiring R]
   { h with map_smulₛₗ := fun f => map_smulₛₗ f }
 #align alg_equiv_class.to_linear_equiv_class AlgEquivClass.toLinearEquivClass
 
+/-- 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] [AlgEquivClass F R A B] (f : F) : A ≃ₐ[R] B :=
+  { (f : A ≃ B), (f : A ≃+* B) with commutes' := commutes f }
+
 instance (F R A B : Type*) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
-    [_h : AlgEquivClass F R A B] : CoeTC F (A ≃ₐ[R] B) where
-  coe f :=
-    { (f : A ≃+* B) with
-      toFun := f
-      invFun := EquivLike.inv f
-      commutes' := AlgHomClass.commutes f }
+    [AlgEquivClass F R A B] : CoeTC F (A ≃ₐ[R] B) :=
+  ⟨toAlgEquiv⟩
 end AlgEquivClass
 
 namespace AlgEquiv

Mathlib/Algebra/Hom/NonUnitalAlg.lean

@@ -93,13 +93,19 @@ variable [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A]
 instance (priority := 100) {F : Type*} [NonUnitalAlgHomClass F R A B] : LinearMapClass F R A B :=
   { ‹NonUnitalAlgHomClass F R A B› with map_smulₛₗ := map_smul }
 
+/-- Turn an element of a type `F` satisfying `NonUnitalAlgHomClass F R A B` into an actual
+`NonUnitalAlgHom`. This is declared as the default coercion from `F` to `A →ₙₐ[R] B`. -/
+@[coe]
+def toNonUnitalAlgHom {F R A B : Type*} [Monoid R] [NonUnitalNonAssocSemiring A]
+    [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B]
+    [NonUnitalAlgHomClass F R A B] (f : F) : A →ₙₐ[R] B :=
+  { (f : A →ₙ+* B) with
+    map_smul' := map_smul f }
+
 instance {F R A B : Type*} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A]
     [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [NonUnitalAlgHomClass F R A B] :
-    CoeTC F (A →ₙₐ[R] B)
-    where coe f :=
-    { (f : A →ₙ+* B) with
-      toFun := f
-      map_smul' := map_smul f }
+    CoeTC F (A →ₙₐ[R] B) :=
+  ⟨toNonUnitalAlgHom⟩
 
 end NonUnitalAlgHomClass
 

Mathlib/Algebra/Star/StarAlgHom.lean

@@ -84,11 +84,15 @@ variable [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A]
 
 variable [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B]
 
-instance [NonUnitalStarAlgHomClass F R A B] : CoeTC F (A →⋆ₙₐ[R] B)
-    where coe f :=
-    { (f : A →ₙₐ[R] B) with
-      toFun := f
-      map_star' := map_star f }
+/-- 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`. -/
+@[coe]
+def toNonUnitalStarAlgHom [NonUnitalStarAlgHomClass F R 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) :=
+  ⟨toNonUnitalStarAlgHom⟩
 
 end NonUnitalStarAlgHomClass
 
@@ -339,11 +343,16 @@ variable [CommSemiring R] [Semiring A] [Algebra R A] [Star A]
 
 variable [Semiring B] [Algebra R B] [Star B] [hF : StarAlgHomClass F R A B]
 
-instance : CoeTC F (A →⋆ₐ[R] B)
-    where coe f :=
-    { (f : A →ₐ[R] B) with
-      toFun := f
-      map_star' := map_star f }
+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`. -/
+@[coe]
+def toStarAlgHom (f : F) : A →⋆ₐ[R] B :=
+  { (f : A →ₐ[R] B) with
+    map_star' := map_star f }
+
+instance : CoeTC F (A →⋆ₐ[R] B) :=
+  ⟨toStarAlgHom⟩
 
 end StarAlgHomClass
 

Mathlib/Order/Hom/Basic.lean

@@ -156,7 +156,7 @@ protected theorem mono (f : F) : Monotone f := fun _ _ => map_rel f
 #align order_hom_class.mono OrderHomClass.mono
 
 /-- Turn an element of a type `F` satisfying `OrderHomClass F α β` into an actual
-`OrderHomClass`. This is declared as the default coercion from `F` to `α →o β`. -/
+`OrderHom`. This is declared as the default coercion from `F` to `α →o β`. -/
 @[coe]
 def toOrderHom (f : F) : α →o β where
   toFun := f

Mathlib/Topology/ContinuousFunction/CocompactMap.lean

@@ -53,8 +53,15 @@ namespace CocompactMapClass
 
 variable {F α β : Type*} [TopologicalSpace α] [TopologicalSpace β] [CocompactMapClass F α β]
 
+/-- Turn an element of a type `F` satisfying `CocompactMapClass F α β` into an actual
+`CocompactMap`. This is declared as the default coercion from `F` to `CocompactMap α β`. -/
+@[coe]
+def toCocompactMap (f : F) : CocompactMap α β :=
+  { (f : C(α, β)) with
+    cocompact_tendsto' := cocompact_tendsto f }
+
 instance : CoeTC F (CocompactMap α β) :=
-  ⟨fun f => ⟨f, cocompact_tendsto f⟩⟩
+  ⟨toCocompactMap⟩
 
 end CocompactMapClass
 

Mathlib/Topology/Order/Hom/Basic.lean

@@ -70,6 +70,8 @@ instance (priority := 100) toOrderHomClass  :
 -- for the original coercion. The original one directly exposed
 -- ContinuousOrderHom.mk which allowed simp to apply more eagerly than in all
 -- the other results in `Topology.Order.Hom.Esakia`.
+/-- Turn an element of a type `F` satisfying `ContinuousOrderHomClass F α β` into an actual
+`ContinuousOrderHom`. This is declared as the default coercion from `F` to `α →Co β`. -/
 @[coe]
 def toContinuousOrderHom (f : F) : α →Co β :=
     { toFun := f
@@ -203,4 +205,3 @@ instance [PartialOrder β] : PartialOrder (α →Co β) :=
   PartialOrder.lift ((↑) : (α →Co β) → α → β) FunLike.coe_injective
 
 end ContinuousOrderHom
-