remove accidentally added file

This reverts commit cd87828c8806169846e59dffc5d7431af68eb699.

src/Init/Core.lean

@@ -2499,12 +2499,17 @@ class Antisymm (r : α → α → Prop) : Prop where
   /-- An antisymmetric relation `r` satisfies `r a b → r b a → a = b`. -/
   antisymm (a b : α) : r a b → r b a → a = b
 
-/-- `Asymm X r` means that the binary relation `r` on `X` is asymmetric, that is,
+/-- `Asymm r` means that the binary relation `r` is asymmetric, that is,
 `r a b → ¬ r b a`. -/
 class Asymm (r : α → α → Prop) : Prop where
   /-- An asymmetric relation satisfies `r a b → ¬ r b a`. -/
   asymm : ∀ a b, r a b → ¬r b a
 
+/-- `Symm r` means that the binary relation `r` is symmetric, that is, `r a b → r b a`.  -/
+class Symm (r : α → α → Prop) : Prop where
+  /-- A symmetric relation satisfies `r a b → r b a`. -/
+  symm : ∀ a b, r a b → r b a
+
 /-- `Total X r` means that the binary relation `r` on `X` is total, that is, that for any
 `x y : X` we have `r x y` or `r y x`. -/
 class Total (r : α → α → Prop) : Prop where

src/Init/Data.lean

@@ -25,7 +25,7 @@ public import Init.Data.SInt
 public import Init.Data.Float
 public import Init.Data.Float32
 public import Init.Data.Option
-public import Init.Data.Ord
+public import Init.Data.OrdRoot
 public import Init.Data.Random
 public import Init.Data.ToString
 public import Init.Data.Range

src/Init/Data/Array/QSort/Basic.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Data.Vector.Basic
-public import Init.Data.Ord
+public import Init.Data.Ord.Basic
 
 public section
 

src/Init/Data/BEq.lean

@@ -23,11 +23,14 @@ class PartialEquivBEq (α) [BEq α] : Prop where
   /-- Transitivity for `BEq`. If `a == b` and `b == c` then `a == c`. -/
   trans : (a : α) == b → b == c → a == c
 
+instance [BEq α] [PartialEquivBEq α] : Std.Symm (α := α) (· == ·) where
+  symm _ _ h := PartialEquivBEq.symm h
+
 /-- `EquivBEq` says that the `BEq` implementation is an equivalence relation. -/
 class EquivBEq (α) [BEq α] : Prop extends PartialEquivBEq α, ReflBEq α
 
-theorem BEq.symm [BEq α] [PartialEquivBEq α] {a b : α} : a == b → b == a :=
-  PartialEquivBEq.symm
+theorem BEq.symm [BEq α] [Std.Symm (α := α) (· == ·)] {a b : α} : a == b → b == a :=
+  Std.Symm.symm a b (r := (· == ·))
 
 theorem BEq.comm [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = (b == a) :=
   Bool.eq_iff_iff.2 ⟨BEq.symm, BEq.symm⟩

src/Init/Data/Int/Compare.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro, Paul Reichert
 module
 
 prelude
-public import all Init.Data.Ord
+public import all Init.Data.Ord.Basic
 public import Init.Data.Int.Order
 
 public section

src/Init/Data/List/MinMax.lean

@@ -147,7 +147,11 @@ theorem min?_replicate [Min α] [Std.IdempotentOp (min : α → α → α)] {n :
   simp [min?_replicate, Nat.ne_of_gt h]
 
 /--
-Requirements are satisfied for `[OrderData α] [Min α] [IsLinearOrder α] [LawfulOrderMin α]`
+This lemma is also applicable given the following instances:
+
+```
+[LE α] [Min α] [IsLinearOrder α] [LawfulOrderMin α]
+```
 -/
 theorem foldl_min [Min α] [Std.IdempotentOp (min : α → α → α)] [Std.Associative (min : α → α → α)]
     {l : List α} {a : α} : l.foldl (init := a) min = min a (l.min?.getD a) := by
@@ -284,7 +288,11 @@ theorem max?_replicate [Max α] [Std.IdempotentOp (max : α → α → α)] {n :
   simp [max?_replicate, Nat.ne_of_gt h]
 
 /--
-Requirements are satisfied for `[OrderData α] [Max α] [LinearOrder α] [LawfulOrderMax α]`
+This lemma is also applicable given the following instances:
+
+```
+[LE α] [Min α] [IsLinearOrder α] [LawfulOrderMax α]
+```
 -/
 theorem foldl_max [Max α] [Std.IdempotentOp (max : α → α → α)] [Std.Associative (max : α → α → α)]
     {l : List α} {a : α} : l.foldl (init := a) max = max a (l.max?.getD a) := by

src/Init/Data/Nat/Compare.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 module
 
 prelude
-public import all Init.Data.Ord
+public import all Init.Data.Ord.Basic
 
 public section
 

src/Init/Data/Ord/Basic.lean

@@ -204,6 +204,7 @@ instance [DecidablePred p] : Decidable (∃ o : Ordering, p o) :=
 theorem eq_eq_of_isLE_of_isLE_swap : ∀ {o : Ordering}, o.isLE → o.swap.isLE → o = .eq := by decide
 theorem eq_eq_of_isGE_of_isGE_swap : ∀ {o : Ordering}, o.isGE → o.swap.isGE → o = .eq := by decide
 theorem eq_eq_of_isLE_of_isGE : ∀ {o : Ordering}, o.isLE → o.isGE → o = .eq := by decide
+theorem eq_eq_iff_isLE_and_isGE : ∀ {o : Ordering}, o = .eq ↔ o.isLE ∧ o.isGE := by decide
 theorem eq_swap_iff_eq_eq : ∀ {o : Ordering}, o = o.swap ↔ o = .eq := by decide
 theorem eq_eq_of_eq_swap : ∀ {o : Ordering}, o = o.swap → o = .eq := eq_swap_iff_eq_eq.mp
 

src/Init/Data/Ord/BitVec.lean

@@ -6,7 +6,7 @@ Authors: Markus Himmel, Paul Reichert, Robin Arnez
 module
 
 prelude
-public import Std.Classes.Ord.Basic
+public import Init.Data.Order.Ord
 public import Init.Data.BitVec.Lemmas
 
 public section

src/Init/Data/Ord/SInt.lean

@@ -6,7 +6,7 @@ Authors: Markus Himmel, Paul Reichert, Robin Arnez
 module
 
 prelude
-public import Std.Classes.Ord.Basic
+public import Init.Data.Order.Ord
 public import Init.Data.SInt.Lemmas
 
 public section

src/Init/Data/Ord/String.lean

@@ -6,7 +6,7 @@ Authors: Markus Himmel, Paul Reichert, Robin Arnez
 module
 
 prelude
-public import Std.Classes.Ord.Basic
+public import Init.Data.Order.Ord
 public import Init.Data.String.Lemmas
 
 public section

src/Init/Data/Ord/UInt.lean

@@ -6,7 +6,7 @@ Authors: Markus Himmel, Paul Reichert, Robin Arnez
 module
 
 prelude
-public import Std.Classes.Ord.Basic
+public import Init.Data.Order.Ord
 public import Init.Data.UInt.Lemmas
 
 public section

src/Init/Data/Ord/Vector.lean

@@ -6,7 +6,7 @@ Authors: Markus Himmel, Paul Reichert, Robin Arnez
 module
 
 prelude
-public import Std.Classes.Ord.Basic
+public import Init.Data.Order.Ord
 public import Init.Data.Vector.Lemmas
 
 public section

src/Init/Data/OrdRoot.lean

@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+public import Init.Data.Ord.Basic
+public import Init.Data.Ord.BitVec
+public import Init.Data.Ord.SInt
+public import Init.Data.Ord.String
+public import Init.Data.Ord.UInt
+public import Init.Data.Ord.Vector

src/Init/Data/Order.lean

@@ -6,7 +6,11 @@ Authors: Paul Reichert
 module
 
 prelude
+public import Init.Data.Order.Ord
 public import Init.Data.Order.Classes
+public import Init.Data.Order.ClassesExtra
 public import Init.Data.Order.Lemmas
+public import Init.Data.Order.LemmasExtra
 public import Init.Data.Order.Factories
+public import Init.Data.Order.FactoriesExtra
 public import Init.Data.Subtype.Order

src/Init/Data/Order/Classes.lean

@@ -96,6 +96,13 @@ public class LawfulOrderLT (α : Type u) [LT α] [LE α] where
 
 end LT
 
+section BEq
+
+public class LawfulOrderBEq (α : Type u) [BEq α] [LE α] where
+  beq_iff_le_and_ge : ∀ a b : α, a == b ↔ a ≤ b ∧ b ≤ a
+
+end BEq
+
 section Min
 
 /--

src/Init/Data/Order/ClassesExtra.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.Order.Classes
+public import Init.Data.Ord.Basic
+
+namespace Std
+
+/--
+This typeclass states that the synthesized `Ord α` instance is compatible with the `LE α`
+instance. This means that according to `compare`, the following are equivalent:
+
+* `a` is less than or equal to `b` according to `compare`.
+* `b` is greater than or equal to `b` according to `compare`.
+* `a ≤ b` holds.
+
+`LawfulOrderOrd α` automatically entails that `Ord α` is oriented (see `OrientedOrd α`)
+and that `LE α` is total.
+
+`Ord α` and `LE α` mutually determine each other in the presence of `LawfulOrderOrd α`.
+-/
+public class LawfulOrderOrd (α : Type u) [Ord α] [LE α] where
+  isLE_compare : ∀ a b : α, (compare a b).isLE ↔ a ≤ b
+  isGE_compare : ∀ a b : α, (compare a b).isGE ↔ b ≤ a
+
+end Std

src/Init/Data/Order/Factories.lean

@@ -66,15 +66,19 @@ public theorem IsLinearOrder.of_le {α : Type u} [LE α]
   le_antisymm := le_antisymm.antisymm
 
 /--
-Returns a `LawfulOrderLT α` instance given certain properties.
-
-If an `OrderData α` instance is compatible with an `LE α` instance, then this lemma derives
-a `LawfulOrderLT α` instance from a property relating the `LE α` and `LT α` instances.
+This lemma derives a `LawfulOrderLT α` instance from a property involving an `LE α` instance.
 -/
 public theorem LawfulOrderLT.of_le {α : Type u} [LT α] [LE α]
     (lt_iff : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬ b ≤ a) : LawfulOrderLT α where
   lt_iff := lt_iff
 
+/--
+This lemma derives a `LawfulOrderBEq α` instance from a property involving an `LE α` instance.
+-/
+public theorem LawfulOrderBEq.of_le {α : Type u} [BEq α] [LE α]
+    (beq_iff : ∀ a b : α, a == b ↔ a ≤ b ∧ b ≤ a) : LawfulOrderBEq α where
+  beq_iff_le_and_ge := by simp [beq_iff]
+
 /--
 This lemma characterizes in terms of `LE α` when a `Min α` instance "behaves like an infimum
 operator".
@@ -188,7 +192,7 @@ public theorem LawfulOrderInf.of_lt {α : Type u} [Min α] [LT α]
       simpa [Decidable.imp_iff_not_or] using min_lt_iff a b c }
 
 /--
-Derives a `LawfulOrderMin α` instance for `OrderData.ofLT` from two properties involving
+Derives a `LawfulOrderMin α` instance for `LE.ofLT` from two properties involving
 `LT α` and `Min α` instances.
 
 The produced instance entails `LawfulOrderInf α` and `MinEqOr α`.
@@ -204,7 +208,7 @@ public theorem LawfulOrderMin.of_lt {α : Type u} [Min α] [LT α]
 
 /--
 This lemma characterizes in terms of `LT α` when a `Max α` instance
-"behaves like an supremum operator" with respect to `OrderData.ofLT α`.
+"behaves like an supremum operator" with respect to `LE.ofLT α`.
 -/
 public def LawfulOrderSup.of_lt {α : Type u} [Max α] [LT α]
     (lt_max_iff : ∀ a b c : α, c < max a b ↔ c < a ∨ c < b) :
@@ -217,7 +221,7 @@ public def LawfulOrderSup.of_lt {α : Type u} [Max α] [LT α]
       simpa [Decidable.imp_iff_not_or] using lt_max_iff a b c }
 
 /--
-Derives a `LawfulOrderMax α` instance for `OrderData.ofLT` from two properties involving `LT α` and
+Derives a `LawfulOrderMax α` instance for `LE.ofLT` from two properties involving `LT α` and
 `Max α` instances.
 
 The produced instance entails `LawfulOrderSup α` and `MaxEqOr α`.

src/Init/Data/Order/FactoriesExtra.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.Order.ClassesExtra
+public import Init.Data.Order.Ord
+
+namespace Std
+
+/--
+Creates an `LE α` instance from an `Ord α` instance.
+
+`OrientedOrd α` must be satisfied so that the resulting `LE α` instance faithfully represents
+the `Ord α` instance.
+-/
+public def LE.ofOrd (α : Type u) [Ord α] : LE α where
+  le a b := (compare a b).isLE
+
+/--
+The `LE α` instance obtained from an `Ord α` instance is compatible with said `Ord α`
+instance if `compare` is oriented, i.e., `compare a b = .lt ↔ compare b a = .gt`.
+-/
+public instance LawfulOrderOrd.of_ord (α : Type u) [Ord α] [OrientedOrd α] :
+    haveI := LE.ofOrd α
+    LawfulOrderOrd α :=
+  letI := LE.ofOrd α
+  { isLE_compare := by simp [LE.ofOrd]
+    isGE_compare := by simp [LE.ofOrd, OrientedCmp.isGE_eq_isLE] }
+
+end Std

src/Init/Data/Order/Lemmas.lean

@@ -9,7 +9,8 @@ prelude
 public import Init.Data.Order.Classes
 public import Init.Data.Order.Factories
 import Init.SimpLemmas
-import Init.Classical
+public import Init.Classical
+public import Init.Data.BEq
 
 namespace Std
 
@@ -35,7 +36,7 @@ public theorem Asymm.total_not {r : α → α → Prop} [i : Asymm r] : Total (
     · exact Or.inl hab
 
 public instance {α : Type u} [LE α] [IsPartialOrder α] :
-    Std.Antisymm (α := α) (· ≤ ·) where
+    Antisymm (α := α) (· ≤ ·) where
   antisymm := IsPartialOrder.le_antisymm
 
 public instance {α : Type u} [LE α] [IsPreorder α] :
@@ -43,12 +44,12 @@ public instance {α : Type u} [LE α] [IsPreorder α] :
       trans := IsPreorder.le_trans _ _ _
 
 public instance {α : Type u} [LE α] [IsPreorder α] :
-    Std.Refl (α := α) (· ≤ ·) where
-  refl a := IsPreorder.le_refl a
+    Refl (α := α) (· ≤ ·) where
+  refl := IsPreorder.le_refl
 
 public instance {α : Type u} [LE α] [IsLinearPreorder α] :
-    Std.Total (α := α) (· ≤ ·) where
-  total a b := IsLinearPreorder.le_total a b
+    Total (α := α) (· ≤ ·) where
+  total := IsLinearPreorder.le_total
 
 end AxiomaticInstances
 
@@ -59,7 +60,7 @@ public theorem le_refl {α : Type u} [LE α] [Refl (α := α) (· ≤ ·)] (a :
 
 public theorem le_antisymm {α : Type u} [LE α] [Std.Antisymm (α := α) (· ≤ ·)] {a b : α}
     (hab : a ≤ b) (hba : b ≤ a) : a = b :=
-  Std.Antisymm.antisymm _ _ hab hba
+  Antisymm.antisymm _ _ hab hba
 
 public theorem le_trans {α : Type u} [LE α] [Trans (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·)] {a b c : α}
     (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c :=
@@ -69,22 +70,6 @@ public theorem le_total {α : Type u} [LE α] [Std.Total (α := α) (· ≤ ·)]
     a ≤ b ∨ b ≤ a :=
   Std.Total.total a b
 
-public instance {α : Type u} [LE α] [IsPreorder α] :
-    Refl (α := α) (· ≤ ·) where
-  refl := IsPreorder.le_refl
-
-public instance {α : Type u} [LE α] [IsPreorder α] :
-    Trans (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·) where
-  trans := IsPreorder.le_trans _ _ _
-
-public instance {α : Type u} [LE α] [IsLinearPreorder α] :
-    Total (α := α) (· ≤ ·) where
-  total := IsLinearPreorder.le_total
-
-public instance {α : Type u} [LE α] [IsPartialOrder α] :
-    Antisymm (α := α) (· ≤ ·) where
-  antisymm := IsPartialOrder.le_antisymm
-
 end LE
 
 section LT
@@ -111,9 +96,8 @@ public instance {α : Type u} [LT α] [LE α] [LawfulOrderLT α] :
 public instance {α : Type u} [LT α] [LE α] [IsPreorder α] [LawfulOrderLT α] :
     Std.Irrefl (α := α) (· < ·) := inferInstance
 
-public instance {α : Type u} [LT α] [LE α]
-    [Trans (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·) ] [LawfulOrderLT α] :
-    Trans (α := α) (· < ·) (· < ·) (· < ·) where
+public instance {α : Type u} [LT α] [LE α] [Trans (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·) ]
+    [LawfulOrderLT α] : Trans (α := α) (· < ·) (· < ·) (· < ·) where
   trans {a b c} hab hbc := by
     simp only [lt_iff_le_and_not_ge] at hab hbc ⊢
     apply And.intro
@@ -172,6 +156,45 @@ public instance instLawfulOrderLT {α : Type u} [LE α] :
 
 end Classical.Order
 
+namespace Std
+section BEq
+
+public theorem beq_iff_le_and_ge {α : Type u} [BEq α] [LE α] [LawfulOrderBEq α]
+    {a b : α} : a == b ↔ a ≤ b ∧ b ≤ a := by
+  simp [LawfulOrderBEq.beq_iff_le_and_ge]
+
+public instance {α : Type u} [BEq α] [LE α] [LawfulOrderBEq α] :
+    Symm (α := α) (· == ·) where
+  symm := by simp_all [beq_iff_le_and_ge]
+
+public instance {α : Type u} [BEq α] [LE α] [LawfulOrderBEq α] [IsPreorder α] : EquivBEq α where
+  rfl := by simp [beq_iff_le_and_ge, le_refl]
+  symm := Symm.symm (r := (· == ·)) _ _
+  trans hab hbc := by
+    simp only [beq_iff_le_and_ge] at hab hbc ⊢
+    exact ⟨le_trans hab.1 hbc.1, le_trans hbc.2 hab.2⟩
+
+public instance {α : Type u} [BEq α] [LE α] [LawfulOrderBEq α] [IsPartialOrder α] :
+    LawfulBEq α where
+  eq_of_beq := by
+    simp only [beq_iff_le_and_ge, and_imp]
+    apply le_antisymm
+
+end BEq
+end Std
+
+namespace Classical.Order
+open Std
+
+public noncomputable scoped instance instBEq {α : Type u} [LE α] : BEq α where
+  beq a b := a ≤ b ∧ b ≤ a
+
+public instance instLawfulOrderBEq {α : Type u} [LE α] :
+    LawfulOrderBEq α where
+  beq_iff_le_and_ge a b := by simp [BEq.beq]
+
+end Classical.Order
+
 namespace Std
 section Min
 
@@ -205,7 +228,6 @@ public theorem min_eq_or {α : Type u} [Min α] [MinEqOr α] {a b : α} :
 public instance {α : Type u} [LE α] [Min α] [IsLinearOrder α] [LawfulOrderInf α] :
     MinEqOr α where
   min_eq_or a b := by
-    open Classical.Order in
     cases le_total (a := a) (b := b)
     · apply Or.inl
       apply le_antisymm
@@ -246,7 +268,6 @@ public instance {α : Type u} [Min α] [MinEqOr α] :
     Std.IdempotentOp (min : α → α → α) where
   idempotent a := by cases MinEqOr.min_eq_or a a <;> assumption
 
-open Classical.Order in
 public instance {α : Type u} [LE α] [Min α] [IsLinearOrder α] [LawfulOrderMin α] :
     Std.Associative (min : α → α → α) where
   assoc a b c := by apply le_antisymm <;> simp [min_le, le_min_iff, le_refl]
@@ -284,7 +305,6 @@ public theorem max_eq_or {α : Type u} [Max α] [MaxEqOr α] {a b : α} :
 public instance {α : Type u} [LE α] [Max α] [IsLinearOrder α] [LawfulOrderSup α] :
     MaxEqOr α where
   max_eq_or a b := by
-    open Classical.Order in
     cases le_total (a := a) (b := b)
     · apply Or.inr
       apply le_antisymm
@@ -328,7 +348,6 @@ public instance {α : Type u} [Max α] [MaxEqOr α] :
     Std.IdempotentOp (max : α → α → α) where
   idempotent a := by cases MaxEqOr.max_eq_or a a <;> assumption
 
-open Classical.Order in
 public instance {α : Type u} [LE α] [Max α] [IsLinearOrder α] [LawfulOrderMax α] :
     Std.Associative (max : α → α → α) where
   assoc a b c := by

src/Init/Data/Order/LemmasExtra.lean

@@ -0,0 +1,178 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+import Init.Data.Order.Lemmas
+public import Init.Data.Order.FactoriesExtra
+public import Init.Data.Order.Ord
+
+namespace Std
+
+public theorem isLE_compare {α : Type u} [Ord α] [LE α] [LawfulOrderOrd α]
+    {a b : α} : (compare a b).isLE ↔ a ≤ b := by
+  simp [← LawfulOrderOrd.isLE_compare]
+
+public theorem isGE_compare {α : Type u} [Ord α] [LE α] [LawfulOrderOrd α]
+    {a b : α} : (compare a b).isGE ↔ b ≤ a := by
+  simp [← LawfulOrderOrd.isGE_compare]
+
+public theorem compare_eq_lt {α : Type u} [Ord α] [LT α] [LE α] [LawfulOrderOrd α] [LawfulOrderLT α]
+    {a b : α} : compare a b = .lt ↔ a < b := by
+  rw [LawfulOrderLT.lt_iff, ← LawfulOrderOrd.isLE_compare, ← LawfulOrderOrd.isGE_compare]
+  cases compare a b <;> simp
+
+public theorem compare_eq_gt {α : Type u} [Ord α] [LT α] [LE α] [LawfulOrderOrd α] [LawfulOrderLT α]
+    {a b : α} : compare a b = .gt ↔ b < a := by
+  rw [LawfulOrderLT.lt_iff, ← LawfulOrderOrd.isGE_compare, ← LawfulOrderOrd.isLE_compare]
+  cases compare a b <;> simp
+
+public theorem compare_eq_eq {α : Type u} [Ord α] [BEq α] [LE α] [LawfulOrderOrd α] [LawfulOrderBEq α]
+    {a b : α} : compare a b = .eq ↔ a == b := by
+  open Classical.Order in
+  rw [LawfulOrderBEq.beq_iff_le_and_ge, ← isLE_compare, ← isGE_compare]
+  cases compare a b <;> simp
+
+public instance {α : Type u} [LE α] [Ord α] [LawfulOrderOrd α] : OrientedOrd α where
+  eq_swap := by
+    open Classical.Order in
+    intro a b
+    apply Eq.symm
+    cases h : compare a b
+    · rw [compare_eq_lt] at h
+      simpa [Ordering.swap_eq_lt, compare_eq_gt] using h
+    · rw [compare_eq_eq] at h
+      simpa [Ordering.swap_eq_eq, compare_eq_eq] using BEq.symm h
+    · rw [compare_eq_gt] at h
+      simpa [Ordering.swap_eq_gt, compare_eq_lt] using h
+
+public instance {α : Type u} [Ord α] [LE α] [LawfulOrderOrd α] [IsPreorder α] : TransOrd α where
+  isLE_trans := by
+    simp only [isLE_compare]
+    apply le_trans
+
+public instance {α : Type u} [Ord α] [BEq α] [LE α] [LawfulOrderOrd α] [LawfulOrderBEq α] :
+    LawfulBEqOrd α where
+  compare_eq_iff_beq := by
+    simp [Ordering.eq_eq_iff_isLE_and_isGE, isLE_compare, isGE_compare, beq_iff_le_and_ge]
+
+public instance {α : Type u} [Ord α] [LE α] [LawfulOrderOrd α] [IsPartialOrder α] : LawfulEqOrd α where
+  eq_of_compare {a b} := by
+    intro h
+    apply le_antisymm
+    · simp [← isLE_compare, h]
+    · simp [← isGE_compare, h]
+
+public instance [Ord α] [LE α] [LawfulOrderOrd α] :
+    Total (α := α) (· ≤ ·) where
+  total a b := by
+    rw [← isLE_compare, ← isGE_compare]
+    cases compare a b <;> simp
+
+public theorem IsLinearPreorder.of_ord {α : Type u} [LE α] [Ord α] [LawfulOrderOrd α]
+    [TransOrd α] : IsLinearPreorder α where
+  le_refl a := by simp [← isLE_compare]
+  le_trans a b c := by simpa [← isLE_compare] using TransOrd.isLE_trans
+  le_total a b := Total.total a b
+
+public theorem IsLinearOrder.of_ord {α : Type u} [LE α] [Ord α] [LawfulOrderOrd α]
+    [TransOrd α] [LawfulEqOrd α] : IsLinearOrder α where
+  toIsLinearPreorder := .of_ord
+  le_antisymm a b hab hba := by
+    apply LawfulEqOrd.eq_of_compare
+    rw [← isLE_compare] at hab
+    rw [← isGE_compare] at hba
+    rw [Ordering.eq_eq_iff_isLE_and_isGE, hab, hba, and_self]
+
+/--
+This lemma derives a `LawfulOrderLT α` instance from a property involving an `Ord α` instance.
+-/
+public instance LawfulOrderLT.of_ord (α : Type u) [Ord α] [LT α] [LE α] [LawfulOrderOrd α]
+    (lt_iff_compare_eq_lt : ∀ a b : α, a < b ↔ compare a b = .lt) :
+    LawfulOrderLT α where
+  lt_iff a b := by
+    simp +contextual [lt_iff_compare_eq_lt, ← isLE_compare (a := a), ← isGE_compare (a := a)]
+
+/--
+This lemma derives a `LawfulOrderBEq α` instance from a property involving an `Ord α` instance.
+-/
+public instance LawfulOrderBEq.of_ord (α : Type u) [Ord α] [BEq α] [LE α] [LawfulOrderOrd α]
+    (beq_iff_compare_eq_eq : ∀ a b : α, a == b ↔ compare a b = .eq) :
+    LawfulOrderBEq α where
+  beq_iff_le_and_ge := by
+    simp [beq_iff_compare_eq_eq, Ordering.eq_eq_iff_isLE_and_isGE, isLE_compare, isGE_compare]
+
+/--
+This lemma derives a `LawfulOrderInf α` instance from a property involving an `Ord α` instance.
+-/
+public instance LawfulOrderInf.of_ord (α : Type u) [Ord α] [Min α] [LE α] [LawfulOrderOrd α]
+    (compare_min_isLE_iff : ∀ a b c : α,
+        (compare a (min b c)).isLE ↔ (compare a b).isLE ∧ (compare a c).isLE) :
+    LawfulOrderInf α where
+  le_min_iff := by simpa [isLE_compare] using compare_min_isLE_iff
+
+/--
+This lemma derives a `LawfulOrderMin α` instance from a property involving an `Ord α` instance.
+-/
+public instance LawfulOrderMin.of_ord (α : Type u) [Ord α] [Min α] [LE α] [LawfulOrderOrd α]
+    (compare_min_isLE_iff : ∀ a b c : α,
+        (compare a (min b c)).isLE ↔ (compare a b).isLE ∧ (compare a c).isLE)
+    (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b) :
+    LawfulOrderMin α where
+  toLawfulOrderInf := .of_ord α compare_min_isLE_iff
+  min_eq_or := min_eq_or
+
+/--
+This lemma derives a `LawfulOrderSup α` instance from a property involving an `Ord α` instance.
+-/
+public instance LawfulOrderSup.of_ord (α : Type u) [Ord α] [Max α] [LE α] [LawfulOrderOrd α]
+    (compare_max_isLE_iff : ∀ a b c : α,
+        (compare (max a b) c).isLE ↔ (compare a c).isLE ∧ (compare b c).isLE) :
+    LawfulOrderSup α where
+  max_le_iff := by simpa [isLE_compare] using compare_max_isLE_iff
+
+/--
+This lemma derives a `LawfulOrderMax α` instance from a property involving an `Ord α` instance.
+-/
+public instance LawfulOrderMax.of_ord (α : Type u) [Ord α] [Max α] [LE α] [LawfulOrderOrd α]
+    (compare_max_isLE_iff : ∀ a b c : α,
+        (compare (max a b) c).isLE ↔ (compare a c).isLE ∧ (compare b c).isLE)
+    (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) :
+    LawfulOrderMax α where
+  toLawfulOrderSup := .of_ord α compare_max_isLE_iff
+  max_eq_or := max_eq_or
+
+end Std
+
+namespace Classical.Order
+open Std
+
+/--
+Derives an `Ord α` instance from an `LE α` instance. Because all elements are comparable with
+`compare`, the resulting `Ord α` instance only makes sense if `LE α` is total.
+-/
+public noncomputable scoped instance instOrd {α : Type u} [LE α] :
+    Ord α where
+  compare a b := if a ≤ b then if b ≤ a then .eq else .lt else .gt
+
+public instance instLawfulOrderOrd {α : Type u} [LE α]
+    [Total (α := α) (· ≤ ·)] :
+    LawfulOrderOrd α where
+  isLE_compare a b := by
+    simp only [compare]
+    by_cases a ≤ b <;> rename_i h
+    · simp only [h, ↓reduceIte, iff_true]
+      split <;> simp
+    · simp [h]
+  isGE_compare a b := by
+    simp only [compare]
+    cases Total.total (r := (· ≤ ·)) a b <;> rename_i h
+    · simp only [h, ↓reduceIte]
+      split <;> simp [*]
+    · simp only [h, ↓reduceIte, iff_true]
+      split <;> simp
+
+end Classical.Order

src/Init/Data/Order/Ord.lean

@@ -6,7 +6,7 @@ Authors: Markus Himmel, Paul Reichert, Robin Arnez
 module
 
 prelude
-public import Init.Data.Ord
+public import Init.Data.Ord.Basic
 
 public section
 

src/Init/Data/Subtype/Order.lean

@@ -12,83 +12,81 @@ public import Init.Data.Order.Lemmas
 import Init.Data.Order.Factories
 import Init.Data.Subtype.Basic
 
-namespace Std
+namespace Subtype
+open Std
 
-public instance {α : Type u} [LE α] {P : α → Prop} : LE (Subtype P) where
+public instance instLE {α : Type u} [LE α] {P : α → Prop} : LE (Subtype P) where
   le a b := a.val ≤ b.val
 
-public instance {α : Type u} [LT α] {P : α → Prop} : LT (Subtype P) where
+public instance instLT {α : Type u} [LT α] {P : α → Prop} : LT (Subtype P) where
   lt a b := a.val < b.val
 
-public instance {α : Type u} [LT α] [LE α] [LawfulOrderLT α]
+public instance instLawfulOrderLT {α : Type u} [LT α] [LE α] [LawfulOrderLT α]
     {P : α → Prop} : LawfulOrderLT (Subtype P) where
   lt_iff a b := by simp [LT.lt, LE.le, LawfulOrderLT.lt_iff]
 
-public instance {α : Type u} [BEq α] {P : α → Prop} : BEq (Subtype P) where
-  beq a b := a.val == b.val
-
-public instance {α : Type u} [Min α] [MinEqOr α] {P : α → Prop} : Min (Subtype P) where
+public instance instMin {α : Type u} [Min α] [MinEqOr α] {P : α → Prop} : Min (Subtype P) where
   min a b := ⟨Min.min a.val b.val, MinEqOr.elim a.property b.property⟩
 
-public instance {α : Type u} [Max α] [MaxEqOr α] {P : α → Prop} : Max (Subtype P) where
+public instance instMax {α : Type u} [Max α] [MaxEqOr α] {P : α → Prop} : Max (Subtype P) where
   max a b := ⟨max a.val b.val, MaxEqOr.elim a.property b.property⟩
 
-public instance {α : Type u} [LE α] [i : Refl (α := α) (· ≤ ·)] {P : α → Prop} :
+public instance instReflLE {α : Type u} [LE α] [i : Refl (α := α) (· ≤ ·)] {P : α → Prop} :
     Refl (α := Subtype P) (· ≤ ·) where
   refl a := i.refl a.val
 
-public instance {α : Type u} [LE α] [i : Antisymm (α := α) (· ≤ ·)] {P : α → Prop} :
+public instance instAntisymmLE {α : Type u} [LE α] [i : Antisymm (α := α) (· ≤ ·)] {P : α → Prop} :
     Antisymm (α := Subtype P) (· ≤ ·) where
   antisymm a b hab hba := private Subtype.ext <| i.antisymm a.val b.val hab hba
 
-public instance {α : Type u} [LE α] [i : Total (α := α) (· ≤ ·)] {P : α → Prop} :
+public instance instTotalLE {α : Type u} [LE α] [i : Total (α := α) (· ≤ ·)] {P : α → Prop} :
     Total (α := Subtype P) (· ≤ ·) where
   total a b := i.total a.val b.val
 
-public instance {α : Type u} [LE α] [i : Trans (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·)]
+public instance instTransLE {α : Type u} [LE α] [i : Trans (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·)]
     {P : α → Prop} :
     Trans (α := Subtype P) (· ≤ ·) (· ≤ ·) (· ≤ ·) where
   trans := i.trans
 
-public instance {α : Type u} [Min α] [MinEqOr α] {P : α → Prop} :
+public instance instMinEqOr {α : Type u} [Min α] [MinEqOr α] {P : α → Prop} :
     MinEqOr (Subtype P) where
   min_eq_or a b := by
     cases min_eq_or (a := a.val) (b := b.val) <;> rename_i h
     · exact Or.inl <| Subtype.ext h
     · exact Or.inr <| Subtype.ext h
 
-public instance {α : Type u} [LE α] [Min α] [LawfulOrderMin α] {P : α → Prop} :
+public instance instLawfulOrderMin {α : Type u} [LE α] [Min α] [LawfulOrderMin α] {P : α → Prop} :
     LawfulOrderMin (Subtype P) where
   le_min_iff _ _ _ := by
     exact le_min_iff (α := α)
 
-public instance {α : Type u} [Max α] [MaxEqOr α] {P : α → Prop} :
+public instance instMaxEqOr {α : Type u} [Max α] [MaxEqOr α] {P : α → Prop} :
     MaxEqOr (Subtype P) where
   max_eq_or a b := by
     cases max_eq_or (a := a.val) (b := b.val) <;> rename_i h
     · exact Or.inl <| Subtype.ext h
     · exact Or.inr <| Subtype.ext h
 
-public instance {α : Type u} [LE α] [Max α] [LawfulOrderMax α] {P : α → Prop} :
+public instance instLawfulOrderMax {α : Type u} [LE α] [Max α] [LawfulOrderMax α] {P : α → Prop} :
     LawfulOrderMax (Subtype P) where
   max_le_iff _ _ _ := by
     open Classical.Order in
     exact max_le_iff (α := α)
 
-public instance {α : Type u} [LE α] [IsPreorder α] {P : α → Prop} :
+public instance instIsPreorder {α : Type u} [LE α] [IsPreorder α] {P : α → Prop} :
     IsPreorder (Subtype P) :=
   IsPreorder.of_le
 
-public instance {α : Type u} [LE α] [IsLinearPreorder α] {P : α → Prop} :
+public instance instIsLinearPreorder {α : Type u} [LE α] [IsLinearPreorder α] {P : α → Prop} :
     IsLinearPreorder (Subtype P) :=
   IsLinearPreorder.of_le
 
-public instance {α : Type u} [LE α] [IsPartialOrder α] {P : α → Prop} :
+public instance instIsPartialOrder {α : Type u} [LE α] [IsPartialOrder α] {P : α → Prop} :
     IsPartialOrder (Subtype P) :=
   IsPartialOrder.of_le
 
-public instance {α : Type u} [LE α] [IsLinearOrder α] {P : α → Prop} :
+public instance instIsLinearOrder {α : Type u} [LE α] [IsLinearOrder α] {P : α → Prop} :
     IsLinearOrder (Subtype P) :=
   IsLinearOrder.of_le
 
-end Std
+end Subtype

src/Init/Data/Subtype/OrderExtra.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Data.Subtype.Order
-public import Init.Data.Ord
+public import Init.Data.Ord.Basic
 
 public instance {α : Type u} [Ord α] {P : α → Prop} : Ord (Subtype P) where
   compare a b := compare a.val b.val

src/Init/Grind/Ordered/Linarith.lean

@@ -8,7 +8,7 @@ prelude
 public import Init.Grind.Ordered.Module
 public import Init.Grind.Ordered.Ring
 public import Init.Grind.Ring.Field
-public import all Init.Data.Ord
+public import all Init.Data.Ord.Basic
 public import all Init.Data.AC
 public import Init.Data.RArray
 

src/Init/Grind/Ring/Poly.lean

@@ -9,7 +9,7 @@ prelude
 public import Init.Data.Nat.Lemmas
 public import Init.Data.Int.LemmasAux
 public import Init.Data.Hashable
-public import all Init.Data.Ord
+public import all Init.Data.Ord.Basic
 public import Init.Data.RArray
 public import Init.Grind.Ring.Basic
 public import Init.Grind.Ring.Field

src/Init/System/IO.lean

@@ -9,7 +9,7 @@ prelude
 public import Init.System.IOError
 public import Init.System.FilePath
 public import Init.System.ST
-public import Init.Data.Ord
+public import Init.Data.Ord.Basic
 public import Init.Data.String.Extra
 
 public section

src/Lean/Data/Name.lean

@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Ord
+public import Init.Data.Ord.Basic
 
 public section
 namespace Lean

src/Lean/Data/RBMap.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Ord
+public import Init.Data.Ord.Basic
 public import Init.Data.Nat.Linear
 
 public section

src/Std.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich
 -/
 prelude
-import Std.Classes
 import Std.Data
 import Std.Do
 import Std.Sat

src/Std/Classes.lean

@@ -1,11 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Paul Reichert
--/
-module
-
-prelude
-public import Std.Classes.Ord
-
-public section

src/Std/Classes/Ord.lean

@@ -1,16 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-module
-
-prelude
-public import Std.Classes.Ord.Basic
-public import Std.Classes.Ord.SInt
-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 section

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

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.AC
+public import Init.Data.Ord.Basic
 public import Std.Data.DTreeMap.Internal.Balanced
 
 @[expose] public section

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

@@ -6,7 +6,6 @@ Authors: Markus Himmel
 module
 
 prelude
-public import Std.Classes.Ord.Basic
 public import Std.Data.Internal.List.Associative
 
 @[expose] public section

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

@@ -6,7 +6,7 @@ Authors: Markus Himmel
 module
 
 prelude
-public import Std.Classes.Ord.Basic
+public import Init.Data.SInt.Basic
 
 @[expose] public section
 

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

@@ -9,7 +9,6 @@ prelude
 public import Init.Data.Nat.Compare
 public import Std.Data.DTreeMap.Internal.Balancing
 public import Std.Data.DTreeMap.Internal.Queries
-public import Std.Classes.Ord.Basic
 
 @[expose] public section
 

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

@@ -6,7 +6,6 @@ Authors: Markus Himmel
 module
 
 prelude
-public import Std.Classes.Ord.Basic
 public import Std.Data.DTreeMap.Internal.Def
 public import Std.Data.Internal.Cut
 

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

@@ -10,7 +10,6 @@ public import Init.Data.Nat.Compare
 public import Std.Data.DTreeMap.Internal.Def
 public import Std.Data.DTreeMap.Internal.Balanced
 public import Std.Data.DTreeMap.Internal.Ordered
-public import Std.Classes.Ord.Basic
 
 @[expose] public section
 

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

@@ -8,7 +8,6 @@ module
 prelude
 public import Init.Data.Option.List
 public import Init.Data.Array.Bootstrap
-public import Std.Classes.Ord.Basic
 public import Std.Data.DTreeMap.Internal.Model
 public import Std.Data.Internal.Cut
 import all Std.Data.Internal.List.Associative

src/Std/Data/DTreeMap/Lemmas.lean

@@ -6,7 +6,7 @@ Authors: Markus Himmel, Paul Reichert
 module
 
 prelude
-public import Std.Data.DTreeMap.Internal.Lemmas
+import Std.Data.DTreeMap.Internal.Lemmas
 public import Std.Data.DTreeMap.Basic
 public import Std.Data.DTreeMap.AdditionalOperations
 

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

@@ -6,7 +6,7 @@ Authors: Markus Himmel, Paul Reichert
 module
 
 prelude
-public import Std.Data.DTreeMap.Internal.Lemmas
+import Std.Data.DTreeMap.Internal.Lemmas
 public import Std.Data.DTreeMap.Raw.Basic
 public import Std.Data.DTreeMap.Raw.AdditionalOperations
 
@@ -1630,12 +1630,22 @@ theorem get_insertMany_list_of_mem [TransCmp cmp] (h : t.WF)
     get (insertMany t l) k' h' = v :=
   Impl.Const.get_insertMany!_list_of_mem h k_eq distinct mem
 
+/-- A variant of `contains_of_contains_insertMany_list` used in `get_insertMany_list`. -/
+theorem contains_of_contains_insertMany_list' [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
+    {l : List (α × β)} {k : α}
+    (h' : contains (insertMany t l) k = true)
+    (w : l.findSomeRev? (fun ⟨a, b⟩ => if cmp a k = .eq then some b else none) = none) :
+    contains t k = true :=
+  Impl.Const.contains_of_contains_insertMany_list' h
+    (by simpa [Impl.Const.insertMany_eq_insertMany!] using h')
+    (by simpa [compare_eq_iff_beq, BEq.comm] using w)
+
 @[grind =] theorem get_insertMany_list [TransCmp cmp] [BEq α] [PartialEquivBEq α] [LawfulBEqCmp cmp] (h : t.WF)
     {l : List (α × β)} {k : α} {h'} :
     get (insertMany t l) k h' =
       match w : l.findSomeRev? (fun ⟨a, b⟩ => if cmp a k = .eq then some b else none) with
       | some v => v
-      | none => get t k (Impl.Const.contains_of_contains_insertMany_list' h (by simpa [Impl.Const.insertMany_eq_insertMany!] using h') w) :=
+      | none => get t k (contains_of_contains_insertMany_list' h h' w) :=
   Impl.Const.get_insertMany!_list h (k := k)
 
 theorem get!_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]

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

@@ -6,7 +6,7 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Std.Data.DTreeMap.Internal.Lemmas
+import Std.Data.DTreeMap.Internal.Lemmas
 public import Std.Data.DTreeMap.Raw.AdditionalOperations
 public import Std.Data.DTreeMap.Raw.Basic
 

src/Std/Data/Internal/Cut.lean

@@ -6,7 +6,7 @@ Authors: Markus Himmel
 module
 
 prelude
-public import Std.Classes.Ord.Basic
+public import Init.Data.Order.Ord
 
 @[expose] public section
 

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

@@ -14,7 +14,7 @@ public import Init.Data.List.Find
 public import Init.Data.List.MinMax
 public import Init.Data.List.Monadic
 public import all Std.Data.Internal.List.Defs
-public import Std.Classes.Ord.Basic
+public import Init.Data.Order.Ord
 import Init.Data.Subtype.Order
 import Init.Data.Order.Lemmas
 

src/Std/Data/TreeMap/Lemmas.lean

@@ -6,7 +6,7 @@ Authors: Markus Himmel, Paul Reichert
 module
 
 prelude
-public import Std.Data.DTreeMap.Lemmas
+import Std.Data.DTreeMap.Lemmas
 public import Std.Data.TreeMap.Basic
 public import Std.Data.TreeMap.AdditionalOperations
 

src/Std/Data/TreeMap/Raw/Lemmas.lean

@@ -6,7 +6,7 @@ Authors: Markus Himmel, Paul Reichert
 module
 
 prelude
-public import Std.Data.DTreeMap.Raw.Lemmas
+import Std.Data.DTreeMap.Raw.Lemmas
 public import Std.Data.TreeMap.Raw.Basic
 public import Std.Data.TreeMap.Raw.AdditionalOperations
 

src/Std/Data/TreeSet/Lemmas.lean

@@ -6,7 +6,8 @@ Authors: Markus Himmel, Paul Reichert
 module
 
 prelude
-public import Std.Data.TreeMap.Lemmas
+import Std.Data.TreeMap.Lemmas
+import Std.Data.DTreeMap.Lemmas
 public import Std.Data.TreeSet.Basic
 public import Std.Data.TreeSet.AdditionalOperations
 

src/Std/Data/TreeSet/Raw/Lemmas.lean

@@ -6,7 +6,8 @@ Authors: Markus Himmel, Paul Reichert
 module
 
 prelude
-public import Std.Data.TreeMap.Raw.Lemmas
+import Std.Data.TreeMap.Raw.Lemmas
+import Std.Data.DTreeMap.Raw.Lemmas
 public import Std.Data.TreeSet.Raw.Basic
 
 @[expose] public section

src/Std/Time/Internal/Bounded.lean

@@ -8,7 +8,7 @@ module
 prelude
 public import Init.Omega
 public import Init.Data.Int.DivMod.Lemmas
-public import Std.Classes.Ord.Basic
+public import Init.Data.Order.Ord
 
 @[expose] public section
 

src/Std/Time/Internal/UnitVal.lean

@@ -6,7 +6,7 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Classes.Ord.Basic
+public import Init.Data.Order.Ord
 public import Std.Internal.Rat
 
 @[expose] public section

src/lake/Lake/Util/Date.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 prelude
-import Init.Data.Ord
+import Init.Data.Ord.Basic
 
 /-!
 #  Date

src/lake/Lake/Util/Name.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 prelude
-import Std.Classes.Ord.String
-import Std.Classes.Ord.UInt
+import Init.Data.Ord.String
+import Init.Data.Ord.UInt
 import Lean.Data.Json
 import Lean.Data.NameMap.Basic
 import Lake.Util.RBArray