feat: port Topology.Order.Hom.Esakia (#3108)

Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
Co-authored-by: Matthew Ballard <matt@mrb.email>

Mathlib.lean

@@ -2719,6 +2719,7 @@ import Mathlib.Topology.OmegaCompletePartialOrder
 import Mathlib.Topology.Order
 import Mathlib.Topology.Order.Basic
 import Mathlib.Topology.Order.Hom.Basic
+import Mathlib.Topology.Order.Hom.Esakia
 import Mathlib.Topology.Order.Lattice
 import Mathlib.Topology.Order.LowerTopology
 import Mathlib.Topology.Order.Priestley

Mathlib/Topology/Order/Hom/Basic.lean

@@ -56,23 +56,33 @@ class ContinuousOrderHomClass (F : Type _) (α β : outParam <| Type _) [Preorde
   map_monotone (f : F) : Monotone f
 #align continuous_order_hom_class ContinuousOrderHomClass
 
-end
+-- Porting note: namespaced these results since there are more than 3 now
+namespace ContinuousOrderHomClass
+
+variable [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β]
+  [ContinuousOrderHomClass F α β]
 
 -- See note [lower instance priority]
-instance (priority := 100) ContinuousOrderHomClass.toOrderHomClass [Preorder α] [Preorder β]
-    [TopologicalSpace α] [TopologicalSpace β] [ContinuousOrderHomClass F α β] :
+instance (priority := 100) toOrderHomClass  :
     OrderHomClass F α β :=
   { ‹ContinuousOrderHomClass F α β› with
     map_rel := ContinuousOrderHomClass.map_monotone }
 #align continuous_order_hom_class.to_continuous_map_class ContinuousOrderHomClass.toContinuousMapClass
 
-instance [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β]
-    [ContinuousOrderHomClass F α β] : CoeTC F (α →Co β) :=
-  ⟨fun f =>
+-- Porting note: following `OrderHomClass.toOrderHom` design, introduced a wrapper
+-- 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`.
+@[coe]
+def toContinuousOrderHom (f : F) : α →Co β :=
     { toFun := f
       monotone' := ContinuousOrderHomClass.map_monotone f
-      continuous_toFun := map_continuous f }⟩
+      continuous_toFun := map_continuous f }
+
+instance : CoeTC F (α →Co β) :=
+  ⟨toContinuousOrderHom⟩
 
+end ContinuousOrderHomClass
 /-! ### Top homomorphisms -/