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
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..9bfa7c43d0 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
@@ -25,14 +26,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 α) :
@@ -81,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
@@ -150,13 +138,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..4795be8352 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
@@ -136,7 +136,7 @@ def insertExtractMax (self : BinaryHeap α lt) (x : α) : α × BinaryHeap α lt
   | none => (x, self)
   | some m =>
     if lt x m then
-      let v := self.vector.set ⟨0, size_pos_of_max e⟩ x
+      let v := self.vector.set 0 x (size_pos_of_max e)
       (m, ⟨heapifyDown lt v ⟨0, size_pos_of_max e⟩ |>.toArray⟩)
     else (x, self)
 
@@ -145,7 +145,7 @@ def replaceMax (self : BinaryHeap α lt) (x : α) : Option α × BinaryHeap α l
   match e : self.max with
   | none => (none, ⟨self.vector.push x |>.toArray⟩)
   | some m =>
-    let v := self.vector.set ⟨0, size_pos_of_max e⟩ x
+    let v := self.vector.set 0 x (size_pos_of_max e)
     (some m, ⟨heapifyDown lt v ⟨0, size_pos_of_max e⟩ |>.toArray⟩)
 
 /-- `O(log n)`. Replace the value at index `i` by `x`. Assumes that `x ≤ self.get i`. -/
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 346f3006e5..f63e38ab37 100644
--- a/Batteries/Data/Fin/Basic.lean
+++ b/Batteries/Data/Fin/Basic.lean
@@ -3,14 +3,17 @@ 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
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 d799e2e6f3..ddc7bbf1cf 100644
--- a/Batteries/Data/Fin/Lemmas.lean
+++ b/Batteries/Data/Fin/Lemmas.lean
@@ -13,76 +13,3 @@ attribute [norm_cast] val_last
 /-! ### clamp -/
 
 @[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_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]
diff --git a/Batteries/Data/List.lean b/Batteries/Data/List.lean
index 3429039dc9..b4081d125e 100644
--- a/Batteries/Data/List.lean
+++ b/Batteries/Data/List.lean
@@ -1,8 +1,10 @@
 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
 import Batteries.Data.List.Monadic
 import Batteries.Data.List.OfFn
 import Batteries.Data.List.Pairwise
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)
diff --git a/Batteries/Data/List/FinRange.lean b/Batteries/Data/List/FinRange.lean
new file mode 100644
index 0000000000..dd6b13724d
--- /dev/null
+++ b/Batteries/Data/List/FinRange.lean
@@ -0,0 +1,26 @@
+/-
+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
+
+@[deprecated (since := "2024-11-19")]
+alias length_list := length_finRange
+
+@[deprecated (since := "2024-11-19")]
+alias getElem_list := getElem_finRange
+
+@[deprecated (since := "2024-11-19")]
+alias list_zero := finRange_zero
+
+@[deprecated (since := "2024-11-19")]
+alias list_succ := finRange_succ
+
+@[deprecated (since := "2024-11-19")]
+alias list_succ_last := finRange_succ_last
+
+@[deprecated (since := "2024-11-19")]
+alias list_reverse := finRange_reverse
diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
index c8fba52299..1e02d90c98 100644
--- a/Batteries/Data/List/Lemmas.lean
+++ b/Batteries/Data/List/Lemmas.lean
@@ -508,6 +508,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
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/Batteries/Data/Vector/Basic.lean b/Batteries/Data/Vector/Basic.lean
index 315e8b932f..475309e1bb 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
@@ -16,287 +17,27 @@ import Batteries.Tactic.Lint.Misc
 `Vector α n` is a thin wrapper around `Array α` for arrays of fixed size `n`.
 -/
 
-namespace Batteries
-
-/-- `Vector α n` is an `Array α` with size `n`. -/
-structure Vector (α : Type u) (n : Nat) extends Array α where
-  /-- Array size. -/
-  size_toArray : toArray.size = n
-deriving Repr, DecidableEq
-
-attribute [simp] Vector.size_toArray
-
 namespace Vector
 
 @[deprecated (since := "2024-10-15")] alias size_eq := size_toArray
 
-/-- Syntax for `Vector α n` -/
-syntax "#v[" withoutPosition(sepBy(term, ", ")) "]" : term
-
-open Lean in
-macro_rules
-  | `(#v[ $elems,* ]) => `(Vector.mk (n := $(quote elems.getElems.size)) #[$elems,*] rfl)
-
-/-- Custom eliminator for `Vector α n` through `Array α` -/
-@[elab_as_elim]
-def elimAsArray {motive : Vector α n → Sort u}
-    (mk : ∀ (a : Array α) (ha : a.size = n), motive ⟨a, ha⟩) :
-    (v : Vector α n) → motive v
-  | ⟨a, ha⟩ => mk a ha
-
-/-- Custom eliminator for `Vector α n` through `List α` -/
-@[elab_as_elim]
-def elimAsList {motive : Vector α n → Sort u}
-    (mk : ∀ (a : List α) (ha : a.length = n), motive ⟨⟨a⟩, ha⟩) :
-    (v : Vector α n) → motive v
-  | ⟨⟨a⟩, ha⟩ => mk a ha
-
-/-- The empty vector. -/
-@[inline] def empty : Vector α 0 := ⟨.empty, rfl⟩
-
-/-- Make an empty vector with pre-allocated capacity. -/
-@[inline] def mkEmpty (capacity : Nat) : Vector α 0 := ⟨.mkEmpty capacity, rfl⟩
-
-/-- Makes a vector of size `n` with all cells containing `v`. -/
-@[inline] def mkVector (n) (v : α) : Vector α n := ⟨mkArray n v, by simp⟩
-
-/-- Returns a vector of size `1` with element `v`. -/
-@[inline] def singleton (v : α) : Vector α 1 := ⟨#[v], rfl⟩
-
-instance [Inhabited α] : Inhabited (Vector α n) where
-  default := mkVector n default
-
-/-- Get an element of a vector using a `Fin` index. -/
-@[inline] def get (v : Vector α n) (i : Fin n) : α :=
-  v.toArray[(i.cast v.size_toArray.symm).1]
-
-/-- Get an element of a vector using a `USize` index and a proof that the index is within bounds. -/
-@[inline] def uget (v : Vector α n) (i : USize) (h : i.toNat < n) : α :=
-  v.toArray.uget i (v.size_toArray.symm ▸ h)
-
-instance : GetElem (Vector α n) Nat α fun _ i => i < n where
-  getElem x i h := get x ⟨i, h⟩
-
-/--
-Get an element of a vector using a `Nat` index. Returns the given default value if the index is out
-of bounds.
--/
-@[inline] def getD (v : Vector α n) (i : Nat) (default : α) : α := v.toArray.getD i default
-
-/-- The last element of a vector. Panics if the vector is empty. -/
-@[inline] def back! [Inhabited α] (v : Vector α n) : α := v.toArray.back!
-
-/-- The last element of a vector, or `none` if the array is empty. -/
-@[inline] def back? (v : Vector α n) : Option α := v.toArray.back?
-
-/-- The last element of a non-empty vector. -/
-@[inline] def back [NeZero n] (v : Vector α n) : α :=
-  -- TODO: change to just `v[n]`
-  have : Inhabited α := ⟨v[0]'(Nat.pos_of_neZero n)⟩
-  v.back!
-
-/-- The first element of a non-empty vector.  -/
-@[inline] def head [NeZero n] (v : Vector α n) := v[0]'(Nat.pos_of_neZero n)
-
-/-- Push an element `x` to the end of a vector. -/
-@[inline] def push (x : α) (v : Vector α n)  : Vector α (n + 1) :=
-  ⟨v.toArray.push x, by simp⟩
+@[deprecated (since := "2024-11-25")] alias setN := set
 
-/-- Remove the last element of a vector. -/
-@[inline] def pop (v : Vector α n) : Vector α (n - 1) :=
-  ⟨Array.pop v.toArray, by simp⟩
-
-/--
-Set an element in a vector using a `Fin` index.
-
-This will perform the update destructively provided that the vector has a reference count of 1.
--/
-@[inline] def set (v : Vector α n) (i : Fin n) (x : α) : Vector α n :=
-  ⟨v.toArray.set (i.cast v.size_toArray.symm) x, by simp⟩
-
-/--
-Set an element in a vector using a `Nat` index. By default, the `get_elem_tactic` is used to
-synthesize a proof that the index is within bounds.
-
-This will perform the update destructively provided that the vector has a reference count of 1.
--/
-@[inline] def setN (v : Vector α n) (i : Nat) (x : α) (h : i < n := by get_elem_tactic) :
-    Vector α n := ⟨v.toArray.setN i x (by simp_all), by simp⟩
-
-/--
-Set an element in a vector using a `Nat` index. Returns the vector unchanged if the index is out of
-bounds.
-
-This will perform the update destructively provided that the vector has a reference count of 1.
--/
-@[inline] def setD (v : Vector α n) (i : Nat) (x : α) : Vector α n :=
-  ⟨v.toArray.setD i x, by simp⟩
-
-/--
-Set an element in a vector using a `Nat` index. Panics if the index is out of bounds.
-
-This will perform the update destructively provided that the vector has a reference count of 1.
--/
-@[inline] def set! (v : Vector α n) (i : Nat) (x : α) : Vector α n :=
-  ⟨v.toArray.set! i x, by simp⟩
-
-/-- Append two vectors. -/
-@[inline] def append (v : Vector α n) (w : Vector α m) : Vector α (n + m) :=
-  ⟨v.toArray ++ w.toArray, by simp⟩
-
-instance : HAppend (Vector α n) (Vector α m) (Vector α (n + m)) where
-  hAppend := append
-
-/-- Creates a vector from another with a provably equal length. -/
-@[inline] protected def cast (h : n = m) (v : Vector α n) : Vector α m :=
-  ⟨v.toArray, by simp [*]⟩
-
-/--
-Extracts the slice of a vector from indices `start` to `stop` (exclusive). If `start ≥ stop`, the
-result is empty. If `stop` is greater than the size of the vector, the size is used instead.
--/
-@[inline] def extract (v : Vector α n) (start stop : Nat) : Vector α (min stop n - start) :=
-  ⟨v.toArray.extract start stop, by simp⟩
+@[deprecated (since := "2024-11-25")] alias setD := setIfInBounds
 
-/-- Maps elements of a vector using the function `f`. -/
-@[inline] def map (f : α → β) (v : Vector α n) : Vector β n :=
-  ⟨v.toArray.map f, by simp⟩
+@[deprecated (since := "2024-11-24")] alias swapN := swap
 
-/-- Maps corresponding elements of two vectors of equal size using the function `f`. -/
-@[inline] def zipWith (a : Vector α n) (b : Vector β n) (f : α → β → φ) : Vector φ n :=
-  ⟨Array.zipWith a.toArray b.toArray f, by simp⟩
+@[deprecated (since := "2024-11-24")] alias swap! := swapIfInBounds
 
-/-- The vector of length `n` whose `i`-th element is `f i`. -/
-@[inline] def ofFn (f : Fin n → α) : Vector α n :=
-  ⟨Array.ofFn f, by simp⟩
-
-/--
-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)
-    (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⟩
-
-/--
-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⟩
-
-/--
-Swaps an element of a vector with a given value using a `Fin` index. 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 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) :
-    α × Vector α n :=
-  let a := v.toArray.swapAtN i x (by simp_all)
-  ⟨a.fst, a.snd, by simp [a]⟩
-
-/--
-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.
-
-This will perform the update destructively provided that the vector has a reference count of 1.
--/
-@[inline] def swapAt! (v : Vector α n) (i : Nat) (x : α) : α × Vector α n :=
-  let a := v.toArray.swapAt! i x
-  ⟨a.fst, a.snd, by simp [a]⟩
-
-/-- The vector `#v[0,1,2,...,n-1]`. -/
-@[inline] def range (n : Nat) : Vector Nat n := ⟨Array.range n, by simp⟩
-
-/--
-Extract the first `m` elements of a vector. If `m` is greater than or equal to the size of the
-vector then the vector is returned unchanged.
--/
-@[inline] def take (v : Vector α n) (m : Nat) : Vector α (min m n) :=
-  ⟨v.toArray.take m, by simp⟩
+@[deprecated (since := "2024-11-24")] alias swapAtN := swapAt
 
 @[deprecated (since := "2024-10-22")] alias shrink := take
 
-/--
-Deletes the first `m` elements of a vector. If `m` is greater than or equal to the size of the
-vector then the empty vector is returned.
--/
-@[inline] def drop (v : Vector α n) (m : Nat) : Vector α (n - m) :=
-  ⟨v.toArray.extract m v.size, by simp⟩
-
-/--
-Compares two vectors of the same size using a given boolean relation `r`. `isEqv v w r` returns
-`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)
-
-instance [BEq α] : BEq (Vector α n) where
-  beq a b := isEqv a b (· == ·)
-
-proof_wanted instLawfulBEq (α n) [BEq α] [LawfulBEq α] : LawfulBEq (Vector α n)
-
-/-- Reverse the elements of a vector. -/
-@[inline] def reverse (v : Vector α n) : Vector α n :=
-  ⟨v.toArray.reverse, by simp⟩
-
-/-- Delete an element of a vector using a `Nat` index and a tactic provided proof. -/
-@[inline] def eraseIdx (v : Vector α n) (i : Nat) (h : i < n := by get_elem_tactic) :
-    Vector α (n-1) :=
-  ⟨v.toArray.eraseIdx i (v.size_toArray.symm ▸ h), by simp [Array.size_eraseIdx]⟩
-
-/-- Delete an element of a vector using a `Nat` index. Panics if the index is out of bounds. -/
-@[inline] def eraseIdx! (v : Vector α n) (i : Nat) : Vector α (n-1) :=
-  if _ : i < n then
-    v.eraseIdx i
-  else
-    have : Inhabited (Vector α (n-1)) := ⟨v.pop⟩
-    panic! "index out of bounds"
-
-/-- Delete the first element of a vector. Returns the empty vector if the input vector is empty. -/
-@[inline] def tail (v : Vector α n) : Vector α (n-1) :=
-  if _ : 0 < n then
-    v.eraseIdx 0
-  else
-    v.cast (by omega)
-
 @[deprecated (since := "2024-11-20")] alias eraseIdxN := eraseIdx
 
-/--
-Finds the first index of a given value in a vector using `==` for comparison. Returns `none` if the
-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
-
-/-- Returns `true` when `v` is a prefix of the vector `w`. -/
-@[inline] def isPrefixOf [BEq α] (v : Vector α m) (w : Vector α n) : Bool :=
-  v.toArray.isPrefixOf w.toArray
+/-- 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 6271f39f02..3cbcd854f2 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,11 @@ 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 +24,208 @@ 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) (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
+  simp [Vector.eraseIdx!, hi]
+
+@[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[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
+
+@[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 w) :
+    (Vector.mk a h).set i x = Vector.mk (a.set i 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 setIfInBounds_mk (a : Array α) (h : a.size = n) (i x) :
+    (Vector.mk a h).setIfInBounds i x = Vector.mk (a.setIfInBounds i x) (by simp [h]) := rfl
+
+@[deprecated (since := "2024-11-25")] alias setN_mk := set_mk
+
+@[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 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
+
+@[deprecated (since := "2024-11-25")] alias swapN_mk := swap_mk
+
+@[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 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
+
+@[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
+
+@[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 : (#v[] : Vector α 0).toArray = #[] := rfl
+
+@[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_all [Array.eraseIdx!]
+
+@[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 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_setIfInBounds (a : Vector α n) (i x) :
+    (a.setIfInBounds i x).toArray = a.toArray.setIfInBounds i x := 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) (hi hj) : (a.swap i j).toArray =
+    a.toArray.swap i j (by simp [hi, hj]) (by simp [hi, hj]) := rfl
+
+@[simp] theorem toArray_swapIfInBounds (a : Vector α n) (i j) :
+    (a.swapIfInBounds i j).toArray = a.toArray.swapIfInBounds i j := 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 h) :
+    ((a.swapAt i x).fst, (a.swapAt i x).snd.toArray) =
+      ((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
+
+@[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
+
+@[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,15 +243,24 @@ defeq issues in the implicit size argument.
     subst h
     simp [pop, back, back!, ← Array.eq_push_pop_back!_of_size_ne_zero]
 
+/-! ### empty lemmas -/
+
+theorem map_empty (f : α → β) : map f #v[] = #v[] := by
+  simp
+
+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} :
@@ -122,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
@@ -132,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
 
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. -/
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.
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
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
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