wip

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/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,272 @@
+module
+
+prelude
+public import Init.Core
+public import Std.Classes.Ord.Basic
+public import Std.Classes.Ord.New.BasicOperations
+
+public section
+
+abbrev PartialOrdering := Option Ordering
+
+def PartialOrdering.isLE : PartialOrdering → Bool
+  | none => false
+  | some o => o.isLE
+
+def PartialOrdering.isGE : PartialOrdering → Bool
+  | none => false
+  | some o => o.isGE
+
+@[ext]
+class PartiallyComparable (α : Type u) where
+  compare : α → α → PartialOrdering
+
+def PartiallyComparable.ofCmp {α : Type u} (cmp : α → α → Ordering) : PartiallyComparable α where
+  compare a b := some (cmp a b)
+
+abbrev PartiallyComparable.ofOrd (α : Type u) [Ord α] : PartiallyComparable α :=
+  .ofCmp Ord.compare
+
+open Classical in
+noncomputable def PartiallyComparable.ofLE (α : Type u) [LE α] : PartiallyComparable α where
+  compare a b :=
+    if a ≤ b then
+      if b ≤ a then some .eq else some .lt
+    else
+      if b ≤ a then some .gt else none
+
+open Classical in
+noncomputable def PartiallyComparable.ofLT (α : Type u) [LT α] : PartiallyComparable α where
+  compare a b := if a < b then some .lt else if b < a then some .gt else some .eq
+
+class LawfulOrientedPartiallyComparableLE {α : Type u} [LE α] (c : PartiallyComparable α) where
+  le_iff_compare_isLE : ∀ a b : α, a ≤ b ↔ (c.compare a b).isLE
+  ge_iff_compare_isGE : ∀ a b : α, b ≤ a ↔ (c.compare a b).isGE
+
+class LawfulOrientedPartiallyComparableLT {α : Type u} [LT α] (c : PartiallyComparable α) where
+  lt_iff_compare_eq_some_lt : ∀ a b : α, a < b ↔ c.compare a b = some .lt
+  gt_iff_compare_eq_some_gt : ∀ a b : α, b < a ↔ c.compare a b = some .gt
+
+class LawfulPartiallyComparableCmp {α : Type u} (c : PartiallyComparable α) (cmp : α → α → Ordering) where
+  compare_eq_some_compare : ∀ a b, c.compare a b = some (cmp a b)
+
+abbrev LawfulPartiallyComparableOrd {α : Type u} [Ord α] (c : PartiallyComparable α) :=
+  LawfulPartiallyComparableCmp c compare
+
+class LawfulPartiallyComparableBEq {α : Type u} [BEq α] (c : PartiallyComparable α) where
+  beq_iff_compare_eq_some_eq : ∀ a b : α, a == b ↔ c.compare a b = some .eq
+
+class LawfulTotallyComparable {α : Type u} (c : PartiallyComparable α) where
+  isSome_compare : ∀ a b, (c.compare a b).isSome
+
+class LawfulPreorder {α : Type u} (pc : PartiallyComparable α) where
+  le_trans : ∀ a b c : α, (pc.compare a b).isLE → (pc.compare b c).isLE → (pc.compare a c).isLE
+  le_refl : ∀ a : α, pc.compare a a = some .eq
+  gt_iff_lt : ∀ a b : α, pc.compare a b = some .gt ↔ pc.compare b a = some .lt
+
+class LawfulLinearPreorder {α : Type u} (pc : PartiallyComparable α) extends
+    LawfulPreorder pc, LawfulTotallyComparable pc
+
+instance (α : Type u) [Ord α] [LawfulLinearPreorder (.ofOrd α)] : Std.TransOrd α :=
+  sorry
+
+instance (α : Type u) [BEq α] [Ord α] [LawfulLinearPreorder (.ofOrd α)]
+    [LawfulPartiallyComparableBEq (.ofOrd α)] : EquivBEq α :=
+  sorry
+
+instance (α : Type u) [BEq α] [Ord α] [LawfulPartiallyComparableBEq (.ofOrd α)] :
+    Std.LawfulBEqOrd α :=
+  sorry
+
+instance (α : Type u) {_ : Ord α} [LawfulLinearPreorder (.ofOrd α)] :
+    haveI : Ord α := Ord.opposite inferInstance; LawfulLinearPreorder (.ofOrd α) :=
+  sorry
+
+class LawfulPartialOrder {α : Type u} (pc : PartiallyComparable α) extends LawfulPreorder pc where
+  le_antisymm : ∀ a b : α, pc.compare a b = some .eq → a = b
+
+class LawfulLinearOrder {α : Type u} (pc : PartiallyComparable α) extends
+    LawfulPartialOrder pc, LawfulLinearPreorder pc
+
+theorem LawfulPartiallyComparableCmp.eq_ofCmp {α : Type u} {cmp : α → α → Ordering} {c : PartiallyComparable α}
+    [i : LawfulPartiallyComparableCmp c cmp] :
+    c = .ofCmp cmp := by
+  ext a b
+  simp [PartiallyComparable.ofCmp, i.compare_eq_some_compare a b]
+
+theorem LawfulPartiallyComparableOrd.eq_ofOrd {α : Type u} [Ord α] {c : PartiallyComparable α}
+    [i : LawfulPartiallyComparableOrd c] :
+    c = .ofOrd α := by
+  simp [LawfulPartiallyComparableCmp.eq_ofCmp (cmp := compare)]
+
+instance (α : Type u) (cmp : α → α → Ordering) : LawfulPartiallyComparableCmp (.ofCmp cmp) cmp where
+  compare_eq_some_compare := fun _ _ => by rfl
+
+instance (α : Type u) [Ord α] : LawfulTotallyComparable (.ofOrd α) where
+  isSome_compare := by simp [PartiallyComparable.ofOrd, PartiallyComparable.ofCmp]
+
+instance (α : Type u) (cmp : α → α → Ordering) [LawfulPartialOrder (.ofCmp cmp)] :
+    Std.LawfulEqCmp cmp where
+  compare_self := by
+    intro a
+    have := LawfulPreorder.le_refl (pc := .ofCmp cmp) a
+    simpa [LawfulPartiallyComparableCmp.compare_eq_some_compare (cmp := cmp)] using this
+  eq_of_compare := by
+    intro a b
+    have := LawfulPartialOrder.le_antisymm (pc := .ofCmp cmp) a b
+    simpa [LawfulPartiallyComparableCmp.compare_eq_some_compare (cmp := cmp)] using this
+
+theorem LawfulOrientedPartiallyComparableLE.eq_ofLE {α : Type u} [LE α] {c : PartiallyComparable α}
+    [i : LawfulOrientedPartiallyComparableLE c] :
+    c = .ofLE α := by
+  ext a b
+  have hle := i.le_iff_compare_isLE a b
+  have hge := i.ge_iff_compare_isGE a b
+  simp only [PartiallyComparable.ofLE, hle, hge]
+  cases c.compare a b
+  · simp [PartialOrdering.isLE, PartialOrdering.isGE]
+  · rename_i o
+    simp only [PartialOrdering.isLE, PartialOrdering.isGE]
+    cases o <;> simp
+
+instance (α : Type u) [LE α] : LawfulOrientedPartiallyComparableLE (.ofLE α) where
+  le_iff_compare_isLE a b := by
+    simp only [PartiallyComparable.ofLE]
+    split <;> split <;> simp_all [PartialOrdering.isLE]
+  ge_iff_compare_isGE a b := by
+    simp only [PartiallyComparable.ofLE]
+    split <;> split <;> simp_all [PartialOrdering.isGE]
+
+theorem LawfulOrientedPartiallyComparableLT.eq_ofLT {α : Type u} [LT α] {c : PartiallyComparable α}
+    [i : LawfulOrientedPartiallyComparableLT c] [LawfulTotallyComparable c] :
+    c = .ofLT α := by
+  ext a b
+  have hlt := i.lt_iff_compare_eq_some_lt a b
+  have hgt := i.gt_iff_compare_eq_some_gt a b
+  simp [PartiallyComparable.ofLT, hlt, hgt]
+  cases h : c.compare a b
+  · have := LawfulTotallyComparable.isSome_compare (c := c) a b
+    simp [h] at this
+  · rename_i o
+    cases o <;> simp_all
+
+instance {α : Type u} [LT α] : LawfulTotallyComparable (.ofLT α) where
+  isSome_compare a b := by
+    simp only [PartiallyComparable.ofLT]
+    split
+    · simp
+    · split <;> simp
+
+instance (α : Type u) [LT α] [Std.Asymm (α := α) (· < ·)] :
+    LawfulOrientedPartiallyComparableLT (.ofLT α) where
+  lt_iff_compare_eq_some_lt a b := by
+    simp [PartiallyComparable.ofLT]
+    constructor
+    · intro h
+      simp [h]
+    · intro h
+      split at h <;> simp_all
+  gt_iff_compare_eq_some_gt a b := by
+    simp [PartiallyComparable.ofLT]
+    split
+    · simp
+      apply Std.Asymm.asymm
+      assumption
+    · simp
+
+section OrderProp
+
+class OrderProp {α : Type u} (P : PartiallyComparable α → Prop) (c : PartiallyComparable α) where
+  inner : P c
+
+variable {α : Type u} {P : PartiallyComparable α → Prop}
+
+instance [Ord α] [LE α] [i : LawfulOrientedPartiallyComparableLE (.ofOrd α)]
+    [OrderProp P (.ofOrd α)] : OrderProp P (.ofLE α) := by
+  rw [← i.eq_ofLE]; infer_instance
+
+instance [Ord α] [LT α] [i : LawfulOrientedPartiallyComparableLT (.ofOrd α)]
+    [LawfulTotallyComparable (.ofOrd α)] [OrderProp P (.ofOrd α)] : OrderProp P (.ofLT α) := by
+  rw [← i.eq_ofLT]; infer_instance
+
+instance [LE α] (cmp : α → α → Ordering) [i : LawfulPartiallyComparableCmp (.ofLE α) cmp]
+    [OrderProp P (.ofLE α)] : OrderProp P (.ofCmp cmp) := by
+  rw [← i.eq_ofCmp]; infer_instance
+
+instance [LE α] [LT α] [i : LawfulOrientedPartiallyComparableLT (.ofLE α)]
+    [LawfulTotallyComparable (.ofLE α)] [OrderProp P (.ofLE α)] : OrderProp P (.ofLT α) := by
+  rw [← i.eq_ofLT]; infer_instance
+
+instance [LT α] [Ord α] [i : LawfulPartiallyComparableOrd (.ofLT α)] [Std.Asymm (α := α) (· < ·)]
+    [OrderProp P (.ofLT α)] : OrderProp P (.ofOrd α) := by
+  rw [← i.eq_ofOrd]; infer_instance
+
+instance [LT α] [LE α] [i : LawfulOrientedPartiallyComparableLE (.ofLT α)] [Std.Asymm (α := α) (· < ·)]
+    [OrderProp P (.ofLT α)] : OrderProp P (.ofLE α) := by
+  rw [← i.eq_ofLE]; infer_instance
+
+end OrderProp
+
+instance (α : Type u) (c : PartiallyComparable α) [Ord α] [LawfulPartiallyComparableOrd c] :
+    OrderProp LawfulPartiallyComparableOrd c where
+  inner := inferInstance
+
+instance (α : Type u) (c : PartiallyComparable α) [Ord α] [OrderProp LawfulPartiallyComparableOrd c] :
+    LawfulPartiallyComparableOrd c :=
+  OrderProp.inner
+
+instance (α : Type u) (c : PartiallyComparable α) [LE α] [LawfulOrientedPartiallyComparableLE c] :
+    OrderProp LawfulOrientedPartiallyComparableLE c where
+  inner := inferInstance
+
+instance (α : Type u) (c : PartiallyComparable α) [LE α]
+    [OrderProp LawfulOrientedPartiallyComparableLE c] : LawfulOrientedPartiallyComparableLE c :=
+  OrderProp.inner
+
+instance (α : Type u) (c : PartiallyComparable α) [LT α] [LawfulOrientedPartiallyComparableLT c] :
+    OrderProp LawfulOrientedPartiallyComparableLT c where
+  inner := inferInstance
+
+instance (α : Type u) (c : PartiallyComparable α) [LT α]
+    [OrderProp LawfulOrientedPartiallyComparableLT c] : LawfulOrientedPartiallyComparableLT c :=
+  OrderProp.inner
+
+instance (α : Type u) (c : PartiallyComparable α) [LawfulTotallyComparable c] :
+    OrderProp LawfulTotallyComparable c where
+  inner := inferInstance
+
+instance (α : Type u) (c : PartiallyComparable α) [OrderProp LawfulTotallyComparable c] :
+    LawfulTotallyComparable c :=
+  OrderProp.inner
+
+theorem lt_iff_le_and_not_ge [LE α] [LT α] [i : LawfulOrientedPartiallyComparableLT (.ofLE α)]
+    {a b : α} : a < b ↔ a ≤ b ∧ ¬ b ≤ a := by
+  simp [i.lt_iff_compare_eq_some_lt, PartiallyComparable.ofLE]
+  split <;> split <;> simp_all
+
+-- Demo: an alternative formulation of the lemma in terms of LT
+-- Note that this is more restrictive because `ofLT` is total by construction.
+example [LE α] [LT α] [LawfulOrientedPartiallyComparableLE (.ofLT α)]
+    [Std.Asymm (α := α) (· < ·)]
+    {a b : α} : a < b ↔ a ≤ b ∧ ¬ b ≤ a := by
+  -- base change works!
+  apply lt_iff_le_and_not_ge
+
+theorem le_total [LE α] [i : LawfulTotallyComparable (.ofLE α)] {a b : α} :
+    a ≤ b ∨ b ≤ a := by
+  have := i.isSome_compare a b
+  simp only [PartiallyComparable.ofLE] at this
+  split at this
+  · exact Or.inl ‹_›
+  · split at this
+    · exact Or.inr ‹_›
+    · cases this
+
+example [LE α] [Ord α]
+    [i : LawfulOrientedPartiallyComparableLE (.ofOrd α)] {a b : α} :
+    (compare a b).isLE ∨ (compare a b).isGE := by
+  -- The required LawfulTotallyComparable (.ofLE α) instance is inferred as expected
+  have := le_total (α := α) (a := a) (b := b)
+  -- Sad: I need to explicitly reference the instance I want.
+  simp [i.le_iff_compare_isLE] at this
+  sorry

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/Test.lean

@@ -0,0 +1,14 @@
+import Std.Classes.Ord.New.PartiallyComparable
+import Std.Data.TreeMap
+
+open Std
+
+def test {α : Type u} [Ord α] [LawfulPartiallyComparableOrd (.ofOrd α)]
+    [LawfulLinearOrder (.ofOrd α)] (a : α) : Option Nat :=
+  (∅ : DTreeMap α (fun _ => Nat)).get? a
+
+example (α : Type u) [Ord α] [LawfulPartiallyComparableOrd (.ofOrd α)]
+    [LawfulLinearOrder (.ofOrd α)] (a : α) :
+    test a = none := by
+  rw [test]
+  rw [DTreeMap.get?_emptyc]

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/Internal/Ordered.lean

@@ -45,24 +45,26 @@ theorem Ordered.compare_left [Ord α] {sz k v l r} (h : (.inner sz k v l r : Imp
     {k'} (hk' : k' ∈ l.toListModel) : compare k'.1 k = .lt :=
   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 α] [LawfulLinearPreorder (.ofOrd α)] {k : α → Ordering} [IsStrictCut compare 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)))
+  sorry
+  -- beq_iff_eq.2 (IsStrictCut.gt_of_isGE_of_gt hcmp (OrientedCmp.gt_of_lt (ho.compare_left hp)))
 
-theorem Ordered.compare_left_not_beq_eq [Ord α] [TransOrd α] {k : α → Ordering}
+theorem Ordered.compare_left_not_beq_eq [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α → Ordering}
     [IsStrictCut compare 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))
+  sorry
+  -- exact IsStrictCut.gt_of_isGE_of_gt hcmp (OrientedCmp.gt_of_lt (ho.compare_left hp))
 
 theorem Ordered.compare_right [Ord α] {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
   exact List.rel_of_pairwise_cons (h.sublist (List.sublist_append_right _ _)) hk'
 
-theorem Ordered.compare_right_not_beq_gt [Ord α] [TransOrd α] {k : α → Ordering}
+theorem Ordered.compare_right_not_beq_gt [Ord α] {k : α → Ordering}
     [IsStrictCut compare 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

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

@@ -30,7 +30,7 @@ namespace Impl
 /-- Well-formedness of tree maps. -/
 inductive WF [Ord α] : {β : α → 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 (.ofOrd α)], 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`. -/

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

@@ -7,6 +7,7 @@ prelude
 import Init.Data.Option.List
 import Init.Data.Array.Bootstrap
 import Std.Classes.Ord.Basic
+import Std.Classes.Ord.New.PartiallyComparable
 import Std.Data.DTreeMap.Internal.Model
 import Std.Data.Internal.Cut
 import Std.Data.Internal.List.Associative
@@ -178,7 +179,7 @@ termination_by sizeOf l + sizeOf r
 ## Verification of model functions
 -/
 
-theorem toListModel_filter_gt_of_gt [Ord α] [TransOrd α] {k : α → Ordering} [IsStrictCut compare k]
+theorem toListModel_filter_gt_of_gt [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α → Ordering} [IsStrictCut compare k]
     {sz k' v' l r} (hcmp : k k' = .gt) (ho : (inner sz k' v' l r).Ordered) :
     (inner sz k' v' l r : Impl α β).toListModel.filter (k ·.1 == .gt) =
       l.toListModel ++ ⟨k', v'⟩ :: r.toListModel.filter (k ·.1 == .gt) := by
@@ -186,7 +187,7 @@ theorem toListModel_filter_gt_of_gt [Ord α] [TransOrd α] {k : α → Ordering}
   · exact Ordered.compare_left_beq_gt ho (Ordering.isGE_of_eq_gt hcmp)
   · simpa
 
-theorem toListModel_filter_gt_of_eq [Ord α] [TransOrd α] {k : α → Ordering} [IsStrictCut compare k]
+theorem toListModel_filter_gt_of_eq [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α → Ordering} [IsStrictCut compare k]
     {sz k' v' l r} (hcmp : k k' = .eq) (ho : (inner sz k' v' l r).Ordered) :
     (inner sz k' v' l r : Impl α β).toListModel.filter (k ·.1 == .gt) = l.toListModel := by
   rw [toListModel_inner, List.filter_append, List.filter_cons_of_neg, List.filter_eq_self.2,
@@ -195,7 +196,7 @@ theorem toListModel_filter_gt_of_eq [Ord α] [TransOrd α] {k : α → Ordering}
   · exact Ordered.compare_left_beq_gt ho (Ordering.isGE_of_eq_eq hcmp)
   · simp_all
 
-theorem toListModel_filter_gt_of_lt [Ord α] [TransOrd α] {k : α → Ordering} [IsStrictCut compare k]
+theorem toListModel_filter_gt_of_lt [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α → Ordering} [IsStrictCut compare k]
     {sz k' v' l r} (hcmp : k k' = .lt) (ho : (inner sz k' v' l r).Ordered) :
     (inner sz k' v' l r : Impl α β).toListModel.filter (k ·.1 == .gt) =
       l.toListModel.filter (k ·.1 == .gt) := by
@@ -203,7 +204,7 @@ theorem toListModel_filter_gt_of_lt [Ord α] [TransOrd α] {k : α → Ordering}
     List.append_nil]
   simpa [hcmp] using Ordered.compare_right_not_beq_gt ho (Ordering.isLE_of_eq_lt hcmp)
 
-theorem toListModel_find?_of_gt [Ord α] [TransOrd α] {k : α → Ordering} [IsStrictCut compare k]
+theorem toListModel_find?_of_gt [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α → Ordering} [IsStrictCut compare k]
     {sz k' v' l r} (hcmp : k k' = .gt) (ho : (inner sz k' v' l r).Ordered) :
     (inner sz k' v' l r : Impl α β).toListModel.find? (k ·.1 == .eq) =
       r.toListModel.find? (k ·.1 == .eq) := by
@@ -212,7 +213,7 @@ theorem toListModel_find?_of_gt [Ord α] [TransOrd α] {k : α → Ordering} [Is
   · simp [hcmp]
   · exact Ordered.compare_left_not_beq_eq ho (Ordering.isGE_of_eq_gt hcmp)
 
-theorem toListModel_find?_of_eq [Ord α] [TransOrd α] {k : α → Ordering} [IsStrictCut compare k]
+theorem toListModel_find?_of_eq [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α → Ordering} [IsStrictCut compare k]
     {sz k' v' l r} (hcmp : k k' = .eq) (ho : (inner sz k' v' l r).Ordered) :
     (inner sz k' v' l r : Impl α β).toListModel.find? (k ·.1 == .eq) = some ⟨k', v'⟩ := by
   rw [toListModel_inner, List.find?_append, List.find?_eq_none.2, Option.none_or,
@@ -220,7 +221,7 @@ theorem toListModel_find?_of_eq [Ord α] [TransOrd α] {k : α → Ordering} [Is
   · simp_all
   · exact Ordered.compare_left_not_beq_eq ho (Ordering.isGE_of_eq_eq hcmp)
 
-theorem toListModel_find?_of_lt [Ord α] [TransOrd α] {k : α → Ordering} [IsCut compare k]
+theorem toListModel_find?_of_lt [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α → Ordering} [IsCut compare k]
     {sz k' v' l r} (hcmp : k k' = .lt) (ho : (inner sz k' v' l r).Ordered) :
     (inner sz k' v' l r : Impl α β).toListModel.find? (k ·.1 == .eq) =
       l.toListModel.find? (k ·.1 == .eq) := by
@@ -228,7 +229,7 @@ theorem toListModel_find?_of_lt [Ord α] [TransOrd α] {k : α → Ordering} [Is
   rw [List.find?_cons_of_neg (by simp [hcmp])]
   refine List.find?_eq_none.2 (fun p hp => by simp [IsCut.lt hcmp (ho.compare_right hp)])
 
-theorem toListModel_filter_lt_of_gt [Ord α] [TransOrd α] {k : α → Ordering} [IsCut compare k]
+theorem toListModel_filter_lt_of_gt [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α → Ordering} [IsCut compare k]
     {sz k' v' l r} (hcmp : k k' = .gt) (ho : (inner sz k' v' l r).Ordered) :
     (inner sz k' v' l r : Impl α β).toListModel.filter (k ·.1 == .lt) =
       r.toListModel.filter (k ·.1 == .lt) := by
@@ -236,7 +237,7 @@ theorem toListModel_filter_lt_of_gt [Ord α] [TransOrd α] {k : α → Ordering}
     List.filter_cons_of_neg (by simp [hcmp])]
   exact fun p hp => by simp [IsCut.gt hcmp (OrientedCmp.gt_of_lt (ho.compare_left hp))]
 
-theorem toListModel_filter_lt_of_eq [Ord α] [TransOrd α] {k : α → Ordering} [IsStrictCut compare k]
+theorem toListModel_filter_lt_of_eq [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α → Ordering} [IsStrictCut compare k]
     {sz k' v' l r} (hcmp : k k' = .eq) (ho : (inner sz k' v' l r).Ordered) :
     (inner sz k' v' l r : Impl α β).toListModel.filter (k ·.1 == .lt) = r.toListModel := by
   rw [toListModel_inner, List.filter_append, List.filter_eq_nil_iff.2, List.nil_append,
@@ -247,7 +248,7 @@ theorem toListModel_filter_lt_of_eq [Ord α] [TransOrd α] {k : α → Ordering}
       by simp [IsStrictCut.gt_of_isGE_of_gt (Ordering.isGE_of_eq_eq hcmp)
           (OrientedCmp.gt_of_lt (ho.compare_left hp))]
 
-theorem toListModel_filter_lt_of_lt [Ord α] [TransOrd α] {k : α → Ordering} [IsCut compare k]
+theorem toListModel_filter_lt_of_lt [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α → Ordering} [IsCut compare k]
     {sz k' v' l r} (hcmp : k k' = .lt) (ho : (inner sz k' v' l r).Ordered) :
     (inner sz k' v' l r : Impl α β).toListModel.filter (k ·.1 == .lt) =
       l.toListModel.filter (k ·.1 == .lt) ++ ⟨k', v'⟩ :: r.toListModel := by
@@ -255,22 +256,22 @@ theorem toListModel_filter_lt_of_lt [Ord α] [TransOrd α] {k : α → Ordering}
     List.append_cancel_left_eq, List.cons.injEq, List.filter_eq_self, beq_iff_eq, true_and]
   exact fun p hp => IsCut.lt hcmp (ho.compare_right hp)
 
-theorem findCell_of_gt [Ord α] [TransOrd α] {k : α → Ordering} [IsStrictCut compare k]
+theorem findCell_of_gt [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α → Ordering} [IsStrictCut compare k]
     {sz k' v' l r} (hcmp : k k' = .gt) (ho : (inner sz k' v' l r : Impl α β).Ordered) :
     List.findCell (inner sz k' v' l r).toListModel k = List.findCell r.toListModel k :=
   Cell.ext (toListModel_find?_of_gt hcmp ho)
 
-theorem findCell_of_eq [Ord α] [TransOrd α] {k : α → Ordering} [IsStrictCut compare k]
+theorem findCell_of_eq [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α → Ordering} [IsStrictCut compare k]
     {sz k' v' l r} (hcmp : k k' = .eq) (ho : (inner sz k' v' l r : Impl α β).Ordered) :
     List.findCell (inner sz k' v' l r).toListModel k = Cell.ofEq k' v' hcmp :=
   Cell.ext (toListModel_find?_of_eq hcmp ho)
 
-theorem findCell_of_lt [Ord α] [TransOrd α] {k : α → Ordering} [IsCut compare k] {sz k' v' l r}
+theorem findCell_of_lt [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α → Ordering} [IsCut compare k] {sz k' v' l r}
     (hcmp : k k' = .lt) (ho : (inner sz k' v' l r : Impl α β).Ordered) :
     List.findCell (inner sz k' v' l r).toListModel k = List.findCell l.toListModel k :=
   Cell.ext (toListModel_find?_of_lt hcmp ho)
 
-theorem toListModel_updateCell [Ord α] [TransOrd α] {k : α}
+theorem toListModel_updateCell [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α}
     {f : Cell α β (compare k) → Cell α β (compare k)} {l : Impl α β} (hlb : l.Balanced)
     (hlo : l.Ordered) :
     (l.updateCell k f hlb).impl.toListModel = l.toListModel.filter (compare k ·.1 == .gt) ++
@@ -300,7 +301,7 @@ theorem toListModel_updateCell [Ord α] [TransOrd α] {k : α}
       toListModel_filter_lt_of_gt hcmp hlo, toListModel_balance, ih hlo.right]
     simp
 
-theorem toListModel_eq_append [Ord α] [TransOrd α] (k : α → Ordering) [IsStrictCut compare k]
+theorem toListModel_eq_append [Ord α] [LawfulLinearPreorder (.ofOrd α)] (k : α → Ordering) [IsStrictCut compare k]
     {l : Impl α β} (ho : l.Ordered) :
     l.toListModel = l.toListModel.filter (k ·.1 == .gt) ++
       (l.toListModel.find? (k ·.1 == .eq)).toList ++
@@ -321,7 +322,7 @@ theorem toListModel_eq_append [Ord α] [TransOrd α] (k : α → Ordering) [IsSt
       simp
   · simp
 
-theorem ordered_updateCell [Ord α] [TransOrd α] {k : α}
+theorem ordered_updateCell [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α}
     {f : Cell α β (compare k) → Cell α β (compare k)}
     {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) : (l.updateCell k f hlb).impl.Ordered := by
   rw [Ordered, toListModel_updateCell _ hlo]
@@ -351,7 +352,8 @@ theorem ordered_updateCell [Ord α] [TransOrd α] {k : α}
 
 open Std.Internal.List
 
-theorem exists_cell_of_updateCell [BEq α] [Ord α] [TransOrd α] [LawfulBEqOrd α] (l : Impl α β) (hlb : l.Balanced)
+theorem exists_cell_of_updateCell [BEq α] [Ord α] [LawfulLinearPreorder (.ofOrd α)]
+    [LawfulPartiallyComparableBEq (.ofOrd α)] (l : Impl α β) (hlb : l.Balanced)
     (hlo : l.Ordered) (k : α)
     (f : Cell α β (compare k) → Cell α β (compare k)) : ∃ (l' : List ((a : α) × β a)),
     l.toListModel.Perm ((l.toListModel.find? (compare k ·.1 == .eq)).toList ++ l') ∧
@@ -376,7 +378,8 @@ theorem Ordered.distinctKeys [BEq α] [Ord α] [LawfulBEqOrd α] {l : Impl α β
     simp [← LawfulBEqOrd.not_compare_eq_iff_beq_eq_false, h])⟩
 
 /-- This is the general theorem to show that modification operations are correct. -/
-theorem toListModel_updateCell_perm [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+theorem toListModel_updateCell_perm [Ord α] [BEq α] [LawfulLinearPreorder (.ofOrd α)]
+    [LawfulPartiallyComparableBEq (.ofOrd α)]
     {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) {k : α}
     {f : Cell α β (compare k) → Cell α β (compare k)}
     {g : List ((a : α) × β a) → List ((a : α) × β a)}
@@ -388,7 +391,7 @@ theorem toListModel_updateCell_perm [Ord α] [TransOrd α] [BEq α] [LawfulBEqOr
   refine h₂.trans (List.Perm.trans ?_ (hg₁ hlo.distinctKeys h₁).symm)
   rwa [hfg, hg₂, List.findCell_inner]
 
-theorem contains_findCell [Ord α] [TransOrd α] {k : α → Ordering} [IsStrictCut compare k]
+theorem contains_findCell [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α → Ordering} [IsStrictCut compare k]
     {l : Impl α β} (hlo : l.Ordered) (h : l.contains' k) :
     (List.findCell l.toListModel k).contains := by
   induction l
@@ -399,7 +402,7 @@ theorem contains_findCell [Ord α] [TransOrd α] {k : α → Ordering} [IsStrict
     · simpa only [findCell_of_gt hcmp hlo] using ih₂ hlo.right h
   · simp [contains'] at h
 
-theorem applyPartition_eq [Ord α] [TransOrd α] {k : α → Ordering} [IsStrictCut compare k] {l : Impl α β}
+theorem applyPartition_eq [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α → Ordering} [IsStrictCut compare k] {l : Impl α β}
     {f : List ((a : α) × β a) → (c : Cell α β k) → (l.contains' k → c.contains) → List ((a : α ) × β a) → δ}
     (hlo : l.Ordered) :
     applyPartition k l f =
@@ -477,7 +480,7 @@ theorem containsKey_toListModel [Ord α] [OrientedOrd α] [BEq α] [LawfulBEqOrd
     · exact ⟨⟨k', v'⟩, by simp, compare_eq_iff_beq.mp (OrientedCmp.eq_symm hcmp)⟩
   · simp [contains'] at h
 
-theorem applyPartition_eq_apply_toListModel [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : Impl α β}
+theorem applyPartition_eq_apply_toListModel [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulBEqOrd α] {k : α} {l : Impl α β}
     (hlo : l.Ordered)
     {f : List ((a : α) × β a) → (c : Cell α β (compare k)) →
       (l.contains' (compare k) → c.contains) → List ((a : α) × β a) → δ}
@@ -494,7 +497,7 @@ theorem applyPartition_eq_apply_toListModel [Ord α] [TransOrd α] [BEq α] [Law
   · simp
   · simp
 
-theorem applyPartition_eq_apply_toListModel' [Ord α] [TransOrd α] {k : α → Ordering}
+theorem applyPartition_eq_apply_toListModel' [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α → Ordering}
     [IsStrictCut compare k] {l : Impl α β} (hlo : l.Ordered)
     {f : List ((a : α) × β a) → (c : Cell α β k) → (l.contains' k → c.contains) → List ((a : α) × β a) → δ}
     (g : (ll : List ((a : α) × β a)) → δ)
@@ -509,7 +512,7 @@ theorem applyPartition_eq_apply_toListModel' [Ord α] [TransOrd α] {k : α →
   · simp
   · simp
 
-theorem applyCell_eq_apply_toListModel [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α}
+theorem applyCell_eq_apply_toListModel [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulBEqOrd α] {k : α}
     {l : Impl α β} (hlo : l.Ordered)
     {f : (c : Cell α β (compare k)) → (l.contains' (compare k) → c.contains) → δ}
     (g : (ll : List ((a : α) × β a)) → (l.contains' (compare k) → containsKey k ll) → δ)
@@ -576,7 +579,7 @@ theorem size_eq_length (t : Impl α β) (htb : t.Balanced) : t.size = t.toListMo
 ### `contains`
 -/
 
-theorem containsₘ_eq_containsKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α}
+theorem containsₘ_eq_containsKey [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulBEqOrd α] {k : α}
     {l : Impl α β} (hlo : l.Ordered) :
     l.containsₘ k = containsKey k l.toListModel := by
   rw [containsₘ, applyCell_eq_apply_toListModel hlo (fun l _ => containsKey k l)]
@@ -588,7 +591,7 @@ theorem containsₘ_eq_containsKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd
   · exact fun l₁ l₂ h a hP => containsKey_of_perm hP
   · exact fun l₁ l₂ h h' => containsKey_append_of_not_contains_right h'
 
-theorem contains_eq_containsKey [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [TransOrd α] {k : α}
+theorem contains_eq_containsKey [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [LawfulLinearPreorder (.ofOrd α)] {k : α}
     {l : Impl α β} (hlo : l.Ordered) :
     l.contains k = containsKey k l.toListModel := by
   rw [contains_eq_containsₘ, containsₘ_eq_containsKey hlo]
@@ -597,7 +600,7 @@ theorem contains_eq_containsKey [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [T
 ### `get?`
 -/
 
-theorem get?ₘ_eq_getValueCast? [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β}
+theorem get?ₘ_eq_getValueCast? [Ord α] [LawfulLinearPreorder (.ofOrd α)] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β}
     (hto : t.Ordered) : t.get?ₘ k = getValueCast? k t.toListModel := by
   rw [get?ₘ, applyCell_eq_apply_toListModel hto (fun l _ => getValueCast? k l)]
   · rintro ⟨(_|p), hp⟩ -
@@ -608,7 +611,7 @@ theorem get?ₘ_eq_getValueCast? [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α
   · exact fun l₁ l₂ h => getValueCast?_of_perm
   · exact fun l₁ l₂ h => getValueCast?_append_of_containsKey_eq_false
 
-theorem get?_eq_getValueCast? [instBEq : BEq α] [Ord α] [i : LawfulBEqOrd α] [TransOrd α]
+theorem get?_eq_getValueCast? [instBEq : BEq α] [Ord α] [i : LawfulBEqOrd α] [LawfulLinearPreorder (.ofOrd α)]
     [LawfulEqOrd α] {k : α} {t : Impl α β}
     (hto : t.Ordered) : t.get? k = getValueCast? k t.toListModel := by
   rw [get?_eq_get?ₘ, get?ₘ_eq_getValueCast? hto]
@@ -617,18 +620,18 @@ theorem get?_eq_getValueCast? [instBEq : BEq α] [Ord α] [i : LawfulBEqOrd α]
 ### `get`
 -/
 
-theorem contains_eq_isSome_get?ₘ [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α]
+theorem contains_eq_isSome_get?ₘ [Ord α] [LawfulLinearPreorder (.ofOrd α)] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α]
     {k : α} {t : Impl α β} (hto : t.Ordered) : contains k t = (t.get?ₘ k).isSome := by
   rw [get?ₘ_eq_getValueCast? hto, contains_eq_containsKey hto, containsKey_eq_isSome_getValueCast?]
 
-theorem getₘ_eq_getValueCast [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {k : α}
+theorem getₘ_eq_getValueCast [Ord α] [LawfulLinearPreorder (.ofOrd α)] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {k : α}
     {t : Impl α β} (h) {h'} (hto : t.Ordered) : t.getₘ k h' = getValueCast k t.toListModel h := by
   simp only [getₘ]
   revert h'
   rw [get?ₘ_eq_getValueCast? hto]
   simp [getValueCast?_eq_some_getValueCast ‹_›]
 
-theorem get_eq_getValueCast [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [TransOrd α] [LawfulEqOrd α] {k : α} {t : Impl α β} {h}
+theorem get_eq_getValueCast [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [LawfulLinearPreorder (.ofOrd α)] [LawfulEqOrd α] {k : α} {t : Impl α β} {h}
     (hto : t.Ordered): t.get k h = getValueCast k t.toListModel (contains_eq_containsKey hto ▸ h) := by
   rw [get_eq_getₘ, getₘ_eq_getValueCast _ hto]
   exact contains_eq_isSome_get?ₘ hto ▸ h
@@ -637,11 +640,11 @@ theorem get_eq_getValueCast [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [Trans
 ### `get!`
 -/
 
-theorem get!ₘ_eq_getValueCast! [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {k : α}
+theorem get!ₘ_eq_getValueCast! [Ord α] [LawfulLinearPreorder (.ofOrd α)] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {k : α}
     [Inhabited (β k)] {t : Impl α β} (hto : t.Ordered) : t.get!ₘ k = getValueCast! k t.toListModel := by
   simp [get!ₘ, get?ₘ_eq_getValueCast? hto, getValueCast!_eq_getValueCast?]
 
-theorem get!_eq_getValueCast! [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [TransOrd α] [LawfulEqOrd α] {k : α} [Inhabited (β k)]
+theorem get!_eq_getValueCast! [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [LawfulLinearPreorder (.ofOrd α)] [LawfulEqOrd α] {k : α} [Inhabited (β k)]
     {t : Impl α β} (hto : t.Ordered) : t.get! k = getValueCast! k t.toListModel := by
   rw [get!_eq_get!ₘ, get!ₘ_eq_getValueCast! hto]
 
@@ -649,12 +652,12 @@ theorem get!_eq_getValueCast! [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [Tra
 ### `getD`
 -/
 
-theorem getDₘ_eq_getValueCastD [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {k : α}
+theorem getDₘ_eq_getValueCastD [Ord α] [LawfulLinearPreorder (.ofOrd α)] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {k : α}
     {t : Impl α β} {fallback : β k} (hto : t.Ordered) :
     t.getDₘ k fallback = getValueCastD k t.toListModel fallback := by
   simp [getDₘ, get?ₘ_eq_getValueCast? hto, getValueCastD_eq_getValueCast?]
 
-theorem getD_eq_getValueCastD [Ord α] [instBEq : BEq α] [LawfulBEqOrd α] [TransOrd α] [LawfulEqOrd α] {k : α}
+theorem getD_eq_getValueCastD [Ord α] [instBEq : BEq α] [LawfulBEqOrd α] [LawfulLinearPreorder (.ofOrd α)] [LawfulEqOrd α] {k : α}
     {t : Impl α β} {fallback : β k} (hto : t.Ordered) :
     t.getD k fallback = getValueCastD k t.toListModel fallback := by
   rw [getD_eq_getDₘ, getDₘ_eq_getValueCastD hto]
@@ -663,7 +666,7 @@ theorem getD_eq_getValueCastD [Ord α] [instBEq : BEq α] [LawfulBEqOrd α] [Tra
 ### `getKey?`
 -/
 
-theorem getKey?ₘ_eq_getKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β}
+theorem getKey?ₘ_eq_getKey? [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β}
     (hto : t.Ordered) : t.getKey?ₘ k = List.getKey? k t.toListModel := by
   rw [getKey?ₘ, applyCell_eq_apply_toListModel hto (fun l _ => List.getKey? k l)]
   · rintro ⟨(_|p), hp⟩ -
@@ -674,7 +677,7 @@ theorem getKey?ₘ_eq_getKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
   · exact fun l₁ l₂ h => List.getKey?_of_perm
   · exact fun l₁ l₂ h => List.getKey?_append_of_containsKey_eq_false
 
-theorem getKey?_eq_getKey? [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β}
+theorem getKey?_eq_getKey? [Ord α] [LawfulLinearPreorder (.ofOrd α)] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β}
     (hto : t.Ordered) : t.getKey? k = List.getKey? k t.toListModel := by
   rw [getKey?_eq_getKey?ₘ, getKey?ₘ_eq_getKey? hto]
 
@@ -682,18 +685,18 @@ theorem getKey?_eq_getKey? [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqO
 ### `getKey`
 -/
 
-theorem contains_eq_isSome_getKey?ₘ [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α}
+theorem contains_eq_isSome_getKey?ₘ [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulBEqOrd α] {k : α}
     {t : Impl α β} (hto : t.Ordered) : contains k t = (t.getKey?ₘ k).isSome := by
   rw [getKey?ₘ_eq_getKey? hto, contains_eq_containsKey hto, containsKey_eq_isSome_getKey?]
 
-theorem getKeyₘ_eq_getKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (h)
+theorem getKeyₘ_eq_getKey [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (h)
     {h'} (hto : t.Ordered) : t.getKeyₘ k h' = List.getKey k t.toListModel h := by
   simp only [getKeyₘ]
   revert h'
   rw [getKey?ₘ_eq_getKey? hto]
   simp [getKey?_eq_some_getKey ‹_›]
 
-theorem getKey_eq_getKey [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} {h}
+theorem getKey_eq_getKey [Ord α] [LawfulLinearPreorder (.ofOrd α)] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} {h}
     (hto : t.Ordered): t.getKey k h = List.getKey k t.toListModel (contains_eq_containsKey hto ▸ h) := by
   rw [getKey_eq_getKeyₘ, getKeyₘ_eq_getKey _ hto]
   exact contains_eq_isSome_getKey?ₘ hto ▸ h
@@ -702,11 +705,11 @@ theorem getKey_eq_getKey [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd
 ### `getKey!`
 -/
 
-theorem getKey!ₘ_eq_getKey! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} [Inhabited α]
+theorem getKey!ₘ_eq_getKey! [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulBEqOrd α] {k : α} [Inhabited α]
     {t : Impl α β} (hto : t.Ordered) : t.getKey!ₘ k = List.getKey! k t.toListModel := by
   simp [getKey!ₘ, getKey?ₘ_eq_getKey? hto, getKey!_eq_getKey?]
 
-theorem getKey!_eq_getKey! [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} [Inhabited α]
+theorem getKey!_eq_getKey! [Ord α] [LawfulLinearPreorder (.ofOrd α)] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} [Inhabited α]
     {t : Impl α β} (hto : t.Ordered) : t.getKey! k = List.getKey! k t.toListModel := by
   rw [getKey!_eq_getKey!ₘ, getKey!ₘ_eq_getKey! hto]
 
@@ -714,12 +717,12 @@ theorem getKey!_eq_getKey! [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqO
 ### `getKeyD`
 -/
 
-theorem getKeyDₘ_eq_getKeyD [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α}
+theorem getKeyDₘ_eq_getKeyD [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulBEqOrd α] {k : α}
     {t : Impl α β} {fallback : α} (hto : t.Ordered) :
     t.getKeyDₘ k fallback = List.getKeyD k t.toListModel fallback := by
   simp [getKeyDₘ, getKey?ₘ_eq_getKey? hto, getKeyD_eq_getKey?]
 
-theorem getKeyD_eq_getKeyD [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α}
+theorem getKeyD_eq_getKeyD [Ord α] [LawfulLinearPreorder (.ofOrd α)] [instBEq : BEq α] [LawfulBEqOrd α] {k : α}
     {t : Impl α β} {fallback : α} (hto : t.Ordered) :
     t.getKeyD k fallback = List.getKeyD k t.toListModel fallback := by
   rw [getKeyD_eq_getKeyDₘ, getKeyDₘ_eq_getKeyD hto]
@@ -732,7 +735,7 @@ variable {β : Type v}
 ### `get?`
 -/
 
-theorem get?ₘ_eq_getValue? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α}
+theorem get?ₘ_eq_getValue? [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulBEqOrd α] {k : α}
     {t : Impl α (fun _ => β)} (hto : t.Ordered) :
     get?ₘ t k = getValue? k t.toListModel := by
   rw [get?ₘ, applyCell_eq_apply_toListModel hto (fun l _ => getValue? k l)]
@@ -744,7 +747,7 @@ theorem get?ₘ_eq_getValue? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {
   · exact fun l₁ l₂ h => getValue?_of_perm
   · exact fun l₁ l₂ h => getValue?_append_of_containsKey_eq_false
 
-theorem get?_eq_getValue? [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α}
+theorem get?_eq_getValue? [Ord α] [LawfulLinearPreorder (.ofOrd α)] [instBEq : BEq α] [LawfulBEqOrd α] {k : α}
     {t : Impl α (fun _ => β)} (hto : t.Ordered) :
     get? t k = getValue? k t.toListModel := by
   rw [get?_eq_get?ₘ, get?ₘ_eq_getValue? hto]
@@ -753,18 +756,18 @@ theorem get?_eq_getValue? [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOr
 ### `get`
 -/
 
-theorem contains_eq_isSome_get?ₘ [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α}
+theorem contains_eq_isSome_get?ₘ [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulBEqOrd α] {k : α}
     {t : Impl α β} (hto : t.Ordered) : contains k t = (get?ₘ t k).isSome := by
   rw [get?ₘ_eq_getValue? hto, contains_eq_containsKey hto, containsKey_eq_isSome_getValue?]
 
-theorem getₘ_eq_getValue [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (h)
+theorem getₘ_eq_getValue [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (h)
     {h'} (hto : t.Ordered) : getₘ t k h' = getValue k t.toListModel h := by
   simp only [getₘ]
   revert h'
   rw [get?ₘ_eq_getValue? hto]
   simp [getValue?_eq_some_getValue ‹_›]
 
-theorem get_eq_getValue [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α}
+theorem get_eq_getValue [Ord α] [LawfulLinearPreorder (.ofOrd α)] [instBEq : BEq α] [LawfulBEqOrd α] {k : α}
     {t : Impl α β} {h} (hto : t.Ordered) :
     get t k h = getValue k t.toListModel (contains_eq_containsKey hto ▸ h) := by
   rw [get_eq_getₘ, getₘ_eq_getValue _ hto]
@@ -774,11 +777,11 @@ theorem get_eq_getValue [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd
 ### `get!`
 -/
 
-theorem get!ₘ_eq_getValue! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} [Inhabited β]
+theorem get!ₘ_eq_getValue! [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulBEqOrd α] {k : α} [Inhabited β]
     {t : Impl α β} (hto : t.Ordered) : get!ₘ t k = getValue! k t.toListModel := by
   simp [get!ₘ, get?ₘ_eq_getValue? hto, getValue!_eq_getValue?]
 
-theorem get!_eq_getValue! [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α}
+theorem get!_eq_getValue! [Ord α] [LawfulLinearPreorder (.ofOrd α)] [instBEq : BEq α] [LawfulBEqOrd α] {k : α}
     [Inhabited β] {t : Impl α β} (hto : t.Ordered) : get! t k = getValue! k t.toListModel := by
   rw [get!_eq_get!ₘ, get!ₘ_eq_getValue! hto]
 
@@ -786,12 +789,12 @@ theorem get!_eq_getValue! [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOr
 ### `getD`
 -/
 
-theorem getDₘ_eq_getValueD [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α}
+theorem getDₘ_eq_getValueD [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulBEqOrd α] {k : α}
     {t : Impl α β} {fallback : β} (hto : t.Ordered) :
     getDₘ t k fallback = getValueD k t.toListModel fallback := by
   simp [getDₘ, get?ₘ_eq_getValue? hto, getValueD_eq_getValue?]
 
-theorem getD_eq_getValueD [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α}
+theorem getD_eq_getValueD [Ord α] [LawfulLinearPreorder (.ofOrd α)] [instBEq : BEq α] [LawfulBEqOrd α] {k : α}
     {t : Impl α β} {fallback : β} (hto : t.Ordered) :
     getD t k fallback = getValueD k t.toListModel fallback := by
   rw [getD_eq_getDₘ, getDₘ_eq_getValueD hto]
@@ -817,11 +820,12 @@ theorem ordered_empty [Ord α] : (.empty : Impl α β).Ordered := by
 ### `insertₘ`
 -/
 
-theorem ordered_insertₘ [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β} (hlb : l.Balanced)
+theorem ordered_insertₘ [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α} {v : β k} {l : Impl α β} (hlb : l.Balanced)
     (hlo : l.Ordered) : (l.insertₘ k v hlb).Ordered :=
   ordered_updateCell _ hlo
 
-theorem toListModel_insertₘ [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k}
+theorem toListModel_insertₘ [Ord α] [BEq α] [LawfulLinearPreorder (.ofOrd α)]
+    [LawfulPartiallyComparableBEq (.ofOrd α)] {k : α} {v : β k}
     {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) :
     (l.insertₘ k v hlb).toListModel.Perm (insertEntry k v l.toListModel) := by
   refine toListModel_updateCell_perm _ hlo ?_ insertEntry_of_perm
@@ -836,11 +840,12 @@ theorem toListModel_insertₘ [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
 ### `insert`
 -/
 
-theorem ordered_insert [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β} (hlb : l.Balanced)
+theorem ordered_insert [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α} {v : β k} {l : Impl α β} (hlb : l.Balanced)
     (hlo : l.Ordered) : (l.insert k v hlb).impl.Ordered := by
   simpa only [insert_eq_insertₘ] using ordered_insertₘ hlb hlo
 
-theorem toListModel_insert [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k}
+theorem toListModel_insert [Ord α] [BEq α] [LawfulLinearPreorder (.ofOrd α)]
+    [LawfulPartiallyComparableBEq (.ofOrd α)] {k : α} {v : β k}
     {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) :
     (l.insert k v hlb).impl.toListModel.Perm (insertEntry k v l.toListModel) := by
   rw [insert_eq_insertₘ]
@@ -850,12 +855,13 @@ theorem toListModel_insert [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k
 ### `insert!`
 -/
 
-theorem WF.insert! {_ : Ord α} [TransOrd α] {k : α} {v : β k} {l : Impl α β}
+theorem WF.insert! {_ : Ord α} [LawfulLinearPreorder (.ofOrd α)] {k : α} {v : β k} {l : Impl α β}
     (h : l.WF) : (l.insert! k v).WF := by
   simpa [insert_eq_insert!] using WF.insert (h := h.balanced) h
 
-theorem toListModel_insert! [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [TransOrd α] {k : α} {v : β k} {l : Impl α β}
-    (hlb : l.Balanced) (hlo : l.Ordered) :
+theorem toListModel_insert! [instBEq : BEq α] [Ord α]
+    [LawfulLinearPreorder (.ofOrd α)] [LawfulPartiallyComparableBEq (.ofOrd α)] {k : α} {v : β k}
+    {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) :
     (l.insert! k v).toListModel.Perm (insertEntry k v l.toListModel) := by
   rw [insert!_eq_insertₘ]
   exact toListModel_insertₘ hlb hlo
@@ -864,11 +870,12 @@ theorem toListModel_insert! [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [Trans
 ### `eraseₘ`
 -/
 
-theorem ordered_eraseₘ [Ord α] [TransOrd α] {k : α} {t : Impl α β} (htb : t.Balanced)
+theorem ordered_eraseₘ [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α} {t : Impl α β} (htb : t.Balanced)
     (hto : t.Ordered) : (t.eraseₘ k htb).Ordered :=
   ordered_updateCell _ hto
 
-theorem toListModel_eraseₘ [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β}
+theorem toListModel_eraseₘ [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α]
+    [LawfulPartiallyComparableBEq (.ofOrd α)] {k : α} {t : Impl α β}
     (htb : t.Balanced) (hto : t.Ordered) :
     (t.eraseₘ k htb).toListModel.Perm (eraseKey k t.toListModel) := by
   refine toListModel_updateCell_perm _ hto ?_ eraseKey_of_perm
@@ -883,11 +890,12 @@ theorem toListModel_eraseₘ [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {
 ### `erase`
 -/
 
-theorem ordered_erase [Ord α] [TransOrd α] {k : α} {t : Impl α β} (htb : t.Balanced)
+theorem ordered_erase [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α} {t : Impl α β} (htb : t.Balanced)
     (hto : t.Ordered) : (t.erase k htb).impl.Ordered := by
   simpa only [erase_eq_eraseₘ] using ordered_eraseₘ htb hto
 
-theorem toListModel_erase [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β}
+theorem toListModel_erase [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α]
+    [LawfulPartiallyComparableBEq (.ofOrd α)] {k : α} {t : Impl α β}
     (htb : t.Balanced) (hto : t.Ordered) :
     (t.erase k htb).impl.toListModel.Perm (eraseKey k t.toListModel) := by
   rw [erase_eq_eraseₘ]
@@ -897,11 +905,12 @@ theorem toListModel_erase [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k :
 ### `erase!`
 -/
 
-theorem WF.erase! {_ : Ord α} [TransOrd α] {k : α} {l : Impl α β}
+theorem WF.erase! {_ : Ord α} [LawfulLinearPreorder (.ofOrd α)] {k : α} {l : Impl α β}
     (h : l.WF) : (l.erase! k).WF := by
   simpa [erase_eq_erase!] using WF.erase (h := h.balanced) h
 
-theorem toListModel_erase! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : Impl α β}
+theorem toListModel_erase! [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α]
+    [LawfulPartiallyComparableBEq (.ofOrd α)] {k : α} {l : Impl α β}
     (hlb : l.Balanced) (hlo : l.Ordered) :
     (l.erase! k).toListModel.Perm (eraseKey k l.toListModel) := by
   rw [erase!_eq_eraseₘ]
@@ -915,7 +924,8 @@ theorem size_containsThenInsert_eq_size [Ord α] (t : Impl α β) :
     containsThenInsert.size t = t.size := by
   induction t <;> rfl
 
-theorem containsThenInsert_fst_eq_containsₘ [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+theorem containsThenInsert_fst_eq_containsₘ [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α]
+    [LawfulPartiallyComparableBEq (.ofOrd α)]
     (t : Impl α β) (htb : t.Balanced) (ho : t.Ordered) (a : α) (b : β a) :
     (t.containsThenInsert a b htb).1 = t.containsₘ a := by
   simp [containsThenInsert, size_containsThenInsert_eq_size, size_eq_length, htb,
@@ -923,11 +933,12 @@ theorem containsThenInsert_fst_eq_containsₘ [Ord α] [TransOrd α] [BEq α] [L
   simp [containsₘ_eq_containsKey ho]
   split <;> simp_all
 
-theorem ordered_containsThenInsert [Ord α] [TransOrd α] {k : α} {v : β k} {t : Impl α β}
+theorem ordered_containsThenInsert [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α} {v : β k} {t : Impl α β}
     (htb : t.Balanced) (hto : t.Ordered) : (t.containsThenInsert k v htb).2.impl.Ordered := by
   simpa only [containsThenInsert_snd_eq_insertₘ, hto] using ordered_insertₘ htb hto
 
-theorem toListModel_containsThenInsert [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α}
+theorem toListModel_containsThenInsert [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α]
+    [LawfulPartiallyComparableBEq (.ofOrd α)] {k : α}
     {v : β k} {t : Impl α β} (htb : t.Balanced) (hto : t.Ordered) :
     (t.containsThenInsert k v htb).2.impl.toListModel.Perm (insertEntry k v t.toListModel) := by
   rw [containsThenInsert_snd_eq_insertₘ]
@@ -937,11 +948,11 @@ theorem toListModel_containsThenInsert [Ord α] [TransOrd α] [BEq α] [LawfulBE
 ### containsThenInsert!
 -/
 
-theorem WF.containsThenInsert! {_ : Ord α} [TransOrd α] {k : α} {v : β k} {t : Impl α β} (h : t.WF) :
+theorem WF.containsThenInsert! {_ : Ord α} [LawfulLinearPreorder (.ofOrd α)] {k : α} {v : β k} {t : Impl α β} (h : t.WF) :
     (t.containsThenInsert! k v).2.WF := by
   simpa [containsThenInsert!_snd_eq_containsThenInsert_snd, h.balanced] using WF.containsThenInsert (h := h.balanced) h
 
-theorem toListModel_containsThenInsert! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α}
+theorem toListModel_containsThenInsert! [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)] {k : α}
     {v : β k} {t : Impl α β} (htb : t.Balanced) (hto : t.Ordered) :
     (t.containsThenInsert! k v).2.toListModel.Perm (insertEntry k v t.toListModel) := by
   rw [containsThenInsert!_snd_eq_insertₘ]
@@ -951,12 +962,12 @@ theorem toListModel_containsThenInsert! [Ord α] [TransOrd α] [BEq α] [LawfulB
 ### `insertIfNew`
 -/
 
-theorem ordered_insertIfNew [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β}
+theorem ordered_insertIfNew [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α} {v : β k} {l : Impl α β}
     (h : l.Balanced) (ho : l.Ordered) : (l.insertIfNew k v h).impl.Ordered := by
   simp [Impl.insertIfNew]
   split <;> simp only [ho, ordered_insert h ho]
 
-theorem toListModel_insertIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k}
+theorem toListModel_insertIfNew [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)] {k : α} {v : β k}
     {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) :
     (l.insertIfNew k v hlb).impl.toListModel.Perm (insertEntryIfNew k v l.toListModel) := by
   simp only [Impl.insertIfNew, insertEntryIfNew, cond_eq_if, contains_eq_containsKey hlo]
@@ -969,15 +980,15 @@ theorem toListModel_insertIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α
 ### `insertIfNew!`
 -/
 
-theorem ordered_insertIfNew! [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β}
+theorem ordered_insertIfNew! [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α} {v : β k} {l : Impl α β}
     (h : l.Balanced) (ho : l.Ordered) : (l.insertIfNew! k v).Ordered := by
   simpa [insertIfNew_eq_insertIfNew!] using ordered_insertIfNew h ho
 
-theorem WF.insertIfNew! {_ : Ord α} [TransOrd α] {k : α} {v : β k} {l : Impl α β}
+theorem WF.insertIfNew! {_ : Ord α} [LawfulLinearPreorder (.ofOrd α)] {k : α} {v : β k} {l : Impl α β}
     (h : l.WF) : (l.insertIfNew! k v).WF := by
   simpa [insertIfNew_eq_insertIfNew!] using h.insertIfNew (h := h.balanced)
 
-theorem toListModel_insertIfNew! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k}
+theorem toListModel_insertIfNew! [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)] {k : α} {v : β k}
     {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) :
     (l.insertIfNew! k v).toListModel.Perm (insertEntryIfNew k v l.toListModel) := by
   simpa [insertIfNew_eq_insertIfNew!] using toListModel_insertIfNew hlb hlo
@@ -986,11 +997,11 @@ theorem toListModel_insertIfNew! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd
 ### containsThenInsertIfNew
 -/
 
-theorem ordered_containsThenInsertIfNew [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β}
+theorem ordered_containsThenInsertIfNew [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α} {v : β k} {l : Impl α β}
     (h : l.Balanced) (ho : l.Ordered) : (l.containsThenInsertIfNew k v h).2.impl.Ordered := by
   simpa only [containsThenInsertIfNew_snd_eq_insertIfNew, h] using ordered_insertIfNew h ho
 
-theorem toListModel_containsThenInsertIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α}
+theorem toListModel_containsThenInsertIfNew [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)] {k : α}
     {v : β k} {t : Impl α β} (htb : t.Balanced) (hto : t.Ordered) :
     (t.containsThenInsertIfNew k v htb).2.impl.toListModel.Perm (insertEntryIfNew k v t.toListModel) := by
   rw [containsThenInsertIfNew_snd_eq_insertIfNew]
@@ -1000,15 +1011,15 @@ theorem toListModel_containsThenInsertIfNew [Ord α] [TransOrd α] [BEq α] [Law
 ### containsThenInsertIfNew!
 -/
 
-theorem ordered_containsThenInsertIfNew! [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β}
+theorem ordered_containsThenInsertIfNew! [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α} {v : β k} {l : Impl α β}
     (h : l.Balanced) (ho : l.Ordered) : (l.containsThenInsertIfNew! k v).2.Ordered := by
   simpa [containsThenInsertIfNew!_snd_eq_insertIfNew!] using ordered_insertIfNew! h ho
 
-theorem WF.containsThenInsertIfNew! {_ : Ord α} [TransOrd α] {k : α} {v : β k} {l : Impl α β}
+theorem WF.containsThenInsertIfNew! {_ : Ord α} [LawfulLinearPreorder (.ofOrd α)] {k : α} {v : β k} {l : Impl α β}
     (h : l.WF) : (l.containsThenInsertIfNew! k v).2.WF := by
   simpa [containsThenInsertIfNew!_snd_eq_insertIfNew!] using WF.insertIfNew! (h := h)
 
-theorem toListModel_containsThenInsertIfNew! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α}
+theorem toListModel_containsThenInsertIfNew! [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)] {k : α}
     {v : β k} {t : Impl α β} (htb : t.Balanced) (hto : t.Ordered) :
     (t.containsThenInsertIfNew k v htb).2.impl.toListModel.Perm (insertEntryIfNew k v t.toListModel) := by
   rw [containsThenInsertIfNew_snd_eq_insertIfNew]
@@ -1066,7 +1077,7 @@ theorem ordered_filter [Ord α] {t : Impl α β} {h} {f : (a : α) → β a →
 ### alter
 -/
 
-theorem toListModel_alterₘ [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α]
+theorem toListModel_alterₘ [Ord α] [LawfulLinearPreorder (.ofOrd α)] [LawfulEqOrd α] [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)]
     {t : Impl α β} {a f} (htb : t.Balanced) (hto : t.Ordered) :
     List.Perm ((t.alterₘ a f htb).toListModel) (alterKey a f t.toListModel) := by
   refine toListModel_updateCell_perm _ hto ?_ alterKey_of_perm
@@ -1082,7 +1093,7 @@ theorem toListModel_alterₘ [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [L
     · simp [eraseKey]
     · simp [insertEntry, containsKey, replaceEntry]
 
-theorem alter_eq_alterₘ [Ord α] [TransOrd α] [LawfulEqOrd α] {t : Impl α β} {a f}
+theorem alter_eq_alterₘ [Ord α] [LawfulLinearPreorder (.ofOrd α)] [LawfulEqOrd α] {t : Impl α β} {a f}
     (htb : t.Balanced) (hto : t.Ordered) :
     (t.alter a f htb).impl = t.alterₘ a f htb := by
   rw [alterₘ]
@@ -1101,12 +1112,12 @@ theorem alter_eq_alterₘ [Ord α] [TransOrd α] [LawfulEqOrd α] {t : Impl α
       simp [Cell.alter, Cell.ofOption, cast]
       cases h₁ : f _ <;> rfl
 
-theorem toListModel_alter [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α]
+theorem toListModel_alter [Ord α] [LawfulLinearPreorder (.ofOrd α)] [LawfulEqOrd α] [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)]
     {t : Impl α β} {a f} (htb : t.Balanced) (hto : t.Ordered) :
     List.Perm (t.alter a f htb).impl.toListModel (alterKey a f t.toListModel) := by
   simpa only [alter_eq_alterₘ, htb, hto] using toListModel_alterₘ htb hto
 
-theorem ordered_alter [Ord α] [TransOrd α] [LawfulEqOrd α] {t : Impl α β} {a f}
+theorem ordered_alter [Ord α] [LawfulLinearPreorder (.ofOrd α)] [LawfulEqOrd α] {t : Impl α β} {a f}
     (htb : t.Balanced) (hto : t.Ordered) : (t.alter a f htb).impl.Ordered := by
   rw [alter_eq_alterₘ htb hto, alterₘ]
   exact ordered_updateCell htb hto
@@ -1131,7 +1142,7 @@ theorem alter_eq_alter! [Ord α] [LawfulEqOrd α] {t : Impl α β} {a f} (htb) :
       · exact glue_eq_glue!
       · rfl
 
-theorem toListModel_alter! [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α]
+theorem toListModel_alter! [Ord α] [LawfulLinearPreorder (.ofOrd α)] [LawfulEqOrd α] [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)]
     {t : Impl α β} {a f} (htb : t.Balanced) (hto : t.Ordered) :
     List.Perm (t.alter! a f).toListModel (alterKey a f t.toListModel) := by
   simpa only [alter_eq_alter!] using toListModel_alter htb hto
@@ -1152,11 +1163,11 @@ theorem modify_eq_alter [Ord α] [LawfulEqOrd α] {t : Impl α β} {a f}
     all_goals
       simp only [← ihl htb.left, ← ihr htb.right, balance_eq_inner hmb]
 
-theorem ordered_modify [Ord α] [TransOrd α] [LawfulEqOrd α] {t : Impl α β} {a f}
+theorem ordered_modify [Ord α] [LawfulLinearPreorder (.ofOrd α)] [LawfulEqOrd α] {t : Impl α β} {a f}
     (htb : t.Balanced) (hto : t.Ordered) : (modify a f t).Ordered :=
   modify_eq_alter htb ▸ ordered_alter htb hto
 
-theorem toListModel_modify [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α]
+theorem toListModel_modify [Ord α] [LawfulLinearPreorder (.ofOrd α)] [LawfulEqOrd α] [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)]
     {t : Impl α β} {a f} (htb : t.Balanced) (hto : t.Ordered) :
     List.Perm (modify a f t).toListModel (modifyKey a f t.toListModel) := by
   simpa only [modify_eq_alter htb, modifyKey_eq_alterKey] using toListModel_alter htb hto
@@ -1165,7 +1176,7 @@ theorem toListModel_modify [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [Law
 ### mergeWith
 -/
 
-theorem ordered_mergeWith [Ord α] [TransOrd α] [LawfulEqOrd α] {t₁ t₂ : Impl α β} {f}
+theorem ordered_mergeWith [Ord α] [LawfulLinearPreorder (.ofOrd α)] [LawfulEqOrd α] {t₁ t₂ : Impl α β} {f}
     (htb : t₁.Balanced) (hto : t₁.Ordered) :
     (t₁.mergeWith f t₂ htb).impl.Ordered := by
   induction t₂ generalizing t₁ with
@@ -1329,7 +1340,7 @@ variable {β : Type v}
 ### getThenInsertIfNew?!
 -/
 
-theorem WF.getThenInsertIfNew?! [Ord α] [TransOrd α] [LawfulEqOrd α] {k : α} {v : β} {t : Impl α β}
+theorem WF.getThenInsertIfNew?! [Ord α] [LawfulLinearPreorder (.ofOrd α)] [LawfulEqOrd α] {k : α} {v : β} {t : Impl α β}
     (h : t.WF) : (getThenInsertIfNew?! t k v).2.WF := by
   rw [getThenInsertIfNew?!.eq_def]
   cases get? t k
@@ -1340,7 +1351,7 @@ theorem WF.getThenInsertIfNew?! [Ord α] [TransOrd α] [LawfulEqOrd α] {k : α}
 ### alter
 -/
 
-theorem toListModel_alterₘ [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α β} {a f}
+theorem toListModel_alterₘ [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)] {t : Impl α β} {a f}
     (htb : t.Balanced) (hto : t.Ordered) :
     List.Perm ((alterₘ a f t htb).toListModel) (Const.alterKey a f t.toListModel) := by
   refine toListModel_updateCell_perm _ hto ?_ Const.alterKey_of_perm
@@ -1356,7 +1367,7 @@ theorem toListModel_alterₘ [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {
     · simp [eraseKey, compare_eq_iff_beq.mp this]
     · simp [insertEntry, containsKey, replaceEntry, compare_eq_iff_beq.mp this]
 
-theorem alter_eq_alterₘ [Ord α] [TransOrd α] {t : Impl α β} {a f}
+theorem alter_eq_alterₘ [Ord α] [LawfulLinearPreorder (.ofOrd α)] {t : Impl α β} {a f}
     (htb : t.Balanced) (hto : t.Ordered) :
     (alter a f t htb).impl = alterₘ a f t htb := by
   rw [alterₘ]
@@ -1375,12 +1386,12 @@ theorem alter_eq_alterₘ [Ord α] [TransOrd α] {t : Impl α β} {a f}
       simp [Cell.Const.alter, Cell.ofOption]
       cases h₁ : f _ <;> rfl
 
-theorem toListModel_alter [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α β} {a f}
+theorem toListModel_alter [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)] {t : Impl α β} {a f}
     (htb : t.Balanced) (hto : t.Ordered) :
     List.Perm (alter a f t htb).impl.toListModel (Const.alterKey a f t.toListModel) := by
   simpa only [alter_eq_alterₘ, htb, hto] using toListModel_alterₘ htb hto
 
-theorem ordered_alter [Ord α] [TransOrd α] {t : Impl α β} {a f}
+theorem ordered_alter [Ord α] [LawfulLinearPreorder (.ofOrd α)] {t : Impl α β} {a f}
     (htb : t.Balanced) (hto : t.Ordered) : (alter a f t htb).impl.Ordered := by
   rw [alter_eq_alterₘ htb hto, alterₘ]
   exact ordered_updateCell htb hto
@@ -1405,7 +1416,7 @@ theorem alter_eq_alter! [Ord α] {t : Impl α β} {a f} (htb) :
       · exact glue_eq_glue!
       · rfl
 
-theorem toListModel_alter! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α β} {a f}
+theorem toListModel_alter! [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)] {t : Impl α β} {a f}
     (htb : t.Balanced) (hto : t.Ordered) :
     List.Perm (alter! a f t).toListModel (Const.alterKey a f t.toListModel) := by
   simpa only [alter_eq_alter!] using toListModel_alter htb hto
@@ -1414,7 +1425,7 @@ theorem toListModel_alter! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t
 ### modify
 -/
 
-theorem modify_eq_alter [Ord α] [TransOrd α] {t : Impl α β} {a f}
+theorem modify_eq_alter [Ord α] [LawfulLinearPreorder (.ofOrd α)] {t : Impl α β} {a f}
     (htb : t.Balanced) :
     modify a f t = (alter a (·.map f) t htb).impl := by
   induction t with
@@ -1427,11 +1438,11 @@ theorem modify_eq_alter [Ord α] [TransOrd α] {t : Impl α β} {a f}
       dsimp
       simp only [← ihl htb.left, ← ihr htb.right, balance_eq_inner hmb]
 
-theorem ordered_modify [Ord α] [TransOrd α] {t : Impl α β} {a f}
+theorem ordered_modify [Ord α] [LawfulLinearPreorder (.ofOrd α)] {t : Impl α β} {a f}
     (htb : t.Balanced) (hto : t.Ordered) : (modify a f t).Ordered :=
   modify_eq_alter htb ▸ ordered_alter htb hto
 
-theorem toListModel_modify [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α β} {a f}
+theorem toListModel_modify [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)] {t : Impl α β} {a f}
     (htb : t.Balanced) (hto : t.Ordered) :
     List.Perm (modify a f t).toListModel (Const.modifyKey a f t.toListModel) := by
   simpa only [modify_eq_alter htb, Const.modifyKey_eq_alterKey] using toListModel_alter htb hto
@@ -1440,7 +1451,7 @@ theorem toListModel_modify [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t
 ### mergeWith
 -/
 
-theorem ordered_mergeWith [Ord α] [TransOrd α] {t₁ t₂ : Impl α β} {f}
+theorem ordered_mergeWith [Ord α] [LawfulLinearPreorder (.ofOrd α)] {t₁ t₂ : Impl α β} {f}
     (htb : t₁.Balanced) (hto : t₁.Ordered) :
     (mergeWith f t₁ t₂ htb).impl.Ordered := by
   induction t₂ generalizing t₁ with
@@ -1469,7 +1480,7 @@ end Const
 ## Deducing that well-formed trees are ordered
 -/
 
-theorem WF.ordered [Ord α] [TransOrd α] {l : Impl α β} (h : WF l) : l.Ordered := by
+theorem WF.ordered [Ord α] [LawfulLinearPreorder (.ofOrd α)] {l : Impl α β} (h : WF l) : l.Ordered := by
   induction h
   · next h => exact h
   · exact ordered_empty
@@ -1546,14 +1557,14 @@ end SameKeys
 ### getThenInsertIfNew?!
 -/
 
-theorem WF.getThenInsertIfNew?! {_ : Ord α} [TransOrd α] [LawfulEqOrd α] {k : α} {v : β k} {t : Impl α β}
+theorem WF.getThenInsertIfNew?! {_ : Ord α} [LawfulLinearPreorder (.ofOrd α)] [LawfulEqOrd α] {k : α} {v : β k} {t : Impl α β}
     (h : t.WF) : (t.getThenInsertIfNew?! k v).2.WF := by
   rw [getThenInsertIfNew?!.eq_def]
   cases get? t k
   · exact h.insertIfNew!
   · exact h
 
-theorem WF.constGetThenInsertIfNew?! {β : Type v} {_ : Ord α} [TransOrd α] {k : α} {v : β} {t : Impl α β}
+theorem WF.constGetThenInsertIfNew?! {β : Type v} {_ : Ord α} [LawfulLinearPreorder (.ofOrd α)] {k : α} {v : β} {t : Impl α β}
     (h : t.WF) : (Const.getThenInsertIfNew?! t k v).2.WF := by
   rw [Const.getThenInsertIfNew?!.eq_def]
   cases Const.get? t k
@@ -1564,7 +1575,7 @@ theorem WF.constGetThenInsertIfNew?! {β : Type v} {_ : Ord α} [TransOrd α] {k
 ### `eraseMany!`
 -/
 
-theorem WF.eraseMany! {_ : Ord α} [TransOrd α] {ρ} [ForIn Id ρ α] {l : ρ}
+theorem WF.eraseMany! {_ : Ord α} [LawfulLinearPreorder (.ofOrd α)] {ρ} [ForIn Id ρ α] {l : ρ}
     {t : Impl α β} (h : t.WF) : (t.eraseMany! l).1.WF :=
   (t.eraseMany! l).2 h (fun _ _ h' => h'.erase!)
 
@@ -1585,7 +1596,7 @@ theorem insertMany_eq_insertMany! {_ : Ord α} {l : List ((a : α) × β a)}
     (t.insertMany l h).val = (t.insertMany! l).val := by
   simp only [insertMany_eq_foldl, insertMany!_eq_foldl]
 
-theorem toListModel_insertMany_list {_ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α]
+theorem toListModel_insertMany_list {_ : Ord α} [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)] [LawfulLinearPreorder (.ofOrd α)]
     {l : List ((a : α) × β a)}
     {t : Impl α β} (h : t.WF) :
     List.Perm (t.insertMany l h.balanced).val.toListModel (t.toListModel.insertList l) := by
@@ -1597,20 +1608,20 @@ theorem toListModel_insertMany_list {_ : Ord α} [BEq α] [LawfulBEqOrd α] [Tra
     exact insertList_perm_of_perm_first (toListModel_insert! h.balanced h.ordered)
       h.insert!.ordered.distinctKeys
 
-theorem toListModel_insertMany!_list {_ : Ord α} [TransOrd α] [BEq α] [LawfulBEqOrd α]
+theorem toListModel_insertMany!_list {_ : Ord α} [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)]
     {l : List ((a : α) × β a)} {t : Impl α β} (h : t.WF) :
     List.Perm (t.insertMany! l).val.toListModel (t.toListModel.insertList l) := by
   simpa only [← insertMany_eq_insertMany! h.balanced] using toListModel_insertMany_list h
 
-theorem WF.insertMany! {_ : Ord α} [TransOrd α] {ρ} [ForIn Id ρ ((a : α) × β a)] {l : ρ}
+theorem WF.insertMany! {_ : Ord α} [LawfulLinearPreorder (.ofOrd α)] {ρ} [ForIn Id ρ ((a : α) × β a)] {l : ρ}
     {t : Impl α β} (h : t.WF) : (t.insertMany! l).1.WF :=
   (t.insertMany! l).2 h (fun _ _ _ h' => h'.insert!)
 
-theorem WF.constInsertMany! {β : Type v} {_ : Ord α} [TransOrd α] {ρ} [ForIn Id ρ (α × β)] {l : ρ}
+theorem WF.constInsertMany! {β : Type v} {_ : Ord α} [LawfulLinearPreorder (.ofOrd α)] {ρ} [ForIn Id ρ (α × β)] {l : ρ}
     {t : Impl α β} (h : t.WF) : (Const.insertMany! t l).1.WF :=
   (Const.insertMany! t l).2 h (fun _ _ _ h' => h'.insert!)
 
-theorem WF.constInsertManyIfNewUnit! {_ : Ord α} [TransOrd α] {ρ} [ForIn Id ρ α] {l : ρ}
+theorem WF.constInsertManyIfNewUnit! {_ : Ord α} [LawfulLinearPreorder (.ofOrd α)] {ρ} [ForIn Id ρ α] {l : ρ}
     {t : Impl α Unit} (h : t.WF) : (Const.insertManyIfNewUnit! t l).1.WF :=
   (Const.insertManyIfNewUnit! t l).2 h (fun _ _ h' => h'.insertIfNew!)
 
@@ -1640,7 +1651,7 @@ theorem insertMany_eq_insertMany! {_ : Ord α} {l : List (α × β)}
     (Const.insertMany t l h).val = (Const.insertMany! t l).val := by
   simp only [insertMany!_eq_foldl, insertMany_eq_foldl]
 
-theorem toListModel_insertMany_list {_ : Ord α} [BEq α] [TransOrd α] [LawfulBEqOrd α]
+theorem toListModel_insertMany_list {_ : Ord α} [BEq α] [LawfulLinearPreorder (.ofOrd α)] [LawfulPartiallyComparableBEq (.ofOrd α)]
     {l : List (α × β)} {t : Impl α β} (h : t.WF) :
     List.Perm (Const.insertMany t l h.balanced).val.toListModel (t.toListModel.insertListConst l) := by
   simp only [insertMany_eq_foldl]
@@ -1651,7 +1662,7 @@ theorem toListModel_insertMany_list {_ : Ord α} [BEq α] [TransOrd α] [LawfulB
     exact insertList_perm_of_perm_first (toListModel_insert! h.balanced h.ordered)
       h.insert!.ordered.distinctKeys
 
-theorem toListModel_insertMany!_list {_ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α]
+theorem toListModel_insertMany!_list {_ : Ord α} [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)] [LawfulLinearPreorder (.ofOrd α)]
     {l : List (α × β)} {t : Impl α β} (h : t.WF) :
     List.Perm (Const.insertMany! t l).val.toListModel (t.toListModel.insertListConst l) := by
   simpa only [← insertMany_eq_insertMany! h.balanced] using toListModel_insertMany_list h
@@ -1673,8 +1684,8 @@ theorem insertManyIfNewUnit_eq_insertManyIfNewUnit! {_ : Ord α} {l : List α}
     (Const.insertManyIfNewUnit t l h).val = (Const.insertManyIfNewUnit! t l).val := by
   simp only [insertManyIfNewUnit_eq_foldl, insertManyIfNewUnit!_eq_foldl]
 
-theorem toListModel_insertManyIfNewUnit_list {_ : Ord α} [TransOrd α] [instBEq : BEq α]
-    [LawfulBEqOrd α] {l : List α} {t : Impl α Unit} (h : t.WF) :
+theorem toListModel_insertManyIfNewUnit_list {_ : Ord α} [LawfulLinearPreorder (.ofOrd α)] [instBEq : BEq α]
+    [LawfulPartiallyComparableBEq (.ofOrd α)] {l : List α} {t : Impl α Unit} (h : t.WF) :
     List.Perm (Const.insertManyIfNewUnit t l h.balanced).val.toListModel
       (t.toListModel.insertListIfNewUnit l) := by
   simp only [insertManyIfNewUnit_eq_foldl]
@@ -1685,7 +1696,7 @@ theorem toListModel_insertManyIfNewUnit_list {_ : Ord α} [TransOrd α] [instBEq
     exact insertListIfNewUnit_perm_of_perm_first (toListModel_insertIfNew! h.balanced h.ordered)
       h.insertIfNew!.ordered.distinctKeys
 
-theorem toListModel_insertManyIfNewUnit!_list {_ : Ord α} [TransOrd α] [BEq α] [LawfulBEqOrd α]
+theorem toListModel_insertManyIfNewUnit!_list {_ : Ord α} [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)]
     {l : List α} {t : Impl α Unit} (h : t.WF) :
     List.Perm (Const.insertManyIfNewUnit! t l).val.toListModel (t.toListModel.insertListIfNewUnit l) := by
   simpa only [← insertManyIfNewUnit_eq_insertManyIfNewUnit! h.balanced] using
@@ -1826,7 +1837,7 @@ theorem WF.map [Ord α] {t : Impl α β} {f : (a : α) → β a → γ a} (h : t
 ### `minEntry?`
 -/
 
-theorem minEntry?ₘ_eq_minEntry? [Ord α] [TransOrd α] {l : Impl α β} (hlo : l.Ordered) :
+theorem minEntry?ₘ_eq_minEntry? [Ord α] [LawfulLinearPreorder (.ofOrd α)] {l : Impl α β} (hlo : l.Ordered) :
     l.minEntry?ₘ = List.minEntry? l.toListModel := by
   rw [minEntry?ₘ, applyPartition_eq_apply_toListModel' hlo]
   simp only [List.append_assoc, reduceCtorEq, imp_false, implies_true, forall_const]
@@ -1839,26 +1850,26 @@ theorem minEntry?ₘ_eq_minEntry? [Ord α] [TransOrd α] {l : Impl α β} (hlo :
       contradiction
   rw [hc, List.nil_append, List.nil_append, minEntry?_eq_head? (by simpa [hc] using h₂)]
 
-theorem minEntry?_eq_minEntry? [Ord α] [TransOrd α] {l : Impl α β} (hlo : l.Ordered) :
+theorem minEntry?_eq_minEntry? [Ord α] [LawfulLinearPreorder (.ofOrd α)] {l : Impl α β} (hlo : l.Ordered) :
     l.minEntry? = List.minEntry? l.toListModel := by
   rw [minEntry?_eq_minEntry?ₘ, minEntry?ₘ_eq_minEntry? hlo]
 
-theorem minKey?_eq_minKey? {_ : Ord α} [TransOrd α] {l : Impl α β} (hlo : l.Ordered) :
+theorem minKey?_eq_minKey? {_ : Ord α} [LawfulLinearPreorder (.ofOrd α)] {l : Impl α β} (hlo : l.Ordered) :
     l.minKey? = List.minKey? l.toListModel := by
   simp only [minKey?_eq_minEntry?_map_fst, minEntry?_eq_minEntry? hlo, List.minKey?]
 
-theorem minKey_eq_minKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : Impl α β}
+theorem minKey_eq_minKey [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)] {l : Impl α β}
     (hlo : l.Ordered) {he} :
     l.minKey he = List.minKey l.toListModel (isEmpty_eq_isEmpty ▸ he) := by
   simp [minKey_eq_get_minKey?, minKey_eq_minEntry_fst, minEntry_eq_get_minEntry?,
     minEntry?_eq_minEntry? hlo, List.minKey?, Option.get_map]
 
-theorem minKey!_eq_minKey! [Ord α] [TransOrd α] [Inhabited α] [BEq α] [LawfulBEqOrd α]
+theorem minKey!_eq_minKey! [Ord α] [LawfulLinearPreorder (.ofOrd α)] [Inhabited α] [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)]
     {l : Impl α β} (hlo : l.Ordered) :
     l.minKey! = List.minKey! l.toListModel := by
   simp [Impl.minKey!_eq_get!_minKey?, List.minKey!_eq_get!_minKey?, minKey?_eq_minKey? hlo]
 
-theorem minKeyD_eq_minKeyD [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : Impl α β}
+theorem minKeyD_eq_minKeyD [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)] {l : Impl α β}
     (hlo : l.Ordered) {fallback} :
     l.minKeyD fallback = List.minKeyD l.toListModel fallback := by
   simp [Impl.minKeyD_eq_getD_minKey?, List.minKeyD_eq_getD_minKey?, minKey?_eq_minKey? hlo]
@@ -1872,31 +1883,31 @@ theorem Ordered.reverse [Ord α] {t : Impl α β} (h : t.Ordered) :
   simp only [Ordered, toListModel_reverse]
   exact List.pairwise_reverse.mpr h
 
-theorem maxEntry?_eq_minEntry? [o : Ord α] [to : TransOrd α] {t : Impl α β} (hlo : t.Ordered) :
+theorem maxEntry?_eq_minEntry? [o : Ord α] [to : LawfulLinearPreorder (.ofOrd α)] {t : Impl α β} (hlo : t.Ordered) :
     t.maxEntry? = (letI := o.opposite; List.minEntry? t.toListModel) := by
   rw [maxEntry?_eq_minEntry?_reverse, @minEntry?_eq_minEntry? _ _ (_) _ _ hlo.reverse]
-  apply @List.minEntry?_of_perm _ _ o.opposite to.opposite (@beqOfOrd _ o.opposite)
+  apply @List.minEntry?_of_perm _ _ o.opposite inferInstance (@beqOfOrd _ o.opposite)
   · exact @hlo.reverse.distinctKeys _ _ (@beqOfOrd _ o.opposite) (_) _
   · rw [toListModel_reverse]
     exact List.reverse_perm t.toListModel
 
-theorem maxKey?_eq_maxKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α β}
+theorem maxKey?_eq_maxKey? [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)] {t : Impl α β}
     (hlo : t.Ordered) :
     t.maxKey? = List.maxKey? t.toListModel := by
   rw [maxKey?_of_perm hlo.distinctKeys (List.reverse_perm t.toListModel).symm, List.maxKey?]
   rw [maxKey?_eq_minKey?_reverse, minKey?_eq_minKey? hlo.reverse, toListModel_reverse]
 
-theorem maxKey_eq_maxKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α β}
+theorem maxKey_eq_maxKey [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)] {t : Impl α β}
     (hlo : t.Ordered) {he} :
     t.maxKey he = List.maxKey t.toListModel (isEmpty_eq_isEmpty ▸ he) := by
   simp only [List.maxKey_eq_get_maxKey?, maxKey_eq_get_maxKey?, maxKey?_eq_maxKey? hlo]
 
-theorem maxKey!_eq_maxKey! [Ord α] [TransOrd α] [Inhabited α] [BEq α] [LawfulBEqOrd α]
+theorem maxKey!_eq_maxKey! [Ord α] [LawfulLinearPreorder (.ofOrd α)] [Inhabited α] [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)]
     {t : Impl α β} (hlo : t.Ordered) :
     t.maxKey! = List.maxKey! t.toListModel := by
   simp only [List.maxKey!_eq_get!_maxKey?, maxKey!_eq_get!_maxKey?, maxKey?_eq_maxKey? hlo]
 
-theorem maxKeyD_eq_maxKeyD [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α β}
+theorem maxKeyD_eq_maxKeyD [Ord α] [LawfulLinearPreorder (.ofOrd α)] [BEq α] [LawfulPartiallyComparableBEq (.ofOrd α)] {t : Impl α β}
     (hlo : t.Ordered) {fallback} :
     t.maxKeyD fallback = List.maxKeyD t.toListModel fallback := by
   simp only [List.maxKeyD_eq_getD_maxKey?, maxKeyD_eq_getD_maxKey?, maxKey?_eq_maxKey? hlo]
@@ -1982,7 +1993,7 @@ end Const
 ### `getEntryLE?` / `getKeyLE?` / ...
 -/
 
-theorem getEntryGE?_eq_find? [Ord α] [TransOrd α] {t : Impl α β} (hto : t.Ordered) {k : α} :
+theorem getEntryGE?_eq_find? [Ord α] [LawfulLinearPreorder (.ofOrd α)] {t : Impl α β} (hto : t.Ordered) {k : α} :
     t.getEntryGE? k = t.toListModel.find? (fun e => (compare e.1 k).isGE) := by
   rw [getEntryGE?_eq_getEntryGE?ₘ, getEntryGE?ₘ, applyPartition_eq hto, List.head?_filter,
     List.findCell_inner]
@@ -2005,20 +2016,20 @@ theorem getEntryGE?_eq_find? [Ord α] [TransOrd α] {t : Impl α β} (hto : t.Or
     · rfl
     · exact ih hto.2
 
-theorem getEntryGT?_eq_find? [Ord α] [TransOrd α] {t : Impl α β} (hto : t.Ordered) {k : α} :
+theorem getEntryGT?_eq_find? [Ord α] [LawfulLinearPreorder (.ofOrd α)] {t : Impl α β} (hto : t.Ordered) {k : α} :
     t.getEntryGT? k = t.toListModel.find? (fun e => (compare e.1 k).isGT) := by
   rw [getEntryGT?_eq_getEntryGT?ₘ, getEntryGT?ₘ, applyPartition_eq hto, List.head?_filter]
   congr; funext x; rw [Bool.eq_iff_iff, beq_iff_eq, Ordering.isGT_iff_eq_gt]
   simp [OrientedCmp.eq_swap (a := k), Ordering.then_eq_lt]
 
-theorem getEntryLE?_eq_findRev? [Ord α] [TransOrd α] {t : Impl α β} (hto : t.Ordered) {k : α} :
+theorem getEntryLE?_eq_findRev? [Ord α] [LawfulLinearPreorder (.ofOrd α)] {t : Impl α β} (hto : t.Ordered) {k : α} :
     getEntryLE? k t = t.toListModel.findRev? (fun e => (compare e.1 k).isLE) := by
   rw [getEntryLE?_eq_getEntryGE?_reverse, @getEntryGE?_eq_find?, List.findRev?_eq_find?_reverse,
     toListModel_reverse]
   · simp only [Ord.opposite, Bool.coe_iff_coe.mp OrientedCmp.isGE_iff_isLE]
   · exact hto.reverse
 
-theorem getEntryLT?_eq_findRev? [Ord α] [TransOrd α] {t : Impl α β} (hto : t.Ordered) {k : α} :
+theorem getEntryLT?_eq_findRev? [Ord α] [LawfulLinearPreorder (.ofOrd α)] {t : Impl α β} (hto : t.Ordered) {k : α} :
     getEntryLT? k t = t.toListModel.findRev? (fun e => (compare e.1 k).isLT) := by
   rw [getEntryLT?_eq_getEntryGT?_reverse, @getEntryGT?_eq_find?, List.findRev?_eq_find?_reverse,
     toListModel_reverse]

src/Std/Data/DTreeMap/Lemmas.lean

@@ -7,6 +7,7 @@ prelude
 import Std.Data.DTreeMap.Internal.Lemmas
 import Std.Data.DTreeMap.Basic
 import Std.Data.DTreeMap.AdditionalOperations
+import Std.Classes.Ord.New.PartiallyComparable
 
 /-!
 # Dependent tree map lemmas
@@ -35,7 +36,7 @@ theorem isEmpty_emptyc : (∅ : DTreeMap α β cmp).isEmpty :=
   Impl.isEmpty_empty
 
 @[simp, grind =]
-theorem isEmpty_insert [TransCmp cmp] {k : α} {v : β k} :
+theorem isEmpty_insert [LawfulLinearPreorder (.ofCmp cmp)] {k : α} {v : β k} :
     (t.insert k v).isEmpty = false :=
   Impl.isEmpty_insert t.wf
 
@@ -3127,16 +3128,16 @@ theorem minKey_eq_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {he km} :
     t.minKey he = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE :=
   Impl.minKey_eq_iff_mem_and_forall t.wf
 
-@[grind =] theorem minKey_insert [TransCmp cmp] {k v} :
+@[grind =] theorem minKey_insert [LawfulLinearPreorder (.ofCmp cmp)] {k v} :
     (t.insert k v).minKey isEmpty_insert =
       t.minKey?.elim k fun k' => if cmp k k' |>.isLE then k else k' :=
   Impl.minKey_insert t.wf
 
-theorem minKey_insert_le_minKey [TransCmp cmp] {k v he} :
+theorem minKey_insert_le_minKey [LawfulLinearPreorder (.ofCmp cmp)] {k v he} :
     cmp (t.insert k v |>.minKey isEmpty_insert) (t.minKey he) |>.isLE :=
   Impl.minKey_insert_le_minKey t.wf
 
-theorem minKey_insert_le_self [TransCmp cmp] {k v} :
+theorem minKey_insert_le_self [LawfulLinearPreorder (.ofCmp cmp)] {k v} :
     cmp (t.insert k v |>.minKey isEmpty_insert) k |>.isLE :=
   Impl.minKey_insert_le_self t.wf
 
@@ -3769,12 +3770,12 @@ theorem maxKey_eq_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {he km} :
     t.maxKey he = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE :=
   Impl.maxKey_eq_iff_mem_and_forall t.wf
 
-@[grind =] theorem maxKey_insert [TransCmp cmp] {k v} :
+@[grind =] theorem maxKey_insert [LawfulLinearPreorder (.ofCmp cmp)] {k v} :
     (t.insert k v).maxKey isEmpty_insert =
       t.maxKey?.elim k fun k' => if cmp k' k |>.isLE then k else k' :=
   Impl.maxKey_insert t.wf
 
-theorem maxKey_le_maxKey_insert [TransCmp cmp] {k v he} :
+theorem maxKey_le_maxKey_insert [LawfulLinearPreorder (.ofCmp cmp)] {k v he} :
     cmp (t.maxKey he) (t.insert k v |>.maxKey isEmpty_insert) |>.isLE :=
   Impl.maxKey_le_maxKey_insert t.wf
 

src/Std/Data/Internal/Cut.lean

@@ -5,6 +5,7 @@ Authors: Markus Himmel
 -/
 prelude
 import Std.Classes.Ord.Basic
+import Std.Classes.Ord.New.PartiallyComparable
 
 set_option autoImplicit false
 
@@ -35,24 +36,24 @@ theorem IsStrictCut.lt_of_isLE_of_lt [IsStrictCut cmp cut] {k k' : α} :
   | lt => exact fun _ => IsCut.lt h₁
   | eq => exact fun h₂ h₃ => by rw [← h₃, IsStrictCut.eq (cmp := cmp) k 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₁))
-  eq _ _ := TransCmp.congr_left
+instance [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α} : IsStrictCut compare (compare k) where
+  lt := sorry -- TransCmp.lt_trans
+  gt h₁ h₂ := sorry -- OrientedCmp.gt_of_lt (TransCmp.lt_trans (OrientedCmp.lt_of_gt h₂)
+    -- (OrientedCmp.lt_of_gt h₁))
+  eq _ _ := sorry -- TransCmp.congr_left
 
 instance [Ord α] : IsStrictCut (compare : α → α → Ordering) (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
-  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')
+instance [Ord α] [LawfulLinearPreorder (.ofOrd α)] {k : α} : IsStrictCut compare fun k' => (compare k k').then .gt where
+  lt {_ _} := sorry -- by simpa [Ordering.then_eq_lt] using TransCmp.lt_trans
+  eq {_ _} := sorry -- by simp [Ordering.then_eq_eq]
+  gt h h' := sorry -- 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')
 
 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}