From 8760a42c73934d6fb194a09547e5f3b1074f062a Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sun, 26 Mar 2023 00:08:19 -0500
Subject: [PATCH 01/11] feat: port Topology.Order.Hom.Esakia


From b09992982fa63b6fb3f1c58040081d804f84068e Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sun, 26 Mar 2023 00:08:19 -0500
Subject: [PATCH 02/11] Initial file copy from mathport

---
 Mathlib/Topology/Order/Hom/Esakia.lean | 383 +++++++++++++++++++++++++
 1 file changed, 383 insertions(+)
 create mode 100644 Mathlib/Topology/Order/Hom/Esakia.lean

diff --git a/Mathlib/Topology/Order/Hom/Esakia.lean b/Mathlib/Topology/Order/Hom/Esakia.lean
new file mode 100644
index 0000000000000..3a5e467079a0a
--- /dev/null
+++ b/Mathlib/Topology/Order/Hom/Esakia.lean
@@ -0,0 +1,383 @@
+/-
+Copyright (c) 2022 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+
+! This file was ported from Lean 3 source module topology.order.hom.esakia
+! leanprover-community/mathlib commit 9822b65bfc4ac74537d77ae318d27df1df662471
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathbin.Order.Hom.Bounded
+import Mathbin.Topology.Order.Hom.Basic
+
+/-!
+# Esakia morphisms
+
+This file defines pseudo-epimorphisms and Esakia morphisms.
+
+We use the `fun_like` design, so each type of morphisms has a companion typeclass which is meant to
+be satisfied by itself and all stricter types.
+
+## Types of morphisms
+
+* `pseudo_epimorphism`: Pseudo-epimorphisms. Maps `f` such that `f a ≤ b` implies the existence of
+  `a'` such that `a ≤ a'` and `f a' = b`.
+* `esakia_hom`: Esakia morphisms. Continuous pseudo-epimorphisms.
+
+## Typeclasses
+
+* `pseudo_epimorphism_class`
+* `esakia_hom_class`
+
+## References
+
+* [Wikipedia, *Esakia space*](https://en.wikipedia.org/wiki/Esakia_space)
+-/
+
+
+open Function
+
+variable {F α β γ δ : Type _}
+
+/-- The type of pseudo-epimorphisms, aka p-morphisms, aka bounded maps, from `α` to `β`. -/
+structure PseudoEpimorphism (α β : Type _) [Preorder α] [Preorder β] extends α →o β where
+  exists_map_eq_of_map_le' ⦃a : α⦄ ⦃b : β⦄ : to_fun a ≤ b → ∃ c, a ≤ c ∧ to_fun c = b
+#align pseudo_epimorphism PseudoEpimorphism
+
+/-- The type of Esakia morphisms, aka continuous pseudo-epimorphisms, from `α` to `β`. -/
+structure EsakiaHom (α β : Type _) [TopologicalSpace α] [Preorder α] [TopologicalSpace β]
+  [Preorder β] extends α →Co β where
+  exists_map_eq_of_map_le' ⦃a : α⦄ ⦃b : β⦄ : to_fun a ≤ b → ∃ c, a ≤ c ∧ to_fun c = b
+#align esakia_hom EsakiaHom
+
+section
+
+/-- `pseudo_epimorphism_class F α β` states that `F` is a type of `⊔`-preserving morphisms.
+
+You should extend this class when you extend `pseudo_epimorphism`. -/
+class PseudoEpimorphismClass (F : Type _) (α β : outParam <| Type _) [Preorder α]
+  [Preorder β] extends RelHomClass F ((· ≤ ·) : α → α → Prop) ((· ≤ ·) : β → β → Prop) where
+  exists_map_eq_of_map_le (f : F) ⦃a : α⦄ ⦃b : β⦄ : f a ≤ b → ∃ c, a ≤ c ∧ f c = b
+#align pseudo_epimorphism_class PseudoEpimorphismClass
+
+/-- `esakia_hom_class F α β` states that `F` is a type of lattice morphisms.
+
+You should extend this class when you extend `esakia_hom`. -/
+class EsakiaHomClass (F : Type _) (α β : outParam <| Type _) [TopologicalSpace α] [Preorder α]
+  [TopologicalSpace β] [Preorder β] extends ContinuousOrderHomClass F α β where
+  exists_map_eq_of_map_le (f : F) ⦃a : α⦄ ⦃b : β⦄ : f a ≤ b → ∃ c, a ≤ c ∧ f c = b
+#align esakia_hom_class EsakiaHomClass
+
+end
+
+export PseudoEpimorphismClass (exists_map_eq_of_map_le)
+
+-- See note [lower instance priority]
+instance (priority := 100) PseudoEpimorphismClass.toTopHomClass [PartialOrder α] [OrderTop α]
+    [Preorder β] [OrderTop β] [PseudoEpimorphismClass F α β] : TopHomClass F α β :=
+  { ‹PseudoEpimorphismClass F α β› with
+    map_top := fun f =>
+      by
+      let ⟨b, h⟩ := exists_map_eq_of_map_le f (@le_top _ _ _ <| f ⊤)
+      rw [← top_le_iff.1 h.1, h.2] }
+#align pseudo_epimorphism_class.to_top_hom_class PseudoEpimorphismClass.toTopHomClass
+
+-- See note [lower instance priority]
+instance (priority := 100) OrderIsoClass.toPseudoEpimorphismClass [Preorder α] [Preorder β]
+    [OrderIsoClass F α β] : PseudoEpimorphismClass F α β :=
+  { OrderIsoClass.toOrderHomClass with
+    exists_map_eq_of_map_le := fun f a b h =>
+      ⟨EquivLike.inv f b, (le_map_inv_iff f).2 h, EquivLike.right_inv _ _⟩ }
+#align order_iso_class.to_pseudo_epimorphism_class OrderIsoClass.toPseudoEpimorphismClass
+
+-- See note [lower instance priority]
+instance (priority := 100) EsakiaHomClass.toPseudoEpimorphismClass [TopologicalSpace α] [Preorder α]
+    [TopologicalSpace β] [Preorder β] [EsakiaHomClass F α β] : PseudoEpimorphismClass F α β :=
+  { ‹EsakiaHomClass F α β› with }
+#align esakia_hom_class.to_pseudo_epimorphism_class EsakiaHomClass.toPseudoEpimorphismClass
+
+instance [Preorder α] [Preorder β] [PseudoEpimorphismClass F α β] :
+    CoeTC F (PseudoEpimorphism α β) :=
+  ⟨fun f => ⟨f, exists_map_eq_of_map_le f⟩⟩
+
+instance [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β]
+    [EsakiaHomClass F α β] : CoeTC F (EsakiaHom α β) :=
+  ⟨fun f => ⟨f, exists_map_eq_of_map_le f⟩⟩
+
+/-! ### Pseudo-epimorphisms -/
+
+
+namespace PseudoEpimorphism
+
+variable [Preorder α] [Preorder β] [Preorder γ] [Preorder δ]
+
+instance : PseudoEpimorphismClass (PseudoEpimorphism α β) α β
+    where
+  coe f := f.toFun
+  coe_injective' f g h := by
+    obtain ⟨⟨_, _⟩, _⟩ := f
+    obtain ⟨⟨_, _⟩, _⟩ := g
+    congr
+  map_rel f := f.monotone'
+  exists_map_eq_of_map_le := PseudoEpimorphism.exists_map_eq_of_map_le'
+
+/-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
+directly. -/
+instance : CoeFun (PseudoEpimorphism α β) fun _ => α → β :=
+  FunLike.hasCoeToFun
+
+@[simp]
+theorem toFun_eq_coe {f : PseudoEpimorphism α β} : f.toFun = (f : α → β) :=
+  rfl
+#align pseudo_epimorphism.to_fun_eq_coe PseudoEpimorphism.toFun_eq_coe
+
+@[ext]
+theorem ext {f g : PseudoEpimorphism α β} (h : ∀ a, f a = g a) : f = g :=
+  FunLike.ext f g h
+#align pseudo_epimorphism.ext PseudoEpimorphism.ext
+
+/-- Copy of a `pseudo_epimorphism` with a new `to_fun` equal to the old one. Useful to fix
+definitional equalities. -/
+protected def copy (f : PseudoEpimorphism α β) (f' : α → β) (h : f' = f) : PseudoEpimorphism α β :=
+  ⟨f.toOrderHom.copy f' h, by simpa only [h.symm, to_fun_eq_coe] using f.exists_map_eq_of_map_le'⟩
+#align pseudo_epimorphism.copy PseudoEpimorphism.copy
+
+@[simp]
+theorem coe_copy (f : PseudoEpimorphism α β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f' :=
+  rfl
+#align pseudo_epimorphism.coe_copy PseudoEpimorphism.coe_copy
+
+theorem copy_eq (f : PseudoEpimorphism α β) (f' : α → β) (h : f' = f) : f.copy f' h = f :=
+  FunLike.ext' h
+#align pseudo_epimorphism.copy_eq PseudoEpimorphism.copy_eq
+
+variable (α)
+
+/-- `id` as a `pseudo_epimorphism`. -/
+protected def id : PseudoEpimorphism α α :=
+  ⟨OrderHom.id, fun a b h => ⟨b, h, rfl⟩⟩
+#align pseudo_epimorphism.id PseudoEpimorphism.id
+
+instance : Inhabited (PseudoEpimorphism α α) :=
+  ⟨PseudoEpimorphism.id α⟩
+
+@[simp]
+theorem coe_id : ⇑(PseudoEpimorphism.id α) = id :=
+  rfl
+#align pseudo_epimorphism.coe_id PseudoEpimorphism.coe_id
+
+@[simp]
+theorem coe_id_orderHom : (PseudoEpimorphism.id α : α →o α) = OrderHom.id :=
+  rfl
+#align pseudo_epimorphism.coe_id_order_hom PseudoEpimorphism.coe_id_orderHom
+
+variable {α}
+
+@[simp]
+theorem id_apply (a : α) : PseudoEpimorphism.id α a = a :=
+  rfl
+#align pseudo_epimorphism.id_apply PseudoEpimorphism.id_apply
+
+/-- Composition of `pseudo_epimorphism`s as a `pseudo_epimorphism`. -/
+def comp (g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β) : PseudoEpimorphism α γ :=
+  ⟨g.toOrderHom.comp f.toOrderHom, fun a b h₀ =>
+    by
+    obtain ⟨b, h₁, rfl⟩ := g.exists_map_eq_of_map_le' h₀
+    obtain ⟨b, h₂, rfl⟩ := f.exists_map_eq_of_map_le' h₁
+    exact ⟨b, h₂, rfl⟩⟩
+#align pseudo_epimorphism.comp PseudoEpimorphism.comp
+
+@[simp]
+theorem coe_comp (g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β) :
+    (g.comp f : α → γ) = g ∘ f :=
+  rfl
+#align pseudo_epimorphism.coe_comp PseudoEpimorphism.coe_comp
+
+@[simp]
+theorem coe_comp_orderHom (g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β) :
+    (g.comp f : α →o γ) = (g : β →o γ).comp f :=
+  rfl
+#align pseudo_epimorphism.coe_comp_order_hom PseudoEpimorphism.coe_comp_orderHom
+
+@[simp]
+theorem comp_apply (g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β) (a : α) :
+    (g.comp f) a = g (f a) :=
+  rfl
+#align pseudo_epimorphism.comp_apply PseudoEpimorphism.comp_apply
+
+@[simp]
+theorem comp_assoc (h : PseudoEpimorphism γ δ) (g : PseudoEpimorphism β γ)
+    (f : PseudoEpimorphism α β) : (h.comp g).comp f = h.comp (g.comp f) :=
+  rfl
+#align pseudo_epimorphism.comp_assoc PseudoEpimorphism.comp_assoc
+
+@[simp]
+theorem comp_id (f : PseudoEpimorphism α β) : f.comp (PseudoEpimorphism.id α) = f :=
+  ext fun a => rfl
+#align pseudo_epimorphism.comp_id PseudoEpimorphism.comp_id
+
+@[simp]
+theorem id_comp (f : PseudoEpimorphism α β) : (PseudoEpimorphism.id β).comp f = f :=
+  ext fun a => rfl
+#align pseudo_epimorphism.id_comp PseudoEpimorphism.id_comp
+
+theorem cancel_right {g₁ g₂ : PseudoEpimorphism β γ} {f : PseudoEpimorphism α β}
+    (hf : Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
+  ⟨fun h => ext <| hf.forall.2 <| FunLike.ext_iff.1 h, congr_arg _⟩
+#align pseudo_epimorphism.cancel_right PseudoEpimorphism.cancel_right
+
+theorem cancel_left {g : PseudoEpimorphism β γ} {f₁ f₂ : PseudoEpimorphism α β} (hg : Injective g) :
+    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
+  ⟨fun h => ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩
+#align pseudo_epimorphism.cancel_left PseudoEpimorphism.cancel_left
+
+end PseudoEpimorphism
+
+/-! ### Esakia morphisms -/
+
+
+namespace EsakiaHom
+
+variable [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [TopologicalSpace γ]
+  [Preorder γ] [TopologicalSpace δ] [Preorder δ]
+
+/-- Reinterpret an `esakia_hom` as a `pseudo_epimorphism`. -/
+def toPseudoEpimorphism (f : EsakiaHom α β) : PseudoEpimorphism α β :=
+  { f with }
+#align esakia_hom.to_pseudo_epimorphism EsakiaHom.toPseudoEpimorphism
+
+instance : EsakiaHomClass (EsakiaHom α β) α β
+    where
+  coe f := f.toFun
+  coe_injective' f g h := by
+    obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
+    obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
+    congr
+  map_rel f := f.monotone'
+  map_continuous f := f.continuous_toFun
+  exists_map_eq_of_map_le f := f.exists_map_eq_of_map_le'
+
+/-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
+directly. -/
+instance : CoeFun (EsakiaHom α β) fun _ => α → β :=
+  FunLike.hasCoeToFun
+
+@[simp]
+theorem toFun_eq_coe {f : EsakiaHom α β} : f.toFun = (f : α → β) :=
+  rfl
+#align esakia_hom.to_fun_eq_coe EsakiaHom.toFun_eq_coe
+
+@[ext]
+theorem ext {f g : EsakiaHom α β} (h : ∀ a, f a = g a) : f = g :=
+  FunLike.ext f g h
+#align esakia_hom.ext EsakiaHom.ext
+
+/-- Copy of an `esakia_hom` with a new `to_fun` equal to the old one. Useful to fix definitional
+equalities. -/
+protected def copy (f : EsakiaHom α β) (f' : α → β) (h : f' = f) : EsakiaHom α β :=
+  ⟨f.toContinuousOrderHom.copy f' h, by
+    simpa only [h.symm, to_fun_eq_coe] using f.exists_map_eq_of_map_le'⟩
+#align esakia_hom.copy EsakiaHom.copy
+
+@[simp]
+theorem coe_copy (f : EsakiaHom α β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f' :=
+  rfl
+#align esakia_hom.coe_copy EsakiaHom.coe_copy
+
+theorem copy_eq (f : EsakiaHom α β) (f' : α → β) (h : f' = f) : f.copy f' h = f :=
+  FunLike.ext' h
+#align esakia_hom.copy_eq EsakiaHom.copy_eq
+
+variable (α)
+
+/-- `id` as an `esakia_hom`. -/
+protected def id : EsakiaHom α α :=
+  ⟨ContinuousOrderHom.id α, fun a b h => ⟨b, h, rfl⟩⟩
+#align esakia_hom.id EsakiaHom.id
+
+instance : Inhabited (EsakiaHom α α) :=
+  ⟨EsakiaHom.id α⟩
+
+@[simp]
+theorem coe_id : ⇑(EsakiaHom.id α) = id :=
+  rfl
+#align esakia_hom.coe_id EsakiaHom.coe_id
+
+@[simp]
+theorem coe_id_continuousOrderHom : (EsakiaHom.id α : α →Co α) = ContinuousOrderHom.id α :=
+  rfl
+#align esakia_hom.coe_id_continuous_order_hom EsakiaHom.coe_id_continuousOrderHom
+
+@[simp]
+theorem coe_id_pseudoEpimorphism :
+    (EsakiaHom.id α : PseudoEpimorphism α α) = PseudoEpimorphism.id α :=
+  rfl
+#align esakia_hom.coe_id_pseudo_epimorphism EsakiaHom.coe_id_pseudoEpimorphism
+
+variable {α}
+
+@[simp]
+theorem id_apply (a : α) : EsakiaHom.id α a = a :=
+  rfl
+#align esakia_hom.id_apply EsakiaHom.id_apply
+
+/-- Composition of `esakia_hom`s as an `esakia_hom`. -/
+def comp (g : EsakiaHom β γ) (f : EsakiaHom α β) : EsakiaHom α γ :=
+  ⟨g.toContinuousOrderHom.comp f.toContinuousOrderHom, fun a b h₀ =>
+    by
+    obtain ⟨b, h₁, rfl⟩ := g.exists_map_eq_of_map_le' h₀
+    obtain ⟨b, h₂, rfl⟩ := f.exists_map_eq_of_map_le' h₁
+    exact ⟨b, h₂, rfl⟩⟩
+#align esakia_hom.comp EsakiaHom.comp
+
+@[simp]
+theorem coe_comp (g : EsakiaHom β γ) (f : EsakiaHom α β) : (g.comp f : α → γ) = g ∘ f :=
+  rfl
+#align esakia_hom.coe_comp EsakiaHom.coe_comp
+
+@[simp]
+theorem comp_apply (g : EsakiaHom β γ) (f : EsakiaHom α β) (a : α) : (g.comp f) a = g (f a) :=
+  rfl
+#align esakia_hom.comp_apply EsakiaHom.comp_apply
+
+@[simp]
+theorem coe_comp_continuousOrderHom (g : EsakiaHom β γ) (f : EsakiaHom α β) :
+    (g.comp f : α →Co γ) = (g : β →Co γ).comp f :=
+  rfl
+#align esakia_hom.coe_comp_continuous_order_hom EsakiaHom.coe_comp_continuousOrderHom
+
+@[simp]
+theorem coe_comp_pseudoEpimorphism (g : EsakiaHom β γ) (f : EsakiaHom α β) :
+    (g.comp f : PseudoEpimorphism α γ) = (g : PseudoEpimorphism β γ).comp f :=
+  rfl
+#align esakia_hom.coe_comp_pseudo_epimorphism EsakiaHom.coe_comp_pseudoEpimorphism
+
+@[simp]
+theorem comp_assoc (h : EsakiaHom γ δ) (g : EsakiaHom β γ) (f : EsakiaHom α β) :
+    (h.comp g).comp f = h.comp (g.comp f) :=
+  rfl
+#align esakia_hom.comp_assoc EsakiaHom.comp_assoc
+
+@[simp]
+theorem comp_id (f : EsakiaHom α β) : f.comp (EsakiaHom.id α) = f :=
+  ext fun a => rfl
+#align esakia_hom.comp_id EsakiaHom.comp_id
+
+@[simp]
+theorem id_comp (f : EsakiaHom α β) : (EsakiaHom.id β).comp f = f :=
+  ext fun a => rfl
+#align esakia_hom.id_comp EsakiaHom.id_comp
+
+theorem cancel_right {g₁ g₂ : EsakiaHom β γ} {f : EsakiaHom α β} (hf : Surjective f) :
+    g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
+  ⟨fun h => ext <| hf.forall.2 <| FunLike.ext_iff.1 h, congr_arg _⟩
+#align esakia_hom.cancel_right EsakiaHom.cancel_right
+
+theorem cancel_left {g : EsakiaHom β γ} {f₁ f₂ : EsakiaHom α β} (hg : Injective g) :
+    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
+  ⟨fun h => ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩
+#align esakia_hom.cancel_left EsakiaHom.cancel_left
+
+end EsakiaHom
+

From 7bfd513ab15169f62d6ae4784ca9d9c7790fbf1b Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sun, 26 Mar 2023 00:08:20 -0500
Subject: [PATCH 03/11] automated fixes

Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
---
 Mathlib.lean                           | 1 +
 Mathlib/Topology/Order/Hom/Esakia.lean | 4 ++--
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 81688371d7383..fb126ea42aace 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1613,6 +1613,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
diff --git a/Mathlib/Topology/Order/Hom/Esakia.lean b/Mathlib/Topology/Order/Hom/Esakia.lean
index 3a5e467079a0a..2cba3f11bcd9a 100644
--- a/Mathlib/Topology/Order/Hom/Esakia.lean
+++ b/Mathlib/Topology/Order/Hom/Esakia.lean
@@ -8,8 +8,8 @@ Authors: Yaël Dillies
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathbin.Order.Hom.Bounded
-import Mathbin.Topology.Order.Hom.Basic
+import Mathlib.Order.Hom.Bounded
+import Mathlib.Topology.Order.Hom.Basic
 
 /-!
 # Esakia morphisms

From e256de4efb22f0a4bfb458131cdb1fae41dee854 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sun, 26 Mar 2023 00:21:24 -0500
Subject: [PATCH 04/11] Partially fix

---
 Mathlib/Topology/Order/Hom/Esakia.lean | 33 ++++++++++++--------------
 1 file changed, 15 insertions(+), 18 deletions(-)

diff --git a/Mathlib/Topology/Order/Hom/Esakia.lean b/Mathlib/Topology/Order/Hom/Esakia.lean
index 2cba3f11bcd9a..6c5a21cc0ff6c 100644
--- a/Mathlib/Topology/Order/Hom/Esakia.lean
+++ b/Mathlib/Topology/Order/Hom/Esakia.lean
@@ -42,13 +42,13 @@ variable {F α β γ δ : Type _}
 
 /-- The type of pseudo-epimorphisms, aka p-morphisms, aka bounded maps, from `α` to `β`. -/
 structure PseudoEpimorphism (α β : Type _) [Preorder α] [Preorder β] extends α →o β where
-  exists_map_eq_of_map_le' ⦃a : α⦄ ⦃b : β⦄ : to_fun a ≤ b → ∃ c, a ≤ c ∧ to_fun c = b
+  exists_map_eq_of_map_le' ⦃a : α⦄ ⦃b : β⦄ : toFun a ≤ b → ∃ c, a ≤ c ∧ toFun c = b
 #align pseudo_epimorphism PseudoEpimorphism
 
 /-- The type of Esakia morphisms, aka continuous pseudo-epimorphisms, from `α` to `β`. -/
 structure EsakiaHom (α β : Type _) [TopologicalSpace α] [Preorder α] [TopologicalSpace β]
   [Preorder β] extends α →Co β where
-  exists_map_eq_of_map_le' ⦃a : α⦄ ⦃b : β⦄ : to_fun a ≤ b → ∃ c, a ≤ c ∧ to_fun c = b
+  exists_map_eq_of_map_le' ⦃a : α⦄ ⦃b : β⦄ : toFun a ≤ b → ∃ c, a ≤ c ∧ toFun c = b
 #align esakia_hom EsakiaHom
 
 section
@@ -75,26 +75,24 @@ export PseudoEpimorphismClass (exists_map_eq_of_map_le)
 
 -- See note [lower instance priority]
 instance (priority := 100) PseudoEpimorphismClass.toTopHomClass [PartialOrder α] [OrderTop α]
-    [Preorder β] [OrderTop β] [PseudoEpimorphismClass F α β] : TopHomClass F α β :=
-  { ‹PseudoEpimorphismClass F α β› with
-    map_top := fun f =>
-      by
-      let ⟨b, h⟩ := exists_map_eq_of_map_le f (@le_top _ _ _ <| f ⊤)
-      rw [← top_le_iff.1 h.1, h.2] }
+    [Preorder β] [OrderTop β] [PseudoEpimorphismClass F α β] : TopHomClass F α β where
+  map_top := fun f => by
+    let ⟨b, h⟩ := exists_map_eq_of_map_le f (@le_top _ _ _ <| f ⊤)
+    rw [← top_le_iff.1 h.1, h.2]
 #align pseudo_epimorphism_class.to_top_hom_class PseudoEpimorphismClass.toTopHomClass
 
 -- See note [lower instance priority]
 instance (priority := 100) OrderIsoClass.toPseudoEpimorphismClass [Preorder α] [Preorder β]
-    [OrderIsoClass F α β] : PseudoEpimorphismClass F α β :=
-  { OrderIsoClass.toOrderHomClass with
-    exists_map_eq_of_map_le := fun f a b h =>
-      ⟨EquivLike.inv f b, (le_map_inv_iff f).2 h, EquivLike.right_inv _ _⟩ }
+    [OrderIsoClass F α β] : PseudoEpimorphismClass F α β where
+  exists_map_eq_of_map_le := fun f _a b h =>
+    ⟨EquivLike.inv f b, (le_map_inv_iff f).2 h, EquivLike.right_inv _ _⟩
 #align order_iso_class.to_pseudo_epimorphism_class OrderIsoClass.toPseudoEpimorphismClass
 
 -- See note [lower instance priority]
 instance (priority := 100) EsakiaHomClass.toPseudoEpimorphismClass [TopologicalSpace α] [Preorder α]
     [TopologicalSpace β] [Preorder β] [EsakiaHomClass F α β] : PseudoEpimorphismClass F α β :=
-  { ‹EsakiaHomClass F α β› with }
+  { ‹EsakiaHomClass F α β› with
+    map_rel := ContinuousOrderHomClass.map_monotone }
 #align esakia_hom_class.to_pseudo_epimorphism_class EsakiaHomClass.toPseudoEpimorphismClass
 
 instance [Preorder α] [Preorder β] [PseudoEpimorphismClass F α β] :
@@ -112,20 +110,19 @@ namespace PseudoEpimorphism
 
 variable [Preorder α] [Preorder β] [Preorder γ] [Preorder δ]
 
-instance : PseudoEpimorphismClass (PseudoEpimorphism α β) α β
-    where
+instance : PseudoEpimorphismClass (PseudoEpimorphism α β) α β where
   coe f := f.toFun
   coe_injective' f g h := by
     obtain ⟨⟨_, _⟩, _⟩ := f
     obtain ⟨⟨_, _⟩, _⟩ := g
     congr
-  map_rel f := f.monotone'
+  map_rel f _ _ h := f.monotone' h
   exists_map_eq_of_map_le := PseudoEpimorphism.exists_map_eq_of_map_le'
 
 /-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
 directly. -/
-instance : CoeFun (PseudoEpimorphism α β) fun _ => α → β :=
-  FunLike.hasCoeToFun
+-- instance : CoeFun (PseudoEpimorphism α β) fun _ => α → β :=
+--   FunLike.hasCoeToFun
 
 @[simp]
 theorem toFun_eq_coe {f : PseudoEpimorphism α β} : f.toFun = (f : α → β) :=

From 74987391a59802f9d8cf5f65e46a76ffa130f9eb Mon Sep 17 00:00:00 2001
From: int-y1 <jason_yuen2007@hotmail.com>
Date: Sat, 6 May 2023 00:59:26 -0700
Subject: [PATCH 05/11] fix

---
 Mathlib/Topology/Order/Hom/Esakia.lean | 23 +++++++++++------------
 1 file changed, 11 insertions(+), 12 deletions(-)

diff --git a/Mathlib/Topology/Order/Hom/Esakia.lean b/Mathlib/Topology/Order/Hom/Esakia.lean
index 6c5a21cc0ff6c..d7a6ee1d27cee 100644
--- a/Mathlib/Topology/Order/Hom/Esakia.lean
+++ b/Mathlib/Topology/Order/Hom/Esakia.lean
@@ -137,7 +137,7 @@ theorem ext {f g : PseudoEpimorphism α β} (h : ∀ a, f a = g a) : f = g :=
 /-- Copy of a `pseudo_epimorphism` with a new `to_fun` equal to the old one. Useful to fix
 definitional equalities. -/
 protected def copy (f : PseudoEpimorphism α β) (f' : α → β) (h : f' = f) : PseudoEpimorphism α β :=
-  ⟨f.toOrderHom.copy f' h, by simpa only [h.symm, to_fun_eq_coe] using f.exists_map_eq_of_map_le'⟩
+  ⟨f.toOrderHom.copy f' h, by simpa only [h.symm, toFun_eq_coe] using f.exists_map_eq_of_map_le'⟩
 #align pseudo_epimorphism.copy PseudoEpimorphism.copy
 
 @[simp]
@@ -153,7 +153,7 @@ variable (α)
 
 /-- `id` as a `pseudo_epimorphism`. -/
 protected def id : PseudoEpimorphism α α :=
-  ⟨OrderHom.id, fun a b h => ⟨b, h, rfl⟩⟩
+  ⟨OrderHom.id, fun _ b h => ⟨b, h, rfl⟩⟩
 #align pseudo_epimorphism.id PseudoEpimorphism.id
 
 instance : Inhabited (PseudoEpimorphism α α) :=
@@ -211,17 +211,17 @@ theorem comp_assoc (h : PseudoEpimorphism γ δ) (g : PseudoEpimorphism β γ)
 
 @[simp]
 theorem comp_id (f : PseudoEpimorphism α β) : f.comp (PseudoEpimorphism.id α) = f :=
-  ext fun a => rfl
+  ext fun _ => rfl
 #align pseudo_epimorphism.comp_id PseudoEpimorphism.comp_id
 
 @[simp]
 theorem id_comp (f : PseudoEpimorphism α β) : (PseudoEpimorphism.id β).comp f = f :=
-  ext fun a => rfl
+  ext fun _ => rfl
 #align pseudo_epimorphism.id_comp PseudoEpimorphism.id_comp
 
 theorem cancel_right {g₁ g₂ : PseudoEpimorphism β γ} {f : PseudoEpimorphism α β}
     (hf : Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
-  ⟨fun h => ext <| hf.forall.2 <| FunLike.ext_iff.1 h, congr_arg _⟩
+  ⟨fun h => ext <| hf.forall.2 <| FunLike.ext_iff.1 h, by intro h; rw [h]⟩
 #align pseudo_epimorphism.cancel_right PseudoEpimorphism.cancel_right
 
 theorem cancel_left {g : PseudoEpimorphism β γ} {f₁ f₂ : PseudoEpimorphism α β} (hg : Injective g) :
@@ -251,7 +251,7 @@ instance : EsakiaHomClass (EsakiaHom α β) α β
     obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
     obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
     congr
-  map_rel f := f.monotone'
+  map_monotone f := f.monotone'
   map_continuous f := f.continuous_toFun
   exists_map_eq_of_map_le f := f.exists_map_eq_of_map_le'
 
@@ -274,7 +274,7 @@ theorem ext {f g : EsakiaHom α β} (h : ∀ a, f a = g a) : f = g :=
 equalities. -/
 protected def copy (f : EsakiaHom α β) (f' : α → β) (h : f' = f) : EsakiaHom α β :=
   ⟨f.toContinuousOrderHom.copy f' h, by
-    simpa only [h.symm, to_fun_eq_coe] using f.exists_map_eq_of_map_le'⟩
+    simpa only [h.symm, toFun_eq_coe] using f.exists_map_eq_of_map_le'⟩
 #align esakia_hom.copy EsakiaHom.copy
 
 @[simp]
@@ -290,7 +290,7 @@ variable (α)
 
 /-- `id` as an `esakia_hom`. -/
 protected def id : EsakiaHom α α :=
-  ⟨ContinuousOrderHom.id α, fun a b h => ⟨b, h, rfl⟩⟩
+  ⟨ContinuousOrderHom.id α, fun _ b h => ⟨b, h, rfl⟩⟩
 #align esakia_hom.id EsakiaHom.id
 
 instance : Inhabited (EsakiaHom α α) :=
@@ -358,17 +358,17 @@ theorem comp_assoc (h : EsakiaHom γ δ) (g : EsakiaHom β γ) (f : EsakiaHom α
 
 @[simp]
 theorem comp_id (f : EsakiaHom α β) : f.comp (EsakiaHom.id α) = f :=
-  ext fun a => rfl
+  ext fun _ => rfl
 #align esakia_hom.comp_id EsakiaHom.comp_id
 
 @[simp]
 theorem id_comp (f : EsakiaHom α β) : (EsakiaHom.id β).comp f = f :=
-  ext fun a => rfl
+  ext fun _ => rfl
 #align esakia_hom.id_comp EsakiaHom.id_comp
 
 theorem cancel_right {g₁ g₂ : EsakiaHom β γ} {f : EsakiaHom α β} (hf : Surjective f) :
     g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
-  ⟨fun h => ext <| hf.forall.2 <| FunLike.ext_iff.1 h, congr_arg _⟩
+  ⟨fun h => ext <| hf.forall.2 <| FunLike.ext_iff.1 h, by intro h; rw [h]⟩
 #align esakia_hom.cancel_right EsakiaHom.cancel_right
 
 theorem cancel_left {g : EsakiaHom β γ} {f₁ f₂ : EsakiaHom α β} (hg : Injective g) :
@@ -377,4 +377,3 @@ theorem cancel_left {g : EsakiaHom β γ} {f₁ f₂ : EsakiaHom α β} (hg : In
 #align esakia_hom.cancel_left EsakiaHom.cancel_left
 
 end EsakiaHom
-

From 8a83142890651eb83464393814cab91258e380eb Mon Sep 17 00:00:00 2001
From: int-y1 <jason_yuen2007@hotmail.com>
Date: Sat, 6 May 2023 01:08:06 -0700
Subject: [PATCH 06/11] code style

---
 Mathlib/Topology/Order/Hom/Esakia.lean | 83 ++++++++++----------------
 1 file changed, 30 insertions(+), 53 deletions(-)

diff --git a/Mathlib/Topology/Order/Hom/Esakia.lean b/Mathlib/Topology/Order/Hom/Esakia.lean
index d7a6ee1d27cee..fe735b27ca9c8 100644
--- a/Mathlib/Topology/Order/Hom/Esakia.lean
+++ b/Mathlib/Topology/Order/Hom/Esakia.lean
@@ -56,8 +56,8 @@ section
 /-- `pseudo_epimorphism_class F α β` states that `F` is a type of `⊔`-preserving morphisms.
 
 You should extend this class when you extend `pseudo_epimorphism`. -/
-class PseudoEpimorphismClass (F : Type _) (α β : outParam <| Type _) [Preorder α]
-  [Preorder β] extends RelHomClass F ((· ≤ ·) : α → α → Prop) ((· ≤ ·) : β → β → Prop) where
+class PseudoEpimorphismClass (F : Type _) (α β : outParam <| Type _) [Preorder α] [Preorder β]
+    extends RelHomClass F ((· ≤ ·) : α → α → Prop) ((· ≤ ·) : β → β → Prop) where
   exists_map_eq_of_map_le (f : F) ⦃a : α⦄ ⦃b : β⦄ : f a ≤ b → ∃ c, a ≤ c ∧ f c = b
 #align pseudo_epimorphism_class PseudoEpimorphismClass
 
@@ -65,7 +65,7 @@ class PseudoEpimorphismClass (F : Type _) (α β : outParam <| Type _) [Preorder
 
 You should extend this class when you extend `esakia_hom`. -/
 class EsakiaHomClass (F : Type _) (α β : outParam <| Type _) [TopologicalSpace α] [Preorder α]
-  [TopologicalSpace β] [Preorder β] extends ContinuousOrderHomClass F α β where
+    [TopologicalSpace β] [Preorder β] extends ContinuousOrderHomClass F α β where
   exists_map_eq_of_map_le (f : F) ⦃a : α⦄ ⦃b : β⦄ : f a ≤ b → ∃ c, a ≤ c ∧ f c = b
 #align esakia_hom_class EsakiaHomClass
 
@@ -76,7 +76,7 @@ export PseudoEpimorphismClass (exists_map_eq_of_map_le)
 -- See note [lower instance priority]
 instance (priority := 100) PseudoEpimorphismClass.toTopHomClass [PartialOrder α] [OrderTop α]
     [Preorder β] [OrderTop β] [PseudoEpimorphismClass F α β] : TopHomClass F α β where
-  map_top := fun f => by
+  map_top f := by
     let ⟨b, h⟩ := exists_map_eq_of_map_le f (@le_top _ _ _ <| f ⊤)
     rw [← top_le_iff.1 h.1, h.2]
 #align pseudo_epimorphism_class.to_top_hom_class PseudoEpimorphismClass.toTopHomClass
@@ -84,7 +84,7 @@ instance (priority := 100) PseudoEpimorphismClass.toTopHomClass [PartialOrder α
 -- See note [lower instance priority]
 instance (priority := 100) OrderIsoClass.toPseudoEpimorphismClass [Preorder α] [Preorder β]
     [OrderIsoClass F α β] : PseudoEpimorphismClass F α β where
-  exists_map_eq_of_map_le := fun f _a b h =>
+  exists_map_eq_of_map_le f _a b h :=
     ⟨EquivLike.inv f b, (le_map_inv_iff f).2 h, EquivLike.right_inv _ _⟩
 #align order_iso_class.to_pseudo_epimorphism_class OrderIsoClass.toPseudoEpimorphismClass
 
@@ -125,8 +125,7 @@ directly. -/
 --   FunLike.hasCoeToFun
 
 @[simp]
-theorem toFun_eq_coe {f : PseudoEpimorphism α β} : f.toFun = (f : α → β) :=
-  rfl
+theorem toFun_eq_coe {f : PseudoEpimorphism α β} : f.toFun = (f : α → β) := rfl
 #align pseudo_epimorphism.to_fun_eq_coe PseudoEpimorphism.toFun_eq_coe
 
 @[ext]
@@ -141,8 +140,7 @@ protected def copy (f : PseudoEpimorphism α β) (f' : α → β) (h : f' = f) :
 #align pseudo_epimorphism.copy PseudoEpimorphism.copy
 
 @[simp]
-theorem coe_copy (f : PseudoEpimorphism α β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f' :=
-  rfl
+theorem coe_copy (f : PseudoEpimorphism α β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f' := rfl
 #align pseudo_epimorphism.coe_copy PseudoEpimorphism.coe_copy
 
 theorem copy_eq (f : PseudoEpimorphism α β) (f' : α → β) (h : f' = f) : f.copy f' h = f :=
@@ -160,26 +158,22 @@ instance : Inhabited (PseudoEpimorphism α α) :=
   ⟨PseudoEpimorphism.id α⟩
 
 @[simp]
-theorem coe_id : ⇑(PseudoEpimorphism.id α) = id :=
-  rfl
+theorem coe_id : ⇑(PseudoEpimorphism.id α) = id := rfl
 #align pseudo_epimorphism.coe_id PseudoEpimorphism.coe_id
 
 @[simp]
-theorem coe_id_orderHom : (PseudoEpimorphism.id α : α →o α) = OrderHom.id :=
-  rfl
+theorem coe_id_orderHom : (PseudoEpimorphism.id α : α →o α) = OrderHom.id := rfl
 #align pseudo_epimorphism.coe_id_order_hom PseudoEpimorphism.coe_id_orderHom
 
 variable {α}
 
 @[simp]
-theorem id_apply (a : α) : PseudoEpimorphism.id α a = a :=
-  rfl
+theorem id_apply (a : α) : PseudoEpimorphism.id α a = a := rfl
 #align pseudo_epimorphism.id_apply PseudoEpimorphism.id_apply
 
 /-- Composition of `pseudo_epimorphism`s as a `pseudo_epimorphism`. -/
 def comp (g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β) : PseudoEpimorphism α γ :=
-  ⟨g.toOrderHom.comp f.toOrderHom, fun a b h₀ =>
-    by
+  ⟨g.toOrderHom.comp f.toOrderHom, fun a b h₀ => by
     obtain ⟨b, h₁, rfl⟩ := g.exists_map_eq_of_map_le' h₀
     obtain ⟨b, h₂, rfl⟩ := f.exists_map_eq_of_map_le' h₁
     exact ⟨b, h₂, rfl⟩⟩
@@ -187,26 +181,22 @@ def comp (g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β) : PseudoEpi
 
 @[simp]
 theorem coe_comp (g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β) :
-    (g.comp f : α → γ) = g ∘ f :=
-  rfl
+    (g.comp f : α → γ) = g ∘ f := rfl
 #align pseudo_epimorphism.coe_comp PseudoEpimorphism.coe_comp
 
 @[simp]
 theorem coe_comp_orderHom (g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β) :
-    (g.comp f : α →o γ) = (g : β →o γ).comp f :=
-  rfl
+    (g.comp f : α →o γ) = (g : β →o γ).comp f := rfl
 #align pseudo_epimorphism.coe_comp_order_hom PseudoEpimorphism.coe_comp_orderHom
 
 @[simp]
 theorem comp_apply (g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β) (a : α) :
-    (g.comp f) a = g (f a) :=
-  rfl
+    (g.comp f) a = g (f a) := rfl
 #align pseudo_epimorphism.comp_apply PseudoEpimorphism.comp_apply
 
 @[simp]
 theorem comp_assoc (h : PseudoEpimorphism γ δ) (g : PseudoEpimorphism β γ)
-    (f : PseudoEpimorphism α β) : (h.comp g).comp f = h.comp (g.comp f) :=
-  rfl
+    (f : PseudoEpimorphism α β) : (h.comp g).comp f = h.comp (g.comp f) := rfl
 #align pseudo_epimorphism.comp_assoc PseudoEpimorphism.comp_assoc
 
 @[simp]
@@ -221,7 +211,7 @@ theorem id_comp (f : PseudoEpimorphism α β) : (PseudoEpimorphism.id β).comp f
 
 theorem cancel_right {g₁ g₂ : PseudoEpimorphism β γ} {f : PseudoEpimorphism α β}
     (hf : Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
-  ⟨fun h => ext <| hf.forall.2 <| FunLike.ext_iff.1 h, by intro h; rw [h]⟩
+  ⟨fun h => ext <| hf.forall.2 <| FunLike.ext_iff.1 h, congr_arg (comp · f)⟩
 #align pseudo_epimorphism.cancel_right PseudoEpimorphism.cancel_right
 
 theorem cancel_left {g : PseudoEpimorphism β γ} {f₁ f₂ : PseudoEpimorphism α β} (hg : Injective g) :
@@ -244,8 +234,7 @@ def toPseudoEpimorphism (f : EsakiaHom α β) : PseudoEpimorphism α β :=
   { f with }
 #align esakia_hom.to_pseudo_epimorphism EsakiaHom.toPseudoEpimorphism
 
-instance : EsakiaHomClass (EsakiaHom α β) α β
-    where
+instance : EsakiaHomClass (EsakiaHom α β) α β where
   coe f := f.toFun
   coe_injective' f g h := by
     obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
@@ -261,8 +250,7 @@ instance : CoeFun (EsakiaHom α β) fun _ => α → β :=
   FunLike.hasCoeToFun
 
 @[simp]
-theorem toFun_eq_coe {f : EsakiaHom α β} : f.toFun = (f : α → β) :=
-  rfl
+theorem toFun_eq_coe {f : EsakiaHom α β} : f.toFun = (f : α → β) := rfl
 #align esakia_hom.to_fun_eq_coe EsakiaHom.toFun_eq_coe
 
 @[ext]
@@ -278,8 +266,7 @@ protected def copy (f : EsakiaHom α β) (f' : α → β) (h : f' = f) : EsakiaH
 #align esakia_hom.copy EsakiaHom.copy
 
 @[simp]
-theorem coe_copy (f : EsakiaHom α β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f' :=
-  rfl
+theorem coe_copy (f : EsakiaHom α β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f' := rfl
 #align esakia_hom.coe_copy EsakiaHom.coe_copy
 
 theorem copy_eq (f : EsakiaHom α β) (f' : α → β) (h : f' = f) : f.copy f' h = f :=
@@ -297,63 +284,53 @@ instance : Inhabited (EsakiaHom α α) :=
   ⟨EsakiaHom.id α⟩
 
 @[simp]
-theorem coe_id : ⇑(EsakiaHom.id α) = id :=
-  rfl
+theorem coe_id : ⇑(EsakiaHom.id α) = id := rfl
 #align esakia_hom.coe_id EsakiaHom.coe_id
 
 @[simp]
-theorem coe_id_continuousOrderHom : (EsakiaHom.id α : α →Co α) = ContinuousOrderHom.id α :=
-  rfl
+theorem coe_id_continuousOrderHom : (EsakiaHom.id α : α →Co α) = ContinuousOrderHom.id α := rfl
 #align esakia_hom.coe_id_continuous_order_hom EsakiaHom.coe_id_continuousOrderHom
 
 @[simp]
 theorem coe_id_pseudoEpimorphism :
-    (EsakiaHom.id α : PseudoEpimorphism α α) = PseudoEpimorphism.id α :=
-  rfl
+    (EsakiaHom.id α : PseudoEpimorphism α α) = PseudoEpimorphism.id α := rfl
 #align esakia_hom.coe_id_pseudo_epimorphism EsakiaHom.coe_id_pseudoEpimorphism
 
 variable {α}
 
 @[simp]
-theorem id_apply (a : α) : EsakiaHom.id α a = a :=
-  rfl
+theorem id_apply (a : α) : EsakiaHom.id α a = a := rfl
 #align esakia_hom.id_apply EsakiaHom.id_apply
 
 /-- Composition of `esakia_hom`s as an `esakia_hom`. -/
 def comp (g : EsakiaHom β γ) (f : EsakiaHom α β) : EsakiaHom α γ :=
-  ⟨g.toContinuousOrderHom.comp f.toContinuousOrderHom, fun a b h₀ =>
-    by
+  ⟨g.toContinuousOrderHom.comp f.toContinuousOrderHom, fun a b h₀ => by
     obtain ⟨b, h₁, rfl⟩ := g.exists_map_eq_of_map_le' h₀
     obtain ⟨b, h₂, rfl⟩ := f.exists_map_eq_of_map_le' h₁
     exact ⟨b, h₂, rfl⟩⟩
 #align esakia_hom.comp EsakiaHom.comp
 
 @[simp]
-theorem coe_comp (g : EsakiaHom β γ) (f : EsakiaHom α β) : (g.comp f : α → γ) = g ∘ f :=
-  rfl
+theorem coe_comp (g : EsakiaHom β γ) (f : EsakiaHom α β) : (g.comp f : α → γ) = g ∘ f := rfl
 #align esakia_hom.coe_comp EsakiaHom.coe_comp
 
 @[simp]
-theorem comp_apply (g : EsakiaHom β γ) (f : EsakiaHom α β) (a : α) : (g.comp f) a = g (f a) :=
-  rfl
+theorem comp_apply (g : EsakiaHom β γ) (f : EsakiaHom α β) (a : α) : (g.comp f) a = g (f a) := rfl
 #align esakia_hom.comp_apply EsakiaHom.comp_apply
 
 @[simp]
 theorem coe_comp_continuousOrderHom (g : EsakiaHom β γ) (f : EsakiaHom α β) :
-    (g.comp f : α →Co γ) = (g : β →Co γ).comp f :=
-  rfl
+    (g.comp f : α →Co γ) = (g : β →Co γ).comp f := rfl
 #align esakia_hom.coe_comp_continuous_order_hom EsakiaHom.coe_comp_continuousOrderHom
 
 @[simp]
 theorem coe_comp_pseudoEpimorphism (g : EsakiaHom β γ) (f : EsakiaHom α β) :
-    (g.comp f : PseudoEpimorphism α γ) = (g : PseudoEpimorphism β γ).comp f :=
-  rfl
+    (g.comp f : PseudoEpimorphism α γ) = (g : PseudoEpimorphism β γ).comp f := rfl
 #align esakia_hom.coe_comp_pseudo_epimorphism EsakiaHom.coe_comp_pseudoEpimorphism
 
 @[simp]
 theorem comp_assoc (h : EsakiaHom γ δ) (g : EsakiaHom β γ) (f : EsakiaHom α β) :
-    (h.comp g).comp f = h.comp (g.comp f) :=
-  rfl
+    (h.comp g).comp f = h.comp (g.comp f) := rfl
 #align esakia_hom.comp_assoc EsakiaHom.comp_assoc
 
 @[simp]
@@ -368,7 +345,7 @@ theorem id_comp (f : EsakiaHom α β) : (EsakiaHom.id β).comp f = f :=
 
 theorem cancel_right {g₁ g₂ : EsakiaHom β γ} {f : EsakiaHom α β} (hf : Surjective f) :
     g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
-  ⟨fun h => ext <| hf.forall.2 <| FunLike.ext_iff.1 h, by intro h; rw [h]⟩
+  ⟨fun h => ext <| hf.forall.2 <| FunLike.ext_iff.1 h, congr_arg (comp · f)⟩
 #align esakia_hom.cancel_right EsakiaHom.cancel_right
 
 theorem cancel_left {g : EsakiaHom β γ} {f₁ f₂ : EsakiaHom α β} (hg : Injective g) :

From a93e398f45f248f723015a0f67fd24804c18dbd2 Mon Sep 17 00:00:00 2001
From: int-y1 <jason_yuen2007@hotmail.com>
Date: Sat, 6 May 2023 01:11:10 -0700
Subject: [PATCH 07/11] docs

---
 Mathlib/Topology/Order/Hom/Esakia.lean | 36 +++++++++++++-------------
 1 file changed, 18 insertions(+), 18 deletions(-)

diff --git a/Mathlib/Topology/Order/Hom/Esakia.lean b/Mathlib/Topology/Order/Hom/Esakia.lean
index fe735b27ca9c8..4063cb115bcd7 100644
--- a/Mathlib/Topology/Order/Hom/Esakia.lean
+++ b/Mathlib/Topology/Order/Hom/Esakia.lean
@@ -16,19 +16,19 @@ import Mathlib.Topology.Order.Hom.Basic
 
 This file defines pseudo-epimorphisms and Esakia morphisms.
 
-We use the `fun_like` design, so each type of morphisms has a companion typeclass which is meant to
+We use the `FunLike` design, so each type of morphisms has a companion typeclass which is meant to
 be satisfied by itself and all stricter types.
 
 ## Types of morphisms
 
-* `pseudo_epimorphism`: Pseudo-epimorphisms. Maps `f` such that `f a ≤ b` implies the existence of
+* `PseudoEpimorphism`: Pseudo-epimorphisms. Maps `f` such that `f a ≤ b` implies the existence of
   `a'` such that `a ≤ a'` and `f a' = b`.
-* `esakia_hom`: Esakia morphisms. Continuous pseudo-epimorphisms.
+* `EsakiaHom`: Esakia morphisms. Continuous pseudo-epimorphisms.
 
 ## Typeclasses
 
-* `pseudo_epimorphism_class`
-* `esakia_hom_class`
+* `PseudoEpimorphismClass`
+* `EsakiaHomClass`
 
 ## References
 
@@ -53,17 +53,17 @@ structure EsakiaHom (α β : Type _) [TopologicalSpace α] [Preorder α] [Topolo
 
 section
 
-/-- `pseudo_epimorphism_class F α β` states that `F` is a type of `⊔`-preserving morphisms.
+/-- `PseudoEpimorphismClass F α β` states that `F` is a type of `⊔`-preserving morphisms.
 
-You should extend this class when you extend `pseudo_epimorphism`. -/
+You should extend this class when you extend `PseudoEpimorphism`. -/
 class PseudoEpimorphismClass (F : Type _) (α β : outParam <| Type _) [Preorder α] [Preorder β]
     extends RelHomClass F ((· ≤ ·) : α → α → Prop) ((· ≤ ·) : β → β → Prop) where
   exists_map_eq_of_map_le (f : F) ⦃a : α⦄ ⦃b : β⦄ : f a ≤ b → ∃ c, a ≤ c ∧ f c = b
 #align pseudo_epimorphism_class PseudoEpimorphismClass
 
-/-- `esakia_hom_class F α β` states that `F` is a type of lattice morphisms.
+/-- `EsakiaHomClass F α β` states that `F` is a type of lattice morphisms.
 
-You should extend this class when you extend `esakia_hom`. -/
+You should extend this class when you extend `EsakiaHom`. -/
 class EsakiaHomClass (F : Type _) (α β : outParam <| Type _) [TopologicalSpace α] [Preorder α]
     [TopologicalSpace β] [Preorder β] extends ContinuousOrderHomClass F α β where
   exists_map_eq_of_map_le (f : F) ⦃a : α⦄ ⦃b : β⦄ : f a ≤ b → ∃ c, a ≤ c ∧ f c = b
@@ -119,7 +119,7 @@ instance : PseudoEpimorphismClass (PseudoEpimorphism α β) α β where
   map_rel f _ _ h := f.monotone' h
   exists_map_eq_of_map_le := PseudoEpimorphism.exists_map_eq_of_map_le'
 
-/-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
+/-- Helper instance for when there's too many metavariables to apply `FunLike.hasCoeToFun`
 directly. -/
 -- instance : CoeFun (PseudoEpimorphism α β) fun _ => α → β :=
 --   FunLike.hasCoeToFun
@@ -133,7 +133,7 @@ theorem ext {f g : PseudoEpimorphism α β} (h : ∀ a, f a = g a) : f = g :=
   FunLike.ext f g h
 #align pseudo_epimorphism.ext PseudoEpimorphism.ext
 
-/-- Copy of a `pseudo_epimorphism` with a new `to_fun` equal to the old one. Useful to fix
+/-- Copy of a `PseudoEpimorphism` with a new `toFun` equal to the old one. Useful to fix
 definitional equalities. -/
 protected def copy (f : PseudoEpimorphism α β) (f' : α → β) (h : f' = f) : PseudoEpimorphism α β :=
   ⟨f.toOrderHom.copy f' h, by simpa only [h.symm, toFun_eq_coe] using f.exists_map_eq_of_map_le'⟩
@@ -149,7 +149,7 @@ theorem copy_eq (f : PseudoEpimorphism α β) (f' : α → β) (h : f' = f) : f.
 
 variable (α)
 
-/-- `id` as a `pseudo_epimorphism`. -/
+/-- `id` as a `PseudoEpimorphism`. -/
 protected def id : PseudoEpimorphism α α :=
   ⟨OrderHom.id, fun _ b h => ⟨b, h, rfl⟩⟩
 #align pseudo_epimorphism.id PseudoEpimorphism.id
@@ -171,7 +171,7 @@ variable {α}
 theorem id_apply (a : α) : PseudoEpimorphism.id α a = a := rfl
 #align pseudo_epimorphism.id_apply PseudoEpimorphism.id_apply
 
-/-- Composition of `pseudo_epimorphism`s as a `pseudo_epimorphism`. -/
+/-- Composition of `PseudoEpimorphism`s as a `PseudoEpimorphism`. -/
 def comp (g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β) : PseudoEpimorphism α γ :=
   ⟨g.toOrderHom.comp f.toOrderHom, fun a b h₀ => by
     obtain ⟨b, h₁, rfl⟩ := g.exists_map_eq_of_map_le' h₀
@@ -229,7 +229,7 @@ namespace EsakiaHom
 variable [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [TopologicalSpace γ]
   [Preorder γ] [TopologicalSpace δ] [Preorder δ]
 
-/-- Reinterpret an `esakia_hom` as a `pseudo_epimorphism`. -/
+/-- Reinterpret an `EsakiaHom` as a `PseudoEpimorphism`. -/
 def toPseudoEpimorphism (f : EsakiaHom α β) : PseudoEpimorphism α β :=
   { f with }
 #align esakia_hom.to_pseudo_epimorphism EsakiaHom.toPseudoEpimorphism
@@ -244,7 +244,7 @@ instance : EsakiaHomClass (EsakiaHom α β) α β where
   map_continuous f := f.continuous_toFun
   exists_map_eq_of_map_le f := f.exists_map_eq_of_map_le'
 
-/-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
+/-- Helper instance for when there's too many metavariables to apply `FunLike.hasCoeToFun`
 directly. -/
 instance : CoeFun (EsakiaHom α β) fun _ => α → β :=
   FunLike.hasCoeToFun
@@ -258,7 +258,7 @@ theorem ext {f g : EsakiaHom α β} (h : ∀ a, f a = g a) : f = g :=
   FunLike.ext f g h
 #align esakia_hom.ext EsakiaHom.ext
 
-/-- Copy of an `esakia_hom` with a new `to_fun` equal to the old one. Useful to fix definitional
+/-- Copy of an `EsakiaHom` with a new `toFun` equal to the old one. Useful to fix definitional
 equalities. -/
 protected def copy (f : EsakiaHom α β) (f' : α → β) (h : f' = f) : EsakiaHom α β :=
   ⟨f.toContinuousOrderHom.copy f' h, by
@@ -275,7 +275,7 @@ theorem copy_eq (f : EsakiaHom α β) (f' : α → β) (h : f' = f) : f.copy f'
 
 variable (α)
 
-/-- `id` as an `esakia_hom`. -/
+/-- `id` as an `EsakiaHom`. -/
 protected def id : EsakiaHom α α :=
   ⟨ContinuousOrderHom.id α, fun _ b h => ⟨b, h, rfl⟩⟩
 #align esakia_hom.id EsakiaHom.id
@@ -302,7 +302,7 @@ variable {α}
 theorem id_apply (a : α) : EsakiaHom.id α a = a := rfl
 #align esakia_hom.id_apply EsakiaHom.id_apply
 
-/-- Composition of `esakia_hom`s as an `esakia_hom`. -/
+/-- Composition of `EsakiaHom`s as an `EsakiaHom`. -/
 def comp (g : EsakiaHom β γ) (f : EsakiaHom α β) : EsakiaHom α γ :=
   ⟨g.toContinuousOrderHom.comp f.toContinuousOrderHom, fun a b h₀ => by
     obtain ⟨b, h₁, rfl⟩ := g.exists_map_eq_of_map_le' h₀

From 7af4414775eae8f365976e188d2a088ecd827faa Mon Sep 17 00:00:00 2001
From: int-y1 <jason_yuen2007@hotmail.com>
Date: Sat, 6 May 2023 01:13:48 -0700
Subject: [PATCH 08/11] uncomment instance

---
 Mathlib/Topology/Order/Hom/Esakia.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Topology/Order/Hom/Esakia.lean b/Mathlib/Topology/Order/Hom/Esakia.lean
index 4063cb115bcd7..458b13ebf3dcc 100644
--- a/Mathlib/Topology/Order/Hom/Esakia.lean
+++ b/Mathlib/Topology/Order/Hom/Esakia.lean
@@ -121,8 +121,8 @@ instance : PseudoEpimorphismClass (PseudoEpimorphism α β) α β where
 
 /-- Helper instance for when there's too many metavariables to apply `FunLike.hasCoeToFun`
 directly. -/
--- instance : CoeFun (PseudoEpimorphism α β) fun _ => α → β :=
---   FunLike.hasCoeToFun
+instance : CoeFun (PseudoEpimorphism α β) fun _ => α → β :=
+  FunLike.hasCoeToFun
 
 @[simp]
 theorem toFun_eq_coe {f : PseudoEpimorphism α β} : f.toFun = (f : α → β) := rfl

From 3eaa079d65845fe775e7f4cd220aeadf94777f95 Mon Sep 17 00:00:00 2001
From: Matthew Ballard <matt@mrb.email>
Date: Mon, 5 Jun 2023 18:03:00 -0400
Subject: [PATCH 09/11] reorder theorems to appease simpNF linter

---
 Mathlib/Topology/Order/Hom/Esakia.lean | 30 +++++++++++++++-----------
 1 file changed, 18 insertions(+), 12 deletions(-)

diff --git a/Mathlib/Topology/Order/Hom/Esakia.lean b/Mathlib/Topology/Order/Hom/Esakia.lean
index 458b13ebf3dcc..eefd2bfaca25d 100644
--- a/Mathlib/Topology/Order/Hom/Esakia.lean
+++ b/Mathlib/Topology/Order/Hom/Esakia.lean
@@ -249,7 +249,12 @@ directly. -/
 instance : CoeFun (EsakiaHom α β) fun _ => α → β :=
   FunLike.hasCoeToFun
 
+-- Porting note: introduced this to appease simpNF linter with `toFun_eq_coe`
 @[simp]
+theorem toContinuousOrderHom_coe {f : EsakiaHom α β} :
+    f.toContinuousOrderHom = (f : α → β) := rfl
+
+-- Porting note: removed simp attribute as simp now solves this
 theorem toFun_eq_coe {f : EsakiaHom α β} : f.toFun = (f : α → β) := rfl
 #align esakia_hom.to_fun_eq_coe EsakiaHom.toFun_eq_coe
 
@@ -283,14 +288,14 @@ protected def id : EsakiaHom α α :=
 instance : Inhabited (EsakiaHom α α) :=
   ⟨EsakiaHom.id α⟩
 
-@[simp]
-theorem coe_id : ⇑(EsakiaHom.id α) = id := rfl
-#align esakia_hom.coe_id EsakiaHom.coe_id
-
 @[simp]
 theorem coe_id_continuousOrderHom : (EsakiaHom.id α : α →Co α) = ContinuousOrderHom.id α := rfl
 #align esakia_hom.coe_id_continuous_order_hom EsakiaHom.coe_id_continuousOrderHom
 
+@[simp]
+theorem coe_id : ⇑(EsakiaHom.id α) = id := rfl
+#align esakia_hom.coe_id EsakiaHom.coe_id
+
 @[simp]
 theorem coe_id_pseudoEpimorphism :
     (EsakiaHom.id α : PseudoEpimorphism α α) = PseudoEpimorphism.id α := rfl
@@ -310,14 +315,6 @@ def comp (g : EsakiaHom β γ) (f : EsakiaHom α β) : EsakiaHom α γ :=
     exact ⟨b, h₂, rfl⟩⟩
 #align esakia_hom.comp EsakiaHom.comp
 
-@[simp]
-theorem coe_comp (g : EsakiaHom β γ) (f : EsakiaHom α β) : (g.comp f : α → γ) = g ∘ f := rfl
-#align esakia_hom.coe_comp EsakiaHom.coe_comp
-
-@[simp]
-theorem comp_apply (g : EsakiaHom β γ) (f : EsakiaHom α β) (a : α) : (g.comp f) a = g (f a) := rfl
-#align esakia_hom.comp_apply EsakiaHom.comp_apply
-
 @[simp]
 theorem coe_comp_continuousOrderHom (g : EsakiaHom β γ) (f : EsakiaHom α β) :
     (g.comp f : α →Co γ) = (g : β →Co γ).comp f := rfl
@@ -328,6 +325,14 @@ theorem coe_comp_pseudoEpimorphism (g : EsakiaHom β γ) (f : EsakiaHom α β) :
     (g.comp f : PseudoEpimorphism α γ) = (g : PseudoEpimorphism β γ).comp f := rfl
 #align esakia_hom.coe_comp_pseudo_epimorphism EsakiaHom.coe_comp_pseudoEpimorphism
 
+@[simp]
+theorem coe_comp (g : EsakiaHom β γ) (f : EsakiaHom α β) : (g.comp f : α → γ) = g ∘ f := rfl
+#align esakia_hom.coe_comp EsakiaHom.coe_comp
+
+@[simp]
+theorem comp_apply (g : EsakiaHom β γ) (f : EsakiaHom α β) (a : α) : (g.comp f) a = g (f a) := rfl
+#align esakia_hom.comp_apply EsakiaHom.comp_apply
+
 @[simp]
 theorem comp_assoc (h : EsakiaHom γ δ) (g : EsakiaHom β γ) (f : EsakiaHom α β) :
     (h.comp g).comp f = h.comp (g.comp f) := rfl
@@ -354,3 +359,4 @@ theorem cancel_left {g : EsakiaHom β γ} {f₁ f₂ : EsakiaHom α β} (hg : In
 #align esakia_hom.cancel_left EsakiaHom.cancel_left
 
 end EsakiaHom
+

From 7ef7c3f12e9ad0de66b8d5332c02f6a09258496e Mon Sep 17 00:00:00 2001
From: Matthew Ballard <matt@mrb.email>
Date: Tue, 6 Jun 2023 17:49:24 -0400
Subject: [PATCH 10/11] rework coercion

the coercion from EsakiaHom to ContinuousOrderHom was an odd duck
compared to the similar ones in this file. The ContinuousOrderHom
constructor was directly exposed in the coercise resulting in simp
rewriting the fields and simpNF complaining. Introduced
EsakiaHomClass.toContinuousOrderHom which wrapped this constructor
and things behave uniformly.
---
 Mathlib/Topology/Order/Hom/Basic.lean  | 24 +++++++++++++++++-------
 Mathlib/Topology/Order/Hom/Esakia.lean | 11 +++++------
 2 files changed, 22 insertions(+), 13 deletions(-)

diff --git a/Mathlib/Topology/Order/Hom/Basic.lean b/Mathlib/Topology/Order/Hom/Basic.lean
index ab6d993c302b7..1f7ab5b2af779 100644
--- a/Mathlib/Topology/Order/Hom/Basic.lean
+++ b/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
+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 =>
+@[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⟩
+-- instance : CoeTC F (α →Co β) :=
+--   ⟨fun f =>
+--     { toFun := f
+--       monotone' := ContinuousOrderHomClass.map_monotone f
+--       continuous_toFun := map_continuous f }⟩
 
+end ContinuousOrderHomClass
 /-! ### Top homomorphisms -/
 
 
diff --git a/Mathlib/Topology/Order/Hom/Esakia.lean b/Mathlib/Topology/Order/Hom/Esakia.lean
index eefd2bfaca25d..8405bac6b35e3 100644
--- a/Mathlib/Topology/Order/Hom/Esakia.lean
+++ b/Mathlib/Topology/Order/Hom/Esakia.lean
@@ -229,7 +229,6 @@ namespace EsakiaHom
 variable [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [TopologicalSpace γ]
   [Preorder γ] [TopologicalSpace δ] [Preorder δ]
 
-/-- Reinterpret an `EsakiaHom` as a `PseudoEpimorphism`. -/
 def toPseudoEpimorphism (f : EsakiaHom α β) : PseudoEpimorphism α β :=
   { f with }
 #align esakia_hom.to_pseudo_epimorphism EsakiaHom.toPseudoEpimorphism
@@ -288,10 +287,6 @@ protected def id : EsakiaHom α α :=
 instance : Inhabited (EsakiaHom α α) :=
   ⟨EsakiaHom.id α⟩
 
-@[simp]
-theorem coe_id_continuousOrderHom : (EsakiaHom.id α : α →Co α) = ContinuousOrderHom.id α := rfl
-#align esakia_hom.coe_id_continuous_order_hom EsakiaHom.coe_id_continuousOrderHom
-
 @[simp]
 theorem coe_id : ⇑(EsakiaHom.id α) = id := rfl
 #align esakia_hom.coe_id EsakiaHom.coe_id
@@ -307,6 +302,10 @@ variable {α}
 theorem id_apply (a : α) : EsakiaHom.id α a = a := rfl
 #align esakia_hom.id_apply EsakiaHom.id_apply
 
+@[simp]
+theorem coe_id_continuousOrderHom : (EsakiaHom.id α : α →Co α) = ContinuousOrderHom.id α := rfl
+#align esakia_hom.coe_id_continuous_order_hom EsakiaHom.coe_id_continuousOrderHom
+
 /-- Composition of `EsakiaHom`s as an `EsakiaHom`. -/
 def comp (g : EsakiaHom β γ) (f : EsakiaHom α β) : EsakiaHom α γ :=
   ⟨g.toContinuousOrderHom.comp f.toContinuousOrderHom, fun a b h₀ => by
@@ -317,7 +316,7 @@ def comp (g : EsakiaHom β γ) (f : EsakiaHom α β) : EsakiaHom α γ :=
 
 @[simp]
 theorem coe_comp_continuousOrderHom (g : EsakiaHom β γ) (f : EsakiaHom α β) :
-    (g.comp f : α →Co γ) = (g : β →Co γ).comp f := rfl
+    (g.comp f : α →Co γ) = (g: β →Co γ).comp f := rfl
 #align esakia_hom.coe_comp_continuous_order_hom EsakiaHom.coe_comp_continuousOrderHom
 
 @[simp]

From dc1fee5475c75748db1714f7cf40bb6118121795 Mon Sep 17 00:00:00 2001
From: Matthew Ballard <matt@mrb.email>
Date: Tue, 6 Jun 2023 18:00:08 -0400
Subject: [PATCH 11/11] add some porting notes

---
 Mathlib/Topology/Order/Hom/Basic.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Topology/Order/Hom/Basic.lean b/Mathlib/Topology/Order/Hom/Basic.lean
index 1f7ab5b2af779..b159ddaf274b6 100644
--- a/Mathlib/Topology/Order/Hom/Basic.lean
+++ b/Mathlib/Topology/Order/Hom/Basic.lean
@@ -56,6 +56,7 @@ class ContinuousOrderHomClass (F : Type _) (α β : outParam <| Type _) [Preorde
   map_monotone (f : F) : Monotone f
 #align continuous_order_hom_class ContinuousOrderHomClass
 
+-- Porting note: namespaced these results since there are more than 3 now
 namespace ContinuousOrderHomClass
 
 variable [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β]
@@ -68,6 +69,10 @@ instance (priority := 100) toOrderHomClass  :
     map_rel := ContinuousOrderHomClass.map_monotone }
 #align continuous_order_hom_class.to_continuous_map_class ContinuousOrderHomClass.toContinuousMapClass
 
+-- 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
@@ -76,11 +81,6 @@ def toContinuousOrderHom (f : F) : α →Co β :=
 
 instance : CoeTC F (α →Co β) :=
   ⟨toContinuousOrderHom⟩
--- instance : CoeTC F (α →Co β) :=
---   ⟨fun f =>
---     { toFun := f
---       monotone' := ContinuousOrderHomClass.map_monotone f
---       continuous_toFun := map_continuous f }⟩
 
 end ContinuousOrderHomClass
 /-! ### Top homomorphisms -/