feat: Ord-related instances for various types (#7687)

This PR provides `Inhabited`, `Ord` (if missing), `TransOrd`, `LawfulEqOrd` and `LawfulBEqOrd` instances for various types, namely `Bool`, `String`, `Nat`, `Int`, `UIntX`, `Option`, `Prod` and date/time types. It also adds a few related theorems, especially about how the `Ord` instance for `Int` relates to `LE` and `LT`. --------- Co-authored-by: Paul Reichert <datokrat@users.noreply.github.com>
2025-03-28 14:31:09 +01:00 · 2025-03-28 14:31:09 +01:00 · d7f5d9a67a
commit d7f5d9a67a
parent 4e51487b1c
27 changed files with 940 additions and 73 deletions
--- a/src/Init/Data/Int/Compare.lean
+++ b/src/Init/Data/Int/Compare.lean
@ -0,0 +1,74 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro, Paul Reichert
+-/
+prelude
+import Init.Data.Ord
+import Init.Data.Int.Order
+
+/-! # Basic lemmas about comparing integers
+
+This file introduces some basic lemmas about `compare` as applied to integers.
+
+Import `Std.Classes.Ord` in order to obtain the `TransOrd` and `LawfulEqOrd` instances for `Int`.
+-/
+namespace Int
+
+protected theorem lt_or_eq_of_le {n m : Int} (h : n ≤ m) : n < m ∨ n = m := by
+  omega
+
+protected theorem le_iff_lt_or_eq {n m : Int} : n ≤ m ↔ n < m ∨ n = m :=
+  ⟨Int.lt_or_eq_of_le, fun | .inl h => Int.le_of_lt h | .inr rfl => Int.le_refl _⟩
+
+theorem compare_eq_ite_lt (a b : Int) :
+    compare a b = if a < b then .lt else if b < a then .gt else .eq := by
+  simp only [compare, compareOfLessAndEq]
+  split
+  · rfl
+  · next h =>
+    match Int.lt_or_eq_of_le (Int.not_lt.1 h) with
+    | .inl h => simp [h, Int.ne_of_gt h]
+    | .inr rfl => simp
+
+theorem compare_eq_ite_le (a b : Int) :
+    compare a b = if a ≤ b then if b ≤ a then .eq else .lt else .gt := by
+  rw [compare_eq_ite_lt]
+  split
+  · next hlt => simp [Int.le_of_lt hlt, Int.not_le.2 hlt]
+  · next hge =>
+    split
+    · next hgt => simp [Int.le_of_lt hgt, Int.not_le.2 hgt]
+    · next hle => simp [Int.not_lt.1 hge, Int.not_lt.1 hle]
+
+protected theorem compare_swap (a b : Int) : (compare a b).swap = compare b a := by
+  simp only [compare_eq_ite_le]; (repeat' split) <;> try rfl
+  next h1 h2 => cases h1 (Int.le_of_not_le h2)
+
+protected theorem compare_eq_eq {a b : Int} : compare a b = .eq ↔ a = b := by
+  rw [compare_eq_ite_lt]; (repeat' split) <;> simp [Int.ne_of_lt, Int.ne_of_gt, *]
+  next hlt hgt => exact Int.le_antisymm (Int.not_lt.1 hgt) (Int.not_lt.1 hlt)
+
+protected theorem compare_eq_lt {a b : Int} : compare a b = .lt ↔ a < b := by
+  rw [compare_eq_ite_lt]; (repeat' split) <;> simp [*]
+
+protected theorem compare_eq_gt {a b : Int} : compare a b = .gt ↔ b < a := by
+  rw [compare_eq_ite_lt]; (repeat' split) <;> simp [Int.le_of_lt, *]
+
+protected theorem compare_ne_gt {a b : Int} : compare a b ≠ .gt ↔ a ≤ b := by
+  rw [compare_eq_ite_le]; (repeat' split) <;> simp [*]
+
+protected theorem compare_ne_lt {a b : Int} : compare a b ≠ .lt ↔ b ≤ a := by
+  rw [compare_eq_ite_le]; (repeat' split) <;> simp [Int.le_of_not_le, *]
+
+protected theorem isLE_compare {a b : Int} :
+    (compare a b).isLE ↔ a ≤ b := by
+  simp only [Int.compare_eq_ite_le]
+  repeat' split <;> simp_all
+
+protected theorem isGE_compare {a b : Int} :
+    (compare a b).isGE ↔ b ≤ a := by
+  rw [← Int.compare_swap, Ordering.isGE_swap]
+  exact Int.isLE_compare
+
+end Int
--- a/src/Init/Data/Nat/Compare.lean
+++ b/src/Init/Data/Nat/Compare.lean
@ -4,17 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 prelude
-import Init.Classical
 import Init.Data.Ord

 /-! # Basic lemmas about comparing natural numbers

 This file introduce some basic lemmas about compare as applied to natural
 numbers.
+
+Import `Std.Classes.Ord` in order to obtain the `TransOrd` and `LawfulEqOrd` instances for `Nat`.
 -/
 namespace Nat

-theorem compare_def_lt (a b : Nat) :
+theorem compare_eq_ite_lt (a b : Nat) :
    compare a b = if a < b then .lt else if b < a then .gt else .eq := by
  simp only [compare, compareOfLessAndEq]
  split
@ -24,9 +25,12 @@ theorem compare_def_lt (a b : Nat) :
    | .inl h => simp [h, Nat.ne_of_gt h]
    | .inr rfl => simp

-theorem compare_def_le (a b : Nat) :
+@[deprecated compare_eq_ite_lt (since := "2025-03_28")]
+def compare_def_lt := compare_eq_ite_lt
+
+theorem compare_eq_ite_le (a b : Nat) :
    compare a b = if a ≤ b then if b ≤ a then .eq else .lt else .gt := by
-  rw [compare_def_lt]
+  rw [compare_eq_ite_lt]
  split
  · next hlt => simp [Nat.le_of_lt hlt, Nat.not_le.2 hlt]
  · next hge =>
@ -34,24 +38,37 @@ theorem compare_def_le (a b : Nat) :
    · next hgt => simp [Nat.le_of_lt hgt, Nat.not_le.2 hgt]
    · next hle => simp [Nat.not_lt.1 hge, Nat.not_lt.1 hle]

+@[deprecated compare_eq_ite_le (since := "2025-03_28")]
+def compare_def_le := compare_eq_ite_le
+
 protected theorem compare_swap (a b : Nat) : (compare a b).swap = compare b a := by
-  simp only [compare_def_le]; (repeat' split) <;> try rfl
+  simp only [compare_eq_ite_le]; (repeat' split) <;> try rfl
  next h1 h2 => cases h1 (Nat.le_of_not_le h2)

 protected theorem compare_eq_eq {a b : Nat} : compare a b = .eq ↔ a = b := by
-  rw [compare_def_lt]; (repeat' split) <;> simp [Nat.ne_of_lt, Nat.ne_of_gt, *]
+  rw [compare_eq_ite_lt]; (repeat' split) <;> simp [Nat.ne_of_lt, Nat.ne_of_gt, *]
  next hlt hgt => exact Nat.le_antisymm (Nat.not_lt.1 hgt) (Nat.not_lt.1 hlt)

 protected theorem compare_eq_lt {a b : Nat} : compare a b = .lt ↔ a < b := by
-  rw [compare_def_lt]; (repeat' split) <;> simp [*]
+  rw [compare_eq_ite_lt]; (repeat' split) <;> simp [*]

 protected theorem compare_eq_gt {a b : Nat} : compare a b = .gt ↔ b < a := by
-  rw [compare_def_lt]; (repeat' split) <;> simp [Nat.le_of_lt, *]
+  rw [compare_eq_ite_lt]; (repeat' split) <;> simp [Nat.le_of_lt, *]

 protected theorem compare_ne_gt {a b : Nat} : compare a b ≠ .gt ↔ a ≤ b := by
-  rw [compare_def_le]; (repeat' split) <;> simp [*]
+  rw [compare_eq_ite_le]; (repeat' split) <;> simp [*]

 protected theorem compare_ne_lt {a b : Nat} : compare a b ≠ .lt ↔ b ≤ a := by
-  rw [compare_def_le]; (repeat' split) <;> simp [Nat.le_of_not_le, *]
+  rw [compare_eq_ite_le]; (repeat' split) <;> simp [Nat.le_of_not_le, *]
+
+protected theorem isLE_compare {a b : Nat} :
+    (compare a b).isLE ↔ a ≤ b := by
+  simp only [Nat.compare_eq_ite_le]
+  repeat' split <;> simp_all
+
+protected theorem isGE_compare {a b : Nat} :
+    (compare a b).isGE ↔ b ≤ a := by
+  rw [← Nat.compare_swap, Ordering.isGE_swap]
+  exact Nat.isLE_compare

 end Nat
--- a/src/Init/Data/Ord.lean
+++ b/src/Init/Data/Ord.lean
@ -304,6 +304,27 @@ theorem then_eq_eq {o₁ o₂ : Ordering} : o₁.then o₂ = eq ↔ o₁ = eq
 theorem then_eq_gt {o₁ o₂ : Ordering} : o₁.then o₂ = gt ↔ o₁ = gt ∨ o₁ = eq ∧ o₂ = gt := by
  cases o₁ <;> cases o₂ <;> decide

+@[simp]
+theorem lt_then {o : Ordering} : lt.then o = lt := rfl
+
+@[simp]
+theorem gt_then {o : Ordering} : gt.then o = gt := rfl
+
+@[simp]
+theorem eq_then {o : Ordering} : eq.then o = o := rfl
+
+theorem isLE_then_iff_or {o₁ o₂ : Ordering} : (o₁.then o₂).isLE ↔ o₁ = lt ∨ (o₁ = eq ∧ o₂.isLE) := by
+  cases o₁ <;> simp
+
+theorem isLE_then_iff_and {o₁ o₂ : Ordering} : (o₁.then o₂).isLE ↔ o₁.isLE ∧ (o₁ = lt ∨ o₂.isLE) := by
+  cases o₁ <;> simp
+
+theorem isLE_left_of_isLE_then {o₁ o₂ : Ordering} (h : (o₁.then o₂).isLE) : o₁.isLE := by
+  cases o₁ <;> simp_all
+
+theorem isGE_left_of_isGE_then {o₁ o₂ : Ordering} (h : (o₁.then o₂).isGE) : o₁.isGE := by
+  cases o₁ <;> simp_all
+
 end Lemmas

 end Ordering
@ -345,6 +366,104 @@ To lexicographically combine two `Ordering`s, use `Ordering.then`.
@[inline] def compareLex (cmp₁ cmp₂ : α → β → Ordering) (a : α) (b : β) : Ordering :=
  (cmp₁ a b).then (cmp₂ a b)

+section Lemmas
+
+@[simp]
+theorem compareLex_eq_eq {α} {cmp₁ cmp₂} {a b : α} :
+    compareLex cmp₁ cmp₂ a b = .eq ↔ cmp₁ a b = .eq ∧ cmp₂ a b = .eq := by
+  simp [compareLex, Ordering.then_eq_eq]
+
+theorem compareOfLessAndEq_eq_swap_of_lt_iff_not_gt_and_ne {α : Type u} [LT α] [DecidableLT α] [DecidableEq α]
+    (h : ∀ x y : α, x < y ↔ ¬ y < x ∧ x ≠ y) {x y : α} :
+    compareOfLessAndEq x y = (compareOfLessAndEq y x).swap := by
+  simp only [compareOfLessAndEq]
+  split
+  · rename_i h'
+    rw [h] at h'
+    simp only [h'.1, h'.2.symm, reduceIte, Ordering.swap_gt]
+  · split
+    · rename_i h'
+      have : ¬ y < y := Not.imp (·.2 rfl) <| (h y y).mp
+      simp only [h', this, reduceIte, Ordering.swap_eq]
+    · rename_i h' h''
+      replace h' := (h y x).mpr ⟨h', Ne.symm h''⟩
+      simp only [h', Ne.symm h'', reduceIte, Ordering.swap_lt]
+
+theorem lt_iff_not_gt_and_ne_of_antisymm_of_total_of_not_le
+    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α]
+    (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y)
+    (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) (not_le : ∀ {x y : α}, ¬ x ≤ y ↔ y < x) (x y : α) :
+    x < y ↔ ¬ y < x ∧ x ≠ y := by
+  simp only [← not_le, Classical.not_not]
+  constructor
+  · intro h
+    have refl := by cases total y y <;> assumption
+    exact ⟨(total _ _).resolve_left h, fun h' => (h' ▸ h) refl⟩
+  · intro ⟨h₁, h₂⟩ h₃
+    exact h₂ (antisymm h₁ h₃)
+
+theorem compareOfLessAndEq_eq_swap
+    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α]
+    (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y)
+    (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) (not_le : ∀ {x y : α}, ¬ x ≤ y ↔ y < x) {x y : α} :
+    compareOfLessAndEq x y = (compareOfLessAndEq y x).swap := by
+  apply compareOfLessAndEq_eq_swap_of_lt_iff_not_gt_and_ne
+  exact lt_iff_not_gt_and_ne_of_antisymm_of_total_of_not_le antisymm total not_le
+
+@[simp]
+theorem compareOfLessAndEq_eq_lt
+    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] {x y : α} :
+    compareOfLessAndEq x y = .lt ↔ x < y := by
+  rw [compareOfLessAndEq]
+  repeat' split <;> simp_all
+
+theorem compareOfLessAndEq_eq_eq
+    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableLE α] [DecidableEq α]
+    (refl : ∀ (x : α), x ≤ x) (not_le : ∀ {x y : α}, ¬ x ≤ y ↔ y < x) {x y : α} :
+    compareOfLessAndEq x y = .eq ↔ x = y := by
+  rw [compareOfLessAndEq]
+  repeat' split <;> try (simp_all; done)
+  simp only [reduceCtorEq, false_iff]
+  rintro rfl
+  rename_i hlt
+  simp [← not_le] at hlt
+  exact hlt (refl x)
+
+theorem compareOfLessAndEq_eq_gt_of_lt_iff_not_gt_and_ne
+    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α] {x y : α}
+    (h : ∀ x y : α, x < y ↔ ¬ y < x ∧ x ≠ y) :
+    compareOfLessAndEq x y = .gt ↔ y < x := by
+  rw [compareOfLessAndEq_eq_swap_of_lt_iff_not_gt_and_ne h, Ordering.swap_eq_gt]
+  exact compareOfLessAndEq_eq_lt
+
+theorem compareOfLessAndEq_eq_gt
+    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α]
+    (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y)
+    (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) (not_le : ∀ {x y : α}, ¬ x ≤ y ↔ y < x) (x y : α) :
+    compareOfLessAndEq x y = .gt ↔ y < x := by
+  apply compareOfLessAndEq_eq_gt_of_lt_iff_not_gt_and_ne
+  exact lt_iff_not_gt_and_ne_of_antisymm_of_total_of_not_le antisymm total not_le
+
+theorem isLE_compareOfLessAndEq
+    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableLE α] [DecidableEq α]
+    (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y)
+    (not_le : ∀ {x y : α}, ¬ x ≤ y ↔ y < x) (total : ∀ (x y : α), x ≤ y ∨ y ≤ x) {x y : α} :
+    (compareOfLessAndEq x y).isLE ↔ x ≤ y := by
+  have refl (a : α) := by cases total a a <;> assumption
+  rw [Ordering.isLE_iff_eq_lt_or_eq_eq, compareOfLessAndEq_eq_lt,
+    compareOfLessAndEq_eq_eq refl not_le]
+  constructor
+  · rintro (h | rfl)
+    · rw [← not_le] at h
+      exact total _ _ |>.resolve_left h
+    · exact refl x
+  · intro hle
+    by_cases hge : x ≥ y
+    · exact Or.inr <| antisymm hle hge
+    · exact Or.inl <| not_le.mp hge
+
+end Lemmas
+
 /--
 `Ord α` provides a computable total order on `α`, in terms of the
 `compare : α → α → Ordering` function.
--- a/src/Std/Classes/Ord.lean
+++ b/src/Std/Classes/Ord.lean
@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel, Paul Reichert
+Authors: Markus Himmel, Paul Reichert, Robin Arnez
 -/
 prelude
 import Init.Data.Ord
@ -66,6 +66,9 @@ abbrev OrientedOrd (α : Type u) [Ord α] := OrientedCmp (compare : α → α

 variable {α : Type u} {cmp : α → α → Ordering}

+theorem OrientedOrd.eq_swap [Ord α] [OrientedOrd α] {a b : α} :
+    compare a b = (compare b a).swap := OrientedCmp.eq_swap
+
 instance [OrientedCmp cmp] : ReflCmp cmp where
  compare_self := Ordering.eq_eq_of_eq_swap OrientedCmp.eq_swap

@ -104,12 +107,12 @@ theorem OrientedCmp.eq_symm [OrientedCmp cmp] {a b : α} : cmp a b = .eq → cmp
  OrientedCmp.eq_comm.1

 theorem OrientedCmp.not_isLE_of_lt [OrientedCmp cmp] {a b : α} :
-    cmp a b = .lt → ¬(cmp b a).isLE := by
+    cmp a b = .lt → ¬ (cmp b a).isLE := by
  rw [OrientedCmp.eq_swap (cmp := cmp) (a := a) (b := b)]
  simp

 theorem OrientedCmp.not_isGE_of_gt [OrientedCmp cmp] {a b : α} :
-    cmp a b = .gt → ¬(cmp b a).isGE := by
+    cmp a b = .gt → ¬ (cmp b a).isGE := by
  rw [OrientedCmp.eq_swap (cmp := cmp) (a := a) (b := b)]
  simp

@ -134,12 +137,12 @@ theorem OrientedCmp.not_gt_of_gt [OrientedCmp cmp] {a b : α} :
  cases cmp b a <;> simp

 theorem OrientedCmp.lt_of_not_isLE [OrientedCmp cmp] {a b : α} :
-    ¬(cmp a b).isLE → cmp b a = .lt := by
+    ¬ (cmp a b).isLE → cmp b a = .lt := by
  rw [OrientedCmp.eq_swap (cmp := cmp) (a := a) (b := b)]
  cases cmp b a <;> simp

 theorem OrientedCmp.gt_of_not_isGE [OrientedCmp cmp] {a b : α} :
-    ¬(cmp a b).isGE → cmp b a = .gt := by
+    ¬ (cmp a b).isGE → cmp b a = .gt := by
  rw [OrientedCmp.eq_swap (cmp := cmp) (a := a) (b := b)]
  cases cmp b a <;> simp

@ -157,11 +160,19 @@ abbrev TransOrd (α : Type u) [Ord α] := TransCmp (compare : α → α → Orde

 variable {α : Type u} {cmp : α → α → Ordering}

+theorem TransOrd.isLE_trans [Ord α] [TransOrd α] {a b c : α} :
+    (compare a b).isLE → (compare b c).isLE → (compare a c).isLE :=
+  TransCmp.isLE_trans
+
 theorem TransCmp.isGE_trans [TransCmp cmp] {a b c : α} (h₁ : (cmp a b).isGE) (h₂ : (cmp b c).isGE) :
    (cmp a c).isGE := by
  rw [OrientedCmp.isGE_iff_isLE] at *
  exact TransCmp.isLE_trans h₂ h₁

+theorem TransOrd.isGE_trans [Ord α] [TransOrd α] {a b c : α} :
+    (compare a b).isGE → (compare b c).isGE → (compare a c).isGE :=
+  TransCmp.isGE_trans
+
 instance TransCmp.opposite [TransCmp cmp] : TransCmp fun a b => cmp b a where
  isLE_trans := flip TransCmp.isLE_trans

@ -228,6 +239,10 @@ theorem TransCmp.gt_of_gt_of_isGE [TransCmp cmp] {a b c : α} (hab : cmp a b = .
  rw [OrientedCmp.gt_iff_lt, OrientedCmp.isGE_iff_isLE] at *
  exact TransCmp.lt_of_isLE_of_lt hbc hab

+theorem TransCmp.gt_of_gt_of_gt [TransCmp cmp] {a b c : α} (hab : cmp a b = .gt)
+    (hbc : cmp b c = .gt) : cmp a c = .gt := by
+  apply gt_of_gt_of_isGE hab (Ordering.isGE_of_eq_gt hbc)
+
 theorem TransCmp.gt_of_isGE_of_gt [TransCmp cmp] {a b c : α} (hab : (cmp a b).isGE)
    (hbc : cmp b c = .gt) : cmp a c = .gt := by
  rw [OrientedCmp.gt_iff_lt, OrientedCmp.isGE_iff_isLE] at *
@ -295,6 +310,9 @@ abbrev LawfulEqOrd (α : Type u) [Ord α] := LawfulEqCmp (compare : α → α

 variable {α : Type u} {cmp : α → α → Ordering} [LawfulEqCmp cmp]

+theorem LawfulEqOrd.eq_of_compare [Ord α] [LawfulEqOrd α] {a b : α} :
+    compare a b = .eq → a = b := LawfulEqCmp.eq_of_compare
+
 instance LawfulEqCmp.opposite [OrientedCmp cmp] [LawfulEqCmp cmp] :
    LawfulEqCmp (fun a b => cmp b a) where
  eq_of_compare := by
@ -435,4 +453,249 @@ theorem lawfulBEq_of_lawfulEqOrd [Ord α] [LawfulEqOrd α] : LawfulBEq α where

 end Internal

+section Instances
+
+theorem TransOrd.compareOfLessAndEq_of_lt_trans_of_lt_iff
+    {α : Type u} [LT α] [DecidableLT α] [DecidableEq α]
+    (lt_trans : ∀ {a b c : α}, a < b → b < c → a < c)
+    (h : ∀ x y : α, x < y ↔ ¬ y < x ∧ x ≠ y) :
+    TransCmp (fun x y : α => compareOfLessAndEq x y) where
+  eq_swap := compareOfLessAndEq_eq_swap_of_lt_iff_not_gt_and_ne h
+  isLE_trans {x y z} h₁ h₂ := by
+    simp only [compare, compareOfLessAndEq, apply_ite Ordering.isLE,
+      Ordering.isLE_lt, Ordering.isLE_eq, Ordering.isLE_gt] at h₁ h₂ ⊢
+    simp only [Bool.if_true_left, Bool.or_false, Bool.or_eq_true, decide_eq_true_eq] at h₁ h₂ ⊢
+    rcases h₁ with (h₁ | rfl)
+    · rcases h₂ with (h₂ | rfl)
+      · exact .inl (lt_trans h₁ h₂)
+      · exact .inl h₁
+    · exact h₂
+
+theorem TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
+    {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableLE α] [DecidableEq α]
+    (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y)
+    (trans : ∀ {x y z : α}, x ≤ y → y ≤ z → x ≤ z) (total : ∀ (x y : α), x ≤ y ∨ y ≤ x)
+    (not_le : ∀ {x y : α}, ¬ x ≤ y ↔ y < x) :
+    TransCmp (fun x y : α => compareOfLessAndEq x y) := by
+  refine compareOfLessAndEq_of_lt_trans_of_lt_iff ?_ ?_
+  · intro a b c
+    simp only [← not_le]
+    intro h₁ h₂ h₃
+    replace h₁ := (total _ _).resolve_left h₁
+    exact h₂ (trans h₃ h₁)
+  · exact lt_iff_not_gt_and_ne_of_antisymm_of_total_of_not_le antisymm total not_le
+
+namespace Bool
+
+instance : TransOrd Bool where
+  eq_swap {x y} := by cases x <;> cases y <;> rfl
+  isLE_trans {x y z} h₁ h₂ := by cases x <;> cases y <;> cases z <;> trivial
+
+instance : LawfulEqOrd Bool where
+  eq_of_compare {x y} := by cases x <;> cases y <;> simp
+
+end Bool
+
+namespace Nat
+
+instance : TransOrd Nat :=
+  TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
+    Nat.le_antisymm Nat.le_trans Nat.le_total Nat.not_le
+
+instance : LawfulEqOrd Nat where
+  eq_of_compare := compareOfLessAndEq_eq_eq Nat.le_refl Nat.not_le |>.mp
+
+end Nat
+
+namespace Int
+
+instance : TransOrd Int :=
+  TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
+    Int.le_antisymm Int.le_trans Int.le_total Int.not_le
+
+instance : LawfulEqOrd Int where
+  eq_of_compare := compareOfLessAndEq_eq_eq Int.le_refl Int.not_le |>.mp
+
+end Int
+
+namespace Fin
+
+variable (n : Nat)
+
+instance : OrientedOrd (Fin n) where
+  eq_swap := OrientedOrd.eq_swap (α := Nat)
+
+instance : TransOrd (Fin n) where
+  isLE_trans := TransOrd.isLE_trans (α := Nat)
+
+instance : LawfulEqOrd (Fin n) where
+  eq_of_compare h := Fin.eq_of_val_eq <| LawfulEqOrd.eq_of_compare h
+
+end Fin
+
+namespace String
+
+instance : TransOrd String :=
+  TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
+    String.le_antisymm String.le_trans String.le_total String.not_le
+
+instance : LawfulEqOrd String where
+  eq_of_compare h := compareOfLessAndEq_eq_eq String.le_refl String.not_le |>.mp h
+
+end String
+
+namespace Char
+
+instance : TransOrd Char :=
+  TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
+    Char.le_antisymm Char.le_trans Char.le_total Char.not_le
+
+instance : LawfulEqOrd Char where
+  eq_of_compare h := compareOfLessAndEq_eq_eq Char.le_refl Char.not_le |>.mp h
+
+end Char
+
+namespace UInt8
+
+instance : TransOrd UInt8 :=
+  TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
+    UInt8.le_antisymm UInt8.le_trans UInt8.le_total UInt8.not_le
+
+instance : LawfulEqOrd UInt8 where
+  eq_of_compare h := compareOfLessAndEq_eq_eq UInt8.le_refl UInt8.not_le |>.mp h
+
+end UInt8
+
+namespace UInt16
+
+instance : TransOrd UInt16 :=
+  TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
+    UInt16.le_antisymm UInt16.le_trans UInt16.le_total UInt16.not_le
+
+instance : LawfulEqOrd UInt16 where
+  eq_of_compare h := compareOfLessAndEq_eq_eq UInt16.le_refl UInt16.not_le |>.mp h
+
+end UInt16
+
+namespace UInt32
+
+instance : TransOrd UInt32 :=
+  TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
+    UInt32.le_antisymm UInt32.le_trans UInt32.le_total UInt32.not_le
+
+instance : LawfulEqOrd UInt32 where
+  eq_of_compare h := compareOfLessAndEq_eq_eq UInt32.le_refl UInt32.not_le |>.mp h
+
+end UInt32
+
+namespace UInt64
+
+instance : TransOrd UInt64 :=
+  TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
+    UInt64.le_antisymm UInt64.le_trans UInt64.le_total UInt64.not_le
+
+instance : LawfulEqOrd UInt64 where
+  eq_of_compare h := compareOfLessAndEq_eq_eq UInt64.le_refl UInt64.not_le |>.mp h
+
+end UInt64
+
+namespace USize
+
+instance : TransOrd USize :=
+  TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
+    USize.le_antisymm USize.le_trans USize.le_total USize.not_le
+
+instance : LawfulEqOrd USize where
+  eq_of_compare h := compareOfLessAndEq_eq_eq USize.le_refl USize.not_le |>.mp h
+
+end USize
+
+namespace Option
+
+instance {α} [Ord α] [OrientedOrd α] : OrientedOrd (Option α) where
+  eq_swap {a b} := by cases a <;> cases b <;> simp [Ord.compare, ← OrientedOrd.eq_swap]
+
+instance {α} [Ord α] [TransOrd α] : TransOrd (Option α) where
+  isLE_trans {a b c} hab hbc := by
+    cases a <;> cases b <;> cases c <;> (try simp_all [Ord.compare]; done)
+    simp only [Ord.compare] at *
+    apply TransOrd.isLE_trans <;> assumption
+
+instance {α} [Ord α] [ReflOrd α] : ReflOrd (Option α) where
+  compare_self {a} := by cases a <;> simp [Ord.compare]
+
+instance {α} [Ord α] [LawfulEqOrd α] : LawfulEqOrd (Option α) where
+  eq_of_compare {a b} := by
+    cases a <;> cases b <;> simp_all [Ord.compare, LawfulEqOrd.eq_of_compare]
+
+instance {α} [Ord α] [BEq α] [LawfulBEqOrd α] : LawfulBEqOrd (Option α) where
+  compare_eq_iff_beq {a b} := by
+    cases a <;> cases b <;> simp_all [Ord.compare, LawfulBEqOrd.compare_eq_iff_beq]
+
+end Option
+
+section Lex
+
+instance {α} {cmp₁ cmp₂} [ReflCmp cmp₁] [ReflCmp cmp₂] :
+    ReflCmp (α := α) (compareLex cmp₁ cmp₂) where
+  compare_self {a} := by simp [compareLex, ReflCmp.compare_self]
+
+instance {α} {cmp₁ cmp₂} [OrientedCmp cmp₁] [OrientedCmp cmp₂] :
+    OrientedCmp (α := α) (compareLex cmp₁ cmp₂) where
+  eq_swap {a b} := by
+    rw [compareLex, compareLex, OrientedCmp.eq_swap (cmp := cmp₁) (a := b), Ordering.swap_then,
+      Ordering.swap_swap, ← OrientedCmp.eq_swap]
+
+instance {α} {cmp₁ cmp₂} [TransCmp cmp₁] [TransCmp cmp₂] :
+    TransCmp (α := α) (compareLex cmp₁ cmp₂) where
+  isLE_trans {a b c} hab hbc := by
+    simp only [compareLex] at *
+    simp only [Ordering.isLE_then_iff_and] at *
+    refine ⟨TransCmp.isLE_trans hab.1 hbc.1, ?_⟩
+    cases hab.2
+    case inl hab' => exact Or.inl <| TransCmp.lt_of_lt_of_isLE hab' hbc.1
+    case inr hab' =>
+      cases hbc.2
+      case inl hbc' => exact Or.inl <| TransCmp.lt_of_isLE_of_lt hab.1 hbc'
+      case inr hbc' => exact Or.inr <| TransCmp.isLE_trans hab' hbc'
+
+instance {α β} {f : α → β} [Ord β] [ReflOrd β] :
+    ReflCmp (compareOn f) where
+  compare_self := ReflOrd.compare_self (α := β)
+
+instance {α β} {f : α → β} [Ord β] [OrientedOrd β] :
+    OrientedCmp (compareOn f) where
+  eq_swap := OrientedOrd.eq_swap (α := β)
+
+instance {α β} {f : α → β} [Ord β] [TransOrd β] :
+    TransCmp (compareOn f) where
+  isLE_trans := TransOrd.isLE_trans (α := β)
+
+attribute [instance] lexOrd in
+instance {α β} [Ord α] [Ord β] [ReflOrd α] [ReflOrd β] :
+    ReflOrd (α × β) :=
+  inferInstanceAs <| ReflCmp (compareLex _ _)
+
+attribute [instance] lexOrd in
+instance {α β} [Ord α] [Ord β] [OrientedOrd α] [OrientedOrd β] :
+    OrientedOrd (α × β) :=
+  inferInstanceAs <| OrientedCmp (compareLex _ _)
+
+attribute [instance] lexOrd in
+instance {α β} [Ord α] [Ord β] [TransOrd α] [TransOrd β] :
+    TransOrd (α × β) :=
+  inferInstanceAs <| TransCmp (compareLex _ _)
+
+attribute [instance] lexOrd in
+instance {α β} [Ord α] [Ord β] [LawfulEqOrd α] [LawfulEqOrd β] : LawfulEqOrd (α × β) where
+  eq_of_compare {a b} h := by
+    simp only [lexOrd, compareLex_eq_eq, compareOn] at h
+    ext
+    · exact LawfulEqOrd.eq_of_compare h.1
+    · exact LawfulEqOrd.eq_of_compare h.2
+
+end Lex
+
+end Instances
+
 end Std
--- a/src/Std/Time/Date/PlainDate.lean
+++ b/src/Std/Time/Date/PlainDate.lean
@ -21,6 +21,7 @@ set_option linter.all true
 `PlainDate` represents a date in the Year-Month-Day (YMD) format. It encapsulates the year, month,
 and day components, with validation to ensure the date is valid.
 -/
+@[ext]
 structure PlainDate where

  /-- The year component of the date. It is represented as an `Offset` type from `Year`. -/
@ -34,13 +35,27 @@ structure PlainDate where

  /-- Validates the date by ensuring that the year, month, and day form a correct and valid date. -/
  valid : year.Valid month day
-  deriving Repr
+deriving Repr, DecidableEq

 instance : Inhabited PlainDate where
  default := ⟨1, 1, 1, by decide⟩

-instance : BEq PlainDate where
-  beq x y := x.day == y.day && x.month == y.month && x.year == y.year
+instance : Ord PlainDate where
+  compare := compareLex (compareOn (·.year)) <| compareLex (compareOn (·.month)) (compareOn (·.day))
+
+theorem PlainDate.compare_def :
+    compare (α := PlainDate) =
+      compareLex (compareOn (·.year)) (compareLex (compareOn (·.month)) (compareOn (·.day))) := rfl
+
+instance : TransOrd PlainDate := inferInstanceAs <| TransCmp (compareLex _ _)
+
+instance : LawfulEqOrd PlainDate where
+  eq_of_compare {a b} h := by
+    simp only [PlainDate.compare_def, compareLex_eq_eq] at h
+    ext
+    · exact LawfulEqOrd.eq_of_compare h.1
+    · exact LawfulEqOrd.eq_of_compare h.2.1
+    · exact LawfulEqOrd.eq_of_compare h.2.2

 namespace PlainDate

--- a/src/Std/Time/Date/Unit/Day.lean
+++ b/src/Std/Time/Date/Unit/Day.lean
@ -17,7 +17,7 @@ set_option linter.all true
 `Ordinal` represents a bounded value for days, which ranges between 1 and 31.
 -/
 def Ordinal := Bounded.LE 1 31
-  deriving Repr, BEq, LE, LT
+deriving Repr, DecidableEq, LE, LT

 instance : OfNat Ordinal n :=
  inferInstanceAs (OfNat (Bounded.LE 1 (1 + (30 : Nat))) n)
@ -30,12 +30,18 @@ instance {x y : Ordinal} : Decidable (x < y) :=

 instance : Inhabited Ordinal where default := 1

+instance : Ord Ordinal := inferInstanceAs <| Ord (Bounded.LE 1 _)
+
+instance : TransOrd Ordinal := inferInstanceAs <| TransOrd (Bounded.LE 1 _)
+
+instance : LawfulEqOrd Ordinal := inferInstanceAs <| LawfulEqOrd (Bounded.LE 1 _)
+
 /--
 `Offset` represents an offset in days. It is defined as an `Int` with a base unit of 86400
 (the number of seconds in a day).
 -/
 def Offset : Type := UnitVal 86400
-  deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
+deriving Repr, DecidableEq, Inhabited, Add, Sub, Neg, LE, LT, ToString

 instance : OfNat Offset n := ⟨UnitVal.ofNat n⟩

@ -45,6 +51,12 @@ instance {x y : Offset} : Decidable (x ≤ y) :=
 instance {x y : Offset} : Decidable (x < y) :=
  inferInstanceAs (Decidable (x.val < y.val))

+instance : Ord Offset := inferInstanceAs <| Ord (UnitVal _)
+
+instance : TransOrd Offset := inferInstanceAs <| TransOrd (UnitVal _)
+
+instance : LawfulEqOrd Offset := inferInstanceAs <| LawfulEqOrd (UnitVal _)
+
 namespace Ordinal

 /--
@ -66,6 +78,14 @@ instance : Repr (OfYear leap) where
 instance : ToString (OfYear leap) where
  toString r := toString r.val

+instance : DecidableEq (OfYear leap) := inferInstanceAs <| DecidableEq (Bounded.LE 1 _)
+
+instance : Ord (OfYear leap) := inferInstanceAs <| Ord (Bounded.LE 1 _)
+
+instance : TransOrd (OfYear leap) := inferInstanceAs <| TransOrd (Bounded.LE 1 _)
+
+instance : LawfulEqOrd (OfYear leap) := inferInstanceAs <| LawfulEqOrd (Bounded.LE 1 _)
+
 namespace OfYear

 /--
--- a/src/Std/Time/Date/Unit/Month.lean
+++ b/src/Std/Time/Date/Unit/Month.lean
@ -19,7 +19,7 @@ set_option linter.all true
 `Ordinal` represents a bounded value for months, which ranges between 1 and 12.
 -/
 def Ordinal := Bounded.LE 1 12
-  deriving Repr, BEq, LE, LT
+deriving Repr, DecidableEq, LE, LT

 instance : OfNat Ordinal n :=
  inferInstanceAs (OfNat (Bounded.LE 1 (1 + (11 : Nat))) n)
@ -33,11 +33,17 @@ instance {x y : Ordinal} : Decidable (x ≤ y) :=
 instance {x y : Ordinal} : Decidable (x < y) :=
  inferInstanceAs (Decidable (x.val < y.val))

+instance : Ord Ordinal := inferInstanceAs <| Ord (Bounded.LE 1 _)
+
+instance : TransOrd Ordinal := inferInstanceAs <| TransOrd (Bounded.LE 1 _)
+
+instance : LawfulEqOrd Ordinal := inferInstanceAs <| LawfulEqOrd (Bounded.LE 1 _)
+
 /--
 `Offset` represents an offset in months. It is defined as an `Int`.
 -/
 def Offset : Type := Int
-  deriving Repr, BEq, Inhabited, Add, Sub, Mul, Div, Neg, ToString, LT, LE, DecidableEq
+deriving Repr, DecidableEq, Inhabited, Add, Sub, Mul, Div, Neg, ToString, LT, LE

 instance {x y : Offset} : Decidable (x ≤ y) :=
  Int.decLe x y
@ -48,10 +54,28 @@ instance {x y : Offset} : Decidable (x < y) :=
 instance : OfNat Offset n :=
  ⟨Int.ofNat n⟩

+instance : Ord Offset := inferInstanceAs <| Ord Int
+
+instance : TransOrd Offset := inferInstanceAs <| TransOrd Int
+
+instance : LawfulEqOrd Offset := inferInstanceAs <| LawfulEqOrd Int
+
 /--
 `Quarter` represents a value between 1 and 4, inclusive, corresponding to the four quarters of a year.
 -/
 def Quarter := Bounded.LE 1 4
+deriving Repr, DecidableEq, LT, LE
+
+instance : OfNat Quarter n := inferInstanceAs <| OfNat (Bounded.LE 1 (1 + (3 : Nat))) n
+
+instance : Inhabited Quarter where
+  default := 1
+
+instance : Ord Quarter := inferInstanceAs <| Ord (Bounded.LE 1 _)
+
+instance : TransOrd Quarter := inferInstanceAs <| TransOrd (Bounded.LE 1 _)
+
+instance : LawfulEqOrd Quarter := inferInstanceAs <| LawfulEqOrd (Bounded.LE 1 _)

 namespace Quarter

--- a/src/Std/Time/Date/Unit/Week.lean
+++ b/src/Std/Time/Date/Unit/Week.lean
@ -19,7 +19,7 @@ set_option linter.all true
 `Ordinal` represents a bounded value for weeks, which ranges between 1 and 53.
 -/
 def Ordinal := Bounded.LE 1 53
-  deriving Repr, BEq, LE, LT
+deriving Repr, DecidableEq, LE, LT

 instance : OfNat Ordinal n :=
  inferInstanceAs (OfNat (Bounded.LE 1 (1 + (52 : Nat))) n)
@ -33,11 +33,17 @@ instance {x y : Ordinal} : Decidable (x < y) :=
 instance : Inhabited Ordinal where
  default := 1

+instance : Ord Ordinal := inferInstanceAs <| Ord (Bounded.LE 1 _)
+
+instance : TransOrd Ordinal := inferInstanceAs <| TransOrd (Bounded.LE 1 _)
+
+instance : LawfulEqOrd Ordinal := inferInstanceAs <| LawfulEqOrd (Bounded.LE 1 _)
+
 /--
 `Offset` represents an offset in weeks.
 -/
 def Offset : Type := UnitVal (86400 * 7)
-  deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
+deriving Repr, DecidableEq, Inhabited, Add, Sub, Neg, LE, LT, ToString

 instance {x y : Offset} : Decidable (x ≤ y) :=
  inferInstanceAs (Decidable (x.val ≤ y.val))
@ -47,6 +53,12 @@ instance {x y : Offset} : Decidable (x < y) :=

 instance : OfNat Offset n := ⟨UnitVal.ofNat n⟩

+instance : Ord Offset := inferInstanceAs <| Ord (UnitVal _)
+
+instance : TransOrd Offset := inferInstanceAs <| TransOrd (UnitVal _)
+
+instance : LawfulEqOrd Offset := inferInstanceAs <| LawfulEqOrd (UnitVal _)
+
 namespace Ordinal

 /--
@ -61,7 +73,18 @@ def ofInt (data : Int) (h : 1 ≤ data ∧ data ≤ 53) : Ordinal :=
 correct bounds—either 1 to 6, representing the possible weeks in a month.
 -/
 def OfMonth := Bounded.LE 1 6
-  deriving Repr
+deriving Repr, DecidableEq
+
+instance : OfNat OfMonth n := inferInstanceAs (OfNat (Bounded.LE 1 (1 + (5 : Nat))) n)
+
+instance : Inhabited OfMonth where
+  default := 1
+
+instance : Ord OfMonth := inferInstanceAs <| Ord (Bounded.LE 1 _)
+
+instance : TransOrd OfMonth := inferInstanceAs <| TransOrd (Bounded.LE 1 _)
+
+instance : LawfulEqOrd OfMonth := inferInstanceAs <| LawfulEqOrd (Bounded.LE 1 _)

 /--
 Creates an `Ordinal` from a natural number, ensuring the value is within bounds.
--- a/src/Std/Time/Date/Unit/Weekday.lean
+++ b/src/Std/Time/Date/Unit/Weekday.lean
@ -38,7 +38,7 @@ inductive Weekday

    /-- Sunday. -/
  | sunday
-  deriving Repr, Inhabited, BEq
+deriving Repr, Inhabited, DecidableEq

 namespace Weekday

@ -46,10 +46,26 @@ namespace Weekday
 `Ordinal` represents a bounded value for weekdays, which ranges between 1 and 7.
 -/
 def Ordinal := Bounded.LE 1 7
+deriving Repr, DecidableEq, LT, LE
+
+instance {x y : Ordinal} : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.val ≤ y.val))
+
+instance {x y : Ordinal} : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.val < y.val))

 instance : OfNat Ordinal n :=
  inferInstanceAs (OfNat (Bounded.LE 1 (1 + (6 : Nat))) n)

+instance : Inhabited Ordinal where
+  default := 1
+
+instance : Ord Ordinal := inferInstanceAs <| Ord (Bounded.LE 1 _)
+
+instance : TransOrd Ordinal := inferInstanceAs <| TransOrd (Bounded.LE 1 _)
+
+instance : LawfulEqOrd Ordinal := inferInstanceAs <| LawfulEqOrd (Bounded.LE 1 _)
+
 /--
 Converts a `Ordinal` representing a day index into a corresponding `Weekday`. This function is useful
 for mapping numerical representations to days of the week.
@ -75,6 +91,17 @@ def toOrdinal : Weekday → Ordinal
  | .saturday => 6
  | .sunday => 7

+instance : Ord Weekday where
+  compare := compareOn toOrdinal
+
+instance : TransOrd Weekday := inferInstanceAs <| TransCmp (compareOn toOrdinal)
+
+theorem toOrdinal.inj {a b : Weekday} (h : toOrdinal a = toOrdinal b) : a = b := by
+  cases a <;> cases b <;> rw [toOrdinal] at * <;> contradiction
+
+instance : LawfulEqOrd Weekday where
+  eq_of_compare := toOrdinal.inj ∘ LawfulEqOrd.eq_of_compare (α := Ordinal)
+
 /--
 Converts a `Weekday` to a `Nat`.
 -/
--- a/src/Std/Time/Date/Unit/Year.lean
+++ b/src/Std/Time/Date/Unit/Year.lean
@ -26,7 +26,7 @@ inductive Era

  /-- The Common Era (CE), represents dates from year 0 onwards. -/
  | ce
-  deriving Repr, Inhabited
+deriving Repr, Inhabited

 instance : ToString Era where
  toString
@ -37,7 +37,7 @@ instance : ToString Era where
 `Offset` represents a year offset, defined as an `Int`.
 -/
 def Offset : Type := Int
-  deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
+deriving Repr, DecidableEq, Inhabited, Add, Sub, Neg, LE, LT, ToString

 instance {x y : Offset} : Decidable (x ≤ y) :=
  let x : Int := x
@ -49,6 +49,12 @@ instance {x y : Offset} : Decidable (x < y) :=

 instance : OfNat Offset n := ⟨Int.ofNat n⟩

+instance : Ord Offset := inferInstanceAs <| Ord Int
+
+instance : TransOrd Offset := inferInstanceAs <| TransOrd Int
+
+instance : LawfulEqOrd Offset := inferInstanceAs <| LawfulEqOrd Int
+
 namespace Offset

 /--
--- a/src/Std/Time/Date/ValidDate.lean
+++ b/src/Std/Time/Date/ValidDate.lean
@ -25,6 +25,20 @@ def ValidDate (leap : Bool) := { val : Month.Ordinal × Day.Ordinal // Valid lea
 instance : Inhabited (ValidDate l) where
  default := ⟨⟨1, 1⟩, (by cases l <;> decide)⟩

+instance : DecidableEq (ValidDate leap) := Subtype.instDecidableEq
+
+instance : Ord (ValidDate leap) where
+  compare a b := compare a.val b.val
+
+instance : OrientedOrd (ValidDate leap) where
+  eq_swap := OrientedOrd.eq_swap (α := Month.Ordinal × Day.Ordinal)
+
+instance : TransOrd (ValidDate leap) where
+  isLE_trans := TransOrd.isLE_trans (α := Month.Ordinal × Day.Ordinal)
+
+instance : LawfulEqOrd (ValidDate leap) where
+  eq_of_compare := Subtype.ext ∘ LawfulEqOrd.eq_of_compare (α := Month.Ordinal × Day.Ordinal)
+
 namespace ValidDate

 /--
--- a/src/Std/Time/DateTime/PlainDateTime.lean
+++ b/src/Std/Time/DateTime/PlainDateTime.lean
@ -18,6 +18,7 @@ set_option linter.all true
 /--
 Represents a date and time with components for Year, Month, Day, Hour, Minute, Second, and Nanosecond.
 -/
+@[ext]
 structure PlainDateTime where

  /--
@ -29,7 +30,22 @@ structure PlainDateTime where
  The `Time` component of a `PlainTime`
  -/
  time : PlainTime
-  deriving Inhabited, BEq, Repr
+deriving Inhabited, DecidableEq, Repr
+
+instance : Ord PlainDateTime where
+  compare := compareLex (compareOn (·.date)) (compareOn (·.time))
+
+theorem PlainDateTime.compare_def :
+    compare (α := PlainDateTime) = compareLex (compareOn (·.date)) (compareOn (·.time)) := rfl
+
+instance : TransOrd PlainDateTime := inferInstanceAs <| TransCmp (compareLex _ _)
+
+instance : LawfulEqOrd PlainDateTime where
+  eq_of_compare {a b} h := by
+    simp only [PlainDateTime.compare_def, compareLex_eq_eq] at h
+    apply PlainDateTime.ext
+    · exact LawfulEqOrd.eq_of_compare h.1
+    · exact LawfulEqOrd.eq_of_compare h.2

 namespace PlainDateTime

--- a/src/Std/Time/DateTime/Timestamp.lean
+++ b/src/Std/Time/DateTime/Timestamp.lean
@ -19,13 +19,14 @@ set_option linter.all true
 /--
 Represents an exact point in time as a UNIX Epoch timestamp.
 -/
+@[ext]
 structure Timestamp where

  /--
  Duration since the unix epoch.
  -/
  val : Duration
-  deriving Repr, BEq, Inhabited
+deriving Repr, DecidableEq, Inhabited

 instance : LE Timestamp where
  le x y := x.val ≤ y.val
@ -42,6 +43,20 @@ instance : ToString Timestamp where
 instance : Repr Timestamp where
  reprPrec s := Repr.addAppParen ("Timestamp.ofNanosecondsSinceUnixEpoch " ++ repr s.val.toNanoseconds)

+instance : Ord Timestamp where
+  compare := compareOn (·.val)
+
+theorem Timestamp.compare_def :
+    compare (α := Timestamp) = compareOn (·.val) := rfl
+
+instance : TransOrd Timestamp := inferInstanceAs <| TransCmp (compareOn _)
+
+instance : LawfulEqOrd Timestamp where
+  eq_of_compare {a b} h := by
+    simp only [Timestamp.compare_def] at h
+    apply Timestamp.ext
+    exact LawfulEqOrd.eq_of_compare h
+
 namespace Timestamp

 /--
--- a/src/Std/Time/Duration.lean
+++ b/src/Std/Time/Duration.lean
@ -16,6 +16,7 @@ set_option linter.all true
 /--
 Represents a time interval with nanoseconds precision.
 -/
+@[ext]
 structure Duration where

  /--
@ -32,7 +33,7 @@ structure Duration where
  Proof that the duration is valid, ensuring that the `second` and `nano` values are correctly related.
  -/
  proof : (second.val ≥ 0 ∧ nano.val ≥ 0) ∨ (second.val ≤ 0 ∧ nano.val ≤ 0)
-  deriving Repr
+deriving Repr, DecidableEq

 instance : ToString Duration where
  toString s :=
@ -47,9 +48,6 @@ instance : ToString Duration where
 instance : Repr Duration where
  reprPrec s := reprPrec (toString s)

-instance : BEq Duration where
-  beq x y := x.second == y.second && y.nano == x.nano
-
 instance : Inhabited Duration where
  default := ⟨0, Bounded.LE.mk 0 (by decide), by decide⟩

@ -58,6 +56,21 @@ instance : OfNat Duration n where
    refine ⟨.ofInt n, ⟨0, by decide⟩, ?_⟩
    simp <;> exact Int.le_total n 0 |>.symm

+instance : Ord Duration where
+  compare := compareLex (compareOn (·.second)) (compareOn (·.nano))
+
+theorem Duration.compare_def :
+    compare (α := Duration) = compareLex (compareOn (·.second)) (compareOn (·.nano)) := rfl
+
+instance : TransOrd Duration := inferInstanceAs <| TransCmp (compareLex _ _)
+
+instance : LawfulEqOrd Duration where
+  eq_of_compare {a b} h := by
+    simp only [Duration.compare_def, compareLex_eq_eq] at h
+    ext
+    · exact LawfulEqOrd.eq_of_compare h.1
+    · exact LawfulEqOrd.eq_of_compare h.2
+
 namespace Duration

 /--
--- a/src/Std/Time/Internal/Bounded.lean
+++ b/src/Std/Time/Internal/Bounded.lean
@ -6,6 +6,7 @@ Authors: Sofia Rodrigues
 prelude
 import Init.Omega
 import Init.Data.Int.DivMod.Lemmas
+import Std.Classes.Ord

 namespace Std
 namespace Time
@ -29,18 +30,32 @@ instance : LE (Bounded rel n m) where
 instance : LT (Bounded rel n m) where
  lt l r := l.val < r.val

+@[always_inline]
+instance : Ord (Bounded rel n m) where
+  compare := compareOn (·.val)
+
@[always_inline]
 instance : Repr (Bounded rel m n) where
  reprPrec n := reprPrec n.val

@[always_inline]
-instance : BEq (Bounded rel n m) where
-  beq x y := (x.val = y.val)
+instance : DecidableEq (Bounded rel n m) := Subtype.instDecidableEq

@[always_inline]
 instance {x y : Bounded rel a b} : Decidable (x ≤ y) :=
  inferInstanceAs (Decidable (x.val ≤ y.val))

+instance : OrientedOrd (Bounded rel n m) where
+  eq_swap := OrientedOrd.eq_swap (α := Int)
+
+instance : TransOrd (Bounded rel n m) where
+  isLE_trans := TransOrd.isLE_trans (α := Int)
+
+instance : LawfulEqOrd (Bounded rel n m) where
+  eq_of_compare := Subtype.ext ∘ LawfulEqOrd.eq_of_compare (α := Int)
+
+variable {rel a b}
+
 /--
 A `Bounded` integer that the relation used is the the less-equal relation so, it includes all
 integers that `lo ≤ val ≤ hi`.
--- a/src/Std/Time/Internal/UnitVal.lean
+++ b/src/Std/Time/Internal/UnitVal.lean
@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sofia Rodrigues
 -/
 prelude
+import Std.Classes.Ord
 import Std.Internal.Rat

 namespace Std
@ -17,6 +18,7 @@ set_option linter.all true
 /--
 A structure representing a unit of a given ratio type `α`.
 -/
+@[ext]
 structure UnitVal (α : Rat) where
  /--
  Creates a `UnitVal` from an `Int`.
@ -27,12 +29,27 @@ structure UnitVal (α : Rat) where
  Value inside the UnitVal Value.
  -/
  val : Int
-  deriving Inhabited, BEq
+deriving Inhabited, DecidableEq

 instance : LE (UnitVal x) where
  le x y := x.val ≤ y.val

-instance { x y : UnitVal z }: Decidable (x ≤ y) :=
+instance : Ord (UnitVal x) where
+  compare x y := compare x.val y.val
+
+theorem UnitVal.compare_def {x} {a b : UnitVal x} :
+    compare a b = compare a.1 b.1 := by rfl
+
+instance : OrientedOrd (UnitVal x) where
+  eq_swap := OrientedOrd.eq_swap (α := Int)
+
+instance : TransOrd (UnitVal x) where
+  isLE_trans := TransOrd.isLE_trans (α := Int)
+
+instance : LawfulEqOrd (UnitVal x) where
+  eq_of_compare := UnitVal.ext ∘ LawfulEqOrd.eq_of_compare (α := Int)
+
+instance {x y : UnitVal z}: Decidable (x ≤ y) :=
  inferInstanceAs (Decidable (x.val ≤ y.val))

 namespace UnitVal
--- a/src/Std/Time/Time/HourMarker.lean
+++ b/src/Std/Time/Time/HourMarker.lean
@ -27,7 +27,23 @@ inductive HourMarker
  Post meridiem.
  -/
  | pm
-  deriving Repr, BEq
+deriving Repr, DecidableEq
+
+instance : Ord HourMarker where
+  compare
+    | .am, .am => .eq
+    | .am, .pm => .lt
+    | .pm, .am => .gt
+    | .pm, .pm => .eq
+
+instance : OrientedOrd HourMarker where
+  eq_swap {a b} := by cases a <;> cases b <;> rfl
+
+instance : TransOrd HourMarker where
+  isLE_trans {a b c} hab hbc := by cases a <;> cases b <;> cases c <;> simp_all
+
+instance : LawfulEqOrd HourMarker where
+  eq_of_compare {a b} h := by cases a <;> cases b <;> simp_all

 namespace HourMarker

--- a/src/Std/Time/Time/PlainTime.lean
+++ b/src/Std/Time/Time/PlainTime.lean
@ -15,6 +15,7 @@ set_option linter.all true
 /--
 Represents a specific point in a day, including hours, minutes, seconds, and nanoseconds.
 -/
+@[ext]
 structure PlainTime where

  /--
@ -36,14 +37,30 @@ structure PlainTime where
  `Nanoseconds` component of the `PlainTime`
  -/
  nanosecond : Nanosecond.Ordinal
-  deriving Repr
+deriving Repr, DecidableEq

 instance : Inhabited PlainTime where
  default := ⟨0, 0, 0, 0, by decide⟩

-instance : BEq PlainTime where
-  beq x y := x.hour.val == y.hour.val && x.minute == y.minute
-          && x.second.val == y.second.val && x.nanosecond == y.nanosecond
+instance : Ord PlainTime where
+  compare := compareLex (compareOn (·.hour)) <| compareLex (compareOn (·.minute)) <|
+      compareLex (compareOn (·.second)) (compareOn (·.nanosecond))
+
+theorem PlainTime.compare_def :
+    compare (α := PlainTime) =
+      (compareLex (compareOn (·.hour)) <| compareLex (compareOn (·.minute)) <|
+          compareLex (compareOn (·.second)) (compareOn (·.nanosecond))) := rfl
+
+instance : TransOrd PlainTime := inferInstanceAs <| TransCmp (compareLex _ _)
+
+instance : LawfulEqOrd PlainTime where
+  eq_of_compare {a b} h := by
+    simp only [PlainTime.compare_def, compareLex_eq_eq] at h
+    ext
+    · exact LawfulEqOrd.eq_of_compare h.1
+    · exact LawfulEqOrd.eq_of_compare h.2.1
+    · exact LawfulEqOrd.eq_of_compare h.2.2.1
+    · exact LawfulEqOrd.eq_of_compare h.2.2.2

 namespace PlainTime

--- a/src/Std/Time/Time/Unit/Hour.lean
+++ b/src/Std/Time/Time/Unit/Hour.lean
@ -21,7 +21,7 @@ set_option linter.all true
 `Ordinal` represents a bounded value for hours, ranging from 0 to 23.
 -/
 def Ordinal := Bounded.LE 0 23
-  deriving Repr, BEq, LE, LT
+deriving Repr, DecidableEq, LE, LT

 instance : OfNat Ordinal n :=
  inferInstanceAs (OfNat (Bounded.LE 0 (0 + (23 : Nat))) n)
@ -35,22 +35,34 @@ instance {x y : Ordinal} : Decidable (x ≤ y) :=
 instance {x y : Ordinal} : Decidable (x < y) :=
  inferInstanceAs (Decidable (x.val < y.val))

+instance : Ord Ordinal := inferInstanceAs <| Ord (Bounded.LE 0 _)
+
+instance : TransOrd Ordinal := inferInstanceAs <| TransOrd (Bounded.LE 0 _)
+
+instance : LawfulEqOrd Ordinal := inferInstanceAs <| LawfulEqOrd (Bounded.LE 0 _)
+
 /--
 `Offset` represents an offset in hours, defined as an `Int`. This can be used to express durations
 or differences in hours.
 -/
 def Offset : Type := UnitVal 3600
-  deriving Repr, BEq, Inhabited, Add, Sub, Neg, ToString, LT, LE
+deriving Repr, DecidableEq, Inhabited, Add, Sub, Neg, ToString, LT, LE

-instance { x y : Offset } : Decidable (x ≤ y) :=
+instance {x y : Offset} : Decidable (x ≤ y) :=
  inferInstanceAs (Decidable (x.val ≤ y.val))

-instance { x y : Offset } : Decidable (x < y) :=
+instance {x y : Offset} : Decidable (x < y) :=
  inferInstanceAs (Decidable (x.val < y.val))

 instance : OfNat Offset n :=
  ⟨UnitVal.ofNat n⟩

+instance : Ord Offset := inferInstanceAs <| Ord (UnitVal _)
+
+instance : TransOrd Offset := inferInstanceAs <| TransOrd (UnitVal _)
+
+instance : LawfulEqOrd Offset := inferInstanceAs <| LawfulEqOrd (UnitVal _)
+
 namespace Ordinal

 /--
--- a/src/Std/Time/Time/Unit/Millisecond.lean
+++ b/src/Std/Time/Time/Unit/Millisecond.lean
@ -20,7 +20,7 @@ set_option linter.all true
 `Ordinal` represents a bounded value for milliseconds, ranging from 0 to 999 milliseconds.
 -/
 def Ordinal := Bounded.LE 0 999
-  deriving Repr, BEq, LE, LT
+deriving Repr, DecidableEq, LE, LT

 instance : OfNat Ordinal n :=
  inferInstanceAs (OfNat (Bounded.LE 0 (0 + (999 : Nat))) n)
@ -34,21 +34,33 @@ instance {x y : Ordinal} : Decidable (x ≤ y) :=
 instance {x y : Ordinal} : Decidable (x < y) :=
  inferInstanceAs (Decidable (x.val < y.val))

+instance : Ord Ordinal := inferInstanceAs <| Ord (Bounded.LE 0 _)
+
+instance : TransOrd Ordinal := inferInstanceAs <| TransOrd (Bounded.LE 0 _)
+
+instance : LawfulEqOrd Ordinal := inferInstanceAs <| LawfulEqOrd (Bounded.LE 0 _)
+
 /--
 `Offset` represents a duration offset in milliseconds.
 -/
 def Offset : Type := UnitVal (1 / 1000)
-  deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
+deriving Repr, DecidableEq, Inhabited, Add, Sub, Neg, LE, LT, ToString

-instance { x y : Offset } : Decidable (x ≤ y) :=
+instance {x y : Offset} : Decidable (x ≤ y) :=
  inferInstanceAs (Decidable (x.val ≤ y.val))

-instance { x y : Offset } : Decidable (x < y) :=
+instance {x y : Offset} : Decidable (x < y) :=
  inferInstanceAs (Decidable (x.val < y.val))

 instance : OfNat Offset n :=
  ⟨UnitVal.ofNat n⟩

+instance : Ord Offset := inferInstanceAs <| Ord (UnitVal _)
+
+instance : TransOrd Offset := inferInstanceAs <| TransOrd (UnitVal _)
+
+instance : LawfulEqOrd Offset := inferInstanceAs <| LawfulEqOrd (UnitVal _)
+
 namespace Offset

 /--
--- a/src/Std/Time/Time/Unit/Minute.lean
+++ b/src/Std/Time/Time/Unit/Minute.lean
@ -20,7 +20,7 @@ set_option linter.all true
 `Ordinal` represents a bounded value for minutes, ranging from 0 to 59. This is useful for representing the minute component of a time.
 -/
 def Ordinal := Bounded.LE 0 59
-  deriving Repr, BEq, LE, LT
+deriving Repr, DecidableEq, LE, LT

 instance : OfNat Ordinal n :=
  inferInstanceAs (OfNat (Bounded.LE 0 (0 + (59 : Nat))) n)
@ -34,21 +34,33 @@ instance {x y : Ordinal} : Decidable (x ≤ y) :=
 instance {x y : Ordinal} : Decidable (x < y) :=
  inferInstanceAs (Decidable (x.val < y.val))

+instance : Ord Ordinal := inferInstanceAs <| Ord (Bounded.LE 0 _)
+
+instance : TransOrd Ordinal := inferInstanceAs <| TransOrd (Bounded.LE 0 _)
+
+instance : LawfulEqOrd Ordinal := inferInstanceAs <| LawfulEqOrd (Bounded.LE 0 _)
+
 /--
 `Offset` represents a duration offset in minutes.
 -/
 def Offset : Type := UnitVal 60
-  deriving Repr, BEq, Inhabited, Add, Sub, Neg, ToString, LT, LE
+deriving Repr, DecidableEq, Inhabited, Add, Sub, Neg, ToString, LT, LE

-instance { x y : Offset } : Decidable (x ≤ y) :=
+instance {x y : Offset} : Decidable (x ≤ y) :=
  inferInstanceAs (Decidable (x.val ≤ y.val))

-instance { x y : Offset } : Decidable (x < y) :=
+instance {x y : Offset} : Decidable (x < y) :=
  inferInstanceAs (Decidable (x.val < y.val))

 instance : OfNat Offset n :=
  ⟨UnitVal.ofInt <| Int.ofNat n⟩

+instance : Ord Offset := inferInstanceAs <| Ord (UnitVal _)
+
+instance : TransOrd Offset := inferInstanceAs <| TransOrd (UnitVal _)
+
+instance : LawfulEqOrd Offset := inferInstanceAs <| LawfulEqOrd (UnitVal _)
+
 namespace Ordinal

 /--
--- a/src/Std/Time/Time/Unit/Nanosecond.lean
+++ b/src/Std/Time/Time/Unit/Nanosecond.lean
@ -19,7 +19,7 @@ set_option linter.all true
 `Ordinal` represents a nanosecond value that is bounded between 0 and 999,999,999 nanoseconds.
 -/
 def Ordinal := Bounded.LE 0 999999999
-  deriving Repr, BEq, LE, LT
+deriving Repr, DecidableEq, LE, LT

 instance : OfNat Ordinal n where
  ofNat := Bounded.LE.ofFin (Fin.ofNat' _ n)
@ -33,21 +33,33 @@ instance {x y : Ordinal} : Decidable (x ≤ y) :=
 instance {x y : Ordinal} : Decidable (x < y) :=
  inferInstanceAs (Decidable (x.val < y.val))

+instance : Ord Ordinal := inferInstanceAs <| Ord (Bounded.LE 0 _)
+
+instance : TransOrd Ordinal := inferInstanceAs <| TransOrd (Bounded.LE 0 _)
+
+instance : LawfulEqOrd Ordinal := inferInstanceAs <| LawfulEqOrd (Bounded.LE 0 _)
+
 /--
 `Offset` represents a time offset in nanoseconds.
 -/
 def Offset : Type := UnitVal (1 / 1000000000)
-  deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
+deriving Repr, DecidableEq, Inhabited, Add, Sub, Neg, LE, LT, ToString

-instance { x y : Offset } : Decidable (x ≤ y) :=
+instance {x y : Offset} : Decidable (x ≤ y) :=
  inferInstanceAs (Decidable (x.val ≤ y.val))

-instance { x y : Offset } : Decidable (x < y) :=
+instance {x y : Offset} : Decidable (x < y) :=
  inferInstanceAs (Decidable (x.val < y.val))

 instance : OfNat Offset n :=
  ⟨UnitVal.ofNat n⟩

+instance : Ord Offset := inferInstanceAs <| Ord (UnitVal _)
+
+instance : TransOrd Offset := inferInstanceAs <| TransOrd (UnitVal _)
+
+instance : LawfulEqOrd Offset := inferInstanceAs <| LawfulEqOrd (UnitVal _)
+
 namespace Offset

 /--
@ -71,10 +83,22 @@ end Offset
 This can be used for operations that involve differences or adjustments within this range.
 -/
 def Span := Bounded.LE (-999999999) 999999999
-  deriving Repr, BEq, LE, LT
+deriving Repr, DecidableEq, LE, LT

 instance : Inhabited Span where default := Bounded.LE.mk 0 (by decide)

+instance {x y : Span} : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.val ≤ y.val))
+
+instance {x y : Span} : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.val < y.val))
+
+instance : Ord Span := inferInstanceAs <| Ord (Bounded.LE _ _)
+
+instance : TransOrd Span := inferInstanceAs <| TransOrd (Bounded.LE _ _)
+
+instance : LawfulEqOrd Span := inferInstanceAs <| LawfulEqOrd (Bounded.LE _ _)
+
 namespace Span

 /--
@ -91,7 +115,21 @@ namespace Ordinal
 `Ordinal` represents a bounded value for nanoseconds in a day, which ranges between 0 and 86400000000000.
 -/
 def OfDay := Bounded.LE 0 86400000000000
-  deriving Repr, BEq, LE, LT
+deriving Repr, DecidableEq, LE, LT
+
+instance : Inhabited OfDay where default := Bounded.LE.mk 0 (by decide)
+
+instance {x y : OfDay} : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.val ≤ y.val))
+
+instance {x y : OfDay} : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.val < y.val))
+
+instance : Ord OfDay := inferInstanceAs <| Ord (Bounded.LE _ _)
+
+instance : TransOrd OfDay := inferInstanceAs <| TransOrd (Bounded.LE _ _)
+
+instance : LawfulEqOrd OfDay := inferInstanceAs <| LawfulEqOrd (Bounded.LE _ _)

 /--
 Creates an `Ordinal` from an integer, ensuring the value is within bounds.
--- a/src/Std/Time/Time/Unit/Second.lean
+++ b/src/Std/Time/Time/Unit/Second.lean
@ -21,9 +21,6 @@ for potential leap second.
 -/
 def Ordinal (leap : Bool) := Bounded.LE 0 (.ofNat (if leap then 60 else 59))

-instance : BEq (Ordinal leap) where
-  beq x y := BEq.beq x.val y.val
-
 instance : LE (Ordinal leap) where
  le x y := LE.le x.val y.val

@ -33,6 +30,9 @@ instance : LT (Ordinal leap) where
 instance : Repr (Ordinal leap) where
  reprPrec r := reprPrec r.val

+instance : ToString (Ordinal leap) where
+  toString r := toString r.val
+
 instance : OfNat (Ordinal leap) n := by
  have inst := inferInstanceAs (OfNat (Bounded.LE 0 (0 + (59 : Nat))) n)
  cases leap
@ -45,21 +45,35 @@ instance {x y : Ordinal leap} : Decidable (x ≤ y) :=
 instance {x y : Ordinal leap} : Decidable (x < y) :=
  inferInstanceAs (Decidable (x.val < y.val))

+instance : DecidableEq (Ordinal leap) := inferInstanceAs <| DecidableEq (Bounded.LE 0 _)
+
+instance : Ord (Ordinal leap) := inferInstanceAs <| Ord (Bounded.LE 0 _)
+
+instance : TransOrd (Ordinal leap) := inferInstanceAs <| TransOrd (Bounded.LE 0 _)
+
+instance : LawfulEqOrd (Ordinal leap) := inferInstanceAs <| LawfulEqOrd (Bounded.LE 0 _)
+
 /--
 `Offset` represents an offset in seconds. It is defined as an `Int`.
 -/
 def Offset : Type := UnitVal 1
-  deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
+deriving Repr, DecidableEq, Inhabited, Add, Sub, Neg, LE, LT, ToString

-instance { x y : Offset } : Decidable (x ≤ y) :=
+instance {x y : Offset} : Decidable (x ≤ y) :=
  inferInstanceAs (Decidable (x.val ≤ y.val))

-instance { x y : Offset } : Decidable (x < y) :=
+instance {x y : Offset} : Decidable (x < y) :=
  inferInstanceAs (Decidable (x.val < y.val))

 instance : OfNat Offset n :=
  ⟨UnitVal.ofNat n⟩

+instance : Ord Offset := inferInstanceAs <| Ord (UnitVal _)
+
+instance : TransOrd Offset := inferInstanceAs <| TransOrd (UnitVal _)
+
+instance : LawfulEqOrd Offset := inferInstanceAs <| LawfulEqOrd (UnitVal _)
+
 namespace Offset

 /--
--- a/src/Std/Time/Zoned/DateTime.lean
+++ b/src/Std/Time/Zoned/DateTime.lean
@ -33,8 +33,13 @@ structure DateTime (tz : TimeZone) where
 instance : BEq (DateTime tz) where
  beq x y := x.timestamp == y.timestamp

-instance : Inhabited (DateTime tz) where
-  default := ⟨Inhabited.default, Thunk.mk fun _ => Inhabited.default⟩
+instance : Ord (DateTime tz) where
+  compare := compareOn (·.timestamp)
+
+instance : TransOrd (DateTime tz) := inferInstanceAs <| TransCmp (compareOn _)
+
+instance : LawfulBEqOrd (DateTime tz) where
+  compare_eq_iff_beq := LawfulBEqOrd.compare_eq_iff_beq (α := Timestamp)

 namespace DateTime

@ -45,6 +50,9 @@ Creates a new `DateTime` out of a `Timestamp` that is in a `TimeZone`.
 def ofTimestamp (tm : Timestamp) (tz : TimeZone) : DateTime tz :=
  DateTime.mk tm (Thunk.mk fun _ => tm.toPlainDateTimeAssumingUTC |>.addSeconds tz.toSeconds)

+instance : Inhabited (DateTime tz) where
+  default := ofTimestamp Inhabited.default tz
+
 /--
 Converts a `DateTime` to the number of days since the UNIX epoch.
 -/
--- a/src/Std/Time/Zoned/Offset.lean
+++ b/src/Std/Time/Zoned/Offset.lean
@ -16,6 +16,7 @@ set_option linter.all true
 /--
 Represents a timezone offset with an hour and second component.
 -/
+@[ext]
 structure Offset where

  /--
@ -27,13 +28,24 @@ structure Offset where
  The same timezone offset in seconds.
  -/
  second : Second.Offset
-  deriving Repr
+deriving Repr, DecidableEq

 instance : Inhabited Offset where
  default := ⟨0⟩

-instance : BEq Offset where
-  beq x y := BEq.beq x.second y.second
+instance : Ord Offset where
+  compare := compareOn (·.second)
+
+theorem Offset.compare_def :
+    compare (α := Offset) = compareOn (·.second) := rfl
+
+instance : TransOrd Offset := inferInstanceAs <| TransCmp (compareOn _)
+
+instance : LawfulEqOrd Offset where
+  eq_of_compare {a b} h := by
+    simp only [Offset.compare_def] at h
+    apply Offset.ext
+    exact LawfulEqOrd.eq_of_compare h

 namespace Offset

--- a/src/Std/Time/Zoned/TimeZone.lean
+++ b/src/Std/Time/Zoned/TimeZone.lean
@ -36,7 +36,7 @@ structure TimeZone where
  Day light saving flag.
  -/
  isDST : Bool
-  deriving Inhabited, Repr, BEq
+deriving Inhabited, Repr, DecidableEq

 namespace TimeZone

--- a/tests/lean/run/dateTimeOrd.lean
+++ b/tests/lean/run/dateTimeOrd.lean
@ -0,0 +1,48 @@
+import Std.Time
+
+open Std.Time
+
+def strictly_ordered {α} [Ord α] : List α → Bool
+  | [] => true
+  | [_] => true
+  | x :: y :: tail => compare x y = .lt && strictly_ordered (y :: tail)
+
+def plainDate1 := PlainDate.ofYearMonthDay? 2020 03 02 |>.get!
+def plainDate2 := PlainDate.ofYearMonthDay? 2025 01 02 |>.get!
+def plainDate3 := PlainDate.ofYearMonthDay? 2025 02 01 |>.get!
+
+example : Std.TransOrd PlainDate := inferInstance
+example : Std.LawfulEqOrd PlainDate := inferInstance
+example : Std.LawfulBEqOrd PlainDate := inferInstance
+example : strictly_ordered
+  [PlainDate.ofYearMonthDay? 2020 03 02 |>.get!,
+   PlainDate.ofYearMonthDay? 2025 01 02 |>.get!,
+   PlainDate.ofYearMonthDay? 2025 02 01 |>.get!] := by decide
+
+def plainTime1 := PlainTime.ofHourMinuteSecondsNano 0 0 0 1
+def plainTime2 := PlainTime.ofHourMinuteSecondsNano 0 0 1 0
+def plainTime3 := PlainTime.ofHourMinuteSecondsNano 0 1 0 0
+def plainTime4 := PlainTime.ofHourMinuteSecondsNano 1 0 0 0
+
+example : Std.TransOrd PlainTime := inferInstance
+example : Std.LawfulEqOrd PlainTime := inferInstance
+example : Std.LawfulBEqOrd PlainTime := inferInstance
+example : strictly_ordered
+  [PlainTime.ofHourMinuteSecondsNano 0 0 0 1,
+   PlainTime.ofHourMinuteSecondsNano 0 0 1 0,
+   PlainTime.ofHourMinuteSecondsNano 0 1 0 0,
+   PlainTime.ofHourMinuteSecondsNano 1 0 0 0] := by decide
+
+example : Std.TransOrd (DateTime TimeZone.GMT) := inferInstance
+example : Std.LawfulBEqOrd (DateTime TimeZone.GMT) := inferInstance
+
+-- We cannot use `decide` here because the reduction gets stuck.
+/-- info: true -/
+#guard_msgs in
+#eval strictly_ordered <|
+  ["Sat Jan 01 01:01:02 2025",
+   "Sat Jan 01 01:02:01 2025",
+   "Sat Jan 01 02:01:01 2025",
+   "Sat Jan 02 01:01:01 2025",
+   "Sat Feb 01 01:01:01 2025",
+   "Sat Jan 01 01:01:01 2026"].map (DateTime.fromAscTimeString . |>.toOption.get!)