From a1e40a1699a4b2818661d301932ce4b877084377 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Sun, 26 Apr 2026 21:28:06 +0300
Subject: [PATCH 1/2] chore(Order/Hom/Basic): delete redundant `EquivLike
 OrderIso` instance

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

diff --git a/Mathlib/Order/Hom/Basic.lean b/Mathlib/Order/Hom/Basic.lean
index 2a23afefce669c..96d3322cc6578a 100644
--- a/Mathlib/Order/Hom/Basic.lean
+++ b/Mathlib/Order/Hom/Basic.lean
@@ -718,16 +718,6 @@ section LE
 
 variable [LE α] [LE β] [LE γ]
 
-instance : EquivLike (α ≃o β) α β where
-  coe f := f.toFun
-  inv f := f.invFun
-  left_inv f := f.left_inv
-  right_inv f := f.right_inv
-  coe_injective' f g h₁ h₂ := by
-    obtain ⟨⟨_, _⟩, _⟩ := f
-    obtain ⟨⟨_, _⟩, _⟩ := g
-    congr
-
 instance : OrderIsoClass (α ≃o β) α β where
   map_le_map_iff f _ _ := f.map_rel_iff'
 

From cf432da75f69e10d9b02c6d117a3285d0d21ab4d Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Mon, 27 Apr 2026 01:56:54 +0300
Subject: [PATCH 2/2] cheeky fix

---
 Mathlib/Order/Hom/Basic.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Mathlib/Order/Hom/Basic.lean b/Mathlib/Order/Hom/Basic.lean
index 96d3322cc6578a..9eaac08c167dc4 100644
--- a/Mathlib/Order/Hom/Basic.lean
+++ b/Mathlib/Order/Hom/Basic.lean
@@ -718,6 +718,9 @@ section LE
 
 variable [LE α] [LE β] [LE γ]
 
+instance : EquivLike (α ≃o β) α β :=
+  inferInstance
+
 instance : OrderIsoClass (α ≃o β) α β where
   map_le_map_iff f _ _ := f.map_rel_iff'