From 7b6c25589a35fb5fb59d9d84f5bb6106743e8372 Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Fri, 21 Aug 2026 21:41:25 -0400 Subject: [PATCH] fix --- src/Init/Data/Dyadic/Basic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Init/Data/Dyadic/Basic.lean b/src/Init/Data/Dyadic/Basic.lean index 68deda6e3c37..33402e74136b 100644 --- a/src/Init/Data/Dyadic/Basic.lean +++ b/src/Init/Data/Dyadic/Basic.lean @@ -697,12 +697,12 @@ theorem toRat_lt_toRat_iff {x y : Dyadic} : x.toRat < y.toRat ↔ x < y := blt_i theorem toRat_le_toRat_iff {x y : Dyadic} : x.toRat ≤ y.toRat ↔ x ≤ y := ble_iff_toRat.symm @[simp] -protected theorem not_le {x y : Dyadic} : ¬x < y ↔ y ≤ x := by +protected theorem not_lt {x y : Dyadic} : ¬x < y ↔ y ≤ x := by simp only [· ≤ ·, · < ·, Bool.not_eq_true, blt_eq_false_iff] @[simp] -protected theorem not_lt {x y : Dyadic} : ¬x ≤ y ↔ y < x := by - rw [← Dyadic.not_le, Decidable.not_not] +protected theorem not_le {x y : Dyadic} : ¬x ≤ y ↔ y < x := by + rw [← Dyadic.not_lt, Decidable.not_not] @[simp] protected theorem le_refl (x : Dyadic) : x ≤ x := by @@ -723,7 +723,7 @@ protected theorem le_total (x y : Dyadic) : x ≤ y ∨ y ≤ x := by exact Rat.le_total instance : Std.LawfulOrderLT Dyadic where - lt_iff a b := by rw [← Dyadic.not_lt, iff_and_self]; exact (Dyadic.le_total _ _).resolve_left + lt_iff a b := by rw [← Dyadic.not_le, iff_and_self]; exact (Dyadic.le_total _ _).resolve_left instance : Std.IsPreorder Dyadic where le_refl := Dyadic.le_refl