From 33d7f346440869364a2cd077bde8cebf73243aaa Mon Sep 17 00:00:00 2001
From: Jared Corduan <jaredcorduan@gmail.com>
Date: Thu, 21 Nov 2024 07:31:31 -0500
Subject: [PATCH 01/31] fix: Readme.md needs "git" token in lakefile.lean
 (#1056)

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 2873f65536..e20b87c09f 100644
--- a/README.md
+++ b/README.md
@@ -6,7 +6,7 @@ The "batteries included" extended library for Lean 4. This is a collection of da
 
 To use `batteries` in your project, add the following to your `lakefile.lean`:
 ```lean
-require "leanprover-community" / "batteries" @ "main"
+require "leanprover-community" / "batteries" @ git "main"
 ```
 Or add the following to your `lakefile.toml`:
 ```toml

From 4efc0bf8d39cd7fb92e59f44ad38091ca14de2ce Mon Sep 17 00:00:00 2001
From: leanprover-community-mathlib4-bot
 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Date: Fri, 22 Nov 2024 09:06:26 +0000
Subject: [PATCH 02/31] chore: bump to nightly-2024-11-22

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index f589f3bf8f..ae2a1d4650 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-21
+leanprover/lean4:nightly-2024-11-22

From 8b52587ff32e2e443cce6109b5305341289339e7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= <fgdorais@gmail.com>
Date: Fri, 22 Nov 2024 19:38:59 -0500
Subject: [PATCH 03/31] chore: fix workflow token (#1059)

---
 .github/workflows/labels-from-status.yml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.github/workflows/labels-from-status.yml b/.github/workflows/labels-from-status.yml
index 8ad37be1ae..147af67f34 100644
--- a/.github/workflows/labels-from-status.yml
+++ b/.github/workflows/labels-from-status.yml
@@ -34,6 +34,7 @@ jobs:
       if: github.event.pull_request.state == 'closed'
       uses: actions-ecosystem/action-remove-labels@v1
       with:
+        github_token: ${{ secrets.GITHUB_TOKEN }}
         labels: |
           WIP
           awaiting-author
@@ -48,6 +49,7 @@ jobs:
         ! contains(github.event.pull_request.labels.*.name, 'WIP')
       uses: actions-ecosystem/action-add-labels@v1
       with:
+        github_token: ${{ secrets.GITHUB_TOKEN }}
         labels: WIP
 
     - name: Label unlabeled other PR as awaiting-review
@@ -59,4 +61,5 @@ jobs:
         ! contains(github.event.pull_request.labels.*.name, 'WIP')
       uses: actions-ecosystem/action-add-labels@v1
       with:
+        github_token: ${{ secrets.GITHUB_TOKEN }}
         labels: awaiting-review

From 0dc51ac7947ff6aa2c16bcffb64c46c7149d1276 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sat, 23 Nov 2024 20:03:43 +1100
Subject: [PATCH 04/31] chore: fix two deprecations (#1061)

---
 Batteries/Lean/Expr.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Batteries/Lean/Expr.lean b/Batteries/Lean/Expr.lean
index 98781ab0aa..17761cfaa0 100644
--- a/Batteries/Lean/Expr.lean
+++ b/Batteries/Lean/Expr.lean
@@ -24,10 +24,10 @@ def toSyntax (e : Expr) : TermElabM Syntax.Term := withFreshMacroScope do
   mvar.mvarId!.assign e
   pure stx
 
-@[deprecated (since := "2024-10-16"), inherit_doc getNumHeadLambdas]
+@[deprecated getNumHeadLambdas (since := "2024-10-16"), inherit_doc getNumHeadLambdas]
 abbrev lambdaArity := @getNumHeadLambdas
 
-@[deprecated (since := "2024-11-13"), inherit_doc getNumHeadForalls]
+@[deprecated getNumHeadForalls(since := "2024-11-13"), inherit_doc getNumHeadForalls]
 abbrev forallArity := @getNumHeadForalls
 
 /-- Like `withApp` but ignores metadata. -/

From 220f518842372e0ee5747482f9d13cf3fa499e96 Mon Sep 17 00:00:00 2001
From: leanprover-community-mathlib4-bot
 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Date: Sat, 23 Nov 2024 09:05:58 +0000
Subject: [PATCH 05/31] chore: bump to nightly-2024-11-23

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index ae2a1d4650..fdc71e836b 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-22
+leanprover/lean4:nightly-2024-11-23

From 4a0cc9424af7acd48ce2e156e1257b718ccb79cf Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sat, 23 Nov 2024 20:42:13 +1100
Subject: [PATCH 06/31] fix test

---
 BatteriesTest/help_cmd.lean | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/BatteriesTest/help_cmd.lean b/BatteriesTest/help_cmd.lean
index 23e3698b6d..f76f95c8c9 100644
--- a/BatteriesTest/help_cmd.lean
+++ b/BatteriesTest/help_cmd.lean
@@ -148,13 +148,12 @@ error: no syntax categories start with foobarbaz
 #help cats foobarbaz
 
 /--
-info:
-category prec [Lean.Parser.Category.prec]
+info: category prec [Lean.Parser.Category.prec]
   `prec` is a builtin syntax category for precedences. A precedence is a value
   that expresses how tightly a piece of syntax binds: for example `1 + 2 * 3` is
-  parsed as `1 + (2 * 3)` because `*` has a higher pr0ecedence than `+`.
+  parsed as `1 + (2 * 3)` because `*` has a higher precedence than `+`.
   Higher numbers denote higher precedence.
-  In addition to literals like `37`, there are some special named priorities:
+  In addition to literals like `37`, there are some special named precedence levels:
   * `arg` for the precedence of function arguments
   * `max` for the highest precedence used in term parsers (not actually the maximum possible value)
   * `lead` for the precedence of terms not supposed to be used as arguments

From 3edeb1e515695b57b20d8c128db6be3703cece8c Mon Sep 17 00:00:00 2001
From: leanprover-community-mathlib4-bot
 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Date: Sun, 24 Nov 2024 06:37:09 +0000
Subject: [PATCH 07/31] Update lean-toolchain for testing
 https://github.com/leanprover/lean4/pull/6194

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index fdc71e836b..7b38e2425b 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-23
+leanprover/lean4-pr-releases:pr-release-6194

From c87de447533223d663f5fd67fd1e602caf725da2 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sun, 24 Nov 2024 18:14:27 +1100
Subject: [PATCH 08/31] fixes for leanprover/lean4#6194

---
 Batteries/Data/Array/Basic.lean  | 18 ++-------------
 Batteries/Data/Array/Lemmas.lean |  2 --
 Batteries/Data/BinaryHeap.lean   |  6 ++---
 Batteries/Data/Vector/Basic.lean | 38 ++++++++++----------------------
 4 files changed, 17 insertions(+), 47 deletions(-)

diff --git a/Batteries/Data/Array/Basic.lean b/Batteries/Data/Array/Basic.lean
index 5631aa3628..9164b1219e 100644
--- a/Batteries/Data/Array/Basic.lean
+++ b/Batteries/Data/Array/Basic.lean
@@ -137,23 +137,9 @@ This will perform the update destructively provided that `a` has a reference cou
 abbrev setN (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) : Array α :=
   a.set i x
 
-/--
-`swapN a i j hi hj` swaps two `Nat` indexed entries in an `Array α`.
-Uses `get_elem_tactic` to supply a proof that the indices are in range.
-`hi` and `hj` are both given a default argument `by get_elem_tactic`.
-This will perform the update destructively provided that `a` has a reference count of 1 when called.
--/
-abbrev swapN (a : Array α) (i j : Nat)
-    (hi : i < a.size := by get_elem_tactic) (hj : j < a.size := by get_elem_tactic) : Array α :=
-  Array.swap a ⟨i,hi⟩ ⟨j, hj⟩
+@[deprecated (since := "2024-11-24")] alias swapN := swap
 
-/--
-`swapAtN a i h x` swaps the entry with index `i : Nat` in the vector for a new entry `x`.
-The old entry is returned alongwith the modified vector.
-Automatically generates proof of `i < a.size` with `get_elem_tactic` where feasible.
--/
-abbrev swapAtN (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) :
-    α × Array α := swapAt a ⟨i,h⟩ x
+@[deprecated (since := "2024-11-24")] alias swapAtN := swapAt
 
 @[deprecated (since := "2024-11-20")] alias eraseIdxN := eraseIdx
 
diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
index 58509c2fb9..155d78889c 100644
--- a/Batteries/Data/Array/Lemmas.lean
+++ b/Batteries/Data/Array/Lemmas.lean
@@ -150,13 +150,11 @@ theorem getElem_insertIdx_loop_gt {as : Array α} {i : Nat} {j : Nat} {hj : j <
     have : j - 1 < j := by omega
     rw [getElem_insertIdx_loop_gt w]
     rw [getElem_swap]
-    simp only [Fin.getElem_fin]
     split <;> rename_i h₂
     · rw [if_neg (by omega), if_neg (by omega)]
       have t : k ≤ j := by omega
       simp [t]
     · rw [getElem_swap]
-      simp only [Fin.getElem_fin]
       rw [if_neg (by omega)]
       split <;> rename_i h₃
       · simp [h₃]
diff --git a/Batteries/Data/BinaryHeap.lean b/Batteries/Data/BinaryHeap.lean
index 897cca1c2a..cf856ad335 100644
--- a/Batteries/Data/BinaryHeap.lean
+++ b/Batteries/Data/BinaryHeap.lean
@@ -67,9 +67,9 @@ def heapifyUp (lt : α → α → Bool) (a : Vector α sz) (i : Fin sz) :
   match i with
   | ⟨0, _⟩ => a
   | ⟨i'+1, hi⟩ =>
-    let j := ⟨i'/2, by get_elem_tactic⟩
+    let j := i'/2
     if lt a[j] a[i] then
-      heapifyUp lt (a.swap i j) j
+      heapifyUp lt (a.swap i j) ⟨j, by get_elem_tactic⟩
     else a
 
 /-- `O(1)`. Build a new empty heap. -/
@@ -107,7 +107,7 @@ def popMax (self : BinaryHeap α lt) : BinaryHeap α lt :=
   if h0 : self.size = 0 then self else
     have hs : self.size - 1 < self.size := Nat.pred_lt h0
     have h0 : 0 < self.size := Nat.zero_lt_of_ne_zero h0
-    let v := self.vector.swap ⟨_, h0⟩ ⟨_, hs⟩ |>.pop
+    let v := self.vector.swap _ _ h0 hs |>.pop
     if h : 0 < self.size - 1 then
       ⟨heapifyDown lt v ⟨0, h⟩ |>.toArray⟩
     else
diff --git a/Batteries/Data/Vector/Basic.lean b/Batteries/Data/Vector/Basic.lean
index 315e8b932f..da83a8cfac 100644
--- a/Batteries/Data/Vector/Basic.lean
+++ b/Batteries/Data/Vector/Basic.lean
@@ -175,26 +175,21 @@ Swap two elements of a vector using `Fin` indices.
 
 This will perform the update destructively provided that the vector has a reference count of 1.
 -/
-@[inline] def swap (v : Vector α n) (i j : Fin n) : Vector α n :=
-  ⟨v.toArray.swap (Fin.cast v.size_toArray.symm i) (Fin.cast v.size_toArray.symm j), by simp⟩
-
-/--
-Swap two elements of a vector using `Nat` indices. By default, the `get_elem_tactic` is used to
-synthesize proofs that the indices are within bounds.
-
-This will perform the update destructively provided that the vector has a reference count of 1.
--/
-@[inline] def swapN (v : Vector α n) (i j : Nat)
+@[inline] def swap (v : Vector α n) (i j : Nat)
     (hi : i < n := by get_elem_tactic) (hj : j < n := by get_elem_tactic) : Vector α n :=
-  ⟨v.toArray.swapN i j (by simp_all) (by simp_all), by simp⟩
+  ⟨v.toArray.swap i j (by simpa using hi) (by simpa using hj), by simp⟩
+
+@[deprecated (since := "2024-11-24")] alias swapN := swap
 
 /--
 Swap two elements of a vector using `Nat` indices. Panics if either index is out of bounds.
 
 This will perform the update destructively provided that the vector has a reference count of 1.
 -/
-@[inline] def swap! (v : Vector α n) (i j : Nat) : Vector α n :=
-  ⟨v.toArray.swap! i j, by simp⟩
+@[inline] def swapIfInBounds (v : Vector α n) (i j : Nat) : Vector α n :=
+  ⟨v.toArray.swapIfInBounds i j, by simp⟩
+
+@[deprecated (since := "2024-11-24")] alias swap! := swapIfInBounds
 
 /--
 Swaps an element of a vector with a given value using a `Fin` index. The original value is returned
@@ -202,22 +197,13 @@ along with the updated vector.
 
 This will perform the update destructively provided that the vector has a reference count of 1.
 -/
-@[inline] def swapAt (v : Vector α n) (i : Fin n) (x : α) : α × Vector α n :=
-  let a := v.toArray.swapAt (Fin.cast v.size_toArray.symm i) x
-  ⟨a.fst, a.snd, by simp [a]⟩
-
-/--
-Swaps an element of a vector with a given value using a `Nat` index. By default, the
-`get_elem_tactic` is used to synthesise a proof that the index is within bounds. The original value
-is returned along with the updated vector.
-
-This will perform the update destructively provided that the vector has a reference count of 1.
--/
-@[inline] def swapAtN (v : Vector α n) (i : Nat) (x : α) (h : i < n := by get_elem_tactic) :
+@[inline] def swapAt (v : Vector α n) (i : Nat) (x : α) (hi : i < n := by get_elem_tactic) :
     α × Vector α n :=
-  let a := v.toArray.swapAtN i x (by simp_all)
+  let a := v.toArray.swapAt i x (by simpa using hi)
   ⟨a.fst, a.snd, by simp [a]⟩
 
+@[deprecated (since := "2024-11-24")] alias swapAtN := swapAt
+
 /--
 Swaps an element of a vector with a given value using a `Nat` index. Panics if the index is out of
 bounds. The original value is returned along with the updated vector.

From 08d6d8d142ecdff2c3ddb20c0f46583a7fa4e8a5 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sun, 24 Nov 2024 18:22:40 +1100
Subject: [PATCH 09/31] fix

---
 BatteriesTest/help_cmd.lean | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/BatteriesTest/help_cmd.lean b/BatteriesTest/help_cmd.lean
index 23e3698b6d..f76f95c8c9 100644
--- a/BatteriesTest/help_cmd.lean
+++ b/BatteriesTest/help_cmd.lean
@@ -148,13 +148,12 @@ error: no syntax categories start with foobarbaz
 #help cats foobarbaz
 
 /--
-info:
-category prec [Lean.Parser.Category.prec]
+info: category prec [Lean.Parser.Category.prec]
   `prec` is a builtin syntax category for precedences. A precedence is a value
   that expresses how tightly a piece of syntax binds: for example `1 + 2 * 3` is
-  parsed as `1 + (2 * 3)` because `*` has a higher pr0ecedence than `+`.
+  parsed as `1 + (2 * 3)` because `*` has a higher precedence than `+`.
   Higher numbers denote higher precedence.
-  In addition to literals like `37`, there are some special named priorities:
+  In addition to literals like `37`, there are some special named precedence levels:
   * `arg` for the precedence of function arguments
   * `max` for the highest precedence used in term parsers (not actually the maximum possible value)
   * `lead` for the precedence of terms not supposed to be used as arguments

From 897bb634d59160910345ea1eed665f622d9146de Mon Sep 17 00:00:00 2001
From: leanprover-community-mathlib4-bot
 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Date: Sun, 24 Nov 2024 07:34:11 +0000
Subject: [PATCH 10/31] Trigger CI for
 https://github.com/leanprover/lean4/pull/6194


From 96f2c13c5df7415a728aad50aeef6b3493968874 Mon Sep 17 00:00:00 2001
From: leanprover-community-mathlib4-bot
 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Date: Sun, 24 Nov 2024 08:50:35 +0000
Subject: [PATCH 11/31] Update lean-toolchain for testing
 https://github.com/leanprover/lean4/pull/6195

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index fdc71e836b..5d2497c823 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-23
+leanprover/lean4-pr-releases:pr-release-6195

From 85cadff63aab36f19c18434921628449ab540bd6 Mon Sep 17 00:00:00 2001
From: leanprover-community-mathlib4-bot
 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Date: Sun, 24 Nov 2024 09:05:13 +0000
Subject: [PATCH 12/31] chore: bump to nightly-2024-11-24

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index fdc71e836b..22be24ab2e 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-23
+leanprover/lean4:nightly-2024-11-24

From 44e2d2e643fd2618b01f9a0592d7dcbd3ffa22de Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= <fgdorais@gmail.com>
Date: Sun, 24 Nov 2024 18:42:43 -0500
Subject: [PATCH 13/31] feat: more vector lemmas (#1062)

---
 Batteries/Data/Vector/Basic.lean  |   7 +-
 Batteries/Data/Vector/Lemmas.lean | 261 ++++++++++++++++++++++++------
 2 files changed, 215 insertions(+), 53 deletions(-)

diff --git a/Batteries/Data/Vector/Basic.lean b/Batteries/Data/Vector/Basic.lean
index 0ae5871356..0273c93c18 100644
--- a/Batteries/Data/Vector/Basic.lean
+++ b/Batteries/Data/Vector/Basic.lean
@@ -9,6 +9,7 @@ import Batteries.Data.List.Basic
 import Batteries.Data.List.Lemmas
 import Batteries.Tactic.Alias
 import Batteries.Tactic.Lint.Misc
+import Batteries.Tactic.PrintPrefix
 
 /-!
 # Vectors
@@ -252,7 +253,7 @@ Compares two vectors of the same size using a given boolean relation `r`. `isEqv
 `true` if and only if `r v[i] w[i]` is true for all indices `i`.
 -/
 @[inline] def isEqv (v w : Vector α n) (r : α → α → Bool) : Bool :=
-  Array.isEqvAux v.toArray w.toArray (by simp) r 0 (by simp)
+  Array.isEqvAux v.toArray w.toArray (by simp) r n (by simp)
 
 instance [BEq α] : BEq (Vector α n) where
   beq a b := isEqv a b (· == ·)
@@ -294,9 +295,7 @@ Finds the first index of a given value in a vector using `==` for comparison. Re
 no element of the index matches the given value.
 -/
 @[inline] def indexOf? [BEq α] (v : Vector α n) (x : α) : Option (Fin n) :=
-  match v.toArray.indexOf? x with
-  | some res => some (res.cast v.size_toArray)
-  | none => none
+  (v.toArray.indexOf? x).map (Fin.cast v.size_toArray)
 
 /-- Returns `true` when `v` is a prefix of the vector `w`. -/
 @[inline] def isPrefixOf [BEq α] (v : Vector α m) (w : Vector α n) : Bool :=
diff --git a/Batteries/Data/Vector/Lemmas.lean b/Batteries/Data/Vector/Lemmas.lean
index 6271f39f02..9a14c4a548 100644
--- a/Batteries/Data/Vector/Lemmas.lean
+++ b/Batteries/Data/Vector/Lemmas.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Shreyas Srinivas. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Shreyas Srinivas, Francois Dorais
+Authors: Shreyas Srinivas, François G. Dorais
 -/
 
 import Batteries.Data.Vector.Basic
@@ -10,50 +10,13 @@ import Batteries.Data.List.Lemmas
 import Batteries.Data.Array.Lemmas
 import Batteries.Tactic.Lint.Simp
 
-/-!
-## Vectors
-Lemmas about `Vector α n`
--/
-
 namespace Batteries
 
 namespace Vector
 
-theorem length_toList {α n} (xs : Vector α n) : xs.toList.length = n := by simp
-
-@[simp] theorem getElem_mk {data : Array α} {size : data.size = n} {i : Nat} (h : i < n) :
-    (Vector.mk data size)[i] = data[i] := rfl
-
-@[simp] theorem getElem_toArray {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toArray.size) :
-    xs.toArray[i] = xs[i]'(by simpa using h) := by
-  cases xs
-  simp
-
-theorem getElem_toList {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toList.length) :
-    xs.toList[i] = xs[i]'(by simpa using h) := by simp
-
-@[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) :
-    (Vector.ofFn f)[i] = f ⟨i, by simpa using h⟩ := by
-  simp [ofFn]
-
-/-- An `empty` vector maps to a `empty` vector. -/
-@[simp]
-theorem map_empty (f : α → β) : map f empty = empty := by
-  rw [map, empty, mk.injEq]
-  exact Array.map_empty f
-
 theorem toArray_injective : ∀ {v w : Vector α n}, v.toArray = w.toArray → v = w
   | {..}, {..}, rfl => rfl
 
-/-- A vector of length `0` is an `empty` vector. -/
-protected theorem eq_empty (v : Vector α 0) : v = empty := by
-  apply Vector.toArray_injective
-  apply Array.eq_empty_of_size_eq_zero v.2
-
-/--
-`Vector.ext` is an extensionality theorem.
-Vectors `a` and `b` are equal to each other if their elements are equal for each valid index.
--/
 @[ext]
 protected theorem ext {a b : Vector α n} (h : (i : Nat) → (_ : i < n) → a[i] = b[i]) : a = b := by
   apply Vector.toArray_injective
@@ -63,26 +26,217 @@ protected theorem ext {a b : Vector α n} (h : (i : Nat) → (_ : i < n) → a[i
     rw [a.size_toArray] at hi
     exact h i hi
 
-@[simp] theorem push_mk {data : Array α} {size : data.size = n} {x : α} :
-    (Vector.mk data size).push x =
-      Vector.mk (data.push x) (by simp [size, Nat.succ_eq_add_one]) := rfl
+/-! ### mk lemmas -/
+
+theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a := rfl
+
+@[simp] theorem allDiff_mk [BEq α] (a : Array α) (h : a.size = n) :
+    (Vector.mk a h).allDiff = a.allDiff := rfl
+
+@[simp] theorem mk_append_mk (a b : Array α) (ha : a.size = n) (hb : b.size = m) :
+    Vector.mk a ha ++ Vector.mk b hb = Vector.mk (a ++ b) (by simp [ha, hb]) := rfl
+
+@[simp] theorem back!_mk [Inhabited α] (a : Array α) (h : a.size = n) :
+    (Vector.mk a h).back! = a.back! := rfl
+
+@[simp] theorem back?_mk (a : Array α) (h : a.size = n) :
+    (Vector.mk a h).back? = a.back? := rfl
+
+@[simp] theorem drop_mk (a : Array α) (h : a.size = n) (m) :
+    (Vector.mk a h).drop m = Vector.mk (a.extract m a.size) (by simp [h]) := rfl
+
+@[simp] theorem eraseIdx!_mk (a : Array α) (h : a.size = n) (i) (hi : i < n) :
+    (Vector.mk a h).eraseIdx! i = Vector.mk (a.eraseIdx! i) (by simp [h, hi]) := by
+  simp [Vector.eraseIdx!, hi]
+
+@[simp] theorem feraseIdx_mk (a : Array α) (h : a.size = n) (i) :
+    (Vector.mk a h).feraseIdx i = Vector.mk (a.feraseIdx (i.cast h.symm)) (by simp [h]) := rfl
+
+@[simp] theorem extract_mk (a : Array α) (h : a.size = n) (start stop) :
+    (Vector.mk a h).extract start stop = Vector.mk (a.extract start stop) (by simp [h]) := rfl
+
+@[simp] theorem getElem_mk (a : Array α) (h : a.size = n) (i) (hi : i < n) :
+    (Vector.mk a h)[i] = a[i] := rfl
+
+@[simp] theorem get_mk (a : Array α) (h : a.size = n) (i) :
+    (Vector.mk a h).get i = a.get (i.cast h.symm) := rfl
+
+@[simp] theorem getD_mk (a : Array α) (h : a.size = n) (i x) :
+    (Vector.mk a h).getD i x = a.getD i x := rfl
+
+@[simp] theorem uget_mk (a : Array α) (h : a.size = n) (i) (hi : i.toNat < n) :
+    (Vector.mk a h).uget i hi = a.uget i (by simp [h, hi]) := rfl
+
+@[simp] theorem indexOf?_mk [BEq α] (a : Array α) (h : a.size = n) (x : α) :
+    (Vector.mk a h).indexOf? x = (a.indexOf? x).map (Fin.cast h) := rfl
+
+@[simp] theorem mk_isEqv_mk (r : α → α → Bool) (a b : Array α) (ha : a.size = n) (hb : b.size = n) :
+    Vector.isEqv (Vector.mk a ha) (Vector.mk b hb) r = Array.isEqv a b r := by
+  simp [Vector.isEqv, Array.isEqv, ha, hb]
+
+@[simp] theorem mk_isPrefixOf_mk [BEq α] (a b : Array α) (ha : a.size = n) (hb : b.size = m) :
+    (Vector.mk a ha).isPrefixOf (Vector.mk b hb) = a.isPrefixOf b := rfl
+
+@[simp] theorem map_mk (a : Array α) (h : a.size = n) (f : α → β) :
+    (Vector.mk a h).map f = Vector.mk (a.map f) (by simp [h]) := rfl
+
+@[simp] theorem pop_mk (a : Array α) (h : a.size = n) :
+    (Vector.mk a h).pop = Vector.mk a.pop (by simp [h]) := rfl
+
+@[simp] theorem push_mk (a : Array α) (h : a.size = n) (x) :
+    (Vector.mk a h).push x = Vector.mk (a.push x) (by simp [h]) := rfl
+
+@[simp] theorem reverse_mk (a : Array α) (h : a.size = n) :
+    (Vector.mk a h).reverse = Vector.mk a.reverse (by simp [h]) := rfl
+
+@[simp] theorem set_mk (a : Array α) (h : a.size = n) (i x) :
+    (Vector.mk a h).set i x = Vector.mk (a.set (i.cast h.symm) x) (by simp [h]) := rfl
+
+@[simp] theorem set!_mk (a : Array α) (h : a.size = n) (i x) :
+    (Vector.mk a h).set! i x = Vector.mk (a.set! i x) (by simp [h]) := rfl
+
+@[simp] theorem setD_mk (a : Array α) (h : a.size = n) (i x) :
+    (Vector.mk a h).setD i x = Vector.mk (a.setD i x) (by simp [h]) := rfl
+
+@[simp] theorem setN_mk (a : Array α) (h : a.size = n) (i x) (hi : i < n) :
+    (Vector.mk a h).setN i x = Vector.mk (a.setN i x) (by simp [h]) := rfl
+
+@[simp] theorem swap_mk (a : Array α) (h : a.size = n) (i j) :
+    (Vector.mk a h).swap i j = Vector.mk (a.swap (i.cast h.symm) (j.cast h.symm)) (by simp [h]) :=
+  rfl
+
+@[simp] theorem swap!_mk (a : Array α) (h : a.size = n) (i j) :
+    (Vector.mk a h).swap! i j = Vector.mk (a.swap! i j) (by simp [h]) := rfl
+
+@[simp] theorem swapN_mk (a : Array α) (h : a.size = n) (i j) (hi : i < n) (hj : j < n) :
+    (Vector.mk a h).swapN i j = Vector.mk (a.swapN i j) (by simp [h]) := rfl
+
+@[simp] theorem swapAt_mk (a : Array α) (h : a.size = n) (i x) : (Vector.mk a h).swapAt i x =
+    ((a.swapAt (i.cast h.symm) x).fst, Vector.mk (a.swapAt (i.cast h.symm) x).snd (by simp [h])) :=
+  rfl
 
-@[simp] theorem pop_mk {data : Array α} {size : data.size = n} :
-    (Vector.mk data size).pop = Vector.mk data.pop (by simp [size]) := rfl
+@[simp] theorem swapAt!_mk (a : Array α) (h : a.size = n) (i x) : (Vector.mk a h).swapAt! i x =
+    ((a.swapAt! i x).fst, Vector.mk (a.swapAt! i x).snd (by simp [h])) := rfl
+
+@[simp] theorem swapAtN_mk (a : Array α) (h : a.size = n) (i x) (hi : i < n) :
+    (Vector.mk a h).swapAtN i x =
+      ((a.swapAtN i x).fst, Vector.mk (a.swapAtN i x).snd (by simp [h])) := rfl
+
+@[simp] theorem take_mk (a : Array α) (h : a.size = n) (m) :
+    (Vector.mk a h).take m = Vector.mk (a.take m) (by simp [h]) := rfl
+
+@[simp] theorem mk_zipWith_mk (f : α → β → γ) (a : Array α) (b : Array β)
+      (ha : a.size = n) (hb : b.size = n) : zipWith (Vector.mk a ha) (Vector.mk b hb) f =
+        Vector.mk (Array.zipWith a b f) (by simp [ha, hb]) := rfl
+
+@[simp] theorem getElem_toArray {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toArray.size) :
+    xs.toArray[i] = xs[i]'(by simpa using h) := by
+  cases xs; simp
+
+/-! ### toArray lemmas -/
+
+@[simp] theorem toArray_append (a : Vector α m) (b : Vector α n) :
+    (a ++ b).toArray = a.toArray ++ b.toArray := rfl
+
+@[simp] theorem toArray_drop (a : Vector α n) (m) :
+    (a.drop m).toArray = a.toArray.extract m a.size := rfl
+
+@[simp] theorem toArray_empty : (Vector.empty (α := α)).toArray = #[] := rfl
+
+@[simp] theorem toArray_mkEmpty (cap) :
+    (Vector.mkEmpty (α := α) cap).toArray = Array.mkEmpty cap := rfl
+
+@[simp] theorem toArray_eraseIdx! (a : Vector α n) (i) (hi : i < n) :
+    (a.eraseIdx! i).toArray = a.toArray.eraseIdx! i := by
+  cases a; simp [hi]
+
+@[simp] theorem toArray_eraseIdxN (a : Vector α n) (i) (hi : i < n) :
+    (a.eraseIdxN i).toArray = a.toArray.eraseIdxN i (by simp [hi]) := rfl
+
+@[simp] theorem toArray_feraseIdx (a : Vector α n) (i) :
+    (a.feraseIdx i).toArray = a.toArray.feraseIdx (i.cast a.size_toArray.symm) := rfl
+
+@[simp] theorem toArray_extract (a : Vector α n) (start stop) :
+    (a.extract start stop).toArray = a.toArray.extract start stop := rfl
+
+@[simp] theorem toArray_map (f : α → β) (a : Vector α n) :
+    (a.map f).toArray = a.toArray.map f := rfl
+
+@[simp] theorem toArray_ofFn (f : Fin n → α) : (Vector.ofFn f).toArray = Array.ofFn f := rfl
+
+@[simp] theorem toArray_pop (a : Vector α n) : a.pop.toArray = a.toArray.pop := rfl
+
+@[simp] theorem toArray_push (a : Vector α n) (x) : (a.push x).toArray = a.toArray.push x := rfl
+
+@[simp] theorem toArray_range : (Vector.range n).toArray = Array.range n := rfl
+
+@[simp] theorem toArray_reverse (a : Vector α n) : a.reverse.toArray = a.toArray.reverse := rfl
+
+@[simp] theorem toArray_set (a : Vector α n) (i x) :
+    (a.set i x).toArray = a.toArray.set (i.cast a.size_toArray.symm) x := rfl
+
+@[simp] theorem toArray_set! (a : Vector α n) (i x) :
+    (a.set! i x).toArray = a.toArray.set! i x := rfl
+
+@[simp] theorem toArray_setD (a : Vector α n) (i x) :
+    (a.setD i x).toArray = a.toArray.setD i x := rfl
+
+@[simp] theorem toArray_setN (a : Vector α n) (i x) (hi : i < n) :
+    (a.setN i x).toArray = a.toArray.setN i x (by simp [hi]) := rfl
+
+@[simp] theorem toArray_singleton (x : α) : (Vector.singleton x).toArray = #[x] := rfl
+
+@[simp] theorem toArray_swap (a : Vector α n) (i j) : (a.swap i j).toArray =
+    a.toArray.swap (i.cast a.size_toArray.symm) (j.cast a.size_toArray.symm) := rfl
+
+@[simp] theorem toArray_swap! (a : Vector α n) (i j) :
+    (a.swap! i j).toArray = a.toArray.swap! i j := rfl
+
+@[simp] theorem toArray_swapN (a : Vector α n) (i j) (hi : i < n) (hj : j < n) :
+    (a.swapN i j).toArray = a.toArray.swapN i j (by simp [hi]) (by simp [hj]) := rfl
+
+@[simp] theorem toArray_swapAt (a : Vector α n) (i x) :
+    ((a.swapAt i x).fst, (a.swapAt i x).snd.toArray) =
+      ((a.toArray.swapAt (i.cast a.size_toArray.symm) x).fst,
+        (a.toArray.swapAt (i.cast a.size_toArray.symm) x).snd) := rfl
+
+@[simp] theorem toArray_swapAt! (a : Vector α n) (i x) :
+    ((a.swapAt! i x).fst, (a.swapAt! i x).snd.toArray) =
+      ((a.toArray.swapAt! i x).fst, (a.toArray.swapAt! i x).snd) := rfl
+
+@[simp] theorem toArray_swapAtN (a : Vector α n) (i x) (hi : i < n) :
+    ((a.swapAtN i x).fst, (a.swapAtN i x).snd.toArray) =
+      ((a.toArray.swapAtN i x (by simp [hi])).fst,
+        (a.toArray.swapAtN i x (by simp [hi])).snd) := rfl
+
+@[simp] theorem toArray_take (a : Vector α n) (m) : (a.take m).toArray = a.toArray.take m := rfl
+
+@[simp] theorem toArray_zipWith (f : α → β → γ) (a : Vector α n) (b : Vector β n) :
+    (Vector.zipWith a b f).toArray = Array.zipWith a.toArray b.toArray f := rfl
+
+/-! ### toList lemmas -/
+
+theorem length_toList {α n} (xs : Vector α n) : xs.toList.length = n := by simp
+
+theorem getElem_toList {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toList.length) :
+    xs.toList[i] = xs[i]'(by simpa using h) := by simp
+
+/-! ### getElem lemmas -/
+
+@[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) :
+    (Vector.ofFn f)[i] = f ⟨i, by simpa using h⟩ := by
+  simp [ofFn]
 
 @[simp] theorem getElem_push_last {v : Vector α n} {x : α} : (v.push x)[n] = x := by
-  rcases v with ⟨data, rfl⟩
-  simp
+  rcases v with ⟨_, rfl⟩; simp
 
 -- The `simpNF` linter incorrectly claims that this lemma can not be applied by `simp`.
 @[simp, nolint simpNF] theorem getElem_push_lt {v : Vector α n} {x : α} {i : Nat} (h : i < n) :
     (v.push x)[i] = v[i] := by
-  rcases v with ⟨data, rfl⟩
-  simp [Array.getElem_push_lt, h]
+  rcases v with ⟨_, rfl⟩; simp [Array.getElem_push_lt, h]
 
 @[simp] theorem getElem_pop {v : Vector α n} {i : Nat} (h : i < n - 1) : (v.pop)[i] = v[i] := by
-  rcases v with ⟨data, rfl⟩
-  simp
+  rcases v with ⟨_, rfl⟩; simp
 
 /--
 Variant of `getElem_pop` that will sometimes fire when `getElem_pop` gets stuck because of
@@ -100,6 +254,15 @@ defeq issues in the implicit size argument.
     subst h
     simp [pop, back, back!, ← Array.eq_push_pop_back!_of_size_ne_zero]
 
+/-! ### empty lemmas -/
+
+@[simp] theorem map_empty (f : α → β) : map f empty = empty := by
+  apply toArray_injective; simp
+
+protected theorem eq_empty (v : Vector α 0) : v = empty := by
+  apply toArray_injective
+  apply Array.eq_empty_of_size_eq_zero v.2
+
 /-! ### Decidable quantifiers. -/
 
 theorem forall_zero_iff {P : Vector α 0 → Prop} :

From dc439388cc078925934b1c3e06276194280822d8 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 25 Nov 2024 11:26:02 +1100
Subject: [PATCH 14/31] fixes

---
 Batteries/Data/Vector/Lemmas.lean | 21 +++++++++------------
 1 file changed, 9 insertions(+), 12 deletions(-)

diff --git a/Batteries/Data/Vector/Lemmas.lean b/Batteries/Data/Vector/Lemmas.lean
index 9a14c4a548..81abd7a463 100644
--- a/Batteries/Data/Vector/Lemmas.lean
+++ b/Batteries/Data/Vector/Lemmas.lean
@@ -45,13 +45,13 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 @[simp] theorem drop_mk (a : Array α) (h : a.size = n) (m) :
     (Vector.mk a h).drop m = Vector.mk (a.extract m a.size) (by simp [h]) := rfl
 
+@[simp] theorem eraseIdx_mk (a : Array α) (h : a.size = n) (i) (h') :
+    (Vector.mk a h).eraseIdx i h' = Vector.mk (a.eraseIdx i) (by simp [h]) := rfl
+
 @[simp] theorem eraseIdx!_mk (a : Array α) (h : a.size = n) (i) (hi : i < n) :
-    (Vector.mk a h).eraseIdx! i = Vector.mk (a.eraseIdx! i) (by simp [h, hi]) := by
+    (Vector.mk a h).eraseIdx! i = Vector.mk (a.eraseIdx i) (by simp [h, hi]) := by
   simp [Vector.eraseIdx!, hi]
 
-@[simp] theorem feraseIdx_mk (a : Array α) (h : a.size = n) (i) :
-    (Vector.mk a h).feraseIdx i = Vector.mk (a.feraseIdx (i.cast h.symm)) (by simp [h]) := rfl
-
 @[simp] theorem extract_mk (a : Array α) (h : a.size = n) (start stop) :
     (Vector.mk a h).extract start stop = Vector.mk (a.extract start stop) (by simp [h]) := rfl
 
@@ -59,7 +59,7 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
     (Vector.mk a h)[i] = a[i] := rfl
 
 @[simp] theorem get_mk (a : Array α) (h : a.size = n) (i) :
-    (Vector.mk a h).get i = a.get (i.cast h.symm) := rfl
+    (Vector.mk a h).get i = a[i] := rfl
 
 @[simp] theorem getD_mk (a : Array α) (h : a.size = n) (i x) :
     (Vector.mk a h).getD i x = a.getD i x := rfl
@@ -146,15 +146,12 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 @[simp] theorem toArray_mkEmpty (cap) :
     (Vector.mkEmpty (α := α) cap).toArray = Array.mkEmpty cap := rfl
 
+@[simp] theorem toArray_eraseIdx (a : Vector α n) (i) (h) :
+    (a.eraseIdx i h).toArray = a.toArray.eraseIdx i (by simp [h]) := rfl
+
 @[simp] theorem toArray_eraseIdx! (a : Vector α n) (i) (hi : i < n) :
     (a.eraseIdx! i).toArray = a.toArray.eraseIdx! i := by
-  cases a; simp [hi]
-
-@[simp] theorem toArray_eraseIdxN (a : Vector α n) (i) (hi : i < n) :
-    (a.eraseIdxN i).toArray = a.toArray.eraseIdxN i (by simp [hi]) := rfl
-
-@[simp] theorem toArray_feraseIdx (a : Vector α n) (i) :
-    (a.feraseIdx i).toArray = a.toArray.feraseIdx (i.cast a.size_toArray.symm) := rfl
+  cases a; simp_all [Array.eraseIdx!]
 
 @[simp] theorem toArray_extract (a : Vector α n) (start stop) :
     (a.extract start stop).toArray = a.toArray.extract start stop := rfl

From 0681948d281fb8d3499952cd954be673c17e6e81 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 25 Nov 2024 19:46:05 +1100
Subject: [PATCH 15/31] rm upstreamed

---
 Batteries/Data/Array/Lemmas.lean | 8 --------
 1 file changed, 8 deletions(-)

diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
index 155d78889c..0b8ed1c745 100644
--- a/Batteries/Data/Array/Lemmas.lean
+++ b/Batteries/Data/Array/Lemmas.lean
@@ -25,14 +25,6 @@ theorem forIn_eq_forIn_toList [Monad m]
 @[deprecated (since := "2024-09-09")] alias data_zipWith := toList_zipWith
 @[deprecated (since := "2024-08-13")] alias zipWith_eq_zipWith_data := data_zipWith
 
-@[simp] theorem size_zipWith (as : Array α) (bs : Array β) (f : α → β → γ) :
-    (as.zipWith bs f).size = min as.size bs.size := by
-  rw [size_eq_length_toList, toList_zipWith, List.length_zipWith]
-
-@[simp] theorem size_zip (as : Array α) (bs : Array β) :
-    (as.zip bs).size = min as.size bs.size :=
-  as.size_zipWith bs Prod.mk
-
 /-! ### filter -/
 
 theorem size_filter_le (p : α → Bool) (l : Array α) :

From 332e0aa7f17c64a29dded0c373a7940600069e5b Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 25 Nov 2024 21:38:46 +1100
Subject: [PATCH 16/31] fix

---
 Batteries/Data/Vector/Lemmas.lean | 55 ++++++++++++++-----------------
 1 file changed, 25 insertions(+), 30 deletions(-)

diff --git a/Batteries/Data/Vector/Lemmas.lean b/Batteries/Data/Vector/Lemmas.lean
index 631daba419..335af56c0d 100644
--- a/Batteries/Data/Vector/Lemmas.lean
+++ b/Batteries/Data/Vector/Lemmas.lean
@@ -102,26 +102,24 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 
 @[deprecated (since := "2024-11-25")] alias setN_mk := set_mk
 
-@[simp] theorem swap_mk (a : Array α) (h : a.size = n) (i j) :
-    (Vector.mk a h).swap i j = Vector.mk (a.swap (i.cast h.symm) (j.cast h.symm)) (by simp [h]) :=
+@[simp] theorem swap_mk (a : Array α) (h : a.size = n) (i j) (hi hj) :
+    (Vector.mk a h).swap i j = Vector.mk (a.swap i j) (by simp [h]) :=
   rfl
 
-@[simp] theorem swap!_mk (a : Array α) (h : a.size = n) (i j) :
-    (Vector.mk a h).swap! i j = Vector.mk (a.swap! i j) (by simp [h]) := rfl
+@[simp] theorem swapIfInBounds_mk (a : Array α) (h : a.size = n) (i j) :
+    (Vector.mk a h).swapIfInBounds i j = Vector.mk (a.swapIfInBounds i j) (by simp [h]) := rfl
 
-@[simp] theorem swapN_mk (a : Array α) (h : a.size = n) (i j) (hi : i < n) (hj : j < n) :
-    (Vector.mk a h).swapN i j = Vector.mk (a.swapN i j) (by simp [h]) := rfl
+@[deprecated (since := "2024-11-25")] alias swapN_mk := swap_mk
 
-@[simp] theorem swapAt_mk (a : Array α) (h : a.size = n) (i x) : (Vector.mk a h).swapAt i x =
-    ((a.swapAt (i.cast h.symm) x).fst, Vector.mk (a.swapAt (i.cast h.symm) x).snd (by simp [h])) :=
+@[simp] theorem swapAt_mk (a : Array α) (h : a.size = n) (i x) (hi) :
+    (Vector.mk a h).swapAt i x =
+      ((a.swapAt i x).fst, Vector.mk (a.swapAt i x).snd (by simp [h])) :=
   rfl
 
 @[simp] theorem swapAt!_mk (a : Array α) (h : a.size = n) (i x) : (Vector.mk a h).swapAt! i x =
     ((a.swapAt! i x).fst, Vector.mk (a.swapAt! i x).snd (by simp [h])) := rfl
 
-@[simp] theorem swapAtN_mk (a : Array α) (h : a.size = n) (i x) (hi : i < n) :
-    (Vector.mk a h).swapAtN i x =
-      ((a.swapAtN i x).fst, Vector.mk (a.swapAtN i x).snd (by simp [h])) := rfl
+@[deprecated (since := "2024-11-25")] alias swapAtN_mk := swapAt_mk
 
 @[simp] theorem take_mk (a : Array α) (h : a.size = n) (m) :
     (Vector.mk a h).take m = Vector.mk (a.take m) (by simp [h]) := rfl
@@ -170,42 +168,39 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 
 @[simp] theorem toArray_reverse (a : Vector α n) : a.reverse.toArray = a.toArray.reverse := rfl
 
-@[simp] theorem toArray_set (a : Vector α n) (i x) :
-    (a.set i x).toArray = a.toArray.set (i.cast a.size_toArray.symm) x := rfl
+@[simp] theorem toArray_set (a : Vector α n) (i x h) :
+    (a.set i x).toArray = a.toArray.set i x (by simpa using h):= rfl
 
 @[simp] theorem toArray_set! (a : Vector α n) (i x) :
     (a.set! i x).toArray = a.toArray.set! i x := rfl
 
-@[simp] theorem toArray_setD (a : Vector α n) (i x) :
-    (a.setD i x).toArray = a.toArray.setD i x := rfl
+@[simp] theorem toArray_setIfInBounds (a : Vector α n) (i x) :
+    (a.setIfInBounds i x).toArray = a.toArray.setIfInBounds i x := rfl
 
-@[simp] theorem toArray_setN (a : Vector α n) (i x) (hi : i < n) :
-    (a.setN i x).toArray = a.toArray.setN i x (by simp [hi]) := rfl
+@[deprecated (since := "2024-11-25")] alias toArray_setD := toArray_setIfInBounds
+@[deprecated (since := "2024-11-25")] alias toArray_setN := toArray_set
 
 @[simp] theorem toArray_singleton (x : α) : (Vector.singleton x).toArray = #[x] := rfl
 
-@[simp] theorem toArray_swap (a : Vector α n) (i j) : (a.swap i j).toArray =
-    a.toArray.swap (i.cast a.size_toArray.symm) (j.cast a.size_toArray.symm) := rfl
+@[simp] theorem toArray_swap (a : Vector α n) (i j) (hi hj) : (a.swap i j).toArray =
+    a.toArray.swap i j (by simp [hi, hj]) (by simp [hi, hj]) := rfl
 
-@[simp] theorem toArray_swap! (a : Vector α n) (i j) :
-    (a.swap! i j).toArray = a.toArray.swap! i j := rfl
+@[simp] theorem toArray_swapIfInBounds (a : Vector α n) (i j) :
+    (a.swapIfInBounds i j).toArray = a.toArray.swapIfInBounds i j := rfl
 
-@[simp] theorem toArray_swapN (a : Vector α n) (i j) (hi : i < n) (hj : j < n) :
-    (a.swapN i j).toArray = a.toArray.swapN i j (by simp [hi]) (by simp [hj]) := rfl
+@[deprecated (since := "2024-11-25")] alias toArray_swap! := toArray_swapIfInBounds
+@[deprecated (since := "2024-11-25")] alias toArray_swapN := toArray_swap
 
-@[simp] theorem toArray_swapAt (a : Vector α n) (i x) :
+@[simp] theorem toArray_swapAt (a : Vector α n) (i x h) :
     ((a.swapAt i x).fst, (a.swapAt i x).snd.toArray) =
-      ((a.toArray.swapAt (i.cast a.size_toArray.symm) x).fst,
-        (a.toArray.swapAt (i.cast a.size_toArray.symm) x).snd) := rfl
+      ((a.toArray.swapAt i x (by simpa using h)).fst,
+        (a.toArray.swapAt i x (by simpa using h)).snd) := rfl
 
 @[simp] theorem toArray_swapAt! (a : Vector α n) (i x) :
     ((a.swapAt! i x).fst, (a.swapAt! i x).snd.toArray) =
       ((a.toArray.swapAt! i x).fst, (a.toArray.swapAt! i x).snd) := rfl
 
-@[simp] theorem toArray_swapAtN (a : Vector α n) (i x) (hi : i < n) :
-    ((a.swapAtN i x).fst, (a.swapAtN i x).snd.toArray) =
-      ((a.toArray.swapAtN i x (by simp [hi])).fst,
-        (a.toArray.swapAtN i x (by simp [hi])).snd) := rfl
+@[deprecated (since := "2024-11-25")] alias toArray_swapAtN := toArray_swapAt
 
 @[simp] theorem toArray_take (a : Vector α n) (m) : (a.take m).toArray = a.toArray.take m := rfl
 

From acd5685b2ae9bb177b418a6e33cab1c3015db2fd Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 25 Nov 2024 21:45:57 +1100
Subject: [PATCH 17/31] long line

---
 Batteries/Data/Vector/Lemmas.lean | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/Batteries/Data/Vector/Lemmas.lean b/Batteries/Data/Vector/Lemmas.lean
index 335af56c0d..9709bf4198 100644
--- a/Batteries/Data/Vector/Lemmas.lean
+++ b/Batteries/Data/Vector/Lemmas.lean
@@ -72,10 +72,11 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
   split <;> simp_all
 
 -- TODO: Restore once on `nightly-2024-11-26`.
--- @[simp] theorem mk_isEqv_mk (r : α → α → Bool) (a b : Array α) (ha : a.size = n) (hb : b.size = n) :
---     Vector.isEqv (Vector.mk a ha) (Vector.mk b hb) r = Array.isEqv a b r := by
---   simp [Vector.isEqv, Array.isEqv, ha, hb]
-
+/-
+@[simp] theorem mk_isEqv_mk (r : α → α → Bool) (a b : Array α) (ha : a.size = n) (hb : b.size = n) :
+    Vector.isEqv (Vector.mk a ha) (Vector.mk b hb) r = Array.isEqv a b r := by
+  simp [Vector.isEqv, Array.isEqv, ha, hb]
+-/
 @[simp] theorem mk_isPrefixOf_mk [BEq α] (a b : Array α) (ha : a.size = n) (hb : b.size = m) :
     (Vector.mk a ha).isPrefixOf (Vector.mk b hb) = a.isPrefixOf b := rfl
 

From 7488499a8aad6ffada87ab6db73673d88dc04c97 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= <fgdorais@gmail.com>
Date: Mon, 25 Nov 2024 20:45:41 -0500
Subject: [PATCH 18/31] feat: add KMP frontend for lists (#1065)

---
 Batteries/Data/List.lean         |  1 +
 Batteries/Data/List/Matcher.lean | 85 ++++++++++++++++++++++++++++++++
 BatteriesTest/kmp_matcher.lean   | 17 ++++++-
 3 files changed, 102 insertions(+), 1 deletion(-)
 create mode 100644 Batteries/Data/List/Matcher.lean

diff --git a/Batteries/Data/List.lean b/Batteries/Data/List.lean
index 3429039dc9..248240370a 100644
--- a/Batteries/Data/List.lean
+++ b/Batteries/Data/List.lean
@@ -3,6 +3,7 @@ import Batteries.Data.List.Count
 import Batteries.Data.List.EraseIdx
 import Batteries.Data.List.Init.Lemmas
 import Batteries.Data.List.Lemmas
+import Batteries.Data.List.Matcher
 import Batteries.Data.List.Monadic
 import Batteries.Data.List.OfFn
 import Batteries.Data.List.Pairwise
diff --git a/Batteries/Data/List/Matcher.lean b/Batteries/Data/List/Matcher.lean
new file mode 100644
index 0000000000..cc3b6db42f
--- /dev/null
+++ b/Batteries/Data/List/Matcher.lean
@@ -0,0 +1,85 @@
+/-
+Copyright (c) 2024 François G. Dorais. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: François G. Dorais
+-/
+import Batteries.Data.Array.Match
+import Batteries.Data.String.Basic
+
+namespace List
+
+/-- Knuth-Morris-Pratt matcher type
+
+This type is used to keep data for running the Knuth-Morris-Pratt (KMP) list matching algorithm.
+KMP is a linear time algorithm to locate all contiguous sublists of a list that match a given
+pattern. Generating the algorithm data is also linear in the length of the pattern but the data can
+be re-used to match the same pattern over multiple lists.
+
+The KMP data for a pattern can be generated using `Matcher.ofList`. Then `Matcher.find?` and
+`Matcher.findAll` can be used to run the algorithm on an input list.
+```
+def m := Matcher.ofList [0,1,1,0]
+
+#eval Option.isSome <| m.find? [2,1,1,0,1,1,2] -- false
+#eval Option.isSome <| m.find? [0,0,1,1,0,0] -- true
+
+#eval Array.size <| m.findAll [0,1,1,0,1,1,0] -- 2
+#eval Array.size <| m.findAll [0,1,1,0,1,1,0,1,1,0] -- 3
+```
+-/
+structure Matcher (α : Type _) extends Array.Matcher α where
+  /-- The pattern for the matcher -/
+  pattern : List α
+
+/-- Make KMP matcher from list pattern. -/
+@[inline] def Matcher.ofList [BEq α] (pattern : List α) : Matcher α where
+  toMatcher := Array.Matcher.ofStream pattern
+  pattern := pattern
+
+/-- List stream that keeps count of items read. -/
+local instance (α) : Stream (List α × Nat) α where
+  next?
+  | ([], _) => none
+  | (x::xs, n) => (x, xs, n+1)
+
+/--
+Find all start and end positions of all infix sublists of `l` matching `m.pattern`.
+The sublists may be overlapping.
+-/
+partial def Matcher.findAll [BEq α] (m : Matcher α) (l : List α) : Array (Nat × Nat) :=
+  loop (l, 0) m.toMatcher #[]
+where
+  /-- Accumulator loop for `List.Matcher.findAll` -/
+  loop (l : List α × Nat) (am : Array.Matcher α) (occs : Array (Nat × Nat)) : Array (Nat × Nat) :=
+    match am.next? l with
+    | none => occs
+    | some (l, am) => loop l am (occs.push (l.snd - m.table.size, l.snd))
+
+/--
+Find the start and end positions of the first infix sublist of `l` matching `m.pattern`,
+or `none` if there is no such sublist.
+-/
+def Matcher.find? [BEq α] (m : Matcher α) (l : List α) : Option (Nat × Nat) :=
+  match m.next? (l, 0) with
+  | none => none
+  | some (l, _) => some (l.snd - m.table.size, l.snd)
+
+/--
+Returns all the start and end positions of all infix sublists of of `l` that match `pattern`.
+The sublists may be overlapping.
+-/
+@[inline] def findAllInfix [BEq α] (l pattern : List α) : Array (Nat × Nat) :=
+  (Matcher.ofList pattern).findAll l
+
+/--
+Returns the start and end positions of the first infix sublist of `l` that matches `pattern`,
+or `none` if there is no such sublist.
+-/
+@[inline] def findInfix? [BEq α] (l pattern : List α) : Option (Nat × Nat) :=
+  (Matcher.ofList pattern).find? l
+
+/--
+Returns true iff `pattern` occurs as an infix sublist of `l`.
+-/
+@[inline] def containsInfix [BEq α] (l pattern : List α) : Bool :=
+  findInfix? l pattern |>.isSome
diff --git a/BatteriesTest/kmp_matcher.lean b/BatteriesTest/kmp_matcher.lean
index f61e42343f..c15a47befd 100644
--- a/BatteriesTest/kmp_matcher.lean
+++ b/BatteriesTest/kmp_matcher.lean
@@ -1,6 +1,9 @@
 import Batteries.Data.String.Matcher
+import Batteries.Data.List.Matcher
 
-/-! Tests for Knuth-Morris-Pratt matching algorithm -/
+/-! # Tests for the Knuth-Morris-Pratt (KMP) matching algorithm -/
+
+/-! ### String API -/
 
 /-- Matcher for pattern "abba" -/
 def m := String.Matcher.ofString "abba"
@@ -24,3 +27,15 @@ def m := String.Matcher.ofString "abba"
 #guard Array.size ("xyxyyxxyx".findAllSubstr "xyx") = 2
 
 #guard Array.size ("xyxyxyyxxyxyx".findAllSubstr "xyx") = 4
+
+/-! ### List API -/
+
+def lm := List.Matcher.ofList [0,1,1,0]
+
+#guard lm.find? [2,1,1,0,1,1,2] == none
+
+#guard lm.find? [0,0,1,1,0,0] == some (1, 5)
+
+#guard (lm.findAll [0,1,1,0,1,1,0]).size == 2
+
+#guard (lm.findAll [0,1,1,0,1,1,0,1,1,0]).size == 3

From f6d16c2a073e0385a362ad3e5d9e7e8260e298d6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= <fgdorais@gmail.com>
Date: Tue, 26 Nov 2024 01:07:46 -0500
Subject: [PATCH 19/31] refactor: add List.finRange and Array.finRange (#1055)

---
 Batteries/Data/Array/Basic.lean   |  3 ++
 Batteries/Data/Array/Lemmas.lean  | 18 +++++++++
 Batteries/Data/Fin.lean           |  1 +
 Batteries/Data/Fin/Basic.lean     | 11 ++++--
 Batteries/Data/Fin/Fold.lean      | 47 ++++++++++++++++++++++
 Batteries/Data/Fin/Lemmas.lean    | 65 -------------------------------
 Batteries/Data/List.lean          |  1 +
 Batteries/Data/List/Basic.lean    |  3 ++
 Batteries/Data/List/FinRange.lean | 60 ++++++++++++++++++++++++++++
 9 files changed, 140 insertions(+), 69 deletions(-)
 create mode 100644 Batteries/Data/Fin/Fold.lean
 create mode 100644 Batteries/Data/List/FinRange.lean

diff --git a/Batteries/Data/Array/Basic.lean b/Batteries/Data/Array/Basic.lean
index 403c42d9e2..3f05693926 100644
--- a/Batteries/Data/Array/Basic.lean
+++ b/Batteries/Data/Array/Basic.lean
@@ -175,6 +175,9 @@ def eraseIdx! (a : Array α) (i : Nat) : Array α :=
     have : Inhabited (Array α) := ⟨a⟩
     panic! s!"index {i} out of bounds"
 
+/-- `finRange n` is the array of all elements of `Fin n` in order. -/
+protected def finRange (n : Nat) : Array (Fin n) := ofFn fun i => i
+
 end Array
 
 
diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
index 8a5544089d..7022ef1cc2 100644
--- a/Batteries/Data/Array/Lemmas.lean
+++ b/Batteries/Data/Array/Lemmas.lean
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Gabriel Ebner
 -/
 import Batteries.Data.List.Lemmas
+import Batteries.Data.List.FinRange
 import Batteries.Data.Array.Basic
 import Batteries.Tactic.SeqFocus
 import Batteries.Util.ProofWanted
@@ -240,3 +241,20 @@ theorem getElem_insertAt_eq (as : Array α) (i : Fin (as.size+1)) (v : α)
   rw [get_insertAt_loop_eq, Fin.getElem_fin, getElem_push_eq]
   exact heq
   exact Nat.le_of_lt_succ i.is_lt
+
+/-! ### ofFn -/
+
+@[simp] theorem toList_ofFn (f : Fin n → α) : (ofFn f).toList = List.ofFn f := by
+  apply List.ext_getElem <;> simp
+
+/-! ### finRange -/
+
+@[simp] theorem size_finRange (n) : (Array.finRange n).size = n := by
+  simp [Array.finRange]
+
+@[simp] theorem getElem_finRange (n i) (h : i < (Array.finRange n).size) :
+    (Array.finRange n)[i] = ⟨i, size_finRange n ▸ h⟩ := by
+  simp [Array.finRange]
+
+@[simp] theorem toList_finRange (n) : (Array.finRange n).toList = List.finRange n := by
+  simp [Array.finRange, List.finRange]
diff --git a/Batteries/Data/Fin.lean b/Batteries/Data/Fin.lean
index 5fe5cc41ca..7a5b9c16e8 100644
--- a/Batteries/Data/Fin.lean
+++ b/Batteries/Data/Fin.lean
@@ -1,2 +1,3 @@
 import Batteries.Data.Fin.Basic
+import Batteries.Data.Fin.Fold
 import Batteries.Data.Fin.Lemmas
diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean
index b61481e33a..f1357f50b0 100644
--- a/Batteries/Data/Fin/Basic.lean
+++ b/Batteries/Data/Fin/Basic.lean
@@ -3,17 +3,20 @@ Copyright (c) 2017 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis, Keeley Hoek, Mario Carneiro
 -/
+import Batteries.Tactic.Alias
+import Batteries.Data.Array.Basic
+import Batteries.Data.List.Basic
 
 namespace Fin
 
 /-- `min n m` as an element of `Fin (m + 1)` -/
 def clamp (n m : Nat) : Fin (m + 1) := ⟨min n m, Nat.lt_succ_of_le (Nat.min_le_right ..)⟩
 
-/-- `enum n` is the array of all elements of `Fin n` in order -/
-def enum (n) : Array (Fin n) := Array.ofFn id
+@[deprecated (since := "2024-11-15")]
+alias enum := Array.finRange
 
-/-- `list n` is the list of all elements of `Fin n` in order -/
-def list (n) : List (Fin n) := (enum n).toList
+@[deprecated (since := "2024-11-15")]
+alias list := List.finRange
 
 /--
 Folds a monadic function over `Fin n` from left to right:
diff --git a/Batteries/Data/Fin/Fold.lean b/Batteries/Data/Fin/Fold.lean
new file mode 100644
index 0000000000..ed37c6b948
--- /dev/null
+++ b/Batteries/Data/Fin/Fold.lean
@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2024 François G. Dorais. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: François G. Dorais
+-/
+import Batteries.Data.List.FinRange
+
+namespace Fin
+
+theorem foldlM_eq_foldlM_finRange [Monad m] (f : α → Fin n → m α) (x) :
+    foldlM n f x = (List.finRange n).foldlM f x := by
+  induction n generalizing x with
+  | zero => simp
+  | succ n ih =>
+    rw [foldlM_succ, List.finRange_succ, List.foldlM_cons]
+    congr; funext
+    rw [List.foldlM_map, ih]
+
+@[deprecated (since := "2024-11-19")]
+alias foldlM_eq_foldlM_list := foldlM_eq_foldlM_finRange
+
+theorem foldrM_eq_foldrM_finRange [Monad m] [LawfulMonad m] (f : Fin n → α → m α) (x) :
+    foldrM n f x = (List.finRange n).foldrM f x := by
+  induction n with
+  | zero => simp
+  | succ n ih => rw [foldrM_succ, ih, List.finRange_succ, List.foldrM_cons, List.foldrM_map]
+
+@[deprecated (since := "2024-11-19")]
+alias foldrM_eq_foldrM_list := foldrM_eq_foldrM_finRange
+
+theorem foldl_eq_foldl_finRange (f : α → Fin n → α) (x) :
+    foldl n f x = (List.finRange n).foldl f x := by
+  induction n generalizing x with
+  | zero => rw [foldl_zero, List.finRange_zero, List.foldl_nil]
+  | succ n ih => rw [foldl_succ, ih, List.finRange_succ, List.foldl_cons, List.foldl_map]
+
+@[deprecated (since := "2024-11-19")]
+alias foldl_eq_foldl_list := foldl_eq_foldl_finRange
+
+theorem foldr_eq_foldr_finRange (f : Fin n → α → α) (x) :
+    foldr n f x = (List.finRange n).foldr f x := by
+  induction n with
+  | zero => rw [foldr_zero, List.finRange_zero, List.foldr_nil]
+  | succ n ih => rw [foldr_succ, ih, List.finRange_succ, List.foldr_cons, List.foldr_map]
+
+@[deprecated (since := "2024-11-19")]
+alias foldr_eq_foldr_list := foldr_eq_foldr_finRange
diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean
index 5010e1310f..90a574cf2c 100644
--- a/Batteries/Data/Fin/Lemmas.lean
+++ b/Batteries/Data/Fin/Lemmas.lean
@@ -14,46 +14,6 @@ attribute [norm_cast] val_last
 
 @[simp] theorem coe_clamp (n m : Nat) : (clamp n m : Nat) = min n m := rfl
 
-/-! ### enum/list -/
-
-@[simp] theorem size_enum (n) : (enum n).size = n := Array.size_ofFn ..
-
-@[simp] theorem enum_zero : (enum 0) = #[] := by simp [enum, Array.ofFn, Array.ofFn.go]
-
-@[simp] theorem getElem_enum (i) (h : i < (enum n).size) : (enum n)[i] = ⟨i, size_enum n ▸ h⟩ :=
-  Array.getElem_ofFn ..
-
-@[simp] theorem length_list (n) : (list n).length = n := by simp [list]
-
-@[simp] theorem getElem_list (i : Nat) (h : i < (list n).length) :
-    (list n)[i] = cast (length_list n) ⟨i, h⟩ := by
-  simp only [list]; rw [← Array.getElem_eq_getElem_toList, getElem_enum, cast_mk]
-
-@[deprecated getElem_list (since := "2024-06-12")]
-theorem get_list (i : Fin (list n).length) : (list n).get i = i.cast (length_list n) := by
-  simp [getElem_list]
-
-@[simp] theorem list_zero : list 0 = [] := by simp [list]
-
-theorem list_succ (n) : list (n+1) = 0 :: (list n).map Fin.succ := by
-  apply List.ext_get; simp; intro i; cases i <;> simp
-
-theorem list_succ_last (n) : list (n+1) = (list n).map castSucc ++ [last n] := by
-  rw [list_succ]
-  induction n with
-  | zero => simp
-  | succ n ih =>
-    rw [list_succ, List.map_cons castSucc, ih]
-    simp [Function.comp_def, succ_castSucc]
-
-theorem list_reverse (n) : (list n).reverse = (list n).map rev := by
-  induction n with
-  | zero => simp
-  | succ n ih =>
-    conv => lhs; rw [list_succ_last]
-    conv => rhs; rw [list_succ]
-    simp [← List.map_reverse, ih, Function.comp_def, rev_succ]
-
 /-! ### foldlM -/
 
 theorem foldlM_loop_lt [Monad m] (f : α → Fin n → m α) (x) (h : i < n) :
@@ -82,15 +42,6 @@ termination_by n - i
 theorem foldlM_succ [Monad m] (f : α → Fin (n+1) → m α) (x) :
     foldlM (n+1) f x = f x 0 >>= foldlM n (fun x j => f x j.succ) := foldlM_loop ..
 
-theorem foldlM_eq_foldlM_list [Monad m] (f : α → Fin n → m α) (x) :
-    foldlM n f x = (list n).foldlM f x := by
-  induction n generalizing x with
-  | zero => simp
-  | succ n ih =>
-    rw [foldlM_succ, list_succ, List.foldlM_cons]
-    congr; funext
-    rw [List.foldlM_map, ih]
-
 /-! ### foldrM -/
 
 theorem foldrM_loop_zero [Monad m] (f : Fin n → α → m α) (x) :
@@ -119,12 +70,6 @@ theorem foldrM_loop [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x
 theorem foldrM_succ [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x) :
     foldrM (n+1) f x = foldrM n (fun i => f i.succ) x >>= f 0 := foldrM_loop ..
 
-theorem foldrM_eq_foldrM_list [Monad m] [LawfulMonad m] (f : Fin n → α → m α) (x) :
-    foldrM n f x = (list n).foldrM f x := by
-  induction n with
-  | zero => simp
-  | succ n ih => rw [foldrM_succ, ih, list_succ, List.foldrM_cons, List.foldrM_map]
-
 /-! ### foldl -/
 
 theorem foldl_loop_lt (f : α → Fin n → α) (x) (h : i < n) :
@@ -162,11 +107,6 @@ theorem foldl_eq_foldlM (f : α → Fin n → α) (x) :
     foldl n f x = foldlM (m:=Id) n f x := by
   induction n generalizing x <;> simp [foldl_succ, foldlM_succ, *]
 
-theorem foldl_eq_foldl_list (f : α → Fin n → α) (x) : foldl n f x = (list n).foldl f x := by
-  induction n generalizing x with
-  | zero => rw [foldl_zero, list_zero, List.foldl_nil]
-  | succ n ih => rw [foldl_succ, ih, list_succ, List.foldl_cons, List.foldl_map]
-
 /-! ### foldr -/
 
 theorem foldr_loop_zero (f : Fin n → α → α) (x) :
@@ -198,11 +138,6 @@ theorem foldr_eq_foldrM (f : Fin n → α → α) (x) :
     foldr n f x = foldrM (m:=Id) n f x := by
   induction n <;> simp [foldr_succ, foldrM_succ, *]
 
-theorem foldr_eq_foldr_list (f : Fin n → α → α) (x) : foldr n f x = (list n).foldr f x := by
-  induction n with
-  | zero => rw [foldr_zero, list_zero, List.foldr_nil]
-  | succ n ih => rw [foldr_succ, ih, list_succ, List.foldr_cons, List.foldr_map]
-
 theorem foldl_rev (f : Fin n → α → α) (x) :
     foldl n (fun x i => f i.rev x) x = foldr n f x := by
   induction n generalizing x with
diff --git a/Batteries/Data/List.lean b/Batteries/Data/List.lean
index 248240370a..b4081d125e 100644
--- a/Batteries/Data/List.lean
+++ b/Batteries/Data/List.lean
@@ -1,6 +1,7 @@
 import Batteries.Data.List.Basic
 import Batteries.Data.List.Count
 import Batteries.Data.List.EraseIdx
+import Batteries.Data.List.FinRange
 import Batteries.Data.List.Init.Lemmas
 import Batteries.Data.List.Lemmas
 import Batteries.Data.List.Matcher
diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean
index 9c0ab14d46..7f3e66e1a6 100644
--- a/Batteries/Data/List/Basic.lean
+++ b/Batteries/Data/List/Basic.lean
@@ -1064,3 +1064,6 @@ where
   loop : List α → List α → List α
   | [], r => reverseAux (a :: r) [] -- Note: `reverseAux` is tail recursive.
   | b :: l, r => bif p b then reverseAux (a :: r) (b :: l) else loop l (b :: r)
+
+/-- `finRange n` lists all elements of `Fin n` in order -/
+def finRange (n : Nat) : List (Fin n) := ofFn fun i => i
diff --git a/Batteries/Data/List/FinRange.lean b/Batteries/Data/List/FinRange.lean
new file mode 100644
index 0000000000..432e3133af
--- /dev/null
+++ b/Batteries/Data/List/FinRange.lean
@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2024 François G. Dorais. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: François G. Dorais
+-/
+import Batteries.Data.List.OfFn
+
+namespace List
+
+@[simp] theorem length_finRange (n) : (List.finRange n).length = n := by
+  simp [List.finRange]
+
+@[deprecated (since := "2024-11-19")]
+alias length_list := length_finRange
+
+@[simp] theorem getElem_finRange (i : Nat) (h : i < (List.finRange n).length) :
+    (finRange n)[i] = Fin.cast (length_finRange n) ⟨i, h⟩ := by
+  simp [List.finRange]
+
+@[deprecated (since := "2024-11-19")]
+alias getElem_list := getElem_finRange
+
+@[simp] theorem finRange_zero : finRange 0 = [] := by simp [finRange, ofFn]
+
+@[deprecated (since := "2024-11-19")]
+alias list_zero := finRange_zero
+
+theorem finRange_succ (n) : finRange (n+1) = 0 :: (finRange n).map Fin.succ := by
+  apply List.ext_getElem; simp; intro i; cases i <;> simp
+
+@[deprecated (since := "2024-11-19")]
+alias list_succ := finRange_succ
+
+theorem finRange_succ_last (n) :
+    finRange (n+1) = (finRange n).map Fin.castSucc ++ [Fin.last n] := by
+  apply List.ext_getElem
+  · simp
+  · intros
+    simp only [List.finRange, List.getElem_ofFn, getElem_append, length_map, length_ofFn,
+      getElem_map, Fin.castSucc_mk, getElem_singleton]
+    split
+    · rfl
+    · next h => exact Fin.eq_last_of_not_lt h
+
+@[deprecated (since := "2024-11-19")]
+alias list_succ_last := finRange_succ_last
+
+theorem finRange_reverse (n) : (finRange n).reverse = (finRange n).map Fin.rev := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    conv => lhs; rw [finRange_succ_last]
+    conv => rhs; rw [finRange_succ]
+    rw [reverse_append, reverse_cons, reverse_nil, nil_append, singleton_append, ← map_reverse,
+      map_cons, ih, map_map, map_map]
+    congr; funext
+    simp [Fin.rev_succ]
+
+@[deprecated (since := "2024-11-19")]
+alias list_reverse := finRange_reverse

From 1bf9dbe6e8a6e247ce9e552d18779c86df606096 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 26 Nov 2024 17:21:26 +1100
Subject: [PATCH 20/31] fix

---
 Batteries/Data/Fin/Basic.lean  |  4 ++--
 Batteries/Data/Fin/Lemmas.lean | 33 ---------------------------------
 2 files changed, 2 insertions(+), 35 deletions(-)

diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean
index f741d02626..f63e38ab37 100644
--- a/Batteries/Data/Fin/Basic.lean
+++ b/Batteries/Data/Fin/Basic.lean
@@ -15,5 +15,5 @@ def clamp (n m : Nat) : Fin (m + 1) := ⟨min n m, Nat.lt_succ_of_le (Nat.min_le
 @[deprecated (since := "2024-11-15")]
 alias enum := Array.finRange
 
-/-- `list n` is the list of all elements of `Fin n` in order -/
-def list (n) : List (Fin n) := (enum n).toList
+@[deprecated (since := "2024-11-15")]
+alias list := List.finRange
diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean
index 8d228c178c..ddc7bbf1cf 100644
--- a/Batteries/Data/Fin/Lemmas.lean
+++ b/Batteries/Data/Fin/Lemmas.lean
@@ -13,36 +13,3 @@ attribute [norm_cast] val_last
 /-! ### clamp -/
 
 @[simp] theorem coe_clamp (n m : Nat) : (clamp n m : Nat) = min n m := rfl
-
-/-! ### foldlM -/
-
-theorem foldlM_eq_foldlM_list [Monad m] (f : α → Fin n → m α) (x) :
-    foldlM n f x = (list n).foldlM f x := by
-  induction n generalizing x with
-  | zero => simp
-  | succ n ih =>
-    rw [foldlM_succ, list_succ, List.foldlM_cons]
-    congr; funext
-    rw [List.foldlM_map, ih]
-
-/-! ### foldrM -/
-
-theorem foldrM_eq_foldrM_list [Monad m] [LawfulMonad m] (f : Fin n → α → m α) (x) :
-    foldrM n f x = (list n).foldrM f x := by
-  induction n with
-  | zero => simp
-  | succ n ih => rw [foldrM_succ, ih, list_succ, List.foldrM_cons, List.foldrM_map]
-
-/-! ### foldl -/
-
-theorem foldl_eq_foldl_list (f : α → Fin n → α) (x) : foldl n f x = (list n).foldl f x := by
-  induction n generalizing x with
-  | zero => rw [foldl_zero, list_zero, List.foldl_nil]
-  | succ n ih => rw [foldl_succ, ih, list_succ, List.foldl_cons, List.foldl_map]
-
-/-! ### foldr -/
-
-theorem foldr_eq_foldr_list (f : Fin n → α → α) (x) : foldr n f x = (list n).foldr f x := by
-  induction n with
-  | zero => rw [foldr_zero, list_zero, List.foldr_nil]
-  | succ n ih => rw [foldr_succ, ih, list_succ, List.foldr_cons, List.foldr_map]

From 00d092aa71e277015c11ef6bcc45d441018a642e Mon Sep 17 00:00:00 2001
From: leanprover-community-mathlib4-bot
 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Date: Tue, 26 Nov 2024 09:06:13 +0000
Subject: [PATCH 21/31] chore: bump to nightly-2024-11-26

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index 1e6741ae1e..ca6a40f05d 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-25
+leanprover/lean4:nightly-2024-11-26

From 29c662a03b65054c0f4d512b81e0ac253b049a3f Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 26 Nov 2024 21:12:48 +1100
Subject: [PATCH 22/31] Restore vector proofs

---
 Batteries/Data/Vector/Lemmas.lean | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/Batteries/Data/Vector/Lemmas.lean b/Batteries/Data/Vector/Lemmas.lean
index 9709bf4198..028f05532c 100644
--- a/Batteries/Data/Vector/Lemmas.lean
+++ b/Batteries/Data/Vector/Lemmas.lean
@@ -65,18 +65,13 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 @[simp] theorem uget_mk (a : Array α) (h : a.size = n) (i) (hi : i.toNat < n) :
     (Vector.mk a h).uget i hi = a.uget i (by simp [h, hi]) := rfl
 
--- TODO: Once on `nightly-2024-11-26`, this will be `rfl` again.
 @[simp] theorem indexOf?_mk [BEq α] (a : Array α) (h : a.size = n) (x : α) :
-    (Vector.mk a h).indexOf? x = (a.indexOf? x).map (Fin.cast h) := by
-  rw [Vector.indexOf?]
-  split <;> simp_all
+    (Vector.mk a h).indexOf? x = (a.indexOf? x).map (Fin.cast h) := rfl
 
--- TODO: Restore once on `nightly-2024-11-26`.
-/-
 @[simp] theorem mk_isEqv_mk (r : α → α → Bool) (a b : Array α) (ha : a.size = n) (hb : b.size = n) :
     Vector.isEqv (Vector.mk a ha) (Vector.mk b hb) r = Array.isEqv a b r := by
   simp [Vector.isEqv, Array.isEqv, ha, hb]
--/
+
 @[simp] theorem mk_isPrefixOf_mk [BEq α] (a b : Array α) (ha : a.size = n) (hb : b.size = m) :
     (Vector.mk a ha).isPrefixOf (Vector.mk b hb) = a.isPrefixOf b := rfl
 

From 3992cab30d93eaaf149f573a0f89c6e158786036 Mon Sep 17 00:00:00 2001
From: leanprover-community-mathlib4-bot
 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Date: Wed, 27 Nov 2024 09:06:17 +0000
Subject: [PATCH 23/31] chore: bump to nightly-2024-11-27

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index ca6a40f05d..5d639a03e3 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-26
+leanprover/lean4:nightly-2024-11-27

From c26f1a3cc2abf0ddd82bf3b56191c13403414615 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 27 Nov 2024 21:54:54 +1100
Subject: [PATCH 24/31] remove upstreamed

---
 Batteries/Data/Array/Basic.lean   |  3 ---
 Batteries/Data/Array/Lemmas.lean  |  5 -----
 Batteries/Data/List/Basic.lean    |  3 ---
 Batteries/Data/List/FinRange.lean | 34 -------------------------------
 4 files changed, 45 deletions(-)

diff --git a/Batteries/Data/Array/Basic.lean b/Batteries/Data/Array/Basic.lean
index 390003c6b4..9164b1219e 100644
--- a/Batteries/Data/Array/Basic.lean
+++ b/Batteries/Data/Array/Basic.lean
@@ -143,9 +143,6 @@ abbrev setN (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tac
 
 @[deprecated (since := "2024-11-20")] alias eraseIdxN := eraseIdx
 
-/-- `finRange n` is the array of all elements of `Fin n` in order. -/
-protected def finRange (n : Nat) : Array (Fin n) := ofFn fun i => i
-
 end Array
 
 
diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
index c8e13f7126..9bfa7c43d0 100644
--- a/Batteries/Data/Array/Lemmas.lean
+++ b/Batteries/Data/Array/Lemmas.lean
@@ -74,11 +74,6 @@ theorem size_set! (a : Array α) (i v) : (a.set! i v).size = a.size := by simp
 
 /-! ### map -/
 
-theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by
-  rw [mapM, mapM.map]; rfl
-
-theorem map_empty (f : α → β) : map f #[] = #[] := mapM_empty f
-
 /-! ### mem -/
 
 theorem mem_singleton : a ∈ #[b] ↔ a = b := by simp
diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean
index 9d21ec50df..e62ef1f3c2 100644
--- a/Batteries/Data/List/Basic.lean
+++ b/Batteries/Data/List/Basic.lean
@@ -1032,6 +1032,3 @@ where
   loop : List α → List α → List α
   | [], r => reverseAux (a :: r) [] -- Note: `reverseAux` is tail recursive.
   | b :: l, r => bif p b then reverseAux (a :: r) (b :: l) else loop l (b :: r)
-
-/-- `finRange n` lists all elements of `Fin n` in order -/
-def finRange (n : Nat) : List (Fin n) := ofFn fun i => i
diff --git a/Batteries/Data/List/FinRange.lean b/Batteries/Data/List/FinRange.lean
index 432e3133af..dd6b13724d 100644
--- a/Batteries/Data/List/FinRange.lean
+++ b/Batteries/Data/List/FinRange.lean
@@ -7,54 +7,20 @@ import Batteries.Data.List.OfFn
 
 namespace List
 
-@[simp] theorem length_finRange (n) : (List.finRange n).length = n := by
-  simp [List.finRange]
-
 @[deprecated (since := "2024-11-19")]
 alias length_list := length_finRange
 
-@[simp] theorem getElem_finRange (i : Nat) (h : i < (List.finRange n).length) :
-    (finRange n)[i] = Fin.cast (length_finRange n) ⟨i, h⟩ := by
-  simp [List.finRange]
-
 @[deprecated (since := "2024-11-19")]
 alias getElem_list := getElem_finRange
 
-@[simp] theorem finRange_zero : finRange 0 = [] := by simp [finRange, ofFn]
-
 @[deprecated (since := "2024-11-19")]
 alias list_zero := finRange_zero
 
-theorem finRange_succ (n) : finRange (n+1) = 0 :: (finRange n).map Fin.succ := by
-  apply List.ext_getElem; simp; intro i; cases i <;> simp
-
 @[deprecated (since := "2024-11-19")]
 alias list_succ := finRange_succ
 
-theorem finRange_succ_last (n) :
-    finRange (n+1) = (finRange n).map Fin.castSucc ++ [Fin.last n] := by
-  apply List.ext_getElem
-  · simp
-  · intros
-    simp only [List.finRange, List.getElem_ofFn, getElem_append, length_map, length_ofFn,
-      getElem_map, Fin.castSucc_mk, getElem_singleton]
-    split
-    · rfl
-    · next h => exact Fin.eq_last_of_not_lt h
-
 @[deprecated (since := "2024-11-19")]
 alias list_succ_last := finRange_succ_last
 
-theorem finRange_reverse (n) : (finRange n).reverse = (finRange n).map Fin.rev := by
-  induction n with
-  | zero => simp
-  | succ n ih =>
-    conv => lhs; rw [finRange_succ_last]
-    conv => rhs; rw [finRange_succ]
-    rw [reverse_append, reverse_cons, reverse_nil, nil_append, singleton_append, ← map_reverse,
-      map_cons, ih, map_map, map_map]
-    congr; funext
-    simp [Fin.rev_succ]
-
 @[deprecated (since := "2024-11-19")]
 alias list_reverse := finRange_reverse

From 0b7e415ddc73df96a3db8b39aca5fb2306d911e9 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 27 Nov 2024 21:56:43 +1100
Subject: [PATCH 25/31] deprecate Vector.empty

---
 Batteries/Data/Vector/Basic.lean  |  4 ++++
 Batteries/Data/Vector/Lemmas.lean | 14 +++++++-------
 2 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/Batteries/Data/Vector/Basic.lean b/Batteries/Data/Vector/Basic.lean
index 0978fadd28..475309e1bb 100644
--- a/Batteries/Data/Vector/Basic.lean
+++ b/Batteries/Data/Vector/Basic.lean
@@ -35,6 +35,10 @@ namespace Vector
 
 @[deprecated (since := "2024-11-20")] alias eraseIdxN := eraseIdx
 
+/-- Use `#v[]` instead. -/
+@[deprecated "Use `#v[]`." (since := "2024-11-27")]
+def empty (α : Type u) : Vector α 0 := #v[]
+
 /--
 Returns `true` when all elements of the vector are pairwise distinct using `==` for comparison.
 -/
diff --git a/Batteries/Data/Vector/Lemmas.lean b/Batteries/Data/Vector/Lemmas.lean
index 028f05532c..d94fd75a7f 100644
--- a/Batteries/Data/Vector/Lemmas.lean
+++ b/Batteries/Data/Vector/Lemmas.lean
@@ -136,7 +136,7 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 @[simp] theorem toArray_drop (a : Vector α n) (m) :
     (a.drop m).toArray = a.toArray.extract m a.size := rfl
 
-@[simp] theorem toArray_empty : (Vector.empty (α := α)).toArray = #[] := rfl
+@[simp] theorem toArray_empty : (#v[] : Vector α 0).toArray = #[] := rfl
 
 @[simp] theorem toArray_mkEmpty (cap) :
     (Vector.mkEmpty (α := α) cap).toArray = Array.mkEmpty cap := rfl
@@ -245,22 +245,22 @@ defeq issues in the implicit size argument.
 
 /-! ### empty lemmas -/
 
-@[simp] theorem map_empty (f : α → β) : map f empty = empty := by
+@[simp] theorem map_empty (f : α → β) : map f #v[] = #v[] := by
   apply toArray_injective; simp
 
-protected theorem eq_empty (v : Vector α 0) : v = empty := by
+protected theorem eq_empty (v : Vector α 0) : v = #v[] := by
   apply toArray_injective
   apply Array.eq_empty_of_size_eq_zero v.2
 
 /-! ### Decidable quantifiers. -/
 
 theorem forall_zero_iff {P : Vector α 0 → Prop} :
-    (∀ v, P v) ↔ P .empty := by
+    (∀ v, P v) ↔ P #v[] := by
   constructor
   · intro h
     apply h
   · intro h v
-    obtain (rfl : v = .empty) := (by ext i h; simp at h)
+    obtain (rfl : v = #v[]) := (by ext i h; simp at h)
     apply h
 
 theorem forall_cons_iff {P : Vector α (n + 1) → Prop} :
@@ -274,7 +274,7 @@ theorem forall_cons_iff {P : Vector α (n + 1) → Prop} :
     apply h
 
 instance instDecidableForallVectorZero (P : Vector α 0 → Prop) :
-    ∀ [Decidable (P .empty)], Decidable (∀ v, P v)
+    ∀ [Decidable (P #v[])], Decidable (∀ v, P v)
   | .isTrue h => .isTrue fun ⟨v, s⟩ => by
     obtain (rfl : v = .empty) := (by ext i h₁ h₂; exact s; cases h₂)
     exact h
@@ -284,7 +284,7 @@ instance instDecidableForallVectorSucc (P : Vector α (n+1) → Prop)
     [Decidable (∀ (x : α) (v : Vector α n), P (v.push x))] : Decidable (∀ v, P v) :=
   decidable_of_iff' (∀ x (v : Vector α n), P (v.push x)) forall_cons_iff
 
-instance instDecidableExistsVectorZero (P : Vector α 0 → Prop) [Decidable (P .empty)] :
+instance instDecidableExistsVectorZero (P : Vector α 0 → Prop) [Decidable (P #v[])] :
     Decidable (∃ v, P v) :=
   decidable_of_iff (¬ ∀ v, ¬ P v) Classical.not_forall_not
 

From 2076057d018822a2583e6238c157f684708d11ed Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 27 Nov 2024 22:01:53 +1100
Subject: [PATCH 26/31] fix tests

---
 BatteriesTest/alias.lean | 16 ++++++++--------
 BatteriesTest/array.lean |  6 +++---
 2 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/BatteriesTest/alias.lean b/BatteriesTest/alias.lean
index aa6fdfc720..4babc46b5e 100644
--- a/BatteriesTest/alias.lean
+++ b/BatteriesTest/alias.lean
@@ -11,16 +11,16 @@ theorem foo : 1 + 1 = 2 := rfl
 
 /-- doc string for `alias foo` -/
 alias foo1 := foo
-@[deprecated] alias foo2 := foo
-@[deprecated foo2] alias _root_.B.foo3 := foo
+@[deprecated (since := "2038-01-20")] alias foo2 := foo
+@[deprecated foo2 (since := "2038-01-20")] alias _root_.B.foo3 := foo
 @[deprecated foo2 "it was never a good idea anyway" (since := "last thursday")] alias foo4 := foo
 
 example : 1 + 1 = 2 := foo1
-/-- warning: `A.foo2` has been deprecated, use `A.foo` instead -/
+/-- warning: `A.foo2` has been deprecated: use `A.foo` instead -/
 #guard_msgs in example : 1 + 1 = 2 := foo2
-/-- warning: `B.foo3` has been deprecated, use `A.foo2` instead -/
+/-- warning: `B.foo3` has been deprecated: use `A.foo2` instead -/
 #guard_msgs in example : 1 + 1 = 2 := B.foo3
-/-- warning: it was never a good idea anyway -/
+/-- warning: `A.foo4` has been deprecated: it was never a good idea anyway -/
 #guard_msgs in example : 1 + 1 = 2 := foo4
 
 /-- doc string for bar -/
@@ -87,7 +87,7 @@ unsafe alias barbaz3 := id
 
 /- iff version -/
 
-@[deprecated] alias ⟨mpId, mprId⟩ := Iff.rfl
+@[deprecated (since := "2038-01-20")] alias ⟨mpId, mprId⟩ := Iff.rfl
 
 /-- info: A.mpId {a : Prop} : a → a -/
 #guard_msgs in #check mpId
@@ -95,9 +95,9 @@ unsafe alias barbaz3 := id
 #guard_msgs in #check mprId
 
 /--
-warning: `A.mpId` has been deprecated, use `Iff.rfl` instead
+warning: `A.mpId` has been deprecated: use `Iff.rfl` instead
 ---
-warning: `A.mprId` has been deprecated, use `Iff.rfl` instead
+warning: `A.mprId` has been deprecated: use `Iff.rfl` instead
 -/
 #guard_msgs in example := And.intro @mpId @mprId
 
diff --git a/BatteriesTest/array.lean b/BatteriesTest/array.lean
index 58bb65b713..e94478ddb6 100644
--- a/BatteriesTest/array.lean
+++ b/BatteriesTest/array.lean
@@ -10,13 +10,13 @@ variable (g : i < (a.set! i v).size)
 variable (j_lt : j < (a.set! i v).size)
 
 #check_simp (a.set! i v).get i g ~> v
-#check_simp (a.set! i v).get! i ~> (a.setD i v)[i]!
+#check_simp (a.set! i v).get! i ~> (a.setIfInBounds i v)[i]!
 #check_simp (a.set! i v).getD i d ~> if i < a.size then v else d
 #check_simp (a.set! i v)[i] ~> v
 
 -- Checks with different index values.
-#check_simp (a.set! i v)[j]'j_lt  ~> (a.setD i v)[j]'_
-#check_simp (a.setD i v)[j]'j_lt !~>
+#check_simp (a.set! i v)[j]'j_lt  ~> (a.setIfInBounds i v)[j]'_
+#check_simp (a.setIfInBounds i v)[j]'j_lt !~>
 
 -- This doesn't work currently.
 -- It will be address in the comprehensive overhaul of array lemmas.

From aab9422bc8bb6a07885b32ea283b17d6addeb933 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 27 Nov 2024 22:06:34 +1100
Subject: [PATCH 27/31] lint

---
 Batteries/Data/Vector/Lemmas.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Batteries/Data/Vector/Lemmas.lean b/Batteries/Data/Vector/Lemmas.lean
index d94fd75a7f..3cbcd854f2 100644
--- a/Batteries/Data/Vector/Lemmas.lean
+++ b/Batteries/Data/Vector/Lemmas.lean
@@ -245,8 +245,8 @@ defeq issues in the implicit size argument.
 
 /-! ### empty lemmas -/
 
-@[simp] theorem map_empty (f : α → β) : map f #v[] = #v[] := by
-  apply toArray_injective; simp
+theorem map_empty (f : α → β) : map f #v[] = #v[] := by
+  simp
 
 protected theorem eq_empty (v : Vector α 0) : v = #v[] := by
   apply toArray_injective

From c933dd9b00271d869e22b802a015092d1e8e454a Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 27 Nov 2024 22:33:25 +1100
Subject: [PATCH 28/31] feat: List.dropPrefix? / dropSuffix? / dropInfix? and
 specification lemmas (#1066)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: François G. Dorais <fgdorais@gmail.com>
---
 Batteries/Data/List/Basic.lean  |  32 +++++++
 Batteries/Data/List/Lemmas.lean | 145 ++++++++++++++++++++++++++++++++
 2 files changed, 177 insertions(+)

diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean
index 7f3e66e1a6..8dbcabb4a8 100644
--- a/Batteries/Data/List/Basic.lean
+++ b/Batteries/Data/List/Basic.lean
@@ -1065,5 +1065,37 @@ where
   | [], r => reverseAux (a :: r) [] -- Note: `reverseAux` is tail recursive.
   | b :: l, r => bif p b then reverseAux (a :: r) (b :: l) else loop l (b :: r)
 
+/-- `dropPrefix? l p` returns
+`some r` if `l = p' ++ r` for some `p'` which is paiwise `==` to `p`,
+and `none` otherwise. -/
+def dropPrefix? [BEq α] : List α → List α → Option (List α)
+  | list, [] => some list
+  | [], _ :: _ => none
+  | a :: as, b :: bs => if a == b then dropPrefix? as bs else none
+
+/-- `dropSuffix? l s` returns
+`some r` if `l = r ++ s'` for some `s'` which is paiwise `==` to `s`,
+and `none` otherwise. -/
+def dropSuffix? [BEq α] (l s : List α) : Option (List α) :=
+  let (r, s') := l.splitAt (l.length - s.length)
+  if s' == s then some r else none
+
+/-- `dropInfix? l i` returns
+`some (p, s)` if `l = p ++ i' ++ s` for some `i'` which is paiwise `==` to `i`,
+and `none` otherwise.
+
+Note that this is an inefficient implementation, and if computation time is a concern you should be
+using the Knuth-Morris-Pratt algorithm as implemented in `Batteries.Data.List.Matcher`.
+-/
+def dropInfix? [BEq α] (l i : List α) : Option (List α × List α) :=
+  go l []
+where
+  /-- Inner loop for `dropInfix?`. -/
+  go : List α → List α → Option (List α × List α)
+  | [], acc => if i.isEmpty then some (acc.reverse, []) else none
+  | a :: as, acc => match (a :: as).dropPrefix? i with
+    | none => go as (a :: acc)
+    | some s => (acc.reverse, s)
+
 /-- `finRange n` lists all elements of `Fin n` in order -/
 def finRange (n : Nat) : List (Fin n) := ofFn fun i => i
diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
index c8fba52299..840940dbaf 100644
--- a/Batteries/Data/List/Lemmas.lean
+++ b/Batteries/Data/List/Lemmas.lean
@@ -15,6 +15,26 @@ namespace List
 @[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) :
     (Array.mk xs)[i] = xs[i] := rfl
 
+/-! ### == -/
+
+@[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
+
+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 using length_eq_of_beq h.2
+
 /-! ### next? -/
 
 @[simp] theorem next?_nil : @next? α [] = none := rfl
@@ -508,6 +528,131 @@ theorem insertP_loop (a : α) (l r : List α) :
   induction l with simp [insertP, insertP.loop, cond]
   | cons _ _ ih => split <;> simp [insertP_loop, ih]
 
+/-! ### dropPrefix?, dropSuffix?, dropInfix?-/
+
+open Option
+
+@[simp] theorem dropPrefix?_nil [BEq α] {p : List α} : dropPrefix? p [] = some p := by
+  simp [dropPrefix?]
+
+theorem dropPrefix?_eq_some_iff [BEq α] {l p s : List α} :
+    dropPrefix? l p = some s ↔ ∃ p', l = p' ++ s ∧ p' == p := by
+  unfold dropPrefix?
+  split
+  · simp
+  · simp
+  · rename_i a as b bs
+    simp only [ite_none_right_eq_some]
+    constructor
+    · rw [dropPrefix?_eq_some_iff]
+      rintro ⟨w, p', rfl, h⟩
+      refine ⟨a :: p', by simp_all⟩
+    · rw [dropPrefix?_eq_some_iff]
+      rintro ⟨p, h, w⟩
+      rw [cons_eq_append_iff] at h
+      obtain (⟨rfl, rfl⟩ | ⟨a', rfl, rfl⟩) := h
+      · simp at w
+      · simp only [cons_beq_cons, Bool.and_eq_true] at w
+        refine ⟨w.1, a', rfl, w.2⟩
+
+theorem dropPrefix?_append_of_beq [BEq α] {l₁ l₂ : List α} (p : List α) (h : l₁ == l₂) :
+    dropPrefix? (l₁ ++ p) l₂ = some p := by
+  simp [dropPrefix?_eq_some_iff, h]
+
+theorem dropSuffix?_eq_some_iff [BEq α] {l p s : List α} :
+    dropSuffix? l s = some p ↔ ∃ s', l = p ++ s' ∧ s' == s := by
+  unfold dropSuffix?
+  rw [splitAt_eq]
+  simp only [ite_none_right_eq_some, some.injEq]
+  constructor
+  · rintro ⟨w, rfl⟩
+    refine ⟨_, by simp, w⟩
+  · rintro ⟨s', rfl, w⟩
+    simp [length_eq_of_beq w, w]
+
+@[simp] theorem dropSuffix?_nil [BEq α] {s : List α} : dropSuffix? s [] = some s := by
+  simp [dropSuffix?_eq_some_iff]
+
+theorem dropInfix?_go_eq_some_iff [BEq α] {i l acc p s : List α} :
+    dropInfix?.go i l acc = some (p, s) ↔ ∃ p',
+      p = acc.reverse ++ p' ∧
+      -- `i` is an infix up to `==`
+      (∃ i', l = p' ++ i' ++ s ∧ i' == i) ∧
+        -- and there is no shorter prefix for which that is the case
+        (∀ p'' i'' s'', l = p'' ++ i'' ++ s'' → i'' == i → p''.length ≥ p'.length) := by
+  unfold dropInfix?.go
+  split
+  · simp only [isEmpty_eq_true, ite_none_right_eq_some, some.injEq, Prod.mk.injEq, nil_eq,
+      append_assoc, append_eq_nil, ge_iff_le, and_imp]
+    constructor
+    · rintro ⟨rfl, rfl, rfl⟩
+      simp
+    · rintro ⟨p', rfl, ⟨_, ⟨rfl, rfl, rfl⟩, h⟩, w⟩
+      simp_all
+  · rename_i a t
+    split <;> rename_i h
+    · rw [dropInfix?_go_eq_some_iff]
+      constructor
+      · rintro ⟨p', rfl, ⟨i', rfl, h₂⟩, w⟩
+        refine ⟨a :: p', ?_⟩
+        simp [h₂]
+        intro p'' i'' s'' h₁ h₂
+        rw [cons_eq_append_iff] at h₁
+        obtain (⟨rfl, h₁⟩ | ⟨p'', rfl, h₁⟩) := h₁
+        · rw [append_assoc, ← h₁] at h
+          have := dropPrefix?_append_of_beq s'' h₂
+          simp_all
+        · simpa using w p'' i'' s'' (by simpa using h₁) h₂
+      · rintro ⟨p', rfl, ⟨i', h₁, h₂⟩, w⟩
+        rw [cons_eq_append_iff] at h₁
+        simp at h₁
+        obtain (⟨⟨rfl, rfl⟩, rfl⟩ | ⟨a', h₁, rfl⟩) := h₁
+        · simp only [nil_beq_iff, isEmpty_eq_true] at h₂
+          simp only [h₂] at h
+          simp at h
+        · rw [append_eq_cons_iff] at h₁
+          obtain (⟨rfl, rfl⟩ | ⟨p', rfl, rfl⟩) := h₁
+          · rw [← cons_append] at h
+            have := dropPrefix?_append_of_beq s h₂
+            simp_all
+          · refine ⟨p', ?_⟩
+            simp only [reverse_cons, append_assoc, singleton_append, append_cancel_left_eq,
+              append_cancel_right_eq, exists_eq_left', ge_iff_le, true_and]
+            refine ⟨h₂, ?_⟩
+            intro p'' i'' s'' h₃ h₄
+            rw [← append_assoc] at h₃
+            rw [h₃] at w
+            simpa using w (a :: p'') i'' s'' (by simp) h₄
+    · rename_i s'
+      simp only [some.injEq, Prod.mk.injEq, append_assoc, ge_iff_le]
+      rw [dropPrefix?_eq_some_iff] at h
+      obtain ⟨p', h, w⟩ := h
+      constructor
+      · rintro ⟨rfl, rfl⟩
+        simpa using ⟨p', by simp_all⟩
+      · rintro ⟨p'', rfl, ⟨i', h₁, h₂⟩, w'⟩
+        specialize w' [] p' s' (by simpa using h) w
+        simp at w'
+        simp [w'] at h₁ ⊢
+        rw [h] at h₁
+        apply append_inj_right h₁
+        replace w := length_eq_of_beq w
+        replace h₂ := length_eq_of_beq h₂
+        simp_all
+
+theorem dropInfix?_eq_some_iff [BEq α] {l i p s : List α} :
+    dropInfix? l i = some (p, s) ↔
+      -- `i` is an infix up to `==`
+      (∃ i', l = p ++ i' ++ s ∧ i' == i) ∧
+        -- and there is no shorter prefix for which that is the case
+        (∀ p' i' s', l = p' ++ i' ++ s' → i' == i → p'.length ≥ p.length) := by
+  unfold dropInfix?
+  rw [dropInfix?_go_eq_some_iff]
+  simp
+
+@[simp] theorem dropInfix?_nil [BEq α] {s : List α} : dropInfix? s [] = some ([], s) := by
+  simp [dropInfix?_eq_some_iff]
+
 /-! ### deprecations -/
 
 @[deprecated (since := "2024-08-15")] alias isEmpty_iff_eq_nil := isEmpty_iff

From 47a6de51b2013f894089d87d529b7e44627f4d88 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 28 Nov 2024 08:07:55 +1100
Subject: [PATCH 29/31] remove upstreamed

---
 Batteries/Data/List/Lemmas.lean | 20 --------------------
 1 file changed, 20 deletions(-)

diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
index 840940dbaf..1e02d90c98 100644
--- a/Batteries/Data/List/Lemmas.lean
+++ b/Batteries/Data/List/Lemmas.lean
@@ -15,26 +15,6 @@ namespace List
 @[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) :
     (Array.mk xs)[i] = xs[i] := rfl
 
-/-! ### == -/
-
-@[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
-
-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 using length_eq_of_beq h.2
-
 /-! ### next? -/
 
 @[simp] theorem next?_nil : @next? α [] = none := rfl

From a41867e14005bbb234f51ce6064d98b0c20701e5 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 28 Nov 2024 08:08:53 +1100
Subject: [PATCH 30/31] fix merge

---
 Batteries/Data/List/Basic.lean | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean
index e62ef1f3c2..1404315159 100644
--- a/Batteries/Data/List/Basic.lean
+++ b/Batteries/Data/List/Basic.lean
@@ -1032,3 +1032,35 @@ where
   loop : List α → List α → List α
   | [], r => reverseAux (a :: r) [] -- Note: `reverseAux` is tail recursive.
   | b :: l, r => bif p b then reverseAux (a :: r) (b :: l) else loop l (b :: r)
+
+/-- `dropPrefix? l p` returns
+`some r` if `l = p' ++ r` for some `p'` which is paiwise `==` to `p`,
+and `none` otherwise. -/
+def dropPrefix? [BEq α] : List α → List α → Option (List α)
+  | list, [] => some list
+  | [], _ :: _ => none
+  | a :: as, b :: bs => if a == b then dropPrefix? as bs else none
+
+/-- `dropSuffix? l s` returns
+`some r` if `l = r ++ s'` for some `s'` which is paiwise `==` to `s`,
+and `none` otherwise. -/
+def dropSuffix? [BEq α] (l s : List α) : Option (List α) :=
+  let (r, s') := l.splitAt (l.length - s.length)
+  if s' == s then some r else none
+
+/-- `dropInfix? l i` returns
+`some (p, s)` if `l = p ++ i' ++ s` for some `i'` which is paiwise `==` to `i`,
+and `none` otherwise.
+
+Note that this is an inefficient implementation, and if computation time is a concern you should be
+using the Knuth-Morris-Pratt algorithm as implemented in `Batteries.Data.List.Matcher`.
+-/
+def dropInfix? [BEq α] (l i : List α) : Option (List α × List α) :=
+  go l []
+where
+  /-- Inner loop for `dropInfix?`. -/
+  go : List α → List α → Option (List α × List α)
+  | [], acc => if i.isEmpty then some (acc.reverse, []) else none
+  | a :: as, acc => match (a :: as).dropPrefix? i with
+    | none => go as (a :: acc)
+    | some s => (acc.reverse, s)

From 030100b990ebf9ba1b15ad90a5bb9607d69e6564 Mon Sep 17 00:00:00 2001
From: leanprover-community-mathlib4-bot
 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Date: Thu, 28 Nov 2024 09:06:21 +0000
Subject: [PATCH 31/31] chore: bump to nightly-2024-11-28

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index 5d639a03e3..b899dceba8 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-27
+leanprover/lean4:nightly-2024-11-28