diff --git a/doc/examples/ICERM2022/meta.lean b/doc/examples/ICERM2022/meta.lean
index 21552678927e..9e8fe40d7fcc 100644
--- a/doc/examples/ICERM2022/meta.lean
+++ b/doc/examples/ICERM2022/meta.lean
@@ -29,7 +29,7 @@ def ex3 (declName : Name) : MetaM Unit := do
     for x in xs do
       trace[Meta.debug] "{x} : {← inferType x}"
 
-def myMin [LT α] [DecidableRel (α := α) (·<·)] (a b : α) : α :=
+def myMin [LT α] [DecidableLT α] (a b : α) : α :=
   if a < b then
     a
   else
diff --git a/releases_drafts/list_lex.md b/releases_drafts/list_lex.md
new file mode 100644
index 000000000000..f1e0511de7d4
--- /dev/null
+++ b/releases_drafts/list_lex.md
@@ -0,0 +1,16 @@
+We replace the inductive predicate `List.lt` with an upstreamed version of `List.Lex` from Mathlib.
+(Previously `Lex.lt` was defined in terms of `<`; now it is generalized to take an arbitrary relation.)
+This subtely changes the notion of ordering on `List α`.
+
+`List.lt` was a weaker relation: in particular if `l₁ < l₂`, then
+`a :: l₁ < b :: l₂` may hold according to `List.lt` even if `a` and `b` are merely incomparable
+(either neither `a < b` nor `b < a`), whereas according to `List.Lex` this would require `a = b`.
+
+When `<` is total, in the sense that `¬ · < ·` is antisymmetric, then the two relations coincide.
+
+Mathlib was already overriding the order instances for `List α`,
+so this change should not be noticed by anyone already using Mathlib.
+
+We simultaneously add the boolean valued `List.lex` function, parameterised by a `BEq` typeclass
+and an arbitrary `lt` function. This will support the flexibility previously provided for `List.lt`,
+via a `==` function which is weaker than strict equality.
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index a5eb7f65971b..176af5833b36 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -2116,14 +2116,37 @@ instance : Commutative Or := ⟨fun _ _ => propext or_comm⟩
 instance : Commutative And := ⟨fun _ _ => propext and_comm⟩
 instance : Commutative Iff := ⟨fun _ _ => propext iff_comm⟩
 
+/-- `IsRefl X r` means the binary relation `r` on `X` is reflexive. -/
+class Refl (r : α → α → Prop) : Prop where
+  /-- A reflexive relation satisfies `r a a`. -/
+  refl : ∀ a, r a a
+
 /--
 `Antisymm (·≤·)` says that `(·≤·)` is antisymmetric, that is, `a ≤ b → b ≤ a → a = b`.
 -/
 class Antisymm (r : α → α → Prop) : Prop where
   /-- An antisymmetric relation `(·≤·)` satisfies `a ≤ b → b ≤ a → a = b`. -/
-  antisymm {a b : α} : r a b → r b a → a = b
+  antisymm (a b : α) : r a b → r b a → a = b
 
 @[deprecated Antisymm (since := "2024-10-16"), inherit_doc Antisymm]
 abbrev _root_.Antisymm (r : α → α → Prop) : Prop := Std.Antisymm r
 
+/-- `Asymm X r` means that the binary relation `r` on `X` 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
+
+/-- `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
+  /-- A total relation satisfies `r a b ∨ r b a`. -/
+  total : ∀ a b, r a b ∨ r b a
+
+/-- `Irrefl X r` means the binary relation `r` on `X` is irreflexive (that is, `r x x` never
+holds). -/
+class Irrefl (r : α → α → Prop) : Prop where
+  /-- An irreflexive relation satisfies `¬ r a a`. -/
+  irrefl : ∀ a, ¬r a a
+
 end Std
diff --git a/src/Init/Data/Array.lean b/src/Init/Data/Array.lean
index 82d5839a3c16..36b1ff3e5f46 100644
--- a/src/Init/Data/Array.lean
+++ b/src/Init/Data/Array.lean
@@ -22,3 +22,4 @@ import Init.Data.Array.Monadic
 import Init.Data.Array.FinRange
 import Init.Data.Array.Perm
 import Init.Data.Array.Find
+import Init.Data.Array.Lex
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index b51e8d386580..e75f765a8cba 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -944,6 +944,19 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α :=
   as.foldl (init := (#[], #[])) fun (as, bs) a =>
     if p a then (as.push a, bs) else (as, bs.push a)
 
+/-! ### Lexicographic ordering -/
+
+instance instLT [LT α] : LT (Array α) := ⟨fun as bs => as.toList < bs.toList⟩
+instance instLE [LT α] : LE (Array α) := ⟨fun as bs => as.toList ≤ bs.toList⟩
+
+instance [DecidableEq α] [LT α] [DecidableLT α] : DecidableLT (Array α) :=
+  inferInstanceAs <| DecidableRel fun (as bs : Array α) => as.toList < bs.toList
+
+instance [DecidableEq α] [LT α] [DecidableLT α] : DecidableLE (Array α) :=
+  inferInstanceAs <| DecidableRel fun (as bs : Array α) => as.toList ≤ bs.toList
+
+-- See `Init.Data.Array.Lex` for the boolean valued lexicographic comparator.
+
 /-! ## Auxiliary functions used in metaprogramming.
 
 We do not currently intend to provide verification theorems for these functions.
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 8c7c1571b401..11ef9b1b5563 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -12,6 +12,7 @@ import Init.Data.List.Monadic
 import Init.Data.List.OfFn
 import Init.Data.Array.Mem
 import Init.Data.Array.DecidableEq
+import Init.Data.Array.Lex
 import Init.TacticsExtra
 import Init.Data.List.ToArray
 
@@ -924,12 +925,26 @@ theorem mem_or_eq_of_mem_setIfInBounds
 
 /-! ### BEq -/
 
+
+@[simp] theorem beq_empty_iff [BEq α] {xs : Array α} : (xs == #[]) = xs.isEmpty := by
+  cases xs
+  simp
+
+@[simp] theorem empty_beq_iff [BEq α] {xs : Array α} : (#[] == xs) = xs.isEmpty := by
+  cases xs
+  simp
+
 @[simp] theorem push_beq_push [BEq α] {a b : α} {v : Array α} {w : Array α} :
     (v.push a == w.push b) = (v == w && a == b) := by
   cases v
   cases w
   simp
 
+theorem size_eq_of_beq [BEq α] {xs ys : Array α} (h : xs == ys) : xs.size = ys.size := by
+  cases xs
+  cases ys
+  simp [List.length_eq_of_beq (by simpa using h)]
+
 @[simp] theorem mkArray_beq_mkArray [BEq α] {a b : α} {n : Nat} :
     (mkArray n a == mkArray n b) = (n == 0 || a == b) := by
   cases n with
@@ -974,6 +989,8 @@ theorem mem_or_eq_of_mem_setIfInBounds
     · intro a
       apply Array.isEqv_self_beq
 
+/-! ### Lexicographic ordering -/
+
 /-! Content below this point has not yet been aligned with `List`. -/
 
 theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := rfl
diff --git a/src/Init/Data/Array/Lex.lean b/src/Init/Data/Array/Lex.lean
new file mode 100644
index 000000000000..65d1bdfeab2e
--- /dev/null
+++ b/src/Init/Data/Array/Lex.lean
@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Kim Morrison
+-/
+prelude
+import Init.Data.Array.Basic
+import Init.Data.Nat.Lemmas
+import Init.Data.Range
+
+namespace Array
+
+/--
+Lexicographic comparator for arrays.
+
+`lex as bs lt` is true if
+- `bs` is larger than `as` and `as` is pairwise equivalent via `==` to the initial segment of `bs`, or
+- there is an index `i` such that `lt as[i] bs[i]`, and for all `j < i`, `as[j] == bs[j]`.
+-/
+def lex [BEq α] (as bs : Array α) (lt : α → α → Bool := by exact (· < ·)) : Bool := Id.run do
+  for h : i in [0 : min as.size bs.size] do
+    -- TODO: `omega` should be able to find this itself.
+    have : i < min as.size bs.size := Membership.get_elem_helper h rfl
+    if lt as[i] bs[i] then
+      return true
+    else if as[i] != bs[i] then
+      return false
+  return as.size < bs.size
+
+end Array
diff --git a/src/Init/Data/Char/Lemmas.lean b/src/Init/Data/Char/Lemmas.lean
index 5025eb7e9e50..a93cc7af78b0 100644
--- a/src/Init/Data/Char/Lemmas.lean
+++ b/src/Init/Data/Char/Lemmas.lean
@@ -9,6 +9,9 @@ import Init.Data.UInt.Lemmas
 
 namespace Char
 
+@[ext] protected theorem ext : {a b : Char} → a.val = b.val → a = b
+  | ⟨_,_⟩, ⟨_,_⟩, rfl => rfl
+
 theorem le_def {a b : Char} : a ≤ b ↔ a.1 ≤ b.1 := .rfl
 theorem lt_def {a b : Char} : a < b ↔ a.1 < b.1 := .rfl
 theorem lt_iff_val_lt_val {a b : Char} : a < b ↔ a.val < b.val := Iff.rfl
@@ -19,9 +22,44 @@ theorem lt_iff_val_lt_val {a b : Char} : a < b ↔ a.val < b.val := Iff.rfl
 protected theorem le_trans {a b c : Char} : a ≤ b → b ≤ c → a ≤ c := UInt32.le_trans
 protected theorem lt_trans {a b c : Char} : a < b → b < c → a < c := UInt32.lt_trans
 protected theorem le_total (a b : Char) : a ≤ b ∨ b ≤ a := UInt32.le_total a.1 b.1
+protected theorem le_antisymm {a b : Char} : a ≤ b → b ≤ a → a = b :=
+  fun h₁ h₂ => Char.ext (UInt32.le_antisymm h₁ h₂)
 protected theorem lt_asymm {a b : Char} (h : a < b) : ¬ b < a := UInt32.lt_asymm h
 protected theorem ne_of_lt {a b : Char} (h : a < b) : a ≠ b := Char.ne_of_val_ne (UInt32.ne_of_lt h)
 
+instance ltIrrefl : Std.Irrefl (· < · : Char → Char → Prop) where
+  irrefl := Char.lt_irrefl
+
+instance leRefl : Std.Refl (· ≤ · : Char → Char → Prop) where
+  refl := Char.le_refl
+
+instance leTrans : Trans (· ≤ · : Char → Char → Prop) (· ≤ ·) (· ≤ ·) where
+  trans := Char.le_trans
+
+instance ltTrans : Trans (· < · : Char → Char → Prop) (· < ·) (· < ·) where
+  trans := Char.lt_trans
+
+-- This instance is useful while setting up instances for `String`.
+def notLTTrans : Trans (¬ · < · : Char → Char → Prop) (¬ · < ·) (¬ · < ·) where
+  trans h₁ h₂ := by simpa using Char.le_trans (by simpa using h₂) (by simpa using h₁)
+
+instance leAntisymm : Std.Antisymm (· ≤ · : Char → Char → Prop) where
+  antisymm _ _ := Char.le_antisymm
+
+-- This instance is useful while setting up instances for `String`.
+def notLTAntisymm : Std.Antisymm (¬ · < · : Char → Char → Prop) where
+  antisymm _ _ h₁ h₂ := Char.le_antisymm (by simpa using h₂) (by simpa using h₁)
+
+instance ltAsymm : Std.Asymm (· < · : Char → Char → Prop) where
+  asymm _ _ := Char.lt_asymm
+
+instance leTotal : Std.Total (· ≤ · : Char → Char → Prop) where
+  total := Char.le_total
+
+-- This instance is useful while setting up instances for `String`.
+def notLTTotal : Std.Total (¬ · < · : Char → Char → Prop) where
+  total := fun x y => by simpa using Char.le_total y x
+
 theorem utf8Size_eq (c : Char) : c.utf8Size = 1 ∨ c.utf8Size = 2 ∨ c.utf8Size = 3 ∨ c.utf8Size = 4 := by
   have := c.utf8Size_pos
   have := c.utf8Size_le_four
@@ -31,9 +69,6 @@ theorem utf8Size_eq (c : Char) : c.utf8Size = 1 ∨ c.utf8Size = 2 ∨ c.utf8Siz
   rw [Char.ofNat, dif_pos]
   rfl
 
-@[ext] protected theorem ext : {a b : Char} → a.val = b.val → a = b
-  | ⟨_,_⟩, ⟨_,_⟩, rfl => rfl
-
 end Char
 
 @[deprecated Char.utf8Size (since := "2024-06-04")] abbrev String.csize := Char.utf8Size
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index f223857146e8..3352b90f44d5 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -162,46 +162,74 @@ theorem isEqv_cons₂ : isEqv (a::as) (b::bs) eqv = (eqv a b && isEqv as bs eqv)
 
 /-! ## Lexicographic ordering -/
 
-/--
-The lexicographic order on lists.
-`[] < a::as`, and `a::as < b::bs` if `a < b` or if `a` and `b` are equivalent and `as < bs`.
--/
-inductive lt [LT α] : List α → List α → Prop where
+/-- Lexicographic ordering for lists. -/
+inductive Lex (r : α → α → Prop) : List α → List α → Prop
   /-- `[]` is the smallest element in the order. -/
-  | nil  (b : α) (bs : List α) : lt [] (b::bs)
+  | nil {a l} : Lex r [] (a :: l)
+  /-- If `a` is indistinguishable from `b` and `as < bs`, then `a::as < b::bs`. -/
+  | cons {a l₁ l₂} (h : Lex r l₁ l₂) : Lex r (a :: l₁) (a :: l₂)
   /-- If `a < b` then `a::as < b::bs`. -/
-  | head {a : α} (as : List α) {b : α} (bs : List α) : a < b → lt (a::as) (b::bs)
-  /-- If `a` and `b` are equivalent and `as < bs`, then `a::as < b::bs`. -/
-  | tail {a : α} {as : List α} {b : α} {bs : List α} : ¬ a < b → ¬ b < a → lt as bs → lt (a::as) (b::bs)
-
-instance [LT α] : LT (List α) := ⟨List.lt⟩
+  | rel {a₁ l₁ a₂ l₂} (h : r a₁ a₂) : Lex r (a₁ :: l₁) (a₂ :: l₂)
 
-instance hasDecidableLt [LT α] [h : DecidableRel (α := α) (· < ·)] : (l₁ l₂ : List α) → Decidable (l₁ < l₂)
-  | [],    []    => isFalse nofun
-  | [],    _::_  => isTrue (List.lt.nil _ _)
-  | _::_, []     => isFalse nofun
+instance decidableLex [DecidableEq α] (r : α → α → Prop) [h : DecidableRel r] :
+    (l₁ l₂ : List α) → Decidable (Lex r l₁ l₂)
+  | [], [] => isFalse nofun
+  | [], _::_ => isTrue Lex.nil
+  | _::_, [] => isFalse nofun
   | a::as, b::bs =>
     match h a b with
-    | isTrue h₁  => isTrue (List.lt.head _ _ h₁)
+    | isTrue h₁ => isTrue (Lex.rel h₁)
     | isFalse h₁ =>
-      match h b a with
-      | isTrue h₂  => isFalse (fun h => match h with
-         | List.lt.head _ _ h₁' => absurd h₁' h₁
-         | List.lt.tail _ h₂' _ => absurd h₂ h₂')
-      | isFalse h₂ =>
-        match hasDecidableLt as bs with
-        | isTrue h₃  => isTrue (List.lt.tail h₁ h₂ h₃)
+      if h₂ : a = b then
+        match decidableLex r as bs with
+        | isTrue h₃ => isTrue (h₂ ▸ Lex.cons h₃)
         | isFalse h₃ => isFalse (fun h => match h with
-           | List.lt.head _ _ h₁' => absurd h₁' h₁
-           | List.lt.tail _ _ h₃' => absurd h₃' h₃)
+          | Lex.rel h₁' => absurd h₁' h₁
+          | Lex.cons h₃' => absurd h₃' h₃)
+      else
+        isFalse (fun h => match h with
+          | Lex.rel h₁' => absurd h₁' h₁
+          | Lex.cons h₂' => h₂ rfl)
+
+@[inherit_doc Lex]
+protected abbrev lt [LT α] : List α → List α → Prop := Lex (· < ·)
+
+instance instLT [LT α] : LT (List α) := ⟨List.lt⟩
+
+/-- Decidability of lexicographic ordering. -/
+instance decidableLT [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List α) :
+    Decidable (l₁ < l₂) := decidableLex (· < ·) l₁ l₂
+
+@[deprecated decidableLT (since := "2024-12-13"), inherit_doc decidableLT]
+abbrev hasDecidableLt := @decidableLT
 
 /-- The lexicographic order on lists. -/
 @[reducible] protected def le [LT α] (a b : List α) : Prop := ¬ b < a
 
-instance [LT α] : LE (List α) := ⟨List.le⟩
+instance instLE [LT α] : LE (List α) := ⟨List.le⟩
+
+instance decidableLE [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List α) :
+    Decidable (l₁ ≤ l₂) :=
+  inferInstanceAs (Decidable (Not _))
+
+/--
+Lexicographic comparator for lists.
+
+* `lex lt [] (b :: bs)` is true.
+* `lex lt as []` is false.
+* `lex lt (a :: as) (b :: bs)` is true if `lt a b` or `a == b` and `lex lt as bs` is true.
+-/
+def lex [BEq α] (l₁ l₂ : List α) (lt : α → α → Bool := by exact (· < ·)) : Bool :=
+  match l₁, l₂ with
+  | [],      _ :: _  => true
+  | _,      []       => false
+  | a :: as, b :: bs => lt a b || (a == b && lex as bs lt)
 
-instance [LT α] [DecidableRel ((· < ·) : α → α → Prop)] : (l₁ l₂ : List α) → Decidable (l₁ ≤ l₂) :=
-  fun _ _ => inferInstanceAs (Decidable (Not _))
+@[simp] theorem lex_nil_nil [BEq α] : lex ([] : List α) [] lt = false := rfl
+@[simp] theorem lex_nil_cons [BEq α] {b} {bs : List α} : lex [] (b :: bs) lt = true := rfl
+@[simp] theorem lex_cons_nil [BEq α] {a} {as : List α} : lex (a :: as) [] lt = false := rfl
+@[simp] theorem lex_cons_cons [BEq α] {a b} {as bs : List α} :
+    lex (a :: as) (b :: bs) lt = (lt a b || (a == b && lex as bs lt)) := rfl
 
 /-! ## Alternative getters -/
 
diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean
index 8731205c3511..e9c81df36018 100644
--- a/src/Init/Data/List/BasicAux.lean
+++ b/src/Init/Data/List/BasicAux.lean
@@ -233,25 +233,34 @@ theorem sizeOf_get [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.g
     apply Nat.lt_trans ih
     simp_arith
 
-theorem le_antisymm [LT α] [s : Std.Antisymm (¬ · < · : α → α → Prop)]
-    {as bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) : as = bs :=
+theorem not_lex_antisymm [DecidableEq α] {r : α → α → Prop} [DecidableRel r]
+    (antisymm : ∀ x y : α, ¬ r x y → ¬ r y x → x = y)
+    {as bs : List α} (h₁ : ¬ Lex r bs as) (h₂ : ¬ Lex r as bs) : as = bs :=
   match as, bs with
   | [],    []    => rfl
-  | [],    _::_ => False.elim <| h₂ (List.lt.nil ..)
-  | _::_, []    => False.elim <| h₁ (List.lt.nil ..)
+  | [],    _::_ => False.elim <| h₂ (List.Lex.nil ..)
+  | _::_, []    => False.elim <| h₁ (List.Lex.nil ..)
   | a::as, b::bs => by
-    by_cases hab : a < b
-    · exact False.elim <| h₂ (List.lt.head _ _ hab)
-    · by_cases hba : b < a
-      · exact False.elim <| h₁ (List.lt.head _ _ hba)
-      · have h₁ : as ≤ bs := fun h => h₁ (List.lt.tail hba hab h)
-        have h₂ : bs ≤ as := fun h => h₂ (List.lt.tail hab hba h)
-        have ih : as = bs := le_antisymm h₁ h₂
-        have : a = b := s.antisymm hab hba
-        simp [this, ih]
-
-instance [LT α] [Std.Antisymm (¬ · < · : α → α → Prop)] :
+    by_cases hab : r a b
+    · exact False.elim <| h₂ (List.Lex.rel hab)
+    · by_cases eq : a = b
+      · subst eq
+        have h₁ : ¬ Lex r bs as := fun h => h₁ (List.Lex.cons h)
+        have h₂ : ¬ Lex r as bs := fun h => h₂ (List.Lex.cons h)
+        simp [not_lex_antisymm antisymm h₁ h₂]
+      · exfalso
+        by_cases hba : r b a
+        · exact h₁ (Lex.rel hba)
+        · exact eq (antisymm _ _ hab hba)
+
+protected theorem le_antisymm [DecidableEq α] [LT α] [DecidableLT α]
+    [i : Std.Antisymm (¬ · < · : α → α → Prop)]
+    {as bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) : as = bs :=
+  not_lex_antisymm i.antisymm h₁ h₂
+
+instance [DecidableEq α] [LT α] [DecidableLT α]
+    [s : Std.Antisymm (¬ · < · : α → α → Prop)] :
     Std.Antisymm (· ≤ · : List α → List α → Prop) where
-  antisymm h₁ h₂ := le_antisymm h₁ h₂
+  antisymm _ _ h₁ h₂ := List.le_antisymm h₁ h₂
 
 end List
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index d1acd91047f2..f9b081a6836e 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -674,6 +674,42 @@ theorem mem_or_eq_of_mem_set : ∀ {l : List α} {n : Nat} {a b : α}, a ∈ l.s
 
 /-! ### BEq -/
 
+@[simp] theorem beq_nil_iff [BEq α] {l : List α} : (l == []) = l.isEmpty := by
+  cases l <;> rfl
+
+@[simp] theorem nil_beq_iff [BEq α] {l : List α} : ([] == l) = l.isEmpty := by
+  cases l <;> rfl
+
+@[simp] theorem cons_beq_cons [BEq α] {a b : α} {l₁ l₂ : List α} :
+    (a :: l₁ == b :: l₂) = (a == b && l₁ == l₂) := rfl
+
+@[simp] theorem concat_beq_concat [BEq α] {a b : α} {l₁ l₂ : List α} :
+    (l₁ ++ [a] == l₂ ++ [b]) = (l₁ == l₂ && a == b) := by
+  induction l₁ generalizing l₂ with
+  | nil => cases l₂ <;> simp
+  | cons x l₁ ih =>
+    cases l₂ with
+    | nil => simp
+    | cons y l₂ => simp [ih, Bool.and_assoc]
+
+theorem length_eq_of_beq [BEq α] {l₁ l₂ : List α} (h : l₁ == l₂) : l₁.length = l₂.length :=
+  match l₁, l₂ with
+  | [], [] => rfl
+  | [], _ :: _ => by simp [beq_nil_iff] at h
+  | _ :: _, [] => by simp [nil_beq_iff] at h
+  | a :: l₁, b :: l₂ => by
+    simp at h
+    simpa [Nat.add_one_inj] using length_eq_of_beq h.2
+
+@[simp] theorem replicate_beq_replicate [BEq α] {a b : α} {n : Nat} :
+    (replicate n a == replicate n b) = (n == 0 || a == b) := by
+  cases n with
+  | zero => simp
+  | succ n =>
+    rw [replicate_succ, replicate_succ, cons_beq_cons, replicate_beq_replicate]
+    rw [Bool.eq_iff_iff]
+    simp +contextual
+
 @[simp] theorem reflBEq_iff [BEq α] : ReflBEq (List α) ↔ ReflBEq α := by
   constructor
   · intro h
@@ -711,75 +747,397 @@ theorem mem_or_eq_of_mem_set : ∀ {l : List α} {n : Nat} {a b : α}, a ∈ l.s
     · intro a
       simp
 
-@[simp] theorem beq_nil_iff [BEq α] {l : List α} : (l == []) = l.isEmpty := by
-  cases l <;> rfl
+/-! ### Lexicographic ordering -/
 
-@[simp] theorem nil_beq_iff [BEq α] {l : List α} : ([] == l) = l.isEmpty := by
-  cases l <;> rfl
 
-@[simp] theorem cons_beq_cons [BEq α] {a b : α} {l₁ l₂ : List α} :
-    (a :: l₁ == b :: l₂) = (a == b && l₁ == l₂) := rfl
+theorem lex_irrefl {r : α → α → Prop} (irrefl : ∀ x, ¬r x x) (l : List α) : ¬Lex r l l := by
+  induction l with
+  | nil => nofun
+  | cons a l ih => intro
+    | .rel h => exact irrefl _ h
+    | .cons h => exact ih h
 
-@[simp] theorem concat_beq_concat [BEq α] {a b : α} {l₁ l₂ : List α} :
-    (l₁ ++ [a] == l₂ ++ [b]) = (l₁ == l₂ && a == b) := by
-  induction l₁ generalizing l₂ with
-  | nil => cases l₂ <;> simp
-  | cons x l₁ ih =>
-    cases l₂ with
-    | nil => simp
-    | cons y l₂ => simp [ih, Bool.and_assoc]
+protected theorem lt_irrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)] (l : List α) : ¬ l < l :=
+  lex_irrefl Std.Irrefl.irrefl l
 
-theorem length_eq_of_beq [BEq α] {l₁ l₂ : List α} (h : l₁ == l₂) : l₁.length = l₂.length :=
-  match l₁, l₂ with
-  | [], [] => rfl
-  | [], _ :: _ => by simp [beq_nil_iff] at h
-  | _ :: _, [] => by simp [nil_beq_iff] at h
-  | a :: l₁, b :: l₂ => by
-    simp at h
-    simpa [Nat.add_one_inj]using length_eq_of_beq h.2
+instance ltIrrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)] : Std.Irrefl (α := List α) (· < ·) where
+  irrefl := List.lt_irrefl
 
-/-! ### Lexicographic ordering -/
+@[simp] theorem not_lex_nil : ¬Lex r l [] := fun h => nomatch h
+
+@[simp] theorem nil_le [LT α] (l : List α) : [] ≤ l := fun h => nomatch h
 
-protected theorem lt_irrefl [LT α] (lt_irrefl : ∀ x : α, ¬x < x) (l : List α) : ¬l < l := by
+@[simp] theorem not_nil_lex_iff : ¬Lex r [] l ↔ l = [] := by
+  constructor
+  · rintro h
+    match l, h with
+    | [], h => rfl
+    | a :: _, h => exact False.elim (h Lex.nil)
+  · rintro rfl
+    exact not_lex_nil
+
+@[simp] theorem le_nil [LT α] (l : List α) : l ≤ [] ↔ l = [] := not_nil_lex_iff
+
+@[simp] theorem nil_lex_cons : Lex r [] (a :: l) := Lex.nil
+
+@[simp] theorem nil_lt_cons [LT α] (a : α) (l : List α) : [] < a :: l := Lex.nil
+
+theorem cons_lex_cons_iff : Lex r (a :: l₁) (b :: l₂) ↔ r a b ∨ a = b ∧ Lex r l₁ l₂ :=
+  ⟨fun | .rel h => .inl h | .cons h => .inr ⟨rfl, h⟩,
+    fun | .inl h => Lex.rel h | .inr ⟨rfl, h⟩ => Lex.cons h⟩
+
+theorem cons_lt_cons_iff [LT α] {a b} {l₁ l₂ : List α} :
+    (a :: l₁) < (b :: l₂) ↔ a < b ∨ a = b ∧ l₁ < l₂ := by
+  dsimp only [instLT, List.lt]
+  simp [cons_lex_cons_iff]
+
+theorem not_cons_lex_cons_iff [DecidableEq α] [DecidableRel r] {a b} {l₁ l₂ : List α} :
+    ¬ Lex r (a :: l₁) (b :: l₂) ↔ (¬ r a b ∧ a ≠ b) ∨ (¬ r a b ∧ ¬ Lex r l₁ l₂) := by
+  rw [cons_lex_cons_iff, not_or, Decidable.not_and_iff_or_not, and_or_left]
+
+theorem cons_le_cons_iff [DecidableEq α] [LT α] [DecidableLT α]
+    [i₀ : Std.Irrefl (· < · : α → α → Prop)]
+    [i₁ : Std.Asymm (· < · : α → α → Prop)]
+    [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
+    {a b} {l₁ l₂ : List α} :
+    (a :: l₁) ≤ (b :: l₂) ↔ a < b ∨ a = b ∧ l₁ ≤ l₂ := by
+  dsimp only [instLE, instLT, List.le, List.lt]
+  simp [not_cons_lex_cons_iff]
+  constructor
+  · rintro (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)
+    · left
+      apply Decidable.byContradiction
+      intro h₃
+      apply h₂
+      exact i₂.antisymm _ _ h₁ h₃
+    · if h₃ : a < b then
+        exact .inl h₃
+      else
+        right
+        exact ⟨i₂.antisymm _ _ h₃ h₁, h₂⟩
+  · rintro (h | ⟨h₁, h₂⟩)
+    · left
+      exact ⟨i₁.asymm _ _ h, fun w => i₀.irrefl _ (w ▸ h)⟩
+    · right
+      exact ⟨fun w => i₀.irrefl _ (h₁ ▸ w), h₂⟩
+
+theorem not_lt_of_cons_le_cons [DecidableEq α] [LT α] [DecidableLT α]
+    [i₀ : Std.Irrefl (· < · : α → α → Prop)]
+    [i₁ : Std.Asymm (· < · : α → α → Prop)]
+    [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
+    {a b : α} {l₁ l₂ : List α} (h : a :: l₁ ≤ b :: l₂) : ¬ b < a := by
+  rw [cons_le_cons_iff] at h
+  rcases h with h | ⟨rfl, h⟩
+  · exact i₁.asymm _ _ h
+  · exact i₀.irrefl _
+
+theorem le_of_cons_le_cons [DecidableEq α] [LT α] [DecidableLT α]
+    [i₀ : Std.Irrefl (· < · : α → α → Prop)]
+    [i₁ : Std.Asymm (· < · : α → α → Prop)]
+    [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
+    {a} {l₁ l₂ : List α} (h : a :: l₁ ≤ a :: l₂) : l₁ ≤ l₂ := by
+  rw [cons_le_cons_iff] at h
+  rcases h with h | ⟨_, h⟩
+  · exact False.elim (i₀.irrefl _ h)
+  · exact h
+
+protected theorem le_refl [LT α] [i₀ : Std.Irrefl (· < · : α → α → Prop)] (l : List α) : l ≤ l := by
   induction l with
-  | nil => nofun
-  | cons a l ih => intro
-    | .head _ _ h => exact lt_irrefl _ h
-    | .tail _ _ h => exact ih h
+  | nil => simp
+  | cons a l ih =>
+    intro
+    | .rel h => exact i₀.irrefl _ h
+    | .cons h₃ => exact ih h₃
 
-protected theorem lt_trans [LT α] [DecidableRel (@LT.lt α _)]
-    (lt_trans : ∀ {x y z : α}, x < y → y < z → x < z)
-    (le_trans : ∀ {x y z : α}, ¬x < y → ¬y < z → ¬x < z)
-    {l₁ l₂ l₃ : List α} (h₁ : l₁ < l₂) (h₂ : l₂ < l₃) : l₁ < l₃ := by
+instance [LT α] [Std.Irrefl (· < · : α → α → Prop)] : Std.Refl (· ≤ · : List α → List α → Prop) where
+  refl := List.le_refl
+
+theorem lex_trans {r : α → α → Prop} [DecidableRel r]
+    (lt_trans : ∀ {x y z : α}, r x y → r y z → r x z)
+    (h₁ : Lex r l₁ l₂) (h₂ : Lex r l₂ l₃) : Lex r l₁ l₃ := by
   induction h₁ generalizing l₃ with
-  | nil => let _::_ := l₃; exact List.lt.nil ..
-  | @head a l₁ b l₂ ab =>
+  | nil => let _::_ := l₃; exact List.Lex.nil ..
+  | @rel a l₁ b l₂ ab =>
     match h₂ with
-    | .head l₂ l₃ bc => exact List.lt.head _ _ (lt_trans ab bc)
-    | .tail _ cb ih =>
-      exact List.lt.head _ _ <| Decidable.by_contra (le_trans · cb ab)
-  | @tail a l₁ b l₂ ab ba h₁ ih2 =>
+    | .rel bc => exact List.Lex.rel (lt_trans ab bc)
+    | .cons ih =>
+      exact List.Lex.rel ab
+  | @cons a l₁ l₂ h₁ ih2 =>
     match h₂ with
-    | .head l₂ l₃ bc =>
-      exact List.lt.head _ _ <| Decidable.by_contra (le_trans ba · bc)
-    | .tail bc cb ih =>
-      exact List.lt.tail (le_trans ab bc) (le_trans cb ba) (ih2 ih)
-
-protected theorem lt_antisymm [LT α]
-    (lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y)
-    {l₁ l₂ : List α} (h₁ : ¬l₁ < l₂) (h₂ : ¬l₂ < l₁) : l₁ = l₂ := by
+    | .rel bc =>
+      exact List.Lex.rel bc
+    | .cons ih =>
+      exact List.Lex.cons (ih2 ih)
+
+protected theorem lt_trans [LT α] [DecidableLT α]
+    [i₁ : Trans (· < · : α → α → Prop) (· < ·) (· < ·)]
+    {l₁ l₂ l₃ : List α} (h₁ : l₁ < l₂) (h₂ : l₂ < l₃) : l₁ < l₃ := by
+  simp only [instLT, List.lt] at h₁ h₂ ⊢
+  exact lex_trans (fun h₁ h₂ => i₁.trans h₁ h₂) h₁ h₂
+
+instance [LT α] [DecidableLT α]
+    [Trans (· < · : α → α → Prop) (· < ·) (· < ·)] :
+    Trans (· < · : List α → List α → Prop) (· < ·) (· < ·) where
+  trans h₁ h₂ := List.lt_trans h₁ h₂
+
+instance [LT α] [DecidableLT α]
+    [Trans (· < · : α → α → Prop) (· < ·) (· < ·)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)] :
+    Trans (· < · : List α → List α → Prop) (· < ·) (· < ·) where
+  trans h₁ h₂ := List.lt_trans h₁ h₂
+
+@[deprecated List.le_antisymm (since := "2024-12-13")]
+protected abbrev lt_antisymm := @List.le_antisymm
+
+protected theorem lt_of_le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
+    [i₀ : Std.Irrefl (· < · : α → α → Prop)]
+    [i₁ : Std.Asymm (· < · : α → α → Prop)]
+    [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
+    [i₃ : Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
+    {l₁ l₂ l₃ : List α} (h₁ : l₁ ≤ l₂) (h₂ : l₂ < l₃) : l₁ < l₃ := by
+  induction h₂ generalizing l₁ with
+  | nil => simp_all
+  | rel hab =>
+    rename_i a b
+    cases l₁ with
+    | nil => simp_all
+    | cons c l₁ =>
+      apply Lex.rel
+      replace h₁ := not_lt_of_cons_le_cons h₁
+      apply Decidable.byContradiction
+      intro h₂
+      have := i₃.trans h₁ h₂
+      contradiction
+  | cons w₃ ih =>
+    rename_i a as bs
+    cases l₁ with
+    | nil => simp_all
+    | cons c l₁ =>
+      have w₄ := not_lt_of_cons_le_cons h₁
+      by_cases w₅ : a = c
+      · subst w₅
+        exact Lex.cons (ih (le_of_cons_le_cons h₁))
+      · exact Lex.rel (Decidable.byContradiction fun w₆ => w₅ (i₂.antisymm _ _ w₄ w₆))
+
+protected theorem le_trans [DecidableEq α] [LT α] [DecidableLT α]
+    [Std.Irrefl (· < · : α → α → Prop)]
+    [Std.Asymm (· < · : α → α → Prop)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)]
+    [Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
+    {l₁ l₂ l₃ : List α} (h₁ : l₁ ≤ l₂) (h₂ : l₂ ≤ l₃) : l₁ ≤ l₃ :=
+  fun h₃ => h₁ (List.lt_of_le_of_lt h₂ h₃)
+
+instance [DecidableEq α] [LT α] [DecidableLT α]
+    [Std.Irrefl (· < · : α → α → Prop)]
+    [Std.Asymm (· < · : α → α → Prop)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)]
+    [Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)] :
+    Trans (· ≤ · : List α → List α → Prop) (· ≤ ·) (· ≤ ·) where
+  trans h₁ h₂ := List.le_trans h₁ h₂
+
+theorem lex_asymm {r : α → α → Prop} [DecidableRel r]
+    (h : ∀ {x y : α}, r x y → ¬ r y x) : ∀ {l₁ l₂ : List α}, Lex r l₁ l₂ → ¬ Lex r l₂ l₁
+  | nil, _, .nil => by simp
+  | x :: l₁, y :: l₂, .rel h₁ =>
+    fun
+    | .rel h₂ => h h₁ h₂
+    | .cons h₂ => h h₁ h₁
+  | x :: l₁, _ :: l₂, .cons h₁ =>
+    fun
+    | .rel h₂ => h h₂ h₂
+    | .cons h₂ => lex_asymm h h₁ h₂
+
+protected theorem lt_asymm [DecidableEq α] [LT α] [DecidableLT α]
+    [i : Std.Asymm (· < · : α → α → Prop)]
+    {l₁ l₂ : List α} (h : l₁ < l₂) : ¬ l₂ < l₁ := lex_asymm (i.asymm _ _) h
+
+instance [DecidableEq α] [LT α] [DecidableLT α]
+    [Std.Asymm (· < · : α → α → Prop)] :
+    Std.Asymm (· < · : List α → List α → Prop) where
+  asymm _ _ := List.lt_asymm
+
+theorem not_lex_total [DecidableEq α] {r : α → α → Prop} [DecidableRel r]
+    (h : ∀ x y : α, ¬ r x y ∨ ¬ r y x) (l₁ l₂ : List α) : ¬ Lex r l₁ l₂ ∨ ¬ Lex r l₂ l₁ := by
+  rw [Decidable.or_iff_not_imp_left, Decidable.not_not]
+  intro w₁ w₂
+  match l₁, l₂, w₁, w₂ with
+  | nil, _ :: _, .nil, w₂ => simp at w₂
+  | x :: _, y :: _, .rel _, .rel _ =>
+    obtain (_ | _) := h x y <;> contradiction
+  | x :: _, _ :: _, .rel _, .cons _ =>
+    obtain (_ | _) := h x x <;> contradiction
+  | x :: _, _ :: _, .cons  _, .rel _ =>
+    obtain (_ | _) := h x x <;> contradiction
+  | _ :: l₁, _ :: l₂, .cons _, .cons _ =>
+    obtain (_ | _) := not_lex_total h l₁ l₂ <;> contradiction
+
+protected theorem le_total [DecidableEq α] [LT α] [DecidableLT α]
+    [i : Std.Total (¬ · < · : α → α → Prop)] {l₁ l₂ : List α} : l₁ ≤ l₂ ∨ l₂ ≤ l₁ :=
+  not_lex_total i.total l₂ l₁
+
+instance [DecidableEq α] [LT α] [DecidableLT α]
+    [Std.Total (¬ · < · : α → α → Prop)] :
+    Std.Total (· ≤ · : List α → List α → Prop) where
+  total _ _ := List.le_total
+
+theorem lex_eq_decide_lex [DecidableEq α] (lt : α → α → Bool) :
+    lex l₁ l₂ lt = decide (Lex (fun x y => lt x y) l₁ l₂) := by
   induction l₁ generalizing l₂ with
   | nil =>
     cases l₂ with
-    | nil => rfl
-    | cons b l₂ => cases h₁ (.nil ..)
+    | nil => simp [lex]
+    | cons b bs => simp [lex]
+  | cons a l₁ ih =>
+    cases l₂ with
+    | nil => simp [lex]
+    | cons b bs =>
+      simp [lex, ih, cons_lex_cons_iff, Bool.beq_eq_decide_eq]
+
+/-- Variant of `lex_eq_true_iff` using an arbitrary comparator. -/
+@[simp] theorem lex_eq_true_iff_lex [DecidableEq α] (lt : α → α → Bool) :
+    lex l₁ l₂ lt = true ↔ Lex (fun x y => lt x y) l₁ l₂ := by
+  simp [lex_eq_decide_lex]
+
+/-- Variant of `lex_eq_false_iff` using an arbitrary comparator. -/
+@[simp] theorem lex_eq_false_iff_not_lex [DecidableEq α] (lt : α → α → Bool) :
+    lex l₁ l₂ lt = false ↔ ¬ Lex (fun x y => lt x y) l₁ l₂ := by
+  simp [Bool.eq_false_iff, lex_eq_true_iff_lex]
+
+@[simp] theorem lex_eq_true_iff_lt [DecidableEq α] [LT α] [DecidableLT α]
+    {l₁ l₂ : List α} : lex l₁ l₂ = true ↔ l₁ < l₂ := by
+  simp only [lex_eq_true_iff_lex, decide_eq_true_eq]
+  exact Iff.rfl
+
+@[simp] theorem lex_eq_false_iff_ge [DecidableEq α] [LT α] [DecidableLT α]
+    {l₁ l₂ : List α} : lex l₁ l₂ = false ↔ l₂ ≤ l₁ := by
+  simp only [lex_eq_false_iff_not_lex, decide_eq_true_eq]
+  exact Iff.rfl
+
+attribute [local simp] Nat.add_one_lt_add_one_iff in
+/--
+`l₁` is lexicographically less than `l₂` if either
+- `l₁` is pairwise equivalent under `· == ·` to `l₂.take l₁.length`,
+  and `l₁` is shorter than `l₂` or
+- there exists an index `i` such that
+  - for all `j < i`, `l₁[j] == l₂[j]` and
+  - `l₁[i] < l₂[i]`
+-/
+theorem lex_eq_true_iff_exists [BEq α] (lt : α → α → Bool) :
+    lex l₁ l₂ lt = true ↔
+      (l₁.isEqv (l₂.take l₁.length) (· == ·) ∧ l₁.length < l₂.length) ∨
+        (∃ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
+          (∀ j, (hj : j < i) →
+            l₁[j]'(Nat.lt_trans hj h₁) == l₂[j]'(Nat.lt_trans hj h₂)) ∧ lt l₁[i] l₂[i]) := by
+  induction l₁ generalizing l₂ with
+  | nil =>
+    cases l₂ with
+    | nil => simp [lex]
+    | cons b bs => simp [lex]
   | cons a l₁ ih =>
     cases l₂ with
-    | nil => cases h₂ (.nil ..)
+    | nil => simp [lex]
     | cons b l₂ =>
-      have ab : ¬a < b := fun ab => h₁ (.head _ _ ab)
-      cases lt_antisymm ab (fun ba => h₂ (.head _ _ ba))
-      rw [ih (fun ll => h₁ (.tail ab ab ll)) (fun ll => h₂ (.tail ab ab ll))]
+      simp only [lex_cons_cons, Bool.or_eq_true, Bool.and_eq_true, ih, isEqv, length_cons]
+      constructor
+      · rintro (hab | ⟨hab, ⟨h₁, h₂⟩ | ⟨i, h₁, h₂, w₁, w₂⟩⟩)
+        · exact .inr ⟨0, by simp [hab]⟩
+        · exact .inl ⟨⟨hab, h₁⟩, by simpa using h₂⟩
+        · refine .inr ⟨i + 1, by simp [h₁],
+            by simp [h₂], ?_, ?_⟩
+          · intro j hj
+            cases j with
+            | zero => simp [hab]
+            | succ j =>
+              simp only [getElem_cons_succ]
+              rw [w₁]
+              simpa using hj
+          · simpa using w₂
+      · rintro (⟨⟨h₁, h₂⟩, h₃⟩ | ⟨i, h₁, h₂, w₁, w₂⟩)
+        · exact .inr ⟨h₁, .inl ⟨h₂, by simpa using h₃⟩⟩
+        · cases i with
+          | zero =>
+            left
+            simpa using w₂
+          | succ i =>
+            right
+            refine ⟨by simpa using w₁ 0 (by simp), ?_⟩
+            right
+            refine ⟨i, by simpa using h₁, by simpa using h₂, ?_, ?_⟩
+            · intro j hj
+              simpa using w₁ (j + 1) (by simpa)
+            · simpa using w₂
+
+attribute [local simp] Nat.add_one_lt_add_one_iff in
+/--
+`l₁` is *not* lexicographically less than `l₂`
+(which you might think of as "`l₂` is lexicographically greater than or equal to `l₁`"") if either
+- `l₁` is pairwise equivalent under `· == ·` to `l₂.take l₁.length` or
+- there exists an index `i` such that
+  - for all `j < i`, `l₁[j] == l₂[j]` and
+  - `l₂[i] < l₁[i]`
+
+This formulation requires that `==` and `lt` are compatible in the following senses:
+- `==` is symmetric
+  (we unnecessarily further assume it is transitive, to make use of the existing typeclasses)
+- `lt` is irreflexive with respect to `==` (i.e. if `x == y` then `lt x y = false`
+- `lt` is asymmmetric  (i.e. `lt x y = true → lt y x = false`)
+- `lt` is antisymmetric with respect to `==` (i.e. `lt x y = false → lt y x = false → x == y`)
+-/
+theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : α → α → Bool)
+    (lt_irrefl : ∀ x y, x == y → lt x y = false)
+    (lt_asymm : ∀ x y, lt x y = true → lt y x = false)
+    (lt_antisymm : ∀ x y, lt x y = false → lt y x = false → x == y) :
+    lex l₁ l₂ lt = false ↔
+      (l₂.isEqv (l₁.take l₂.length) (· == ·)) ∨
+        (∃ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
+          (∀ j, (hj : j < i) →
+            l₁[j]'(Nat.lt_trans hj h₁) == l₂[j]'(Nat.lt_trans hj h₂)) ∧ lt l₂[i] l₁[i]) := by
+  induction l₁ generalizing l₂ with
+  | nil =>
+    cases l₂ with
+    | nil => simp [lex]
+    | cons b bs => simp [lex]
+  | cons a l₁ ih =>
+    cases l₂ with
+    | nil => simp [lex]
+    | cons b l₂ =>
+      simp only [lex_cons_cons, Bool.or_eq_false_iff, Bool.and_eq_false_imp, ih, isEqv,
+        Bool.and_eq_true, length_cons]
+      constructor
+      · rintro ⟨hab, h⟩
+        if eq : b == a then
+          specialize h (BEq.symm eq)
+          obtain (h | ⟨i, h₁, h₂, w₁, w₂⟩) := h
+          · exact .inl ⟨eq, h⟩
+          · refine .inr ⟨i + 1, by simpa using h₁, by simpa using h₂, ?_, ?_⟩
+            · intro j hj
+              cases j with
+              | zero => simpa using BEq.symm eq
+              | succ j =>
+                simp only [getElem_cons_succ]
+                rw [w₁]
+                simpa using hj
+            · simpa using w₂
+        else
+          right
+          have hba : lt b a :=
+            Decidable.byContradiction fun hba => eq (lt_antisymm _ _ (by simpa using hba) hab)
+          exact ⟨0, by simp, by simp, by simpa⟩
+      · rintro (⟨eq, h⟩ | ⟨i, h₁, h₂, w₁, w₂⟩)
+        · exact ⟨lt_irrefl _ _ (BEq.symm eq), fun _ => .inl h⟩
+        · cases i with
+          | zero =>
+            simp at w₂
+            refine ⟨lt_asymm _ _ w₂, ?_⟩
+            intro eq
+            exfalso
+            simp [lt_irrefl _ _ (BEq.symm eq)] at w₂
+          | succ i =>
+            refine ⟨lt_irrefl _ _ (by simpa using w₁ 0 (by simp)), ?_⟩
+            refine fun _ => .inr ⟨i, by simpa using h₁, by simpa using h₂, ?_, ?_⟩
+            · intro j hj
+              simpa using w₁ (j + 1) (by simpa)
+            · simpa using w₂
 
 /-! ### foldlM and foldrM -/
 
diff --git a/src/Init/Data/List/MinMax.lean b/src/Init/Data/List/MinMax.lean
index 02b84badc2c8..1f0248e1d488 100644
--- a/src/Init/Data/List/MinMax.lean
+++ b/src/Init/Data/List/MinMax.lean
@@ -85,7 +85,7 @@ theorem min?_eq_some_iff [Min α] [LE α] [anti : Std.Antisymm ((· : α) ≤ ·
   cases xs with
   | nil => simp at h₁
   | cons x xs =>
-    exact congrArg some <| anti.1
+    exact congrArg some <| anti.1 _ _
       ((le_min?_iff le_min_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)
       (h₂ _ (min?_mem min_eq_or (xs := x::xs) rfl))
 
@@ -156,7 +156,7 @@ theorem max?_eq_some_iff [Max α] [LE α] [anti : Std.Antisymm ((· : α) ≤ ·
   cases xs with
   | nil => simp at h₁
   | cons x xs =>
-    exact congrArg some <| anti.1
+    exact congrArg some <| anti.1 _ _
       (h₂ _ (max?_mem max_eq_or (xs := x::xs) rfl))
       ((max?_le_iff max_le_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)
 
diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean
index aa363eb9fa6a..dec45472a4d8 100644
--- a/src/Init/Data/List/ToArray.lean
+++ b/src/Init/Data/List/ToArray.lean
@@ -7,6 +7,7 @@ prelude
 import Init.Data.List.Impl
 import Init.Data.List.Nat.Erase
 import Init.Data.List.Monadic
+import Init.Data.Array.Lex
 
 /-! ### Lemmas about `List.toArray`.
 
diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean
index aebae331e144..e046df9b9a11 100644
--- a/src/Init/Data/Nat/Basic.lean
+++ b/src/Init/Data/Nat/Basic.lean
@@ -445,10 +445,10 @@ protected theorem le_antisymm_iff {a b : Nat} : a = b ↔ a ≤ b ∧ b ≤ a :=
 protected theorem eq_iff_le_and_ge : ∀{a b : Nat}, a = b ↔ a ≤ b ∧ b ≤ a := @Nat.le_antisymm_iff
 
 instance : Std.Antisymm ( . ≤ . : Nat → Nat → Prop) where
-  antisymm h₁ h₂ := Nat.le_antisymm h₁ h₂
+  antisymm _ _ h₁ h₂ := Nat.le_antisymm h₁ h₂
 
 instance : Std.Antisymm (¬ . < . : Nat → Nat → Prop) where
-  antisymm h₁ h₂ := Nat.le_antisymm (Nat.ge_of_not_lt h₂) (Nat.ge_of_not_lt h₁)
+  antisymm _ _ h₁ h₂ := Nat.le_antisymm (Nat.ge_of_not_lt h₂) (Nat.ge_of_not_lt h₁)
 
 protected theorem add_le_add_left {n m : Nat} (h : n ≤ m) (k : Nat) : k + n ≤ k + m :=
   match le.dest h with
diff --git a/src/Init/Data/Ord.lean b/src/Init/Data/Ord.lean
index 1b669bc6cee6..35ce3dc9fb5e 100644
--- a/src/Init/Data/Ord.lean
+++ b/src/Init/Data/Ord.lean
@@ -210,12 +210,18 @@ Derive an `LT` instance from an `Ord` instance.
 protected def toLT (_ : Ord α) : LT α :=
   ltOfOrd
 
+instance [i : Ord α] : DecidableRel (@LT.lt _ (Ord.toLT i)) :=
+  inferInstanceAs (DecidableRel (fun a b => compare a b = Ordering.lt))
+
 /--
 Derive an `LE` instance from an `Ord` instance.
 -/
 protected def toLE (_ : Ord α) : LE α :=
   leOfOrd
 
+instance [i : Ord α] : DecidableRel (@LE.le _ (Ord.toLE i)) :=
+  inferInstanceAs (DecidableRel (fun a b => (compare a b).isLE))
+
 /--
 Invert the order of an `Ord` instance.
 -/
@@ -248,6 +254,6 @@ protected def arrayOrd [a : Ord α] : Ord (Array α) where
   compare x y :=
     let _ : LT α := a.toLT
     let _ : BEq α := a.toBEq
-    compareOfLessAndBEq x.toList y.toList
+    if List.lex x.toList y.toList then .lt else if x == y then .eq else .gt
 
 end Ord
diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean
index 999dacf35088..c3cf066bbbbb 100644
--- a/src/Init/Data/String/Basic.lean
+++ b/src/Init/Data/String/Basic.lean
@@ -21,8 +21,10 @@ instance : LT String :=
   ⟨fun s₁ s₂ => s₁.data < s₂.data⟩
 
 @[extern "lean_string_dec_lt"]
-instance decLt (s₁ s₂ : @& String) : Decidable (s₁ < s₂) :=
-  List.hasDecidableLt s₁.data s₂.data
+instance decidableLT (s₁ s₂ : @& String) : Decidable (s₁ < s₂) :=
+  List.decidableLT s₁.data s₂.data
+
+@[deprecated decidableLT (since := "2024-12-13")] abbrev decLt := @decidableLT
 
 @[reducible] protected def le (a b : String) : Prop := ¬ b < a
 
diff --git a/src/Init/Data/String/Lemmas.lean b/src/Init/Data/String/Lemmas.lean
index 3153eea5c3e7..fa787eb47fce 100644
--- a/src/Init/Data/String/Lemmas.lean
+++ b/src/Init/Data/String/Lemmas.lean
@@ -12,10 +12,39 @@ protected theorem data_eq_of_eq {a b : String} (h : a = b) : a.data = b.data :=
   h ▸ rfl
 protected theorem ne_of_data_ne {a b : String} (h : a.data ≠ b.data) : a ≠ b :=
   fun h' => absurd (String.data_eq_of_eq h') h
-@[simp] protected theorem lt_irrefl (s : String) : ¬ s < s :=
-  List.lt_irrefl Char.lt_irrefl s.data
+
+@[simp] protected theorem not_le {a b : String} : ¬ a ≤ b ↔ b < a := Decidable.not_not
+@[simp] protected theorem not_lt {a b : String} : ¬ a < b ↔ b ≤ a := Iff.rfl
+@[simp] protected theorem le_refl (a : String) : a ≤ a := List.le_refl _
+@[simp] protected theorem lt_irrefl (a : String) : ¬ a < a := List.lt_irrefl _
+
+attribute [local instance] Char.notLTTrans Char.notLTAntisymm Char.notLTTotal
+
+protected theorem le_trans {a b c : String} : a ≤ b → b ≤ c → a ≤ c := List.le_trans
+protected theorem lt_trans {a b c : String} : a < b → b < c → a < c := List.lt_trans
+protected theorem le_total (a b : String) : a ≤ b ∨ b ≤ a := List.le_total
+protected theorem le_antisymm {a b : String} : a ≤ b → b ≤ a → a = b := fun h₁ h₂ => String.ext (List.le_antisymm (as := a.data) (bs := b.data) h₁ h₂)
+protected theorem lt_asymm {a b : String} (h : a < b) : ¬ b < a := List.lt_asymm h
 protected theorem ne_of_lt {a b : String} (h : a < b) : a ≠ b := by
   have := String.lt_irrefl a
   intro h; subst h; contradiction
 
+instance ltIrrefl : Std.Irrefl (· < · : Char → Char → Prop) where
+  irrefl := Char.lt_irrefl
+
+instance leRefl : Std.Refl (· ≤ · : Char → Char → Prop) where
+  refl := Char.le_refl
+
+instance leTrans : Trans (· ≤ · : Char → Char → Prop) (· ≤ ·) (· ≤ ·) where
+  trans := Char.le_trans
+
+instance leAntisymm : Std.Antisymm (· ≤ · : Char → Char → Prop) where
+  antisymm _ _ := Char.le_antisymm
+
+instance ltAsymm : Std.Asymm (· < · : Char → Char → Prop) where
+  asymm _ _ := Char.lt_asymm
+
+instance leTotal : Std.Total (· ≤ · : Char → Char → Prop) where
+  total := Char.le_total
+
 end String
diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean
index 41e38c37d630..3edac5b5c44e 100644
--- a/src/Init/Data/Vector/Basic.lean
+++ b/src/Init/Data/Vector/Basic.lean
@@ -6,6 +6,7 @@ Authors: Shreyas Srinivas, François G. Dorais, Kim Morrison
 
 prelude
 import Init.Data.Array.Lemmas
+import Init.Data.Range
 
 /-!
 # Vectors
@@ -280,3 +281,29 @@ no element of the index matches the given value.
 /-- Returns `true` if `p` returns `true` for all elements of the vector. -/
 @[inline] def all (v : Vector α n) (p : α → Bool) : Bool :=
   v.toArray.all p
+
+/-! ### Lexicographic ordering -/
+
+instance instLT [LT α] : LT (Vector α n) := ⟨fun v w => v.toArray < w.toArray⟩
+instance instLE [LT α] : LE (Vector α n) := ⟨fun v w => v.toArray ≤ w.toArray⟩
+
+instance [DecidableEq α] [LT α] [DecidableLT α] : DecidableLT (Vector α n) :=
+  inferInstanceAs <| DecidableRel fun (v w : Vector α n) => v.toArray < w.toArray
+
+instance [DecidableEq α] [LT α] [DecidableLT α] : DecidableLE (Vector α n) :=
+  inferInstanceAs <| DecidableRel fun (v w : Vector α n) => v.toArray ≤ w.toArray
+
+/--
+Lexicographic comparator for vectors.
+
+`lex v w lt` is true if
+- `v` is pairwise equivalent via `==` to `w`, or
+- there is an index `i` such that `lt v[i] w[i]`, and for all `j < i`, `v[j] == w[j]`.
+-/
+def lex [BEq α] (v w : Vector α n) (lt : α → α → Bool := by exact (· < ·)) : Bool := Id.run do
+  for h : i in [0 : n] do
+    if lt v[i] w[i] then
+      return true
+    else if v[i] != w[i] then
+      return false
+  return false
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index e6a408253f70..20e29dc7904f 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1126,6 +1126,11 @@ class LT (α : Type u) where
 /-- `a > b` is an abbreviation for `b < a`. -/
 @[reducible] def GT.gt {α : Type u} [LT α] (a b : α) : Prop := LT.lt b a
 
+/-- Abbreviation for `DecidableRel (· < · : α → α → Prop)`. -/
+abbrev DecidableLT (α : Type u) [LT α] := DecidableRel (LT.lt : α → α → Prop)
+/-- Abbreviation for `DecidableRel (· ≤ · : α → α → Prop)`. -/
+abbrev DecidableLE (α : Type u) [LE α] := DecidableRel (LE.le : α → α → Prop)
+
 /-- `Max α` is the typeclass which supports the operation `max x y` where `x y : α`.-/
 class Max (α : Type u) where
   /-- The maximum operation: `max x y`. -/
diff --git a/src/Lean/Compiler/LCNF/Probing.lean b/src/Lean/Compiler/LCNF/Probing.lean
index f2e781d3765f..38a16c71c6b7 100644
--- a/src/Lean/Compiler/LCNF/Probing.lean
+++ b/src/Lean/Compiler/LCNF/Probing.lean
@@ -21,7 +21,7 @@ def map (f : α → CompilerM β) : Probe α β := fun data => data.mapM f
 def filter (f : α → CompilerM Bool) : Probe α α := fun data => data.filterM f
 
 @[inline]
-def sorted [Inhabited α] [inst : LT α] [DecidableRel inst.lt] : Probe α α := fun data => return data.qsort (· < ·)
+def sorted [Inhabited α] [LT α] [DecidableLT α] : Probe α α := fun data => return data.qsort (· < ·)
 
 @[inline]
 def sortedBySize : Probe Decl (Nat × Decl) := fun decls =>
diff --git a/tests/lean/run/bubble.lean b/tests/lean/run/bubble.lean
index 19296830e5ba..083caa690cad 100644
--- a/tests/lean/run/bubble.lean
+++ b/tests/lean/run/bubble.lean
@@ -1,4 +1,4 @@
-def List.bubblesort [LT α] [DecidableRel (· < · : α → α → Prop)] (l : List α) : {l' : List α // l.length = l'.length} :=
+def List.bubblesort [LT α] [DecidableLT α] (l : List α) : {l' : List α // l.length = l'.length} :=
   match l with
   | [] => ⟨[], rfl⟩
   | x :: xs =>
diff --git a/tests/lean/run/constructor_as_variable.lean b/tests/lean/run/constructor_as_variable.lean
index d594702a1d2d..802b911c2384 100644
--- a/tests/lean/run/constructor_as_variable.lean
+++ b/tests/lean/run/constructor_as_variable.lean
@@ -101,6 +101,8 @@ def ctorSuggestion1 (pair : MyProd) : Nat :=
 error: invalid pattern, constructor or constant marked with '[match_pattern]' expected
 
 Suggestions:
+  'List.Lex.below.cons',
+  'List.Lex.cons',
   'List.Pairwise.below.cons',
   'List.Pairwise.cons',
   'List.Perm.below.cons',
@@ -127,6 +129,8 @@ inductive StringList : Type where
 error: invalid pattern, constructor or constant marked with '[match_pattern]' expected
 
 Suggestions:
+  'List.Lex.below.cons',
+  'List.Lex.cons',
   'List.Pairwise.below.cons',
   'List.Pairwise.cons',
   'List.Perm.below.cons',