From e11ef3ee4eb7b08ac76cbe8339486b5a7b47bb0a Mon Sep 17 00:00:00 2001
From: Wrenna Robson <wren.robson@gmail.com>
Date: Thu, 30 Oct 2025 13:21:26 +0000
Subject: [PATCH] fix: Remove redundant instance requirement (#10941)

This PR removes a redundant instance requirement from
`Std.instIrreflLtOfIsPreorderOfLawfulOrderLT`.
---
 src/Init/Data/Order/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·) ]