diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index e75f765a8c..3ed6171ff6 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -949,13 +949,7 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α :=
 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.
+-- See `Init.Data.Array.Lex.Basic` for the boolean valued lexicographic comparator.
 
 /-! ## Auxiliary functions used in metaprogramming.
 
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 11ef9b1b55..726fff9ede 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -12,7 +12,8 @@ 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.Data.Array.Lex.Basic
+import Init.Data.Range.Lemmas
 import Init.TacticsExtra
 import Init.Data.List.ToArray
 
@@ -925,7 +926,6 @@ theorem mem_or_eq_of_mem_setIfInBounds
 
 /-! ### BEq -/
 
-
 @[simp] theorem beq_empty_iff [BEq α] {xs : Array α} : (xs == #[]) = xs.isEmpty := by
   cases xs
   simp
@@ -989,7 +989,12 @@ theorem size_eq_of_beq [BEq α] {xs ys : Array α} (h : xs == ys) : xs.size = ys
     · intro a
       apply Array.isEqv_self_beq
 
-/-! ### Lexicographic ordering -/
+/-! ### isEqv -/
+
+@[simp] theorem isEqv_eq [DecidableEq α] {l₁ l₂ : Array α} : l₁.isEqv l₂ (· == ·) = (l₁ = l₂) := by
+  cases l₁
+  cases l₂
+  simp
 
 /-! Content below this point has not yet been aligned with `List`. -/
 
@@ -1752,9 +1757,8 @@ theorem getElem_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt :
   conv => rhs; rw [← List.getElem_append_left (bs := bs.toList) (h' := h')]
   apply List.get_of_eq; rw [toList_append]
 
-theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i)
-    (hlt : i - as.size < bs.size := Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) :
-    (as ++ bs)[i] = bs[i - as.size] := by
+theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i) :
+    (as ++ bs)[i] = bs[i - as.size]'(Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) := by
   simp only [← getElem_toList]
   have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, toList_append] at h
   conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
@@ -2097,8 +2101,7 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
 theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse := by simp
 
 @[simp] theorem take_toArray (l : List α) (n : Nat) : l.toArray.take n = (l.take n).toArray := by
-  apply ext'
-  simp
+  apply Array.ext <;> simp
 
 @[simp] theorem mapM_toArray [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) :
     l.toArray.mapM f = List.toArray <$> l.mapM f := by
@@ -2352,6 +2355,12 @@ theorem foldr_map' (g : α → β) (f : α → α → α) (f' : β → β → β
   rw [← List.foldl_hom (f := Prod.snd) (g₂ := fun bs x => bs.push x.2) (H := by simp), ← List.foldl_map]
   simp
 
+/-! ### take -/
+
+@[simp] theorem take_size (a : Array α) : a.take a.size = a := by
+  cases a
+  simp
+
 end Array
 
 namespace List
@@ -2390,7 +2399,6 @@ theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α)
     apply ext'
     simp [ih, flatMap_toArray_cons]
 
-
 end Array
 
 /-! ### Deprecations -/
diff --git a/src/Init/Data/Array/Lex.lean b/src/Init/Data/Array/Lex.lean
index 65d1bdfeab..a700084e4b 100644
--- a/src/Init/Data/Array/Lex.lean
+++ b/src/Init/Data/Array/Lex.lean
@@ -4,27 +4,5 @@ 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
+import Init.Data.Array.Lex.Basic
+import Init.Data.Array.Lex.Lemmas
diff --git a/src/Init/Data/Array/Lex/Basic.lean b/src/Init/Data/Array/Lex/Basic.lean
new file mode 100644
index 0000000000..65d1bdfeab
--- /dev/null
+++ b/src/Init/Data/Array/Lex/Basic.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/Array/Lex/Lemmas.lean b/src/Init/Data/Array/Lex/Lemmas.lean
new file mode 100644
index 0000000000..cf4bdc379e
--- /dev/null
+++ b/src/Init/Data/Array/Lex/Lemmas.lean
@@ -0,0 +1,216 @@
+/-
+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.Lemmas
+import Init.Data.List.Lex
+
+namespace Array
+
+/-! ### Lexicographic ordering -/
+
+@[simp] theorem lt_toArray [LT α] (l₁ l₂ : List α) : l₁.toArray < l₂.toArray ↔ l₁ < l₂ := Iff.rfl
+@[simp] theorem le_toArray [LT α] (l₁ l₂ : List α) : l₁.toArray ≤ l₂.toArray ↔ l₁ ≤ l₂ := Iff.rfl
+
+theorem not_lt_iff_ge [LT α] (l₁ l₂ : List α) : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
+theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List α) :
+    ¬ l₁ ≤ l₂ ↔ l₂ < l₁ :=
+  Decidable.not_not
+
+@[simp] theorem lex_empty [BEq α] {lt : α → α → Bool} (l : Array α) : l.lex #[] lt = false := by
+  simp [lex, Id.run]
+
+@[simp] theorem singleton_lex_singleton [BEq α] {lt : α → α → Bool} : #[a].lex #[b] lt = lt a b := by
+  simp only [lex, List.getElem_toArray, List.getElem_singleton]
+  cases lt a b <;> cases a != b <;> simp [Id.run]
+
+private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs ys : Array α} :
+     (#[a] ++ xs).lex (#[b] ++ ys) lt =
+       (lt a b || a == b && xs.lex ys lt) := by
+  simp only [lex, Id.run]
+  simp only [Std.Range.forIn'_eq_forIn'_range', size_append, size_toArray, List.length_singleton,
+    Nat.add_comm 1]
+  simp [Nat.add_min_add_right, List.range'_succ, getElem_append_left, List.range'_succ_left,
+    getElem_append_right]
+  cases lt a b
+  · rw [bne]
+    cases a == b <;> simp
+  · simp
+
+@[simp] theorem _root_.List.lex_toArray [BEq α] (lt : α → α → Bool) (l₁ l₂ : List α) :
+    l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt := by
+  induction l₁ generalizing l₂ with
+  | nil => cases l₂ <;> simp [lex, Id.run]
+  | cons x l₁ ih =>
+    cases l₂ with
+    | nil => simp [lex, Id.run]
+    | cons y l₂ =>
+      rw [List.toArray_cons, List.toArray_cons y, cons_lex_cons, List.lex, ih]
+
+@[simp] theorem lex_toList [BEq α] (lt : α → α → Bool) (l₁ l₂ : Array α) :
+    l₁.toList.lex l₂.toList lt = l₁.lex l₂ lt := by
+  cases l₁ <;> cases l₂ <;> simp
+
+protected theorem lt_irrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)] (l : Array α) : ¬ l < l :=
+  List.lt_irrefl l.toList
+
+instance ltIrrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)] : Std.Irrefl (α := Array α) (· < ·) where
+  irrefl := Array.lt_irrefl
+
+@[simp] theorem empty_le [LT α] (l : Array α) : #[] ≤ l := List.nil_le l.toList
+
+@[simp] theorem le_empty [LT α] (l : Array α) : l ≤ #[] ↔ l = #[] := by
+  cases l
+  simp
+
+@[simp] theorem empty_lt_push [LT α] (l : Array α) (a : α) : #[] < l.push a := by
+  rcases l with (_ | ⟨x, l⟩) <;> simp
+
+protected theorem le_refl [LT α] [i₀ : Std.Irrefl (· < · : α → α → Prop)] (l : Array α) : l ≤ l :=
+  List.le_refl l.toList
+
+instance [LT α] [Std.Irrefl (· < · : α → α → Prop)] : Std.Refl (· ≤ · : Array α → Array α → Prop) where
+  refl := Array.le_refl
+
+protected theorem lt_trans [LT α] [DecidableLT α]
+    [i₁ : Trans (· < · : α → α → Prop) (· < ·) (· < ·)]
+    {l₁ l₂ l₃ : Array α} (h₁ : l₁ < l₂) (h₂ : l₂ < l₃) : l₁ < l₃ :=
+  List.lt_trans h₁ h₂
+
+instance [LT α] [DecidableLT α]
+    [Trans (· < · : α → α → Prop) (· < ·) (· < ·)] :
+    Trans (· < · : Array α → Array α → Prop) (· < ·) (· < ·) where
+  trans h₁ h₂ := Array.lt_trans h₁ h₂
+
+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₃ : Array α} (h₁ : l₁ ≤ l₂) (h₂ : l₂ < l₃) : l₁ < l₃ :=
+  List.lt_of_le_of_lt h₁ h₂
+
+protected theorem le_trans [DecidableEq α] [LT α] [DecidableLT α]
+    [Std.Irrefl (· < · : α → α → Prop)]
+    [Std.Asymm (· < · : α → α → Prop)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)]
+    [Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
+    {l₁ l₂ l₃ : Array α} (h₁ : l₁ ≤ l₂) (h₂ : l₂ ≤ l₃) : l₁ ≤ l₃ :=
+  fun h₃ => h₁ (Array.lt_of_le_of_lt h₂ h₃)
+
+instance [DecidableEq α] [LT α] [DecidableLT α]
+    [Std.Irrefl (· < · : α → α → Prop)]
+    [Std.Asymm (· < · : α → α → Prop)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)]
+    [Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)] :
+    Trans (· ≤ · : Array α → Array α → Prop) (· ≤ ·) (· ≤ ·) where
+  trans h₁ h₂ := Array.le_trans h₁ h₂
+
+protected theorem lt_asymm [DecidableEq α] [LT α] [DecidableLT α]
+    [i : Std.Asymm (· < · : α → α → Prop)]
+    {l₁ l₂ : Array α} (h : l₁ < l₂) : ¬ l₂ < l₁ := List.lt_asymm h
+
+instance [DecidableEq α] [LT α] [DecidableLT α]
+    [Std.Asymm (· < · : α → α → Prop)] :
+    Std.Asymm (· < · : Array α → Array α → Prop) where
+  asymm _ _ := Array.lt_asymm
+
+protected theorem le_total [DecidableEq α] [LT α] [DecidableLT α]
+    [i : Std.Total (¬ · < · : α → α → Prop)] {l₁ l₂ : Array α} : l₁ ≤ l₂ ∨ l₂ ≤ l₁ :=
+  List.le_total
+
+instance [DecidableEq α] [LT α] [DecidableLT α]
+    [Std.Total (¬ · < · : α → α → Prop)] :
+    Std.Total (· ≤ · : Array α → Array α → Prop) where
+  total _ _ := Array.le_total
+
+@[simp] theorem lex_eq_true_iff_lt [DecidableEq α] [LT α] [DecidableLT α]
+    {l₁ l₂ : Array α} : lex l₁ l₂ = true ↔ l₁ < l₂ := by
+  cases l₁
+  cases l₂
+  simp
+
+@[simp] theorem lex_eq_false_iff_ge [DecidableEq α] [LT α] [DecidableLT α]
+    {l₁ l₂ : Array α} : lex l₁ l₂ = false ↔ l₂ ≤ l₁ := by
+  cases l₁
+  cases l₂
+  simp [List.not_lt_iff_ge]
+
+instance [DecidableEq α] [LT α] [DecidableLT α] : DecidableLT (Array α) :=
+  fun l₁ l₂ => decidable_of_iff (lex l₁ l₂ = true) lex_eq_true_iff_lt
+
+instance [DecidableEq α] [LT α] [DecidableLT α] : DecidableLE (Array α) :=
+  fun l₁ l₂ => decidable_of_iff (lex l₂ l₁ = false) lex_eq_false_iff_ge
+
+/--
+`l₁` is lexicographically less than `l₂` if either
+- `l₁` is pairwise equivalent under `· == ·` to `l₂.take l₁.size`,
+  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₁.size) (· == ·) ∧ l₁.size < l₂.size) ∨
+        (∃ (i : Nat) (h₁ : i < l₁.size) (h₂ : i < l₂.size),
+          (∀ j, (hj : j < i) →
+            l₁[j]'(Nat.lt_trans hj h₁) == l₂[j]'(Nat.lt_trans hj h₂)) ∧ lt l₁[i] l₂[i]) := by
+  cases l₁
+  cases l₂
+  simp [List.lex_eq_true_iff_exists]
+
+/--
+`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₂.size) (· == ·)) ∨
+        (∃ (i : Nat) (h₁ : i < l₁.size) (h₂ : i < l₂.size),
+          (∀ j, (hj : j < i) →
+            l₁[j]'(Nat.lt_trans hj h₁) == l₂[j]'(Nat.lt_trans hj h₂)) ∧ lt l₂[i] l₁[i]) := by
+  cases l₁
+  cases l₂
+  simp_all [List.lex_eq_false_iff_exists]
+
+theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Array α} :
+    l₁ < l₂ ↔
+      (l₁ = l₂.take l₁.size ∧ l₁.size < l₂.size) ∨
+        (∃ (i : Nat) (h₁ : i < l₁.size) (h₂ : i < l₂.size),
+          (∀ j, (hj : j < i) →
+            l₁[j]'(Nat.lt_trans hj h₁) = l₂[j]'(Nat.lt_trans hj h₂)) ∧ l₁[i] < l₂[i]) := by
+  cases l₁
+  cases l₂
+  simp [List.lt_iff_exists]
+
+theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
+    [Std.Irrefl (· < · : α → α → Prop)]
+    [Std.Asymm (· < · : α → α → Prop)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)] {l₁ l₂ : Array α} :
+    l₁ ≤ l₂ ↔
+      (l₁ = l₂.take l₁.size) ∨
+        (∃ (i : Nat) (h₁ : i < l₁.size) (h₂ : i < l₂.size),
+          (∀ j, (hj : j < i) →
+            l₁[j]'(Nat.lt_trans hj h₁) = l₂[j]'(Nat.lt_trans hj h₂)) ∧ l₁[i] < l₂[i]) := by
+  cases l₁
+  cases l₂
+  simp [List.le_iff_exists]
+
+end Array
diff --git a/src/Init/Data/Array/Monadic.lean b/src/Init/Data/Array/Monadic.lean
index 8056b54b71..02456a25da 100644
--- a/src/Init/Data/Array/Monadic.lean
+++ b/src/Init/Data/Array/Monadic.lean
@@ -79,8 +79,31 @@ theorem foldrM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : α → β
   rw [List.filter_toArray] -- Why doesn't this fire via `simp`?
   simp [List.foldrM_filter]
 
+/-! ### forM -/
+
+@[congr] theorem forM_congr [Monad m] {as bs : Array α} (w : as = bs)
+    {f : α → m PUnit} :
+    forM f as = forM f bs := by
+  cases as <;> cases bs
+  simp_all
+
+@[simp] theorem forM_map [Monad m] [LawfulMonad m] (l : Array α) (g : α → β) (f : β → m PUnit) :
+    (l.map g).forM f = l.forM (fun a => f (g a)) := by
+  cases l
+  simp
+
 /-! ### forIn' -/
 
+@[congr] theorem forIn'_congr [Monad m] {as bs : Array α} (w : as = bs)
+    {b b' : β} (hb : b = b')
+    {f : (a' : α) → a' ∈ as → β → m (ForInStep β)}
+    {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)}
+    (h : ∀ a m b, f a (by simpa [w] using m) b = g a m b) :
+    forIn' as b f = forIn' bs b' g := by
+  cases as <;> cases bs
+  simp only [mk.injEq, mem_toArray, List.forIn'_toArray] at w h ⊢
+  exact List.forIn'_congr w hb h
+
 /--
 We can express a for loop over an array as a fold,
 in which whenever we reach `.done b` we keep that value through the rest of the fold.
@@ -120,6 +143,12 @@ theorem forIn'_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
   cases l
   simp [List.foldl_map]
 
+@[simp] theorem forIn'_map [Monad m] [LawfulMonad m]
+    (l : Array α) (g : α → β) (f : (b : β) → b ∈ l.map g → γ → m (ForInStep γ)) :
+    forIn' (l.map g) init f = forIn' l init fun a h y => f (g a) (mem_map_of_mem g h) y := by
+  cases l
+  simp
+
 /--
 We can express a for loop over an array as a fold,
 in which whenever we reach `.done b` we keep that value through the rest of the fold.
@@ -156,4 +185,10 @@ theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
   cases l
   simp [List.foldl_map]
 
+@[simp] theorem forIn_map [Monad m] [LawfulMonad m]
+    (l : Array α) (g : α → β) (f : β → γ → m (ForInStep γ)) :
+    forIn (l.map g) init f = forIn l init fun a y => f (g a) y := by
+  cases l
+  simp
+
 end Array
diff --git a/src/Init/Data/List.lean b/src/Init/Data/List.lean
index 2ed68e0d02..6c0cb85bd6 100644
--- a/src/Init/Data/List.lean
+++ b/src/Init/Data/List.lean
@@ -28,3 +28,4 @@ import Init.Data.List.ToArrayImpl
 import Init.Data.List.MapIdx
 import Init.Data.List.OfFn
 import Init.Data.List.FinRange
+import Init.Data.List.Lex
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index f9b081a683..a06c12d4d9 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -747,397 +747,15 @@ theorem length_eq_of_beq [BEq α] {l₁ l₂ : List α} (h : l₁ == l₂) : l
     · intro a
       simp
 
-/-! ### Lexicographic ordering -/
+/-! ### isEqv -/
 
-
-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
-
-protected theorem lt_irrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)] (l : List α) : ¬ l < l :=
-  lex_irrefl Std.Irrefl.irrefl l
-
-instance ltIrrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)] : Std.Irrefl (α := List α) (· < ·) where
-  irrefl := List.lt_irrefl
-
-@[simp] theorem not_lex_nil : ¬Lex r l [] := fun h => nomatch h
-
-@[simp] theorem nil_le [LT α] (l : List α) : [] ≤ l := fun h => nomatch h
-
-@[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 => simp
-  | cons a l ih =>
-    intro
-    | .rel h => exact i₀.irrefl _ h
-    | .cons h₃ => exact ih h₃
-
-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.Lex.nil ..
-  | @rel a l₁ b l₂ ab =>
-    match h₂ with
-    | .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
-    | .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
+@[simp] theorem isEqv_eq [DecidableEq α] {l₁ l₂ : List α} : l₁.isEqv l₂ (· == ·) = (l₁ = l₂) := by
   induction l₁ generalizing l₂ with
-  | nil =>
-    cases l₂ with
-    | nil => simp [lex]
-    | cons b bs => simp [lex]
+  | nil => cases l₂ <;> simp
   | 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 => simp [lex]
-    | cons b l₂ =>
-      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₂
+    | nil => simp
+    | cons b l₂ => simp [isEqv, ih]
 
 /-! ### foldlM and foldrM -/
 
diff --git a/src/Init/Data/List/Lex.lean b/src/Init/Data/List/Lex.lean
new file mode 100644
index 0000000000..d006105039
--- /dev/null
+++ b/src/Init/Data/List/Lex.lean
@@ -0,0 +1,430 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.List.Lemmas
+
+namespace List
+
+/-! ### Lexicographic ordering -/
+
+@[simp] theorem lex_lt [LT α] (l₁ l₂ : List α) : Lex (· < ·) l₁ l₂ ↔ l₁ < l₂ := Iff.rfl
+@[simp] theorem not_lex_lt [LT α] (l₁ l₂ : List α) : ¬ Lex (· < ·) l₁ l₂ ↔ l₂ ≤ l₁ := Iff.rfl
+
+theorem not_lt_iff_ge [LT α] (l₁ l₂ : List α) : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
+theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List α) :
+    ¬ l₁ ≤ l₂ ↔ l₂ < l₁ :=
+  Decidable.not_not
+
+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
+
+protected theorem lt_irrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)] (l : List α) : ¬ l < l :=
+  lex_irrefl Std.Irrefl.irrefl l
+
+instance ltIrrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)] : Std.Irrefl (α := List α) (· < ·) where
+  irrefl := List.lt_irrefl
+
+@[simp] theorem not_lex_nil : ¬Lex r l [] := fun h => nomatch h
+
+@[simp] theorem nil_le [LT α] (l : List α) : [] ≤ l := fun h => nomatch h
+
+@[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 only [not_cons_lex_cons_iff, ne_eq]
+  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 => simp
+  | cons a l ih =>
+    intro
+    | .rel h => exact i₀.irrefl _ h
+    | .cons h₃ => exact ih h₃
+
+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.Lex.nil ..
+  | @rel a l₁ b l₂ ab =>
+    match h₂ with
+    | .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
+    | .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₂
+
+@[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 => 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 => simp [lex]
+    | cons b l₂ =>
+      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₂
+
+theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} :
+    l₁ < l₂ ↔
+      (l₁ = 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₂)) ∧ l₁[i] < l₂[i]) := by
+  rw [← lex_eq_true_iff_lt, lex_eq_true_iff_exists]
+  simp
+
+theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
+    [Std.Irrefl (· < · : α → α → Prop)]
+    [Std.Asymm (· < · : α → α → Prop)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)] {l₁ l₂ : List α} :
+    l₁ ≤ l₂ ↔
+      (l₁ = 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₂)) ∧ l₁[i] < l₂[i]) := by
+  rw [← lex_eq_false_iff_ge, lex_eq_false_iff_exists]
+  · simp only [isEqv_eq, beq_iff_eq, decide_eq_true_eq]
+    simp only [eq_comm]
+    conv => lhs; simp +singlePass [exists_comm]
+  · simpa using Std.Irrefl.irrefl
+  · simpa using Std.Asymm.asymm
+  · simpa using Std.Antisymm.antisymm
+
+end List
diff --git a/src/Init/Data/List/Monadic.lean b/src/Init/Data/List/Monadic.lean
index 040765fc5e..6d3c533d48 100644
--- a/src/Init/Data/List/Monadic.lean
+++ b/src/Init/Data/List/Monadic.lean
@@ -124,7 +124,8 @@ theorem foldrM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : α → β
 
 /-! ### forM -/
 
--- We use `List.forM` as the simp normal form, rather that `ForM.forM`.
+-- We currently use `List.forM` as the simp normal form, rather that `ForM.forM`.
+-- (This should probably be revisited.)
 -- As such we need to replace `List.forM_nil` and `List.forM_cons`:
 
 @[simp] theorem forM_nil' [Monad m] : ([] : List α).forM f = (pure .unit : m PUnit) := rfl
@@ -137,6 +138,10 @@ theorem foldrM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : α → β
     (l₁ ++ l₂).forM f = (do l₁.forM f; l₂.forM f) := by
   induction l₁ <;> simp [*]
 
+@[simp] theorem forM_map [Monad m] [LawfulMonad m] (l : List α) (g : α → β) (f : β → m PUnit) :
+    (l.map g).forM f = l.forM (fun a => f (g a)) := by
+  induction l <;> simp [*]
+
 /-! ### forIn' -/
 
 theorem forIn'_loop_congr [Monad m] {as bs : List α}
@@ -259,6 +264,11 @@ theorem forIn'_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
   generalize l.attach = l'
   induction l' generalizing init <;> simp_all
 
+@[simp] theorem forIn'_map [Monad m] [LawfulMonad m]
+    (l : List α) (g : α → β) (f : (b : β) → b ∈ l.map g → γ → m (ForInStep γ)) :
+    forIn' (l.map g) init f = forIn' l init fun a h y => f (g a) (mem_map_of_mem g h) y := by
+  induction l generalizing init <;> simp_all
+
 /--
 We can express a for loop over a list as a fold,
 in which whenever we reach `.done b` we keep that value through the rest of the fold.
@@ -307,6 +317,11 @@ theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
   simp only [forIn_eq_foldlM]
   induction l generalizing init <;> simp_all
 
+@[simp] theorem forIn_map [Monad m] [LawfulMonad m]
+    (l : List α) (g : α → β) (f : β → γ → m (ForInStep γ)) :
+    forIn (l.map g) init f = forIn l init fun a y => f (g a) y := by
+  induction l generalizing init <;> simp_all
+
 /-! ### allM -/
 
 theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as : List α) :
diff --git a/src/Init/Data/List/Range.lean b/src/Init/Data/List/Range.lean
index 0648fd1744..7b5906aef3 100644
--- a/src/Init/Data/List/Range.lean
+++ b/src/Init/Data/List/Range.lean
@@ -84,11 +84,15 @@ theorem head?_range' (n : Nat) : (range' s n).head? = if n = 0 then none else so
 @[simp] theorem head_range' (n : Nat) (h) : (range' s n).head h = s := by
   repeat simp_all [head?_range', head_eq_iff_head?_eq_some]
 
-@[simp]
 theorem map_add_range' (a) : ∀ s n step, map (a + ·) (range' s n step) = range' (a + s) n step
   | _, 0, _ => rfl
   | s, n + 1, step => by simp [range', map_add_range' _ (s + step) n step, Nat.add_assoc]
 
+theorem range'_succ_left : range' (s + 1) n step = (range' s n step).map (· + 1) := by
+  apply ext_getElem
+  · simp
+  · simp [Nat.add_right_comm]
+
 theorem range'_append : ∀ s m n step : Nat,
     range' s m step ++ range' (s + step * m) n step = range' s (n + m) step
   | _, 0, _, _ => rfl
diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean
index dec45472a4..ce2a7814c9 100644
--- a/src/Init/Data/List/ToArray.lean
+++ b/src/Init/Data/List/ToArray.lean
@@ -7,7 +7,7 @@ prelude
 import Init.Data.List.Impl
 import Init.Data.List.Nat.Erase
 import Init.Data.List.Monadic
-import Init.Data.Array.Lex
+import Init.Data.Array.Lex.Basic
 
 /-! ### Lemmas about `List.toArray`.
 
@@ -29,6 +29,11 @@ theorem toArray_inj {a b : List α} (h : a.toArray = b.toArray) : a = b := by
     (a.toArrayAux b).size = b.size + a.length := by
   simp [size]
 
+-- This is not a `@[simp]` lemma because it is pushing `toArray` inwards.
+theorem toArray_cons (a : α) (l : List α) : (a :: l).toArray = #[a] ++ l.toArray := by
+  apply ext'
+  simp
+
 @[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
   apply ext'
   simp
@@ -112,6 +117,18 @@ theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
   subst h
   rw [foldlM_toList]
 
+/-- Variant of `forM_toArray` with a side condition for the `stop` argument. -/
+@[simp] theorem forM_toArray' [Monad m] (l : List α) (f : α → m PUnit) (h : stop = l.toArray.size) :
+    (l.toArray.forM f 0 stop) = l.forM f := by
+  subst h
+  rw [Array.forM]
+  simp only [size_toArray, foldlM_toArray']
+  induction l <;> simp_all
+
+theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) :
+    (l.toArray.forM f) = l.forM f := by
+  simp
+
 /-- Variant of `foldr_toArray` with a side condition for the `start` argument. -/
 @[simp] theorem foldr_toArray' (f : α → β → β) (init : β) (l : List α)
     (h : start = l.toArray.size) :
diff --git a/src/Init/Data/Option/Monadic.lean b/src/Init/Data/Option/Monadic.lean
index 68c6b0a66f..2d520c680a 100644
--- a/src/Init/Data/Option/Monadic.lean
+++ b/src/Init/Data/Option/Monadic.lean
@@ -10,7 +10,17 @@ import Init.Control.Lawful.Basic
 
 namespace Option
 
-@[congr] theorem forIn'_congr [Monad m] [LawfulMonad m]{as bs : Option α} (w : as = bs)
+@[simp] theorem forM_none [Monad m] (f : α → m PUnit) :
+    none.forM f = pure .unit := rfl
+
+@[simp] theorem forM_some [Monad m] (f : α → m PUnit) (a : α) :
+    (some a).forM f = f a := rfl
+
+@[simp] theorem forM_map [Monad m] [LawfulMonad m] (o : Option α) (g : α → β) (f : β → m PUnit) :
+    (o.map g).forM f = o.forM (fun a => f (g a)) := by
+  cases o <;> simp
+
+@[congr] theorem forIn'_congr [Monad m] [LawfulMonad m] {as bs : Option α} (w : as = bs)
     {b b' : β} (hb : b = b')
     {f : (a' : α) → a' ∈ as → β → m (ForInStep β)}
     {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)}
@@ -48,6 +58,11 @@ theorem forIn'_pure_yield_eq_pelim [Monad m] [LawfulMonad m]
       o.pelim b (fun a h => f a h b) := by
   cases o <;> simp
 
+@[simp] theorem forIn'_map [Monad m] [LawfulMonad m]
+    (o : Option α) (g : α → β) (f : (b : β) → b ∈ o.map g → γ → m (ForInStep γ)) :
+    forIn' (o.map g) init f = forIn' o init fun a h y => f (g a) (mem_map_of_mem g h) y := by
+  cases o <;> simp
+
 theorem forIn_eq_elim [Monad m] [LawfulMonad m]
     (o : Option α) (f : (a : α) → β → m (ForInStep β)) (b : β) :
     forIn o b f =
@@ -72,4 +87,9 @@ theorem forIn_pure_yield_eq_elim [Monad m] [LawfulMonad m]
       o.elim b (fun a => f a b) := by
   cases o <;> simp
 
+@[simp] theorem forIn_map [Monad m] [LawfulMonad m]
+    (o : Option α) (g : α → β) (f : β → γ → m (ForInStep γ)) :
+    forIn (o.map g) init f = forIn o init fun a y => f (g a) y := by
+  cases o <;> simp
+
 end Option
diff --git a/src/Init/Data/Range/Basic.lean b/src/Init/Data/Range/Basic.lean
index b2f7ecbe24..0fa732dabc 100644
--- a/src/Init/Data/Range/Basic.lean
+++ b/src/Init/Data/Range/Basic.lean
@@ -23,7 +23,7 @@ namespace Range
 universe u v
 
 /-- The number of elements in the range. -/
-def size (r : Range) : Nat := (r.stop - r.start + r.step - 1) / r.step
+@[simp] def size (r : Range) : Nat := (r.stop - r.start + r.step - 1) / r.step
 
 @[inline] protected def forIn' [Monad m] (range : Range) (init : β)
     (f : (i : Nat) → i ∈ range → β → m (ForInStep β)) : m β :=
diff --git a/src/Init/Data/Range/Lemmas.lean b/src/Init/Data/Range/Lemmas.lean
index bc9c07c23c..63eaa573bd 100644
--- a/src/Init/Data/Range/Lemmas.lean
+++ b/src/Init/Data/Range/Lemmas.lean
@@ -70,7 +70,7 @@ private theorem forIn'_loop_eq_forIn'_range' [Monad m] (r : Std.Range)
       rw [Nat.div_eq_iff] <;> omega
     simp [this]
 
-theorem forIn'_eq_forIn'_range' [Monad m] (r : Std.Range)
+@[simp] theorem forIn'_eq_forIn'_range' [Monad m] (r : Std.Range)
     (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) :
     forIn' r init f =
       forIn' (List.range' r.start r.size r.step) init (fun a h => f a (mem_of_mem_range' h)) := by
@@ -78,7 +78,7 @@ theorem forIn'_eq_forIn'_range' [Monad m] (r : Std.Range)
   simp only [size]
   rw [forIn'_loop_eq_forIn'_range']
 
-theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
+@[simp] theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
     (init : β) (f : Nat → β → m (ForInStep β)) :
     forIn r init f = forIn (List.range' r.start r.size r.step) init f := by
   simp only [forIn, forIn'_eq_forIn'_range']
@@ -96,7 +96,7 @@ private theorem forM_loop_eq_forM_range' [Monad m] (r : Std.Range) (f : Nat →
       rw [Nat.div_eq_iff] <;> omega
     simp [this]
 
-theorem forM_eq_forM_range' [Monad m] (r : Std.Range) (f : Nat → m PUnit) :
+@[simp] theorem forM_eq_forM_range' [Monad m] (r : Std.Range) (f : Nat → m PUnit) :
     forM r f = forM (List.range' r.start r.size r.step) f := by
   simp only [forM, Range.forM, forM_loop_eq_forM_range', size]
 
diff --git a/src/Init/Data/String/Lemmas.lean b/src/Init/Data/String/Lemmas.lean
index fa787eb47f..d13cadd13a 100644
--- a/src/Init/Data/String/Lemmas.lean
+++ b/src/Init/Data/String/Lemmas.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Char.Lemmas
+import Init.Data.List.Lex
 
 namespace String
 
diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean
index 3edac5b5c4..44553e7634 100644
--- a/src/Init/Data/Vector/Basic.lean
+++ b/src/Init/Data/Vector/Basic.lean
@@ -287,12 +287,6 @@ no element of the index matches the given value.
 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.
 
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index 5f4a47c7a2..f9a85fd66b 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -1016,6 +1016,13 @@ theorem mem_setIfInBounds (v : Vector α n) (i : Nat) (hi : i < n) (a : α) :
       · rintro ⟨a, ha⟩
         simpa using Array.isEqv_self_beq ..
 
+/-! ### isEqv -/
+
+@[simp] theorem isEqv_eq [DecidableEq α] {l₁ l₂ : Vector α n} : l₁.isEqv l₂ (· == ·) = (l₁ = l₂) := by
+  cases l₁
+  cases l₂
+  simp
+
 /-! Content below this point has not yet been aligned with `List` and `Array`. -/
 
 @[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) :
@@ -1096,6 +1103,12 @@ theorem getElem_append_right {a : Vector α n} {b : Vector α m} {i : Nat} (h :
   cases b
   simp
 
+/-! ### take -/
+
+@[simp] theorem take_size (a : Vector α n) : a.take n = a.cast (by simp) := by
+  rcases a with ⟨a, rfl⟩
+  simp
+
 /-! ### swap -/
 
 theorem getElem_swap (a : Vector α n) (i j : Nat) {hi hj} (k : Nat) (hk : k < n) :
diff --git a/src/Init/Data/Vector/Lex.lean b/src/Init/Data/Vector/Lex.lean
new file mode 100644
index 0000000000..3d4f3a296b
--- /dev/null
+++ b/src/Init/Data/Vector/Lex.lean
@@ -0,0 +1,202 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.Vector.Basic
+import Init.Data.Vector.Lemmas
+import Init.Data.Array.Lex.Lemmas
+
+namespace Vector
+
+
+/-! ### Lexicographic ordering -/
+
+@[simp] theorem lt_toArray [LT α] (l₁ l₂ : Vector α n) : l₁.toArray < l₂.toArray ↔ l₁ < l₂ := Iff.rfl
+@[simp] theorem le_toArray [LT α] (l₁ l₂ : Vector α n) : l₁.toArray ≤ l₂.toArray ↔ l₁ ≤ l₂ := Iff.rfl
+
+@[simp] theorem lt_toList [LT α] (l₁ l₂ : Vector α n) : l₁.toList < l₂.toList ↔ l₁ < l₂ := Iff.rfl
+@[simp] theorem le_toList [LT α] (l₁ l₂ : Vector α n) : l₁.toList ≤ l₂.toList ↔ l₁ ≤ l₂ := Iff.rfl
+
+@[simp] theorem mk_lt_mk [LT α] :
+    Vector.mk (α := α) (n := n) data₁ size₁ < Vector.mk data₂ size₂ ↔ data₁ < data₂ := Iff.rfl
+
+@[simp] theorem mk_le_mk [LT α] :
+    Vector.mk (α := α) (n := n) data₁ size₁ ≤ Vector.mk data₂ size₂ ↔ data₁ ≤ data₂ := Iff.rfl
+
+@[simp] theorem mk_lex_mk [BEq α] (lt : α → α → Bool) {l₁ l₂ : Array α} {n₁ : l₁.size = n} {n₂ : l₂.size = n} :
+    (Vector.mk l₁ n₁).lex (Vector.mk l₂ n₂) lt = l₁.lex l₂ lt := by
+  simp [Vector.lex, Array.lex, n₁, n₂]
+  rfl
+
+@[simp] theorem lex_toArray [BEq α] (lt : α → α → Bool) (l₁ l₂ : Vector α n) :
+    l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt := by
+  cases l₁
+  cases l₂
+  simp
+
+@[simp] theorem lex_toList [BEq α] (lt : α → α → Bool) (l₁ l₂ : Vector α n) :
+    l₁.toList.lex l₂.toList lt = l₁.lex l₂ lt := by
+  rcases l₁ with ⟨⟨l₁⟩, n₁⟩
+  rcases l₂ with ⟨⟨l₂⟩, n₂⟩
+  simp
+
+@[simp] theorem lex_empty
+    [BEq α] {lt : α → α → Bool} (l₁ : Vector α 0) : l₁.lex #v[] lt = false := by
+  cases l₁
+  simp_all
+
+@[simp] theorem singleton_lex_singleton [BEq α] {lt : α → α → Bool} : #v[a].lex #v[b] lt = lt a b := by
+  simp only [lex, getElem_mk, List.getElem_toArray, List.getElem_singleton]
+  cases lt a b <;> cases a != b <;> simp [Id.run]
+
+protected theorem lt_irrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)] (l : Vector α n) : ¬ l < l :=
+  Array.lt_irrefl l.toArray
+
+instance ltIrrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)] : Std.Irrefl (α := Vector α n) (· < ·) where
+  irrefl := Vector.lt_irrefl
+
+@[simp] theorem empty_le [LT α] (l : Vector α 0) : #v[] ≤ l := Array.empty_le l.toArray
+
+@[simp] theorem le_empty [LT α] (l : Vector α 0) : l ≤ #v[] ↔ l = #v[] := by
+  cases l
+  simp
+
+protected theorem le_refl [LT α] [i₀ : Std.Irrefl (· < · : α → α → Prop)] (l : Vector α n) : l ≤ l :=
+  Array.le_refl l.toArray
+
+instance [LT α] [Std.Irrefl (· < · : α → α → Prop)] : Std.Refl (· ≤ · : Vector α n → Vector α n → Prop) where
+  refl := Vector.le_refl
+
+protected theorem lt_trans [LT α] [DecidableLT α]
+    [i₁ : Trans (· < · : α → α → Prop) (· < ·) (· < ·)]
+    {l₁ l₂ l₃ : Vector α n} (h₁ : l₁ < l₂) (h₂ : l₂ < l₃) : l₁ < l₃ :=
+  Array.lt_trans h₁ h₂
+
+instance [LT α] [DecidableLT α]
+    [Trans (· < · : α → α → Prop) (· < ·) (· < ·)] :
+    Trans (· < · : Vector α n → Vector α n → Prop) (· < ·) (· < ·) where
+  trans h₁ h₂ := Vector.lt_trans h₁ h₂
+
+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₃ : Vector α n} (h₁ : l₁ ≤ l₂) (h₂ : l₂ < l₃) : l₁ < l₃ :=
+  Array.lt_of_le_of_lt h₁ h₂
+
+protected theorem le_trans [DecidableEq α] [LT α] [DecidableLT α]
+    [Std.Irrefl (· < · : α → α → Prop)]
+    [Std.Asymm (· < · : α → α → Prop)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)]
+    [Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
+    {l₁ l₂ l₃ : Vector α n} (h₁ : l₁ ≤ l₂) (h₂ : l₂ ≤ l₃) : l₁ ≤ l₃ :=
+  fun h₃ => h₁ (Vector.lt_of_le_of_lt h₂ h₃)
+
+instance [DecidableEq α] [LT α] [DecidableLT α]
+    [Std.Irrefl (· < · : α → α → Prop)]
+    [Std.Asymm (· < · : α → α → Prop)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)]
+    [Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)] :
+    Trans (· ≤ · : Vector α n → Vector α n → Prop) (· ≤ ·) (· ≤ ·) where
+  trans h₁ h₂ := Vector.le_trans h₁ h₂
+
+protected theorem lt_asymm [DecidableEq α] [LT α] [DecidableLT α]
+    [i : Std.Asymm (· < · : α → α → Prop)]
+    {l₁ l₂ : Vector α n} (h : l₁ < l₂) : ¬ l₂ < l₁ := Array.lt_asymm h
+
+instance [DecidableEq α] [LT α] [DecidableLT α]
+    [Std.Asymm (· < · : α → α → Prop)] :
+    Std.Asymm (· < · : Vector α n → Vector α n → Prop) where
+  asymm _ _ := Vector.lt_asymm
+
+protected theorem le_total [DecidableEq α] [LT α] [DecidableLT α]
+    [i : Std.Total (¬ · < · : α → α → Prop)] {l₁ l₂ : Vector α n} : l₁ ≤ l₂ ∨ l₂ ≤ l₁ :=
+  Array.le_total
+
+instance [DecidableEq α] [LT α] [DecidableLT α]
+    [Std.Total (¬ · < · : α → α → Prop)] :
+    Std.Total (· ≤ · : Vector α n → Vector α n → Prop) where
+  total _ _ := Vector.le_total
+
+@[simp] theorem lex_eq_true_iff_lt [DecidableEq α] [LT α] [DecidableLT α]
+    {l₁ l₂ : Vector α n} : lex l₁ l₂ = true ↔ l₁ < l₂ := by
+  cases l₁
+  cases l₂
+  simp
+
+@[simp] theorem lex_eq_false_iff_ge [DecidableEq α] [LT α] [DecidableLT α]
+    {l₁ l₂ : Vector α n} : lex l₁ l₂ = false ↔ l₂ ≤ l₁ := by
+  cases l₁
+  cases l₂
+  simp [Array.not_lt_iff_ge]
+
+instance [DecidableEq α] [LT α] [DecidableLT α] : DecidableLT (Vector α n) :=
+  fun l₁ l₂ => decidable_of_iff (lex l₁ l₂ = true) lex_eq_true_iff_lt
+
+instance [DecidableEq α] [LT α] [DecidableLT α] : DecidableLE (Vector α n) :=
+  fun l₁ l₂ => decidable_of_iff (lex l₂ l₁ = false) lex_eq_false_iff_ge
+
+/--
+`l₁` is lexicographically less than `l₂` if either
+- `l₁` is pairwise equivalent under `· == ·` to `l₂.take l₁.size`,
+  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) {l₁ l₂ : Vector α n} :
+    lex l₁ l₂ lt = true ↔
+      (∃ (i : Nat) (h : i < n), (∀ j, (hj : j < i) → l₁[j] == l₂[j]) ∧ lt l₁[i] l₂[i]) := by
+  rcases l₁ with ⟨l₁, n₁⟩
+  rcases l₂ with ⟨l₂, n₂⟩
+  simp [Array.lex_eq_true_iff_exists, n₁, n₂]
+
+/--
+`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)
+    {l₁ l₂ : Vector α n} :
+    lex l₁ l₂ lt = false ↔
+      (l₂.isEqv l₁ (· == ·)) ∨
+        (∃ (i : Nat) (h : i < n),(∀ j, (hj : j < i) → l₁[j] == l₂[j]) ∧ lt l₂[i] l₁[i]) := by
+  rcases l₁ with ⟨l₁, rfl⟩
+  rcases l₂ with ⟨l₂, n₂⟩
+  simp_all [Array.lex_eq_false_iff_exists, n₂]
+
+theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Vector α n} :
+    l₁ < l₂ ↔
+      (∃ (i : Nat) (h : i < n), (∀ j, (hj : j < i) → l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]) := by
+  cases l₁
+  cases l₂
+  simp_all [Array.lt_iff_exists]
+
+theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
+    [Std.Irrefl (· < · : α → α → Prop)]
+    [Std.Asymm (· < · : α → α → Prop)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)] {l₁ l₂ : Vector α n} :
+    l₁ ≤ l₂ ↔
+      (l₁ = l₂) ∨
+        (∃ (i : Nat) (h : i < n), (∀ j, (hj : j < i) → l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]) := by
+  rcases l₁ with ⟨l₁, rfl⟩
+  rcases l₂ with ⟨l₂, n₂⟩
+  simp [Array.le_iff_exists, ← n₂]
+
+end Vector
diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean
index 1bd4a700d6..b9e238b6da 100644
--- a/src/Init/PropLemmas.lean
+++ b/src/Init/PropLemmas.lean
@@ -362,6 +362,10 @@ theorem exists_prop' {p : Prop} : (∃ _ : α, p) ↔ Nonempty α ∧ p :=
 @[simp] theorem exists_prop : (∃ _h : a, b) ↔ a ∧ b :=
   ⟨fun ⟨hp, hq⟩ => ⟨hp, hq⟩, fun ⟨hp, hq⟩ => ⟨hp, hq⟩⟩
 
+@[simp] theorem exists_idem {P : Prop} (f : P → P → Sort _) :
+    (∃ (p₁ : P), ∃ (p₂ : P), f p₁ p₂) ↔ ∃ (p : P), f p p :=
+  ⟨fun ⟨p, _, h⟩ => ⟨p, h⟩, fun ⟨p, h⟩ => ⟨p, p, h⟩⟩
+
 @[simp] theorem exists_apply_eq_apply (f : α → β) (a' : α) : ∃ a, f a = f a' := ⟨a', rfl⟩
 
 theorem forall_prop_of_true {p : Prop} {q : p → Prop} (h : p) : (∀ h' : p, q h') ↔ q h :=