diff --git a/src/Init/Data/Order/Lemmas.lean b/src/Init/Data/Order/Lemmas.lean
index 0f228f3ea6..d28c26b224 100644
--- a/src/Init/Data/Order/Lemmas.lean
+++ b/src/Init/Data/Order/Lemmas.lean
@@ -110,7 +110,7 @@ public instance {α : Type u} [LT α] [LE α] [LawfulOrderLT α] :
     intro h h'
     exact h.2.elim h'.1
 
-public instance {α : Type u} [LT α] [LE α] [IsPreorder α] [LawfulOrderLT α] :
+public instance {α : Type u} [LT α] [LE α] [LawfulOrderLT α] :
     Std.Irrefl (α := α) (· < ·) := inferInstance
 
 public instance {α : Type u} [LT α] [LE α] [Trans (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·) ]