From 77d79f705fda0b3b9fb4d08e7f6d86f96508bfe6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Thu, 3 Jul 2025 08:04:25 -0400 Subject: [PATCH] fix: typos in Std.Classes.Ord.Basic (#9145) This PR fixes two typos. --- src/Std/Classes/Ord/Basic.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Std/Classes/Ord/Basic.lean b/src/Std/Classes/Ord/Basic.lean index 750b86e580..11e1197af8 100644 --- a/src/Std/Classes/Ord/Basic.lean +++ b/src/Std/Classes/Ord/Basic.lean @@ -440,12 +440,12 @@ theorem LawfulBEqCmp.lawfulBEq [inst : LawfulBEqCmp cmp] [LawfulEqCmp cmp] : Law instance LawfulBEqOrd.lawfulBEq [Ord α] [LawfulBEqOrd α] [LawfulEqOrd α] : LawfulBEq α := LawfulBEqCmp.lawfulBEq (cmp := compare) -instance LawfulBEqCmp.lawfulBEqCmp [inst : LawfulBEqCmp cmp] [LawfulBEq α] : LawfulEqCmp cmp where +instance LawfulBEqCmp.lawfulEqCmp [inst : LawfulBEqCmp cmp] [LawfulBEq α] : LawfulEqCmp cmp where compare_self := by simp only [compare_eq_iff_beq, beq_self_eq_true, implies_true] eq_of_compare := by simp only [compare_eq_iff_beq, beq_iff_eq, imp_self, implies_true] -theorem LawfulBEqOrd.lawfulBEqOrd [Ord α] [LawfulBEqOrd α] [LawfulBEq α] : LawfulEqOrd α := - LawfulBEqCmp.lawfulBEqCmp +theorem LawfulBEqOrd.lawfulEqOrd [Ord α] [LawfulBEqOrd α] [LawfulBEq α] : LawfulEqOrd α := + LawfulBEqCmp.lawfulEqCmp instance LawfulBEqCmp.opposite [OrientedCmp cmp] [LawfulBEqCmp cmp] : LawfulBEqCmp (fun a b => cmp b a) where