diff --git a/Mathlib/Order/Hom/Basic.lean b/Mathlib/Order/Hom/Basic.lean
index 2a23afefce669c..9eaac08c167dc4 100644
--- a/Mathlib/Order/Hom/Basic.lean
+++ b/Mathlib/Order/Hom/Basic.lean
@@ -718,15 +718,8 @@ 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 : EquivLike (α ≃o β) α β :=
+  inferInstance
 
 instance : OrderIsoClass (α ≃o β) α β where
   map_le_map_iff f _ _ := f.map_rel_iff'