wip: realizing that this approach is suboptimal for Cmp

src/Std/Classes/Ord.lean

@@ -12,5 +12,6 @@ public import Std.Classes.Ord.UInt
 public import Std.Classes.Ord.String
 public import Std.Classes.Ord.BitVec
 public import Std.Classes.Ord.Vector
+public import Std.Classes.Ord.New.Util
 
 public section

src/Std/Classes/Ord/New/BasicOperations.lean

@@ -0,0 +1,149 @@
+module
+
+prelude
+import Init.Core
+public import Init.Data.Ord
+public import Std.Classes.Ord.New.Util
+
+public section
+
+section LT
+
+class BLT (α : Type u) where
+  LT : α → α → Bool
+
+class LawfulBLT (α : Type u) [LT α] [BLT α] where
+  lt_iff_lt : ∀ a b : α, LT.lt a b ↔ BLT.LT a b
+
+instance [LT α] [BLT α] [LawfulBLT α] : DecidableLT α :=
+  fun a b => if h : BLT.LT a b then .isTrue (LawfulBLT.lt_iff_lt .. |>.mpr h) else .isFalse (h.imp (LawfulBLT.lt_iff_lt ..).mp)
+
+def LT.ofBLT (α : Type u) [BLT α] : LT α where
+  lt a b := BLT.LT a b
+
+instance [BLT α] :
+    haveI : LT α := LT.ofBLT α
+    LawfulBLT α :=
+  letI : LT α := LT.ofBLT α
+  ⟨by simp [LT.ofBLT]⟩
+
+end LT
+
+section LE
+
+class BLE (α : Type u) where
+  LE : α → α → Bool
+
+class LawfulBLE (α : Type u) [LE α] [BLE α] where
+  le_iff_le : ∀ a b : α, LE.le a b ↔ BLE.LE a b
+
+instance [LE α] [BLE α] [LawfulBLE α] : DecidableLE α :=
+  fun a b => if h : BLE.LE a b then .isTrue (LawfulBLE.le_iff_le .. |>.mpr h) else .isFalse (h.imp (LawfulBLE.le_iff_le ..).mp)
+
+def LE.ofBLE (α : Type u) [BLE α] : LE α where
+  le a b := BLE.LE a b
+
+instance [BLE α] :
+    haveI : LE α := LE.ofBLE α
+    LawfulBLE α :=
+  letI : LE α := LE.ofBLE α
+  ⟨by simp [LE.ofBLE]⟩
+
+end LE
+
+section Ord
+
+class NoncomputableOrd (α : Type u) where
+  noncomputableOrd : Noncomputable (Ord α)
+
+def NoncomputableOrd.ofComputable {α : Type u} [Ord α] : NoncomputableOrd α where
+  noncomputableOrd := .comp inferInstance
+
+class LawfulOrd (α : Type u) [ni : NoncomputableOrd α] [ci : Ord α] where
+  eq : ni.noncomputableOrd.inst = ci
+
+noncomputable def NoncomputableOrd.compare {α : Type u} [NoncomputableOrd α] (a b : α) : Ordering :=
+  noncomputableOrd.inst.compare a b
+
+theorem LawfulOrd.compare_eq_compare {α : Type u} [NoncomputableOrd α] [Ord α] [LawfulOrd α]
+    {a b : α} : NoncomputableOrd.compare a b = Ord.compare a b := by
+  simp [NoncomputableOrd.compare, LawfulOrd.eq]
+
+instance {α : Type u} [NoncomputableOrd α] :
+    haveI : Ord α := NoncomputableOrd.noncomputableOrd.inst
+    LawfulOrd α :=
+  letI : Ord α := NoncomputableOrd.noncomputableOrd.inst
+  ⟨rfl⟩
+
+example {α : Type u} [Ord α] :
+    haveI : NoncomputableOrd α := NoncomputableOrd.ofComputable
+    LawfulOrd α :=
+  inferInstance
+
+-- Making an `Ord` instance noncomputable and then computable again is definitionally equal to the
+-- identity.
+example {α : Type u} [Ord α] :
+    NoncomputableOrd.ofComputable.noncomputableOrd.inst = (inferInstance : Ord α) :=
+  rfl
+
+instance [Ord α] :
+    haveI : NoncomputableOrd α := NoncomputableOrd.ofComputable
+    LawfulOrd α :=
+  letI : NoncomputableOrd α := NoncomputableOrd.ofComputable
+  ⟨by simp [NoncomputableOrd.ofComputable, Noncomputable.inst]⟩
+
+end Ord
+
+section BEq
+
+/-!
+One might consider using `HasEquiv.{u, 0}` instead of `NoncomputableBEq`.
+-/
+
+class NoncomputableBEq (α : Type u) where
+  IsEq : α → α → Prop
+
+@[expose]
+def NoncomputableBEq.ofRel (P : α → α → Prop) : NoncomputableBEq α where
+  IsEq := P
+
+def NoncomputableBEq.ofComputable {α : Type u} [BEq α] : NoncomputableBEq α where
+  IsEq a b := a == b
+
+-- sadly, the canonical name is already taken
+class LawfulComputableBEq (α : Type u) [NoncomputableBEq α] [BEq α] where
+  isEq_iff_beq : ∀ a b : α, NoncomputableBEq.IsEq a b ↔ a == b
+
+noncomputable def BEq.ofNoncomputable {α : Type u} [NoncomputableBEq α] : BEq α where
+  beq a b := open scoped Classical in decide (NoncomputableBEq.IsEq a b)
+
+instance {α : Type u} [NoncomputableBEq α] :
+    haveI : BEq α := .ofNoncomputable
+    LawfulComputableBEq α :=
+  letI : BEq α := .ofNoncomputable
+  ⟨fun _ _ => by simp [BEq.ofNoncomputable]⟩
+
+instance [BEq α] :
+    haveI : NoncomputableBEq α := NoncomputableBEq.ofComputable
+    LawfulComputableBEq α :=
+  letI : NoncomputableBEq α := NoncomputableBEq.ofComputable
+  ⟨by simp [NoncomputableBEq.ofComputable]⟩
+
+end BEq
+
+namespace Classical.Order
+
+noncomputable section
+
+scoped instance (priority := low) ordOfNoncomputableOrd [NoncomputableOrd α] : Ord α :=
+  NoncomputableOrd.noncomputableOrd.inst
+
+structure WithClassical (α : Type u) where
+  inner : α
+
+instance {α : Type u} [NoncomputableOrd α] : Ord (WithClassical α) where
+  compare a b := NoncomputableOrd.compare a.inner b.inner
+
+end
+
+end Classical.Order

src/Std/Classes/Ord/New/Comparable.lean

@@ -0,0 +1,209 @@
+module
+
+prelude
+public import Init.Core
+public import Std.Classes.Ord.Basic
+public import Std.Classes.Ord.New.PartiallyComparable
+
+public section
+
+class Comparable (α : Type u) extends PartiallyComparable α, NoncomputableOrd α
+
+def Comparable.GT {α : Type u} [Comparable α] (a b : α) : Prop :=
+  open Classical.Order in
+  compare a b = .gt
+
+class ComputablyComparable (α : Type u) extends Comparable α, ComputablyPartiallyComparable α, Ord α
+
+-- TODO: This is already oriented!
+class LawfulComparable (α : Type u) [Comparable α] extends
+    LawfulPartiallyComparable α where
+  eq_lt_iff_lt : ∀ a b : α, NoncomputableOrd.compare a b = .lt ↔ LT.lt a b := by exact Iff.rfl
+  isLE_iff_le : ∀ a b : α, (NoncomputableOrd.compare a b).isLE ↔ LE.le a b := by exact Iff.rfl
+
+class LawfulOrientedComparable (α : Type u) [Comparable α] extends LawfulComparable α where
+  eq_gt_iff_gt : ∀ (a b : α), NoncomputableOrd.compare a b = .gt ↔ LT.lt b a := by exact Iff.rfl
+
+theorem Comparable.compare_eq_lt_iff_lt {α : Type u} [Ord α] [Comparable α]
+    [LawfulComparable α] [LawfulOrd α] : ∀ {a b : α}, compare a b = .lt ↔ a < b := by
+  intro a b
+  simp [← LawfulOrd.compare_eq_compare, LawfulComparable.eq_lt_iff_lt]
+
+theorem Comparable.compare_eq_gt_iff_gt {α : Type u} [Ord α] [Comparable α]
+    [LawfulOrientedComparable α] [LawfulOrd α] : ∀ {a b : α}, compare a b = .gt ↔ b < a := by
+  intro a b
+  simp [← LawfulOrd.compare_eq_compare, LawfulOrientedComparable.eq_gt_iff_gt]
+
+theorem Comparable.compare_isLE {α : Type u} [Ord α] [Comparable α] [LawfulOrd α] [LawfulComparable α]
+    {a b : α} : (compare a b).isLE ↔ a ≤ b := by
+  simp [← LawfulOrd.compare_eq_compare, LawfulComparable.isLE_iff_le]
+
+theorem Comparable.compare_eq_gt {α : Type u} [Ord α] [Comparable α]
+    [LawfulOrientedComparable α] [LawfulOrd α] {a b : α} :
+    compare a b = .gt ↔ compare b a = .lt := by
+  simp [← LawfulOrd.compare_eq_compare, LawfulOrientedComparable.eq_gt_iff_gt,
+    LawfulComparable.eq_lt_iff_lt]
+
+instance (α : Type u) [Ord α] [Comparable α] [LawfulOrd α] [LawfulOrientedComparable α] :
+    Std.OrientedOrd α where
+  eq_swap := by
+    intro a b
+    cases h : compare b a
+    · simp [Comparable.compare_eq_gt, h]
+    · simp only [Ordering.swap_eq]
+      cases h' : compare a b
+      · simp_all [← Comparable.compare_eq_gt]
+      · rfl
+      · simp_all [Comparable.compare_eq_gt]
+    · simp [← Comparable.compare_eq_gt, h]
+
+instance (α : Type u) [BEq α] [Ord α] [Comparable α] [LawfulComputableBEq α] [LawfulOrd α]
+    [LawfulOrientedComparable α] :
+    Std.LawfulBEqOrd α where
+  compare_eq_iff_beq {a b} := by
+    cases h : compare a b
+    all_goals simp [PartiallyComparable.beq_iff_le_ge, ← LawfulComparable.isLE_iff_le,
+      LawfulOrd.compare_eq_compare, Std.OrientedOrd.eq_swap (a := b), h]
+
+@[expose]
+def Comparable.leOfNoncomputableOrd (α : Type u) [NoncomputableOrd α] : LE α where
+  le a b := (NoncomputableOrd.compare a b).isLE
+
+@[expose]
+def Comparable.ltOfNoncomputableOrd (α : Type u) [NoncomputableOrd α] : LT α where
+  lt a b := (NoncomputableOrd.compare a b).isLT
+
+@[expose]
+def Comparable.noncomputableBEqOfNoncomputableOrd (α : Type u) [NoncomputableOrd α] :
+    NoncomputableBEq α :=
+  .ofRel fun a b => NoncomputableOrd.compare a b = .eq
+
+structure Comparable.OfNoncomputableOrdArgs (α : Type u) where
+  instNoncomputableOrd : NoncomputableOrd α := by
+    try (infer_instance; done)
+    all_goals (exact NoncomputableOrd.ofComputable; done)
+  instLE : LE α := by
+    try (infer_instance; done)
+    try (exact LE.ofBLE; done)
+    all_goals (exact Comparable.leOfNoncomputableOrd _; done)
+  instLT : LT α := by
+    try (infer_instance; done)
+    try (exact LT.ofBLT; done)
+    all_goals (exact Comparable.ltOfNoncomputableOrd _; done)
+  instNoncomputableBEq : NoncomputableBEq α := by
+    try (infer_instance; done)
+    try (exact NoncomputableBEq.ofComputable; done)
+    all_goals (exact Comparable.noncomputableBEqOfNoncomputableOrd _; done)
+
+def Comparable.ofNoncomputableOrd {α : Type u} (args : OfNoncomputableOrdArgs α) : Comparable α where
+  toNoncomputableOrd := args.instNoncomputableOrd
+  toLE := args.instLE
+  toLT := args.instLT
+  toNoncomputableBEq := args.instNoncomputableBEq
+
+@[expose]
+def Comparable.bleOfOrd (α : Type u) [Ord α] : BLE α where
+  LE a b := (compare a b).isLE
+
+@[expose]
+def Comparable.leOfOrd (α : Type u) [Ord α] : LE α where
+  le a b := (compare a b).isLE
+
+@[expose]
+def Comparable.bltOfOrd (α : Type u) [Ord α] : BLT α where
+  LT a b := (compare a b).isLT
+
+@[expose]
+def Comparable.ltOfOrd (α : Type u) [Ord α] : LT α where
+  lt a b := (compare a b).isLT
+
+@[expose]
+def Comparable.beqOfOrd (α : Type u) [Ord α] :
+    BEq α :=
+  ⟨fun a b => compare a b = .eq⟩
+
+@[expose]
+def Comparable.noncomputableBEqOfOrd (α : Type u) [Ord α] :
+    NoncomputableBEq α :=
+  .ofRel fun a b => compare a b = .eq
+
+structure ComputablyComparable.OfOrdArgs (α : Type u) where
+  instOrd : Ord α := by
+    all_goals (infer_instance; done)
+  instNoncomputableOrd : NoncomputableOrd α := by
+    try (infer_instance; done)
+    all_goals (exact NoncomputableOrd.ofComputable; done)
+  instBLE : BLE α := by
+    try (infer_instance; done)
+    all_goals (exact Comparable.bleOfOrd _; done)
+  instLE : LE α := by
+    try (infer_instance; done)
+    all_goals (exact Comparable.leOfOrd _; done)
+  instBLT : BLT α := by
+    try (infer_instance; done)
+    all_goals (exact Comparable.bltOfOrd _; done)
+  instLT : LT α := by
+    try (infer_instance; done)
+    all_goals (exact Comparable.ltOfOrd _; done)
+  instBEq : BEq α := by
+    try (infer_instance; done)
+    all_goals (exact Comparable.beqOfOrd _; done)
+  instNoncomputableBEq : NoncomputableBEq α := by
+    try (infer_instance; done)
+    all_goals (exact Comparable.noncomputableBEqOfOrd _; done)
+
+abbrev ComputablyComparable.ofOrd {α : Type u} (args : OfOrdArgs α) : ComputablyComparable α where
+  toOrd := args.instOrd
+  toNoncomputableOrd := args.instNoncomputableOrd
+  toBLE := args.instBLE
+  toLE := args.instLE
+  toBLT := args.instBLT
+  toLT := args.instLT
+  toBEq := args.instBEq
+  toNoncomputableBEq := args.instNoncomputableBEq
+
+abbrev Comparable.ofOrd (α : Type u) [Ord α] : Comparable α :=
+  ComputablyComparable.ofOrd {} |>.toComparable
+
+instance (α : Type u) [Ord α] :
+    haveI : BLE α := Comparable.bleOfOrd α
+    haveI : LE α := Comparable.leOfOrd α
+    LawfulBLE α :=
+  letI : BLE α := Comparable.bleOfOrd α
+  letI : LE α := Comparable.leOfOrd α
+  ⟨by simp [Comparable.bleOfOrd, Comparable.leOfOrd]⟩
+
+instance (α : Type u) [Ord α] :
+    haveI : BLT α := Comparable.bltOfOrd α
+    haveI : LT α := Comparable.ltOfOrd α
+    LawfulBLT α :=
+  letI : BLT α := Comparable.bltOfOrd α
+  letI : LT α := Comparable.ltOfOrd α
+  ⟨by simp [Comparable.bltOfOrd, Comparable.ltOfOrd]⟩
+
+def Comparable.lawful (alpha : Type u) [NoncomputableOrd alpha]
+    (oriented : ∀ a b : alpha, NoncomputableOrd.compare a b = .lt → NoncomputableOrd.compare b a = .lt) :
+    haveI : Comparable alpha := .ofNoncomputableOrd {}
+    LawfulComparable alpha :=
+  letI : Comparable alpha := .ofNoncomputableOrd {}
+  haveI : LawfulPartiallyComparable alpha := sorry
+  ⟨sorry, sorry⟩
+
+def ComputablyComparable.lawful (α : Type u) [Ord α]
+    (oriented : ∀ a b : α, compare a b = .lt → compare b a = .lt) :
+    haveI : ComputablyComparable α := .ofOrd {}
+    LawfulComparable α :=
+  letI : ComputablyComparable α := .ofOrd {}
+  haveI : LawfulPartiallyComparable α := sorry
+  ⟨sorry, sorry⟩
+
+-- Cmp conundrum
+-- Cmp induces Comparable, but only up to propositional equality
+-- At the moment, Ord -> cmp -> Ord is definitionally equal to id
+-- It would be weird and potentially inefficient to pass around a whole
+--   `Comparable` instance (or worse) as an explicit argument
+-- `ToComparable α β`: `β` can be converted into a `Comparable` instance?
+--   For example, `ComparisonFn α` might just contain a compare function
+--   But there might also simply be a `InferredComparableInstance α [Comparable α]`
+--   type, which is a subsingleton.
+-- Instead of `OrientedCmp cmp`, perhaps use `OrientedComparable α (i := .ofFn cmp)`?

src/Std/Classes/Ord/New/Examples.lean

@@ -0,0 +1,4 @@
+module
+
+prelude
+import Std.Classes.Ord.New.Instances

src/Std/Classes/Ord/New/Instances.lean

@@ -0,0 +1,19 @@
+module
+
+prelude
+public import Std.Classes.Ord.New.Comparable
+import Init.Data.Nat.Lemmas
+
+instance : BLE Nat where
+  LE a b := a ≤ b
+
+instance : BLT Nat where
+  LT a b := a < b
+
+instance : ComputablyComparable Nat := .ofOrd {}
+
+instance : LawfulComparable Nat where
+  lt_iff_le_not_ge a b := by omega
+  eq_lt_iff_lt a b := sorry
+  isLE_iff_le := sorry
+  beq_iff_le_ge := sorry

src/Std/Classes/Ord/New/LinearOrder.lean

@@ -0,0 +1,27 @@
+module
+
+prelude
+public import Std.Classes.Ord.New.LinearPreorder
+public import Std.Classes.Ord.New.PartialOrder
+
+public section
+
+class LawfulLinearOrder (α : Type u) [Comparable α] extends LawfulLinearPreorder α, LawfulPartialOrder α
+
+instance (α : Type u) [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearOrder α] :
+    Std.LawfulEqOrd α where
+  eq_of_compare h := by
+    apply LawfulPartialOrder.toAntisymm.antisymm
+    · simp [← Comparable.compare_isLE, h]
+    · rw [Std.OrientedOrd.eq_swap, Ordering.swap_eq_eq] at h
+      simp [← Comparable.compare_isLE, h]
+
+instance (α : Type u) [Comparable α] [LawfulLinearPreorder α] [Std.Antisymm (α := α) (· ≤ ·)] :
+    LawfulLinearOrder α where
+
+instance (α : Type u) [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α]
+    [Std.LawfulEqOrd α] : Std.Antisymm (α := α) (· ≤ ·) where
+  antisymm a b := by
+    cases h : compare a b
+    all_goals simp [← Comparable.compare_isLE, ← Std.LawfulEqOrd.compare_eq_iff_eq (α := α),
+      Std.OrientedOrd.eq_swap (a := b), h]

src/Std/Classes/Ord/New/LinearPreorder.lean

@@ -0,0 +1,16 @@
+module
+
+prelude
+public import Std.Classes.Ord.Basic
+public import Std.Classes.Ord.New.Preorder
+
+public section
+
+class LawfulLinearPreorder (α : Type u) [Comparable α] extends LawfulPreorder α,
+    LawfulOrientedComparable α
+
+instance (α : Type u) [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] :
+    Std.TransOrd α where
+  isLE_trans := by
+    simp [Comparable.compare_isLE]
+    apply LawfulPreorder.le_trans

src/Std/Classes/Ord/New/PartialOrder.lean

@@ -0,0 +1,9 @@
+module
+
+prelude
+public import Std.Classes.Ord.New.LinearPreorder
+
+public section
+
+class LawfulPartialOrder (α : Type u) [PartiallyComparable α] extends LawfulPreorder α,
+    Std.Antisymm (α := α) (· ≤ ·) where

src/Std/Classes/Ord/New/PartiallyComparable.lean

@@ -0,0 +1,106 @@
+module
+
+prelude
+public import Init.Core
+public import Std.Classes.Ord.New.BasicOperations
+
+public section
+
+class PartiallyComparable (α : Type u) extends LT α, LE α, NoncomputableBEq α
+
+instance (α : Type u) [LT α] [LE α] [NoncomputableBEq α] : PartiallyComparable α where
+
+class ComputablyPartiallyComparable α extends PartiallyComparable α, BLE α, BLT α, BEq α
+
+class LawfulPartiallyComparable (α : Type u) [PartiallyComparable α] where
+    lt_iff_le_not_ge : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬ b ≤ a := by exact fun _ _ => Iff.rfl
+    beq_iff_le_ge : ∀ a b : α, NoncomputableBEq.IsEq a b ↔ a ≤ b ∧ b ≤ a := by
+      exact fun _ _ => Iff.rfl
+
+structure PartiallyComparable.OfLEArgs (α : Type u) where
+  instLE : LE α := by
+    try (infer_instance; done)
+    try (exact LE.ofBLE; done)
+  instLT : LT α := by
+    try (infer_instance; done)
+    try (exact LT.ofBLT; done)
+    try (exact ⟨fun a b => a ≤ b ∧ ¬ b ≤ a⟩; done)
+  instNoncomputableBEq : NoncomputableBEq α := by
+    try (infer_instance; done)
+    try (exact NoncomputableBEq.ofComputable; done)
+    try (exact NoncomputableBEq.ofRel fun a b => a ≤ b ∧ b ≤ a; done)
+
+@[expose]
+def PartiallyComparable.ofLE (args : OfLEArgs α) : PartiallyComparable α where
+  toLE := args.instLE
+  toLT := args.instLT
+  toNoncomputableBEq := args.instNoncomputableBEq
+
+@[expose]
+def PartiallyComparable.bltOfBLE (α : Type u) [BLE α] : BLT α where
+  LT a b := BLE.LE a b && ! BLE.LE b a
+
+@[expose]
+def PartiallyComparable.ltOfBLE (α : Type u) [BLE α] : LT α where
+  lt a b := BLE.LE a b ∧ ¬ BLE.LE b a
+
+structure ComputablyPartiallyComparable.OfBLEArgs (α : Type u) where
+  instBLE : BLE α := by
+    try (infer_instance; done)
+  instLE : LE α := by
+    try (infer_instance; done)
+    try (exact LE.ofBLE α; done)
+  instBLT : BLT α := by
+    try (infer_instance; done)
+    try (exact PartiallyComparable.bltOfBLE α; done)
+  instLT : LT α := by
+    try (infer_instance; done)
+    try (exact PartiallyComparable.ltOfBLE α; done)
+  instBEq : BEq α := by
+    try (infer_instance; done)
+    try (exact ⟨fun a b => BLE.LE a b ∧ BLE.LE b a⟩; done)
+  instNoncomputableBEq : NoncomputableBEq α := by
+    try (infer_instance; done)
+    try (exact NoncomputableBEq.ofComputable; done)
+    try (exact NoncomputableBEq.ofRel fun a b => BLE.LE a b && BLE.LE b a; done)
+
+def ComputablyPartiallyComparable.ofBLE (args : OfBLEArgs α) : ComputablyPartiallyComparable α where
+  toBLE := args.instBLE
+  toLE := args.instLE
+  toBLT := args.instBLT
+  toLT := args.instLT
+  toBEq := args.instBEq
+  toNoncomputableBEq := args.instNoncomputableBEq
+
+instance PartiallyComparable.lawful [LE α] :
+    haveI : PartiallyComparable α := .ofLE {}
+    LawfulPartiallyComparable α :=
+  letI : PartiallyComparable α := .ofLE {}
+  { beq_iff_le_ge := by intro a b; simp [NoncomputableBEq.ofRel, PartiallyComparable.ofLE] }
+
+instance (α : Type u) [BLE α] :
+    haveI : BLT α := PartiallyComparable.bltOfBLE α
+    haveI : LT α := PartiallyComparable.ltOfBLE α
+    LawfulBLT α :=
+  letI : BLT α := PartiallyComparable.bltOfBLE α
+  letI : LT α := PartiallyComparable.ltOfBLE α
+  ⟨fun a b => by simp [PartiallyComparable.ltOfBLE, PartiallyComparable.bltOfBLE]⟩
+
+instance (α : Type u) [BLE α] :
+    haveI : BLT α := PartiallyComparable.bltOfBLE α
+    haveI : LT α := PartiallyComparable.ltOfBLE α
+    LawfulBLT α :=
+  letI : BLT α := PartiallyComparable.bltOfBLE α
+  letI : LT α := PartiallyComparable.ltOfBLE α
+  ⟨fun a b => by simp [PartiallyComparable.ltOfBLE, PartiallyComparable.bltOfBLE]⟩
+
+theorem PartiallyComparable.beq_iff_le_ge {α : Type u} [BEq α] [PartiallyComparable α]
+    [LawfulComputableBEq α] [LawfulPartiallyComparable α] {a b : α} :
+    a == b ↔ a ≤ b ∧ b ≤ a := by
+  simp [← LawfulComputableBEq.isEq_iff_beq, LawfulPartiallyComparable.beq_iff_le_ge]
+
+theorem PartiallyComparable.beq_eq_false_of_lt {α : Type u} [BEq α] [PartiallyComparable α]
+    [LawfulComputableBEq α] [LawfulPartiallyComparable α] {a b : α} (h : a < b) :
+    (a == b) = false := by
+  rw [LawfulPartiallyComparable.lt_iff_le_not_ge] at h
+  simp [← Bool.not_eq_true, beq_iff_le_ge, h]

src/Std/Classes/Ord/New/Preorder.lean

@@ -0,0 +1,20 @@
+module
+
+prelude
+public import Std.Classes.Ord.New.Comparable
+
+public section
+
+class LawfulPreorder (α : Type u) [PartiallyComparable α] extends LawfulPartiallyComparable α where
+  le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
+  le_refl : ∀ a : α, a ≤ a
+
+instance (α : Type u) [PartiallyComparable α] [LawfulPreorder α] :
+    Trans (α := α) (· < ·) (· < ·) (· < ·) where
+  trans {a b c} hab hbc := by
+    rw [LawfulPartiallyComparable.lt_iff_le_not_ge] at *
+    constructor
+    · exact LawfulPreorder.le_trans _ _ _ hab.1 hbc.1
+    · intro h
+      have : c ≤ b := LawfulPreorder.le_trans _ _ _ h hab.1
+      exact hbc.2 this

src/Std/Classes/Ord/New/Util.lean

@@ -0,0 +1,30 @@
+module
+
+prelude
+public import Init.Core
+
+public section
+
+inductive Noncomputable (α : Type u) where
+  | comp : α → Noncomputable α
+  | noncomp : (P : α → Prop) → (h : Nonempty (Subtype P)) → Noncomputable α
+
+class Noncomputable' (α : Type u) where
+  get : (choose : (P : α → Prop) → Nonempty (Subtype P) → α) → α
+  get_const : ∀ c c', get c = get c'
+
+attribute [class] Noncomputable
+
+@[expose]
+noncomputable def Noncomputable.inst [i : Noncomputable α] : α :=
+  match i with
+  | .comp a => a
+  | .noncomp P _ => (Classical.ofNonempty : Subtype P)
+
+@[expose]
+noncomputable def Noncomputable'.inst [i : Noncomputable' α] : α :=
+  i.get (fun P _ => (Classical.ofNonempty : Subtype P).val)
+
+@[expose]
+def Noncomputable'.comp {α : Type u} (a : α) : Noncomputable' α :=
+  ⟨fun _ => a, fun _ _ => rfl⟩

src/Std/Classes/Test.lean

@@ -0,0 +1,145 @@
+prelude
+import Init.Core
+import Init.Data.Ord
+import Lean
+
+namespace Std.Classes.Test
+
+class BLE (α : Type u) where
+  LE : α → α → Bool
+
+class LE (α : Type u) where
+  LE : α → α → Prop
+
+class LawfulBLE (α : Type u) [LE α] [BLE α] where
+  ble_iff_le : ∀ a b : α, BLE.LE a b ↔ LE.LE a b
+
+abbrev DecidableLE (α : Type u) [LE α] :=
+  DecidableRel (fun a b : α => LE.LE a b)
+
+instance (α : Type u) [BLE α] [LE α] [LawfulBLE α] : DecidableLE α :=
+  fun a b => if h : BLE.LE a b then
+      .isTrue (LawfulBLE.ble_iff_le _ _ |>.mp h)
+    else
+      .isFalse (h.imp (LawfulBLE.ble_iff_le _ _).mpr)
+
+class BLT (α : Type u) where
+  LT : α → α → Bool
+
+class LT (α : Type u) where
+  LT : α → α → Prop
+
+class LawfulBLT (α : Type u) [LT α] [BLT α] where
+  blt_iff_lt : ∀ a b : α, BLT.LT a b ↔ LT.LT a b
+
+abbrev DecidableLT (α : Type u) [LT α] := DecidableRel (fun a b : α => LT.LT a b)
+
+instance (α : Type u) [BLT α] [LT α] [LawfulBLT α] : DecidableLT α :=
+  fun a b => if h : BLT.LT a b then
+      .isTrue (LawfulBLT.blt_iff_lt _ _ |>.mp h)
+    else
+      .isFalse (h.imp (LawfulBLT.blt_iff_lt _ _).mpr)
+
+class Ord (α : Type u) where
+  compare : α → α → Ordering
+
+class Noncomputable (α : Type u) where
+  Predicate : α → Prop
+  nonempty : Nonempty (Subtype Predicate)
+  subsingleton : Subsingleton (Subtype Predicate)
+
+def Noncomputable.ofComputable {α : Type u} (a : α) : Noncomputable α where
+  Predicate := (· = a)
+  nonempty := ⟨⟨a, rfl⟩⟩
+  subsingleton := .intro fun a b => Subtype.ext (a.2.trans b.2.symm)
+
+noncomputable def Noncomputable.get (i : Noncomputable α := by infer_instance) :=
+  haveI := i.nonempty
+  (Classical.ofNonempty (α := Subtype i.Predicate)).val
+
+abbrev LogicalOrd (α : Type u) := Noncomputable (Ord α)
+
+noncomputable def LogicalOrd.instOrd {α : Type u} [i : LogicalOrd α] : Ord α :=
+  Noncomputable.get
+
+noncomputable def LogicalOrd.compare {α : Type u} [LogicalOrd α] (a b : α) : Ordering :=
+  LogicalOrd.instOrd.compare a b
+
+class OrdForOrd (α : Type u) [LogicalOrd α] [i : Ord α] where
+  eq : LogicalOrd.instOrd = i
+
+class LogicalOrd.LawfulLT (α : Type u) [LT α] [LogicalOrd α] where
+  compare_eq_lt_iff_lt {a b : α} : LogicalOrd.compare a b = .lt ↔ LT.LT a b
+  compare_eq_gt_iff_gt {a b : α} : LogicalOrd.compare a b = .gt ↔ LT.LT b a
+
+class LogicalOrd.LawfulLE (α : Type u) [LE α] [LogicalOrd α] where
+  compare_isLE_iff_le {a b : α} : (LogicalOrd.compare a b).isLE ↔ LE.LE a b
+  compare_eq_ge_iff_ge {a b : α} : (LogicalOrd.compare a b).isLE ↔ LE.LE b a
+
+class LogicalOrd.LawfulBLT (α : Type u) [BLT α] [LogicalOrd α] where
+  compare_eq_lt_iff_lt {a b : α} : LogicalOrd.compare a b = .lt ↔ BLT.LT a b
+  compare_eq_gt_iff_gt {a b : α} : LogicalOrd.compare a b = .gt ↔ BLT.LT b a
+
+class LogicalOrd.LawfulBLE (α : Type u) [BLE α] [LogicalOrd α] where
+  compare_isBLE_iff_le {a b : α} : (LogicalOrd.compare a b).isLE ↔ BLE.LE a b
+  compare_eq_ge_iff_ge {a b : α} : (LogicalOrd.compare a b).isLE ↔ BLE.LE b a
+
+class Min (α : Type u) where
+  min : α → α → α
+
+abbrev LogicalMin (α : Type u) := Noncomputable (Min α)
+
+class Max (α : Type u) where
+  max : α → α → α
+
+abbrev LogicalMax (α : Type u) := Noncomputable (Max α)
+
+class LogicalMin.LawfulMin (α : Type u) [LogicalMin α] [i : Min α] where
+  eq : Noncomputable.get = i
+
+class LogicalMax.LawfulMax (α : Type u) [LogicalMax α] [i : Max α] where
+  eq : Noncomputable.get = i
+
+def Ord.ofBLE {α} [BLE α] : Ord α where
+  compare a b := if BLE.LE a b then
+      if BLE.LE b a then .eq else .lt
+    else
+      .gt
+
+noncomputable def BLE.ofLE {α} [i : Std.Classes.Test.LE α] : BLE α where
+  LE a b := open scoped Classical in decide (i.LE a b)
+
+def LogicalOrd.ofBLE {α} [BLE α] : LogicalOrd α := .ofComputable .ofBLE
+
+class Assign {α : Type u} (a : outParam α) (b : α) where
+  eq : a = b
+
+instance (α : Type u) (a : α) : Assign a a where
+  eq := rfl
+
+attribute [local instance] LogicalOrd.ofBLE in
+example [BLE α] [BLT α] [LogicalOrd.ofBLE.LawfulBLE α] [LogicalOrd.ofBLE.LawfulBLT α] (a b : α)
+    (h : BLT.LT a b) : BLE.LE a b := by
+  simp only [← LogicalOrd.LawfulBLE.compare_isBLE_iff_le,
+    ← LogicalOrd.LawfulBLT.compare_eq_lt_iff_lt] at ⊢ h
+  simp [h]
+
+theorem s [BLE α] [BLT α] {x : LogicalOrd α} [Assign x LogicalOrd.ofBLE] [LogicalOrd.LawfulBLE α] [LogicalOrd.LawfulBLT α] {a b : α}
+    (h : BLT.LT a b) : BLE.LE a b := by
+  simp only [← LogicalOrd.LawfulBLE.compare_isBLE_iff_le,
+    ← LogicalOrd.LawfulBLT.compare_eq_lt_iff_lt] at ⊢ h
+  simp [h]
+
+example [BLE α] [BLT α] [LogicalOrd.ofBLE.LawfulBLE α] [LogicalOrd.ofBLE.LawfulBLT α]
+    (a b : α) (h : BLT.LT a b) : BLE.LE a b := s h
+
+theorem t [BLE α] [BLT α] {x : LogicalOrd α} [LogicalOrd.LawfulBLE α] [LogicalOrd.LawfulBLT α] {a b : α}
+    (h : BLT.LT a b) (_x : x = LogicalOrd.ofBLE := by rfl) : BLE.LE a b := by
+  simp only [← LogicalOrd.LawfulBLE.compare_isBLE_iff_le,
+    ← LogicalOrd.LawfulBLT.compare_eq_lt_iff_lt] at ⊢ h
+  simp [h]
+
+example [BLE α] [BLT α] [LogicalOrd.ofBLE.LawfulBLE α] [LogicalOrd.ofBLE.LawfulBLT α]
+    (a b : α) (h : BLT.LT a b) : BLE.LE a b := t h
+
+end Std.Classes.Test

src/Std/Data/DTreeMap/Basic.lean

@@ -67,7 +67,7 @@ structure DTreeMap (α : Type u) (β : α → Type v) (cmp : α → α → Order
   /-- Internal implementation detail of the tree map. -/
   inner : DTreeMap.Internal.Impl α β
   /-- Internal implementation detail of the tree map. -/
-  wf : letI : Ord α := ⟨cmp⟩; inner.WF
+  wf : letI : Ord α := ⟨cmp⟩; letI := Comparable.ofOrd α; inner.WF
 
 namespace DTreeMap
 open Internal (Impl)
@@ -79,7 +79,7 @@ use the empty collection notations `∅` and `{}` to create an empty tree map. `
 -/
 @[inline]
 def empty : DTreeMap α β cmp :=
-  letI : Ord α := ⟨cmp⟩; ⟨Internal.Impl.empty, .empty⟩
+  letI : Ord α := ⟨cmp⟩; letI := Comparable.ofOrd α; ⟨Internal.Impl.empty, .empty⟩
 
 instance : EmptyCollection (DTreeMap α β cmp) where
   emptyCollection := empty
@@ -104,7 +104,9 @@ key and value will be replaced.
 -/
 @[inline]
 def insert (t : DTreeMap α β cmp) (a : α) (b : β a) : DTreeMap α β cmp :=
-  letI : Ord α := ⟨cmp⟩; ⟨(t.inner.insert a b t.wf.balanced).impl, .insert t.wf⟩
+  letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
+  ⟨(t.inner.insert a b t.wf.balanced).impl, .insert t.wf⟩
 
 instance : Singleton ((a : α) × β a) (DTreeMap α β cmp) where
   singleton e := (∅ : DTreeMap α β cmp).insert e.1 e.2
@@ -121,7 +123,9 @@ returns the map unaltered.
 -/
 @[inline]
 def insertIfNew (t : DTreeMap α β cmp) (a : α) (b : β a) : DTreeMap α β cmp :=
-  letI : Ord α := ⟨cmp⟩; ⟨(t.inner.insertIfNew a b t.wf.balanced).impl, t.wf.insertIfNew⟩
+  letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α;
+  ⟨(t.inner.insertIfNew a b t.wf.balanced).impl, t.wf.insertIfNew⟩
 
 /--
 Checks whether a key is present in a map and unconditionally inserts a value for the key.
@@ -131,6 +135,7 @@ Equivalent to (but potentially faster than) calling `contains` followed by `inse
 @[inline]
 def containsThenInsert (t : DTreeMap α β cmp) (a : α) (b : β a) : Bool × DTreeMap α β cmp :=
   letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
   let p := t.inner.containsThenInsert a b t.wf.balanced
   (p.1, ⟨p.2.impl, t.wf.containsThenInsert⟩)
 
@@ -145,6 +150,7 @@ Equivalent to (but potentially faster than) calling `contains` followed by `inse
 def containsThenInsertIfNew (t : DTreeMap α β cmp) (a : α) (b : β a) :
     Bool × DTreeMap α β cmp :=
   letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
   let p := t.inner.containsThenInsertIfNew a b t.wf.balanced
   (p.1, ⟨p.2.impl, t.wf.containsThenInsertIfNew⟩)
 
@@ -163,6 +169,7 @@ Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 def getThenInsertIfNew? [LawfulEqCmp cmp] (t : DTreeMap α β cmp) (a : α) (b : β a) :
     Option (β a) × DTreeMap α β cmp :=
   letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
   let p := t.inner.getThenInsertIfNew? a b t.wf.balanced
   (p.1, ⟨p.2, t.wf.getThenInsertIfNew?⟩)
 
@@ -176,7 +183,9 @@ Observe that this is different behavior than for lists: for lists, `∈` uses `=
 -/
 @[inline]
 def contains (t : DTreeMap α β cmp) (a : α) : Bool :=
-  letI : Ord α := ⟨cmp⟩; t.inner.contains a
+  letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
+  t.inner.contains a
 
 instance : Membership α (DTreeMap α β cmp) where
   mem m a := m.contains a
@@ -197,7 +206,9 @@ def isEmpty (t : DTreeMap α β cmp) : Bool :=
 /-- Removes the mapping for the given key if it exists. -/
 @[inline]
 def erase (t : DTreeMap α β cmp) (a : α) : DTreeMap α β cmp :=
-  letI : Ord α := ⟨cmp⟩; ⟨(t.inner.erase a t.wf.balanced).impl, .erase t.wf⟩
+  letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
+  ⟨(t.inner.erase a t.wf.balanced).impl, .erase t.wf⟩
 
 /--
 Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.
@@ -437,7 +448,9 @@ def entryAtIdx? (t : DTreeMap α β cmp) (n : Nat) : Option ((a : α) × β a) :
 /-- Returns the key-value pair with the `n`-th smallest key. -/
 @[inline]
 def entryAtIdx (t : DTreeMap α β cmp) (n : Nat) (h : n < t.size) : (a : α) × β a :=
-  letI : Ord α := ⟨cmp⟩; Impl.entryAtIdx t.inner t.wf.balanced n h
+  letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
+  Impl.entryAtIdx t.inner t.wf.balanced n h
 
 /-- Returns the key-value pair with the `n`-th smallest key, or panics if `n` is at least `t.size`. -/
 @[inline]
@@ -462,7 +475,9 @@ def keyAtIndex? (t : DTreeMap α β cmp) (n : Nat) : Option α :=
 /-- Returns the `n`-th smallest key. -/
 @[inline]
 def keyAtIdx (t : DTreeMap α β cmp) (n : Nat) (h : n < t.size) : α :=
-  letI : Ord α := ⟨cmp⟩; Impl.keyAtIdx t.inner t.wf.balanced n h
+  letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
+  Impl.keyAtIdx t.inner t.wf.balanced n h
 
 @[inline, inherit_doc keyAtIdx, deprecated keyAtIdx (since := "2025-03-25")]
 def keyAtIndex (t : DTreeMap α β cmp) (n : Nat) (h : n < t.size) : α :=
@@ -696,6 +711,7 @@ variable {β : Type v}
 def getThenInsertIfNew? (t : DTreeMap α β cmp) (a : α) (b : β) :
     Option β × DTreeMap α β cmp :=
   letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
   let p := Impl.Const.getThenInsertIfNew? t.inner a b t.wf.balanced
   (p.1, ⟨p.2, t.wf.constGetThenInsertIfNew?⟩)
 
@@ -797,7 +813,9 @@ def entryAtIdx? (t : DTreeMap α β cmp) (n : Nat) : Option (α × β) :=
 
 @[inline, inherit_doc DTreeMap.entryAtIdx]
 def entryAtIdx (t : DTreeMap α β cmp) (n : Nat) (h : n < t.size) : α × β :=
-  letI : Ord α := ⟨cmp⟩; Impl.Const.entryAtIdx t.inner t.wf.balanced n h
+  letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
+  Impl.Const.entryAtIdx t.inner t.wf.balanced n h
 
 @[inline, inherit_doc DTreeMap.entryAtIdx!]
 def entryAtIdx! [Inhabited (α × β)] (t : DTreeMap α β cmp) (n : Nat) : α × β :=
@@ -868,7 +886,9 @@ variable {δ : Type w} {m : Type w → Type w₂} [Monad m]
 /-- Removes all mappings of the map for which the given function returns `false`. -/
 @[inline]
 def filter (f : (a : α) → β a → Bool) (t : DTreeMap α β cmp) : DTreeMap α β cmp :=
-  letI : Ord α := ⟨cmp⟩; ⟨t.inner.filter f t.wf.balanced |>.impl, t.wf.filter⟩
+  letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
+  ⟨t.inner.filter f t.wf.balanced |>.impl, t.wf.filter⟩
 
 /-- Folds the given monadic function over the mappings in the map in ascending order. -/
 @[inline]
@@ -990,7 +1010,9 @@ def toList (t : DTreeMap α β cmp) : List ((a : α) × β a) :=
 @[inline]
 def ofList (l : List ((a : α) × β a)) (cmp : α → α → Ordering := by exact compare) :
     DTreeMap α β cmp :=
-  letI : Ord α := ⟨cmp⟩; ⟨Impl.ofList l, Impl.WF.empty.insertMany⟩
+  letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
+  ⟨Impl.ofList l, Impl.WF.empty.insertMany⟩
 
 @[inline, inherit_doc ofList, deprecated ofList (since := "2025-02-12")]
 def fromList (l : List ((a : α) × β a)) (cmp : α → α → Ordering) : DTreeMap α β cmp :=
@@ -1005,7 +1027,9 @@ def toArray (t : DTreeMap α β cmp) : Array ((a : α) × β a) :=
 @[inline]
 def ofArray (a : Array ((a : α) × β a)) (cmp : α → α → Ordering := by exact compare) :
     DTreeMap α β cmp :=
-  letI : Ord α := ⟨cmp⟩; ⟨Impl.ofArray a, Impl.WF.empty.insertMany⟩
+  letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
+  ⟨Impl.ofArray a, Impl.WF.empty.insertMany⟩
 
 @[inline, inherit_doc ofArray, deprecated ofArray (since := "2025-02-12")]
 def fromArray (a : Array ((a : α) × β a)) (cmp : α → α → Ordering) : DTreeMap α β cmp :=
@@ -1018,7 +1042,9 @@ This function ensures that the value is used linearly.
 -/
 @[inline]
 def modify [LawfulEqCmp cmp] (t : DTreeMap α β cmp) (a : α) (f : β a → β a) : DTreeMap α β cmp :=
-  letI : Ord α := ⟨cmp⟩; ⟨t.inner.modify a f, t.wf.modify⟩
+  letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
+  ⟨t.inner.modify a f, t.wf.modify⟩
 
 /--
 Modifies in place the value associated with a given key,
@@ -1029,7 +1055,9 @@ This function ensures that the value is used linearly.
 @[inline]
 def alter [LawfulEqCmp cmp] (t : DTreeMap α β cmp) (a : α) (f : Option (β a) → Option (β a)) :
     DTreeMap α β cmp :=
-  letI : Ord α := ⟨cmp⟩; ⟨t.inner.alter a f t.wf.balanced |>.impl, t.wf.alter⟩
+  letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
+  ⟨t.inner.alter a f t.wf.balanced |>.impl, t.wf.alter⟩
 
 /--
 Returns a map that contains all mappings of `t₁` and `t₂`. In case that both maps contain the
@@ -1049,7 +1077,9 @@ Hence, the runtime of this method scales logarithmically in the size of `t₁` a
 @[inline]
 def mergeWith [LawfulEqCmp cmp] (mergeFn : (a : α) → β a → β a → β a) (t₁ t₂ : DTreeMap α β cmp) :
     DTreeMap α β cmp :=
-  letI : Ord α := ⟨cmp⟩; ⟨t₁.inner.mergeWith mergeFn t₂.inner t₁.wf.balanced |>.impl, t₁.wf.mergeWith⟩
+  letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
+  ⟨t₁.inner.mergeWith mergeFn t₂.inner t₁.wf.balanced |>.impl, t₁.wf.mergeWith⟩
 
 @[inline, inherit_doc mergeWith, deprecated mergeWith (since := "2025-02-12")]
 def mergeBy [LawfulEqCmp cmp] (mergeFn : (a : α) → β a → β a → β a) (t₁ t₂ : DTreeMap α β cmp) :
@@ -1067,6 +1097,7 @@ def toList (t : DTreeMap α β cmp) : List (α × β) :=
 @[inline, inherit_doc DTreeMap.ofList]
 def ofList (l : List (α × β)) (cmp : α → α → Ordering := by exact compare) : DTreeMap α β cmp :=
   letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
   ⟨Impl.Const.ofList l, Impl.WF.empty.constInsertMany⟩
 
 @[inline, inherit_doc DTreeMap.toArray]
@@ -1076,31 +1107,39 @@ def toArray (t : DTreeMap α β cmp) : Array (α × β) :=
 @[inline, inherit_doc DTreeMap.ofList]
 def ofArray (a : Array (α × β)) (cmp : α → α → Ordering := by exact compare) : DTreeMap α β cmp :=
   letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
   ⟨Impl.Const.ofArray a, Impl.WF.empty.constInsertMany⟩
 
 /-- Transforms a list of keys into a tree map. -/
 @[inline]
 def unitOfList (l : List α) (cmp : α → α → Ordering := by exact compare) : DTreeMap α Unit cmp :=
   letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
   ⟨Impl.Const.unitOfList l, Impl.WF.empty.constInsertManyIfNewUnit⟩
 
 /-- Transforms an array of keys into a tree map. -/
 @[inline]
 def unitOfArray (a : Array α) (cmp : α → α → Ordering := by exact compare) : DTreeMap α Unit cmp :=
   letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
   ⟨Impl.Const.unitOfArray a, Impl.WF.empty.constInsertManyIfNewUnit⟩
 
 @[inline, inherit_doc DTreeMap.modify]
 def modify (t : DTreeMap α β cmp) (a : α) (f : β → β) : DTreeMap α β cmp :=
-  letI : Ord α := ⟨cmp⟩; ⟨Impl.Const.modify a f t.inner, t.wf.constModify⟩
+  letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
+  ⟨Impl.Const.modify a f t.inner, t.wf.constModify⟩
 
 @[inline, inherit_doc DTreeMap.alter]
 def alter (t : DTreeMap α β cmp) (a : α) (f : Option β → Option β) : DTreeMap α β cmp :=
-  letI : Ord α := ⟨cmp⟩; ⟨Impl.Const.alter a f t.inner t.wf.balanced |>.impl, t.wf.constAlter⟩
+  letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
+  ⟨Impl.Const.alter a f t.inner t.wf.balanced |>.impl, t.wf.constAlter⟩
 
 @[inline, inherit_doc DTreeMap.mergeWith]
 def mergeWith (mergeFn : α → β → β → β) (t₁ t₂ : DTreeMap α β cmp) : DTreeMap α β cmp :=
-  letI : Ord α := ⟨cmp⟩;
+  letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
   ⟨Impl.Const.mergeWith mergeFn t₁.inner t₂.inner t₁.wf.balanced |>.impl, t₁.wf.constMergeWith⟩
 
 @[inline, inherit_doc mergeWith, deprecated mergeWith (since := "2025-02-12")]
@@ -1119,7 +1158,9 @@ appearance.
 -/
 @[inline]
 def insertMany {ρ} [ForIn Id ρ ((a : α) × β a)] (t : DTreeMap α β cmp) (l : ρ) : DTreeMap α β cmp :=
-  letI : Ord α := ⟨cmp⟩; ⟨t.inner.insertMany l t.wf.balanced, t.wf.insertMany⟩
+  letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
+  ⟨t.inner.insertMany l t.wf.balanced, t.wf.insertMany⟩
 
 /--
 Erases multiple mappings from the tree map by iterating over the given collection and calling
@@ -1127,7 +1168,9 @@ Erases multiple mappings from the tree map by iterating over the given collectio
 -/
 @[inline]
 def eraseMany {ρ} [ForIn Id ρ α] (t : DTreeMap α β cmp) (l : ρ) : DTreeMap α β cmp :=
-  letI : Ord α := ⟨cmp⟩; ⟨t.inner.eraseMany l t.wf.balanced, t.wf.eraseMany⟩
+  letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
+  ⟨t.inner.eraseMany l t.wf.balanced, t.wf.eraseMany⟩
 
 namespace Const
 
@@ -1135,7 +1178,9 @@ variable {β : Type v}
 
 @[inline, inherit_doc DTreeMap.insertMany]
 def insertMany {ρ} [ForIn Id ρ (α × β)] (t : DTreeMap α β cmp) (l : ρ) : DTreeMap α β cmp :=
-  letI : Ord α := ⟨cmp⟩; ⟨Impl.Const.insertMany t.inner l t.wf.balanced, t.wf.constInsertMany⟩
+  letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
+  ⟨Impl.Const.insertMany t.inner l t.wf.balanced, t.wf.constInsertMany⟩
 
 /--
 Inserts multiple elements into the tree map by iterating over the given collection and calling
@@ -1143,7 +1188,8 @@ Inserts multiple elements into the tree map by iterating over the given collecti
 -/
 @[inline]
 def insertManyIfNewUnit {ρ} [ForIn Id ρ α] (t : DTreeMap α Unit cmp) (l : ρ) : DTreeMap α Unit cmp :=
-  letI : Ord α := ⟨cmp⟩;
+  letI : Ord α := ⟨cmp⟩
+  letI := Comparable.ofOrd α
   ⟨Impl.Const.insertManyIfNewUnit t.inner l t.wf.balanced, t.wf.constInsertManyIfNewUnit⟩
 
 end Const

src/Std/Data/DTreeMap/Internal/Model.lean

@@ -1007,28 +1007,28 @@ theorem getEntryLT?.eq_go [Ord α] (k : α) (x) (t : Impl α β) :
     simp only [go, Option.none_or, *]
   case _ ih _ => rw [← ih, Option.or_assoc, Option.some_or]
 
-theorem some_getEntryGE_eq_getEntryGE? [Ord α] [TransOrd α] (k : α) (t : Impl α β) {ho he} :
+theorem some_getEntryGE_eq_getEntryGE? [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] (k : α) (t : Impl α β) {ho he} :
     some (getEntryGE k t ho he) = getEntryGE? k t := by
   rw [getEntryGE?]; apply of_eq_true
   induction t, none using tree_split_ind (compare k) <;>
     simp only [*, getEntryGE?.go, getEntryGE, getEntryGED, ← Option.or_some,
       getEntryGE?.eq_go] <;> contradiction
 
-theorem some_getEntryGT_eq_getEntryGT? [Ord α] [TransOrd α] (k : α) (t : Impl α β) {ho he} :
+theorem some_getEntryGT_eq_getEntryGT? [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] (k : α) (t : Impl α β) {ho he} :
     some (getEntryGT k t ho he) = getEntryGT? k t := by
   rw [getEntryGT?]; apply of_eq_true
   induction t, none using tree_split_ind (compare k) <;>
     simp only [*, getEntryGT?.go, getEntryGT, getEntryGTD, ← Option.or_some,
       getEntryGT?.eq_go, ↓reduceDIte, reduceCtorEq] <;> contradiction
 
-theorem some_getEntryLE_eq_getEntryLE? [Ord α] [TransOrd α] (k : α) (t : Impl α β) {ho he} :
+theorem some_getEntryLE_eq_getEntryLE? [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] (k : α) (t : Impl α β) {ho he} :
     some (getEntryLE k t ho he) = getEntryLE? k t := by
   rw [getEntryLE?]; apply of_eq_true
   induction t, none using tree_split_ind (compare k) <;>
     simp only [*, getEntryLE?.go, getEntryLE, getEntryLED, ← Option.or_some,
       getEntryLE?.eq_go] <;> contradiction
 
-theorem some_getEntryLT_eq_getEntryLT? [Ord α] [TransOrd α] (k : α) (t : Impl α β) {ho he} :
+theorem some_getEntryLT_eq_getEntryLT? [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] (k : α) (t : Impl α β) {ho he} :
     some (getEntryLT k t ho he) = getEntryLT? k t := by
   rw [getEntryLT?]; apply of_eq_true
   induction t, none using tree_split_ind (compare k) <;>
@@ -1083,14 +1083,14 @@ theorem getKeyLED_eq_getD_getKeyLE? [Ord α] {t : Impl α β} {k fallback : α}
 theorem getKeyLTD_eq_getD_getKeyLT? [Ord α] {t : Impl α β} {k fallback : α} :
     t.getKeyLTD k fallback = (t.getKeyLT? k).getD fallback := rfl
 
-theorem getKeyGE_eq_getEntryGE [Ord α] [TransOrd α] {t : Impl α β} {k : α} {hto he} :
+theorem getKeyGE_eq_getEntryGE [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] {t : Impl α β} {k : α} {hto he} :
     getKeyGE k t hto he = (getEntryGE k t hto he).1 := by
   induction t using tree_split_ind_no_gen (compare k) <;> simp only [getKeyGE, getEntryGE, *]
   · contradiction
   · rw [getKeyGED, getEntryGED, getKeyGE?_eq_getEntryGE?]; symm
     exact (Option.getD_map _ _ _).symm
 
-theorem getKeyGT_eq_getEntryGT [Ord α] [TransOrd α] {t : Impl α β} {k : α} {hto he} :
+theorem getKeyGT_eq_getEntryGT [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] {t : Impl α β} {k : α} {hto he} :
     getKeyGT k t hto he = (getEntryGT k t hto he).1 := by
   induction t using tree_split_ind_no_gen (compare k) <;>
     simp only [getKeyGT, getEntryGT, *, ↓reduceDIte, reduceCtorEq]
@@ -1098,14 +1098,14 @@ theorem getKeyGT_eq_getEntryGT [Ord α] [TransOrd α] {t : Impl α β} {k : α}
   · rw [getKeyGTD, getEntryGTD, getKeyGT?_eq_getEntryGT?]; symm
     exact (Option.getD_map _ _ _).symm
 
-theorem getKeyLE_eq_getEntryLE [Ord α] [TransOrd α] {t : Impl α β} {k : α} {hto he} :
+theorem getKeyLE_eq_getEntryLE [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] {t : Impl α β} {k : α} {hto he} :
     getKeyLE k t hto he = (getEntryLE k t hto he).1 := by
   induction t using tree_split_ind_no_gen (compare k) <;> simp only [getKeyLE, getEntryLE, *]
   · contradiction
   · rw [getKeyLED, getEntryLED, getKeyLE?_eq_getEntryLE?]; symm
     exact (Option.getD_map _ _ _).symm
 
-theorem getKeyLT_eq_getEntryLT [Ord α] [TransOrd α] {t : Impl α β} {k : α} {hto he} :
+theorem getKeyLT_eq_getEntryLT [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] {t : Impl α β} {k : α} {hto he} :
     getKeyLT k t hto he = (getEntryLT k t hto he).1 := by
   induction t using tree_split_ind_no_gen (compare k) <;>
     simp only [getKeyLT, getEntryLT, *, ↓reduceDIte, reduceCtorEq]
@@ -1181,7 +1181,7 @@ theorem getEntryLED_eq_getD_getEntryLE? [Ord α] {t : Impl α fun _ => β} {k :
 theorem getEntryLTD_eq_getD_getEntryLT? [Ord α] {t : Impl α fun _ => β} {k : α} {fallback : α × β} :
     getEntryLTD k t fallback = (getEntryLT? k t).getD fallback := rfl
 
-theorem getEntryGE_eq [Ord α] [TransOrd α] {t : Impl α fun _ => β} (hto : t.Ordered) {k : α} (he) :
+theorem getEntryGE_eq [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] {t : Impl α fun _ => β} (hto : t.Ordered) {k : α} (he) :
     getEntryGE k t hto he = (letI e := Impl.getEntryGE k t hto he; (e.1, e.2)) := by
   induction t using tree_split_ind_no_gen (compare k) <;> simp only [getEntryGE, Impl.getEntryGE, *]
   · contradiction
@@ -1189,7 +1189,7 @@ theorem getEntryGE_eq [Ord α] [TransOrd α] {t : Impl α fun _ => β} (hto : t.
     rw [getEntryGED, Impl.getEntryGED, getEntryGE?_eq_map]
     exact Option.getD_map (fun x => (x.1, x.2)) ⟨_, _⟩ (Impl.getEntryGE? k l)
 
-theorem getEntryGT_eq [Ord α] [TransOrd α] {t : Impl α fun _ => β} (hto : t.Ordered) {k : α} (he) :
+theorem getEntryGT_eq [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] {t : Impl α fun _ => β} (hto : t.Ordered) {k : α} (he) :
     getEntryGT k t hto he = (letI e := Impl.getEntryGT k t hto he; (e.1, e.2)) := by
   induction t using tree_split_ind_no_gen (compare k) <;>
     simp only [getEntryGT, Impl.getEntryGT, *, ↓reduceDIte, reduceCtorEq]
@@ -1198,7 +1198,7 @@ theorem getEntryGT_eq [Ord α] [TransOrd α] {t : Impl α fun _ => β} (hto : t.
     rw [getEntryGTD, Impl.getEntryGTD, getEntryGT?_eq_map]
     exact Option.getD_map (fun x => (x.1, x.2)) ⟨_, _⟩ (Impl.getEntryGT? k l)
 
-theorem getEntryLE_eq [Ord α] [TransOrd α] {t : Impl α fun _ => β} (hto : t.Ordered) {k : α} (he) :
+theorem getEntryLE_eq [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] {t : Impl α fun _ => β} (hto : t.Ordered) {k : α} (he) :
     getEntryLE k t hto he = (letI e := Impl.getEntryLE k t hto he; (e.1, e.2)) := by
   induction t using tree_split_ind_no_gen (compare k) <;> simp only [getEntryLE, Impl.getEntryLE, *]
   · contradiction
@@ -1206,7 +1206,7 @@ theorem getEntryLE_eq [Ord α] [TransOrd α] {t : Impl α fun _ => β} (hto : t.
     rw [getEntryLED, Impl.getEntryLED, getEntryLE?_eq_map]
     exact Option.getD_map (fun x => (x.1, x.2)) ⟨_, _⟩ (Impl.getEntryLE? k r)
 
-theorem getEntryLT_eq [Ord α] [TransOrd α] {t : Impl α fun _ => β} (hto : t.Ordered) {k : α} (he) :
+theorem getEntryLT_eq [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] {t : Impl α fun _ => β} (hto : t.Ordered) {k : α} (he) :
     getEntryLT k t hto he = (letI e := Impl.getEntryLT k t hto he; (e.1, e.2)) := by
   induction t using tree_split_ind_no_gen (compare k) <;>
     simp only [getEntryLT, Impl.getEntryLT, *, ↓reduceDIte, reduceCtorEq]

src/Std/Data/DTreeMap/Internal/Ordered.lean

@@ -7,6 +7,7 @@ prelude
 import Std.Classes.Ord.Basic
 import Std.Data.DTreeMap.Internal.Def
 import Std.Data.Internal.Cut
+import Std.Classes.Ord.New.LinearPreorder
 
 /-!
 # `Ordered` predicate
@@ -26,45 +27,47 @@ namespace Std.DTreeMap.Internal.Impl
 open Std.Internal
 
 /-- Implementation detail of the tree map -/
-def Ordered [Ord α] (t : Impl α β) : Prop :=
-  t.toListModel.Pairwise (fun a b => compare a.1 b.1 = .lt)
+def Ordered [LT α] (t : Impl α β) : Prop :=
+  t.toListModel.Pairwise (fun a b => a.1 < b.1)
 
 /-!
 ## Lemmas about the `Ordered` predicate
 -/
 
-theorem Ordered.left [Ord α] {sz k v l r} (h : (.inner sz k v l r : Impl α β).Ordered) :
+theorem Ordered.left [LT α] {sz k v l r} (h : (.inner sz k v l r : Impl α β).Ordered) :
     l.Ordered :=
   h.sublist (by simp)
 
-theorem Ordered.right [Ord α] {sz k v l r} (h : (.inner sz k v l r : Impl α β).Ordered) :
+theorem Ordered.right [LT α] {sz k v l r} (h : (.inner sz k v l r : Impl α β).Ordered) :
     r.Ordered :=
   h.sublist (by simp)
 
-theorem Ordered.compare_left [Ord α] {sz k v l r} (h : (.inner sz k v l r : Impl α β).Ordered)
-    {k'} (hk' : k' ∈ l.toListModel) : compare k'.1 k = .lt :=
+theorem Ordered.gt_left [LT α] {sz k v l r} (h : (.inner sz k v l r : Impl α β).Ordered)
+    {k'} (hk' : k' ∈ l.toListModel) : k'.1 < k :=
   h.rel_of_mem_append hk' List.mem_cons_self
 
-theorem Ordered.compare_left_beq_gt [Ord α] [TransOrd α] {k : α → Ordering} [IsStrictCut compare k]
+theorem Ordered.compare_left_beq_gt [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α]
+    {k : α → Ordering} [IsStrictCut k]
     {sz k' v' l r} (ho : (.inner sz k' v' l r : Impl α β).Ordered) (hcmp : (k k').isGE)
     (p) (hp : p ∈ l.toListModel) : k p.1 == .gt :=
- beq_iff_eq.2 (IsStrictCut.gt_of_isGE_of_gt hcmp (OrientedCmp.gt_of_lt (ho.compare_left hp)))
+  beq_iff_eq.2 (IsStrictCut.gt_of_isGE_of_gt hcmp (ho.gt_left hp))
 
-theorem Ordered.compare_left_not_beq_eq [Ord α] [TransOrd α] {k : α → Ordering}
-    [IsStrictCut compare k] {sz k' v' l r}
+theorem Ordered.compare_left_not_beq_eq [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α]
+    {k : α → Ordering}
+    [IsStrictCut k] {sz k' v' l r}
     (ho : (.inner sz k' v' l r : Impl α β).Ordered) (hcmp : (k k').isGE)
     (p) (hp : p ∈ l.toListModel) : ¬(k p.1 == .eq) := by
   suffices k p.fst = .gt by simp [this]
-  exact IsStrictCut.gt_of_isGE_of_gt hcmp (OrientedCmp.gt_of_lt (ho.compare_left hp))
+  exact IsStrictCut.gt_of_isGE_of_gt hcmp (ho.gt_left hp)
 
-theorem Ordered.compare_right [Ord α] {sz k v l r}
+theorem Ordered.lt_right [LT α] {sz k v l r}
     (h : (.inner sz k v l r : Impl α β).Ordered) {k'} (hk' : k' ∈ r.toListModel) :
-    compare k k'.1 = .lt := by
+    k < k'.1 := by
   exact List.rel_of_pairwise_cons (h.sublist (List.sublist_append_right _ _)) hk'
 
-theorem Ordered.compare_right_not_beq_gt [Ord α] [TransOrd α] {k : α → Ordering}
-    [IsStrictCut compare k] {sz k' v' l r}
+theorem Ordered.compare_right_not_beq_gt [Ord α] [Comparable α] [LawfulOrd α] [LawfulComparable α]
+    {k : α → Ordering} [IsStrictCut k] {sz k' v' l r}
     (ho : (.inner sz k' v' l r : Impl α β).Ordered) (hcmp : (k k').isLE)
     (p) (hp : p ∈ r.toListModel) : ¬(k p.1 == .gt) := by
   suffices k p.fst = .lt by simp [this]
-  exact IsStrictCut.lt_of_isLE_of_lt hcmp (ho.compare_right hp)
+  exact IsStrictCut.lt_of_isLE_of_lt hcmp (ho.lt_right hp)

src/Std/Data/DTreeMap/Internal/Queries.lean

@@ -538,7 +538,7 @@ def getEntryLTD [Ord α] (k : α) (t : Impl α β) (fallback : (a : α) × β a)
   t.getEntryLT? k |>.getD fallback
 
 /-- Implementation detail of the tree map -/
-def getEntryGE [Ord α] [TransOrd α] (k : α) :
+def getEntryGE [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] (k : α) :
     (t : Impl α β) → (ho : t.Ordered) → (he : ∃ a ∈ t, (compare a k).isGE) → (a : α) × β a
   | .leaf, _, he => False.elim <| by obtain ⟨_, ha, _⟩ := he; cases ha
   | .inner _ ky y l r, ho, he => match hkky : compare k ky with
@@ -551,7 +551,7 @@ def getEntryGE [Ord α] [TransOrd α] (k : α) :
       exact TransCmp.gt_of_isGE_of_gt hc hkky
 
 /-- Implementation detail of the tree map -/
-def getEntryGT [Ord α] [TransOrd α] (k : α) :
+def getEntryGT [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] (k : α) :
     (t : Impl α β) → (ho : t.Ordered) → (he : ∃ a ∈ t, compare a k = .gt) → (a : α) × β a
   | .leaf, _, he => False.elim <| by obtain ⟨_, ha, _⟩ := he; cases ha
   | .inner _ ky y l r, ho, he => if hkky : compare k ky = .lt then
@@ -565,7 +565,7 @@ def getEntryGT [Ord α] [TransOrd α] (k : α) :
           simpa [← Ordering.isGE_eq_false, Bool.not_eq_false] using hkky
 
 /-- Implementation detail of the tree map -/
-def getEntryLE [Ord α] [TransOrd α] (k : α) :
+def getEntryLE [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] (k : α) :
     (t : Impl α β) → (ho : t.Ordered) → (he : ∃ a ∈ t, (compare a k).isLE) → (a : α) × β a
   | .leaf, _, he => False.elim <| by obtain ⟨_, ha, _⟩ := he; cases ha
   | .inner _ ky y l r, ho, he => match hkky : compare k ky with
@@ -578,7 +578,7 @@ def getEntryLE [Ord α] [TransOrd α] (k : α) :
       exact TransCmp.lt_of_isLE_of_lt hc hkky
 
 /-- Implementation detail of the tree map -/
-def getEntryLT [Ord α] [TransOrd α] (k : α) :
+def getEntryLT [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α](k : α) :
     (t : Impl α β) → (ho : t.Ordered) → (he : ∃ a ∈ t, compare a k = .lt) → (a : α) × β a
   | .leaf, _, he => False.elim <| by obtain ⟨_, ha, _⟩ := he; cases ha
   | .inner _ ky y l r, ho, he => if hkky : compare k ky = .gt then
@@ -678,7 +678,7 @@ def getKeyLTD [Ord α] (k : α) (t : Impl α β) (fallback : α) : α :=
   t.getKeyLT? k |>.getD fallback
 
 /-- Implementation detail of the tree map -/
-def getKeyGE [Ord α] [TransOrd α] (k : α) :
+def getKeyGE [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] (k : α) :
     (t : Impl α β) → (ho : t.Ordered) → (he : ∃ a ∈ t, (compare a k).isGE) → α
   | .leaf, _, he => False.elim <| by obtain ⟨_, ha, _⟩ := he; cases ha
   | .inner _ ky y l r, ho, he => match hkky : compare k ky with
@@ -691,7 +691,7 @@ def getKeyGE [Ord α] [TransOrd α] (k : α) :
       exact TransCmp.gt_of_isGE_of_gt hc hkky
 
 /-- Implementation detail of the tree map -/
-def getKeyGT [Ord α] [TransOrd α] (k : α) :
+def getKeyGT [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] (k : α) :
     (t : Impl α β) → (ho : t.Ordered) → (he : ∃ a ∈ t, compare a k = .gt) → α
   | .leaf, _, he => False.elim <| by obtain ⟨_, ha, _⟩ := he; cases ha
   | .inner _ ky y l r, ho, he => if hkky : compare k ky = .lt then
@@ -705,7 +705,7 @@ def getKeyGT [Ord α] [TransOrd α] (k : α) :
           simpa [← Ordering.isGE_eq_false, Bool.not_eq_false] using hkky
 
 /-- Implementation detail of the tree map -/
-def getKeyLE [Ord α] [TransOrd α] (k : α) :
+def getKeyLE [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] (k : α) :
     (t : Impl α β) → (ho : t.Ordered) → (he : ∃ a ∈ t, (compare a k).isLE) → α
   | .leaf, _, he => False.elim <| by obtain ⟨_, ha, _⟩ := he; cases ha
   | .inner _ ky y l r, ho, he => match hkky : compare k ky with
@@ -718,7 +718,7 @@ def getKeyLE [Ord α] [TransOrd α] (k : α) :
       exact TransCmp.lt_of_isLE_of_lt hc hkky
 
 /-- Implementation detail of the tree map -/
-def getKeyLT [Ord α] [TransOrd α] (k : α) :
+def getKeyLT [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] (k : α) :
     (t : Impl α β) → (ho : t.Ordered) → (he : ∃ a ∈ t, compare a k = .lt) → α
   | .leaf, _, he => False.elim <| by obtain ⟨_, ha, _⟩ := he; cases ha
   | .inner _ ky y l r, ho, he => if hkky : compare k ky = .gt then
@@ -905,7 +905,7 @@ def getEntryLTD [Ord α] (k : α) (t : Impl α β) (fallback : α × β) : α ×
   getEntryLT? k t |>.getD fallback
 
 /-- Implementation detail of the tree map -/
-def getEntryGE [Ord α] [TransOrd α] (k : α) :
+def getEntryGE [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] (k : α) :
     (t : Impl α β) → (ho : t.Ordered) → (he : ∃ a ∈ t, (compare a k).isGE) → α × β
   | .leaf, _, he => False.elim <| by obtain ⟨_, ha, _⟩ := he; cases ha
   | .inner _ ky y l r, ho, he => match hkky : compare k ky with
@@ -918,7 +918,7 @@ def getEntryGE [Ord α] [TransOrd α] (k : α) :
       exact TransCmp.gt_of_isGE_of_gt hc hkky
 
 /-- Implementation detail of the tree map -/
-def getEntryGT [Ord α] [TransOrd α] (k : α) :
+def getEntryGT [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] (k : α) :
     (t : Impl α β) → (ho : t.Ordered) → (he : ∃ a ∈ t, compare a k = .gt) → α × β
   | .leaf, _, he => False.elim <| by obtain ⟨_, ha, _⟩ := he; cases ha
   | .inner _ ky y l r, ho, he => if hkky : compare k ky = .lt then
@@ -932,7 +932,7 @@ def getEntryGT [Ord α] [TransOrd α] (k : α) :
           simpa [← Ordering.isGE_eq_false, Bool.not_eq_false] using hkky
 
 /-- Implementation detail of the tree map -/
-def getEntryLE [Ord α] [TransOrd α] (k : α) :
+def getEntryLE [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] (k : α) :
     (t : Impl α β) → (ho : t.Ordered) → (he : ∃ a ∈ t, (compare a k).isLE) → α × β
   | .leaf, _, he => False.elim <| by obtain ⟨_, ha, _⟩ := he; cases ha
   | .inner _ ky y l r, ho, he => match hkky : compare k ky with
@@ -945,7 +945,7 @@ def getEntryLE [Ord α] [TransOrd α] (k : α) :
       exact TransCmp.lt_of_isLE_of_lt hc hkky
 
 /-- Implementation detail of the tree map -/
-def getEntryLT [Ord α] [TransOrd α] (k : α) :
+def getEntryLT [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] (k : α) :
     (t : Impl α β) → (ho : t.Ordered) → (he : ∃ a ∈ t, compare a k = .lt) → α × β
   | .leaf, _, he => False.elim <| by obtain ⟨_, ha, _⟩ := he; cases ha
   | .inner _ ky y l r, ho, he => if hkky : compare k ky = .gt then

src/Std/Data/DTreeMap/Internal/WF/Defs.lean

@@ -5,6 +5,7 @@ Authors: Markus Himmel, Paul Reichert
 -/
 prelude
 import Std.Data.DTreeMap.Internal.Operations
+import Std.Classes.Ord.New.LinearPreorder
 
 /-!
 # Well-formedness predicate on size-bounded trees
@@ -28,9 +29,9 @@ namespace Std.DTreeMap.Internal
 namespace Impl
 
 /-- Well-formedness of tree maps. -/
-inductive WF [Ord α] : {β : α → Type v} → Impl α β → Prop where
+inductive WF [Ord α] [Comparable α] : {β : α → Type v} → Impl α β → Prop where
   /-- This is the actual well-formedness invariant: the tree must be a balanced BST. -/
-  | wf {t} : Balanced t → (∀ [TransOrd α], Ordered t) → WF t
+  | wf {t} : Balanced t → (∀ [LawfulLinearPreorder α], Ordered t) → WF t
   /-- The empty tree is well-formed. Later shown to be subsumed by `.wf`. -/
   | empty : WF .empty
   /-- `insert` preserves well-formedness. Later shown to be subsumed by `.wf`. -/
@@ -62,30 +63,31 @@ inductive WF [Ord α] : {β : α → Type v} → Impl α β → Prop where
 A well-formed tree is balanced. This is needed here already because we need to know that the
 tree is balanced to call the optimized modification functions.
 -/
-theorem WF.balanced [Ord α] {t : Impl α β} (h : WF t) : t.Balanced := by
+theorem WF.balanced [Ord α] [Comparable α] {t : Impl α β} (h : WF t) : t.Balanced := by
   induction h <;> (try apply SizedBalancedTree.balanced_impl) <;> try apply BalancedTree.balanced_impl
   case wf htb hto => exact htb
   case empty => exact balanced_empty
   case modify ih => exact balanced_modify ih
   case constModify ih => exact Const.balanced_modify ih
 
-theorem WF.eraseMany [Ord α] {ρ} [ForIn Id ρ α] {t : Impl α β} {l : ρ} {h} (hwf : WF t) :
-    WF (t.eraseMany l h).val :=
+theorem WF.eraseMany [Ord α] [Comparable α] {ρ} [ForIn Id ρ α] {t : Impl α β} {l : ρ} {h}
+    (hwf : WF t) : WF (t.eraseMany l h).val :=
   (t.eraseMany l h).2 hwf fun _ _ _ hwf' => hwf'.erase
 
-theorem WF.insertMany [Ord α] {ρ} [ForIn Id ρ ((a : α) × β a)] {t : Impl α β} {l : ρ} {h} (hwf : WF t) :
-    WF (t.insertMany l h).val :=
+theorem WF.insertMany [Ord α] [Comparable α] {ρ} [ForIn Id ρ ((a : α) × β a)] {t : Impl α β} {l : ρ}
+    {h} (hwf : WF t) : WF (t.insertMany l h).val :=
   (t.insertMany l h).2 hwf fun _ _ _ _ hwf' => hwf'.insert
 
-theorem WF.constInsertMany [Ord α] {β : Type v} {ρ} [ForIn Id ρ (α × β)] {t : Impl α (fun _ => β)}
-    {l : ρ} {h} (hwf : WF t) : WF (Impl.Const.insertMany t l h).val :=
+theorem WF.constInsertMany [Ord α] [Comparable α] {β : Type v} {ρ} [ForIn Id ρ (α × β)]
+    {t : Impl α (fun _ => β)} {l : ρ} {h} (hwf : WF t) : WF (Impl.Const.insertMany t l h).val :=
   (Impl.Const.insertMany t l h).2 hwf fun _ _ _ _ hwf' => hwf'.insert
 
-theorem WF.constInsertManyIfNewUnit [Ord α] {ρ} [ForIn Id ρ α] {t : Impl α (fun _ => Unit)} {l : ρ}
-    {h} (hwf : WF t) : WF (Impl.Const.insertManyIfNewUnit t l h).val :=
+theorem WF.constInsertManyIfNewUnit [Ord α] [Comparable α] {ρ} [ForIn Id ρ α]
+    {t : Impl α (fun _ => Unit)} {l : ρ} {h}
+    (hwf : WF t) : WF (Impl.Const.insertManyIfNewUnit t l h).val :=
   (Impl.Const.insertManyIfNewUnit t l h).2 hwf fun _ _ _ hwf' => hwf'.insertIfNew
 
-theorem WF.getThenInsertIfNew? [Ord α] [LawfulEqOrd α] {t : Impl α β} {k v} {h : t.WF} :
+theorem WF.getThenInsertIfNew? [Ord α] [Comparable α] [LawfulEqOrd α] {t : Impl α β} {k v} {h : t.WF} :
     (t.getThenInsertIfNew? k v h.balanced).2.WF := by
   simp only [Impl.getThenInsertIfNew?]
   split
@@ -96,7 +98,7 @@ section Const
 
 variable {β : Type v}
 
-theorem WF.constGetThenInsertIfNew? [Ord α] {t : Impl α β} {k v} {h : t.WF} :
+theorem WF.constGetThenInsertIfNew? [Ord α] [Comparable α] {t : Impl α β} {k v} {h : t.WF} :
     (Impl.Const.getThenInsertIfNew? t k v h.balanced).2.WF := by
   simp only [Impl.Const.getThenInsertIfNew?]
   split

src/Std/Data/DTreeMap/Raw/Basic.lean

@@ -79,9 +79,10 @@ implementation details and should not be accessed by users.
 -/
 structure WF (t : Raw α β cmp) where
   /-- Internal implementation detail of the tree map. -/
-  out : letI : Ord α := ⟨cmp⟩; t.inner.WF
+  out : letI : Ord α := ⟨cmp⟩; letI := Comparable.ofOrd α; t.inner.WF
 
-instance {t : Raw α β cmp} : Coe t.WF (letI : Ord α := ⟨cmp⟩; t.inner.WF) where
+instance {t : Raw α β cmp} :
+    Coe t.WF (letI : Ord α := ⟨cmp⟩; letI := Comparable.ofOrd α; t.inner.WF) where
   coe h := h.out
 
 @[inline, inherit_doc DTreeMap.empty]

src/Std/Data/Internal/Cut.lean

@@ -5,6 +5,7 @@ Authors: Markus Himmel
 -/
 prelude
 import Std.Classes.Ord.Basic
+import Std.Classes.Ord.New.LinearPreorder
 
 set_option autoImplicit false
 
@@ -12,47 +13,54 @@ universe u
 
 namespace Std.Internal
 
-class IsCut {α : Type u} (cmp : α → α → Ordering) (cut : α → Ordering) where
-  lt {k k'} : cut k' = .lt → cmp k' k = .lt → cut k = .lt
-  gt {k k'} : cut k' = .gt → cmp k' k = .gt → cut k = .gt
+class IsCut {α : Type u} [Comparable α] (cut : α → Ordering) where
+  lt {k k'} : cut k' = .lt → k' < k → cut k = .lt
+  gt {k k'} : cut k' = .gt → k < k' → cut k = .gt
 
-class IsStrictCut {α : Type u} (cmp : α → α → Ordering) (cut : α → Ordering) extends IsCut cmp cut where
-  eq (k) {k'} : cut k' = .eq → cut k = cmp k' k
+-- TODO: It is not nice that we need an `Ord` instance here
+class IsStrictCut {α : Type u} [Ord α] [Comparable α] (cut : α → Ordering) extends IsCut cut where
+  eq (k) {k'} : cut k' = .eq → cut k = compare k' k
 
 variable {α : Type u} {cmp : α → α → Ordering} {cut : α → Ordering}
 
-theorem IsStrictCut.gt_of_isGE_of_gt [IsStrictCut cmp cut] {k k' : α} :
-    (cut k').isGE → cmp k' k = .gt → cut k = .gt := by
+theorem IsStrictCut.gt_of_isGE_of_gt [Ord α] [Comparable α] [LawfulOrd α]
+    [LawfulOrientedComparable α] [IsStrictCut cut] {k k' : α} :
+    (cut k').isGE → k < k' → cut k = .gt := by
   cases h₁ : cut k' with
   | lt => rintro ⟨⟩
   | gt => exact fun _ => IsCut.gt h₁
-  | eq => exact fun h₂ h₃ => by rw [← h₃, IsStrictCut.eq (cmp := cmp) k h₁]
+  | eq => exact fun h₂ h₃ => by simp [IsStrictCut.eq k h₁, Comparable.compare_eq_gt_iff_gt, h₃]
 
-theorem IsStrictCut.lt_of_isLE_of_lt [IsStrictCut cmp cut] {k k' : α} :
-    (cut k').isLE → cmp k' k = .lt → cut k = .lt := by
+theorem IsStrictCut.lt_of_isLE_of_lt [Ord α] [Comparable α] [LawfulOrd α] [LawfulComparable α]
+    [IsStrictCut cut] {k k' : α} :
+    (cut k').isLE → k' < k → cut k = .lt := by
   cases h₁ : cut k' with
   | gt => rintro ⟨⟩
   | lt => exact fun _ => IsCut.lt h₁
-  | eq => exact fun h₂ h₃ => by rw [← h₃, IsStrictCut.eq (cmp := cmp) k h₁]
+  | eq => exact fun h₂ h₃ => by simp [IsStrictCut.eq k h₁, Comparable.compare_eq_lt_iff_lt, h₃]
 
-instance [Ord α] [TransOrd α] {k : α} : IsStrictCut compare (compare k) where
-  lt := TransCmp.lt_trans
-  gt h₁ h₂ := OrientedCmp.gt_of_lt (TransCmp.lt_trans (OrientedCmp.lt_of_gt h₂)
-    (OrientedCmp.lt_of_gt h₁))
+instance {_ : Ord α} [Comparable α] [LawfulLinearPreorder α] [LawfulOrd α] {k : α} :
+    IsStrictCut (compare k) where
+  lt h₁ h₂ := by
+    simp only [Comparable.compare_eq_lt_iff_lt] at ⊢ h₁
+    exact Trans.trans h₁ h₂
+  gt h₁ h₂ := by
+    simp only [Comparable.compare_eq_gt_iff_gt] at ⊢ h₁
+    exact Trans.trans h₂ h₁
   eq _ _ := TransCmp.congr_left
 
-instance [Ord α] : IsStrictCut (compare : α → α → Ordering) (fun _ => .lt) where
+instance [Ord α] [Comparable α] : IsStrictCut (fun _ : α => .lt) where
   lt := by simp
   gt := by simp
   eq := by simp
 
-instance [Ord α] [TransOrd α] {k : α} : IsStrictCut compare fun k' => (compare k k').then .gt where
-  lt {_ _} := by simpa [Ordering.then_eq_lt] using TransCmp.lt_trans
+instance [Ord α] [Comparable α] [LawfulOrd α] [LawfulLinearPreorder α] {k : α} :
+    IsStrictCut fun k' => (compare k k').then .gt where
+  lt {_ _} := by simpa [Ordering.then_eq_lt, Comparable.compare_eq_lt_iff_lt] using Trans.trans
   eq {_ _} := by simp [Ordering.then_eq_eq]
-  gt h h' := by
-    simp only [Ordering.then_eq_gt, and_true] at h ⊢
-    rcases h with (h | h)
-    · exact .inl (TransCmp.gt_trans h h')
-    · exact .inl (TransCmp.gt_of_eq_of_gt h h')
+  gt {_ _} := by
+    simp [Ordering.then_eq_gt, ← Ordering.isGE_iff_eq_gt_or_eq_eq, ← Comparable.compare_eq_gt_iff_gt]
+    intro h₁ h₂
+    exact TransOrd.isGE_trans h₁ (Ordering.isGE_of_eq_gt h₂)
 
 end Std.Internal

src/Std/Data/Internal/List/Associative.lean

@@ -1895,7 +1895,7 @@ theorem Const.keys_filter [BEq α] [EquivBEq α] {β : Type v}
     rw [List.filter_cons]
     specialize ih hl.tail
     replace hl := hl.containsKey_eq_false
-    simp only [keys_cons, List.attach_cons, getValue_cons, ↓reduceDIte, 
+    simp only [keys_cons, List.attach_cons, getValue_cons, ↓reduceDIte,
       List.filter_cons, BEq.rfl, List.filter_map, Function.comp_def]
     have (x : { x // x ∈ keys tl }) : (k == x.val) = False := eq_false <| by
       intro h
@@ -3413,7 +3413,7 @@ theorem length_insertListIfNewUnit [BEq α] [EquivBEq α]
     rw [ih]
     · rw [length_insertEntryIfNew]
       specialize distinct_both hd
-      simp only [List.contains_cons, BEq.rfl, Bool.true_or, 
+      simp only [List.contains_cons, BEq.rfl, Bool.true_or,
         ] at distinct_both
       cases eq : containsKey hd l with
       | true => simp [eq] at distinct_both
@@ -3424,7 +3424,7 @@ theorem length_insertListIfNewUnit [BEq α] [EquivBEq α]
     · simp only [pairwise_cons] at distinct_toInsert
       apply And.right distinct_toInsert
     · intro a
-      simp only [List.contains_cons, 
+      simp only [List.contains_cons,
         ] at distinct_both
       rw [containsKey_insertEntryIfNew]
       simp only [Bool.or_eq_true]
@@ -3969,7 +3969,7 @@ theorem getValue!_alterKey [EquivBEq α] {k k' : α} [Inhabited β] {f : Option
         (f (getValue? k l)).get!
       else
         getValue! k' l := by
-  simp only [hl, getValue!_eq_getValue?, getValue?_alterKey, 
+  simp only [hl, getValue!_eq_getValue?, getValue?_alterKey,
     apply_ite Option.get!]
 
 theorem getValueD_alterKey [EquivBEq α] {k k' : α} {fallback : β} {f : Option β → Option β}
@@ -3979,7 +3979,7 @@ theorem getValueD_alterKey [EquivBEq α] {k k' : α} {fallback : β} {f : Option
         f (getValue? k l) |>.getD fallback
       else
         getValueD k' l fallback := by
-  simp only [hl, getValueD_eq_getValue?, getValue?_alterKey, 
+  simp only [hl, getValueD_eq_getValue?, getValue?_alterKey,
     apply_ite (Option.getD · fallback)]
 
 theorem getKey?_alterKey [EquivBEq α] {k k' : α} {f : Option β → Option β} (l : List ((_ : α) × β))
@@ -5013,7 +5013,7 @@ theorem length_filter_eq_length_iff [BEq α] [LawfulBEq α] {f : (a : α) → β
     {l : List ((a : α) × β a)} (distinct : DistinctKeys l) :
     (l.filter fun p => f p.1 p.2).length = l.length ↔
       ∀ (a : α) (h : containsKey a l), (f a (getValueCast a l h)) = true := by
-  simp [← List.filterMap_eq_filter, 
+  simp [← List.filterMap_eq_filter,
     forall_mem_iff_forall_contains_getValueCast (p := fun a b => f a b = true) distinct]
 
 theorem length_filter_key_eq_length_iff [BEq α] [EquivBEq α] {f : α → Bool}
@@ -5205,7 +5205,7 @@ theorem getValue?_filter {β : Type v} [BEq α] [EquivBEq α]
     getValue? k (l.filter fun p => (f p.1 p.2)) =
       (getValue? k l).pfilter (fun v h =>
         f (getKey k l (containsKey_eq_isSome_getValue?.trans (Option.isSome_of_eq_some h))) v) := by
-  simp only [getValue?_eq_getEntry?, distinct, getEntry?_filter, 
+  simp only [getValue?_eq_getEntry?, distinct, getEntry?_filter,
     Option.pfilter_eq_pbind_ite, ← Option.bind_guard, Option.guard_def,
     Option.pbind_map, Option.map_bind, Function.comp_def, apply_ite,
     Option.map_some, Option.map_none]
@@ -5380,14 +5380,14 @@ theorem length_filter_eq_length_iff {β : Type v} [BEq α] [EquivBEq α]
     {f : (_ : α) → β → Bool} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) :
     (l.filter fun p => (f p.1 p.2)).length = l.length ↔
       ∀ (a : α) (h : containsKey a l), (f (getKey a l h) (getValue a l h)) = true := by
-  simp [← List.filterMap_eq_filter, Option.guard, 
+  simp [← List.filterMap_eq_filter, Option.guard,
     forall_mem_iff_forall_contains_getKey_getValue (p := fun a b => f a b = true) distinct]
 
 theorem length_filter_key_eq_length_iff {β : Type v} [BEq α] [EquivBEq α]
     {f : (_ : α) → Bool} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) :
     (l.filter fun p => f p.1).length = l.length ↔
       ∀ (a : α) (h : containsKey a l), f (getKey a l h)  = true := by
-  simp [← List.filterMap_eq_filter, 
+  simp [← List.filterMap_eq_filter,
     forall_mem_iff_forall_contains_getKey_getValue (p := fun a b => f a = true) distinct]
 
 theorem isEmpty_filterMap_eq_true [BEq α] [EquivBEq α] {β : Type v} {γ : Type w}