diff --git a/.github/workflows/docs-release.yml b/.github/workflows/docs-release.yml
index 2926a31340..2c8a5c57f6 100644
--- a/.github/workflows/docs-release.yml
+++ b/.github/workflows/docs-release.yml
@@ -40,6 +40,8 @@ jobs:
       - name: Release Docs
         uses: softprops/action-gh-release@v2
         with:
+          prerelease: ${{ contains(github.ref, 'rc') }}
+          make_latest: ${{ !contains(github.ref, 'rc') }}
           files: |
             docs/docs-${{ github.ref_name }}.tar.gz
             docs/docs-${{ github.ref_name }}.zip
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.lean b/Batteries.lean
index 5db6bc2f6f..adc763d947 100644
--- a/Batteries.lean
+++ b/Batteries.lean
@@ -56,7 +56,6 @@ import Batteries.Lean.Meta.SavedState
 import Batteries.Lean.Meta.Simp
 import Batteries.Lean.Meta.UnusedNames
 import Batteries.Lean.MonadBacktrack
-import Batteries.Lean.NameMap
 import Batteries.Lean.NameMapAttribute
 import Batteries.Lean.PersistentHashMap
 import Batteries.Lean.PersistentHashSet
diff --git a/Batteries/Classes/SatisfiesM.lean b/Batteries/Classes/SatisfiesM.lean
index 834cbbea68..a89dad3dfd 100644
--- a/Batteries/Classes/SatisfiesM.lean
+++ b/Batteries/Classes/SatisfiesM.lean
@@ -185,14 +185,15 @@ theorem SatisfiesM_EStateM_eq :
       rw [EStateM.run_map, EStateM.run]
       split <;> simp_all
 
-@[simp] theorem SatisfiesM_ReaderT_eq [Monad m] :
+theorem SatisfiesM_ReaderT_eq [Monad m] :
     SatisfiesM (m := ReaderT ρ m) p x ↔ ∀ s, SatisfiesM p (x.run s) :=
   (exists_congr fun a => by exact ⟨fun eq _ => eq ▸ rfl, funext⟩).trans Classical.skolem.symm
 
 theorem SatisfiesM_StateRefT_eq [Monad m] :
-    SatisfiesM (m := StateRefT' ω σ m) p x ↔ ∀ s, SatisfiesM p (x s) := by simp [ReaderT.run]
+    SatisfiesM (m := StateRefT' ω σ m) p x ↔ ∀ s, SatisfiesM p (x s) := by
+  simp [SatisfiesM_ReaderT_eq, ReaderT.run]
 
-@[simp] theorem SatisfiesM_StateT_eq [Monad m] [LawfulMonad m] :
+theorem SatisfiesM_StateT_eq [Monad m] [LawfulMonad m] :
     SatisfiesM (m := StateT ρ m) (α := α) p x ↔ ∀ s, SatisfiesM (m := m) (p ·.1) (x.run s) := by
   change SatisfiesM (m := StateT ρ m) (α := α) p x ↔ ∀ s, SatisfiesM (m := m) (p ·.1) (x s)
   refine .trans ⟨fun ⟨f, eq⟩ => eq ▸ ?_, fun ⟨f, h⟩ => ?_⟩ Classical.skolem.symm
@@ -201,7 +202,7 @@ theorem SatisfiesM_StateRefT_eq [Monad m] :
   · refine ⟨fun s => (fun ⟨⟨a, s'⟩, h⟩ => ⟨⟨a, h⟩, s'⟩) <$> f s, funext fun s => ?_⟩
     show _ >>= _ = _; simp [← h]
 
-@[simp] theorem SatisfiesM_ExceptT_eq [Monad m] [LawfulMonad m] :
+theorem SatisfiesM_ExceptT_eq [Monad m] [LawfulMonad m] :
     SatisfiesM (m := ExceptT ρ m) (α := α) p x ↔
       SatisfiesM (m := m) (∀ a, · = .ok a → p a) x.run := by
   change _ ↔ SatisfiesM (m := m) (∀ a, · = .ok a → p a) x
@@ -247,9 +248,6 @@ instance : MonadSatisfying (Except ε) where
     | .error e => .error e
   val_eq {α p x?} h := by cases x? <;> simp
 
--- This will be redundant after nightly-2024-11-08.
-attribute [ext] ReaderT.ext
-
 instance [Monad m] [LawfulMonad m][MonadSatisfying m] : MonadSatisfying (ReaderT ρ m) where
   satisfying {α p x} h :=
     have h' := SatisfiesM_ReaderT_eq.mp h
@@ -263,9 +261,6 @@ instance [Monad m] [LawfulMonad m][MonadSatisfying m] : MonadSatisfying (ReaderT
 instance [Monad m] [LawfulMonad m] [MonadSatisfying m] : MonadSatisfying (StateRefT' ω σ m) :=
   inferInstanceAs <| MonadSatisfying (ReaderT _ _)
 
--- This will be redundant after nightly-2024-11-08.
-attribute [ext] StateT.ext
-
 instance [Monad m] [LawfulMonad m] [MonadSatisfying m] : MonadSatisfying (StateT ρ m) where
   satisfying {α p x} h :=
     have h' := SatisfiesM_StateT_eq.mp h
diff --git a/Batteries/Data/Array/Basic.lean b/Batteries/Data/Array/Basic.lean
index 403c42d9e2..9164b1219e 100644
--- a/Batteries/Data/Array/Basic.lean
+++ b/Batteries/Data/Array/Basic.lean
@@ -46,7 +46,7 @@ considered.
 protected def minD [ord : Ord α]
     (xs : Array α) (d : α) (start := 0) (stop := xs.size) : α :=
   if h: start < xs.size ∧ start < stop then
-    xs.minWith (xs.get ⟨start, h.left⟩) (start + 1) stop
+    xs.minWith xs[start] (start + 1) stop
   else
     d
 
@@ -60,7 +60,7 @@ considered.
 protected def min? [ord : Ord α]
     (xs : Array α) (start := 0) (stop := xs.size) : Option α :=
   if h : start < xs.size ∧ start < stop then
-    some $ xs.minD (xs.get ⟨start, h.left⟩) start stop
+    some $ xs.minD xs[start] start stop
   else
     none
 
@@ -135,45 +135,13 @@ A proof by `get_elem_tactic` is provided as a default argument for `h`.
 This will perform the update destructively provided that `a` has a reference count of 1 when called.
 -/
 abbrev setN (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) : Array α :=
-  a.set ⟨i, h⟩ x
+  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
 
-/--
-`eraseIdxN a i h` Removes the element at position `i` from a vector of length `n`.
-`h : i < a.size` has a default argument `by get_elem_tactic` which tries to supply a proof
-that the index is valid.
-This function takes worst case O(n) time because it has to backshift all elements at positions
-greater than i.
--/
-abbrev eraseIdxN (a : Array α) (i : Nat) (h : i < a.size := by get_elem_tactic) : Array α :=
-  a.feraseIdx ⟨i, h⟩
-
-/--
-Remove the element at a given index from an array, panics if index is out of bounds.
--/
-def eraseIdx! (a : Array α) (i : Nat) : Array α :=
-  if h : i < a.size then
-    a.feraseIdx ⟨i, h⟩
-  else
-    have : Inhabited (Array α) := ⟨a⟩
-    panic! s!"index {i} out of bounds"
+@[deprecated (since := "2024-11-20")] alias eraseIdxN := eraseIdx
 
 end Array
 
@@ -201,7 +169,7 @@ subarray, or `none` if the subarray is empty.
 def popHead? (as : Subarray α) : Option (α × Subarray α) :=
   if h : as.start < as.stop
     then
-      let head := as.array.get ⟨as.start, Nat.lt_of_lt_of_le h as.stop_le_array_size⟩
+      let head := as.array[as.start]'(Nat.lt_of_lt_of_le h as.stop_le_array_size)
       let tail :=
         { as with
           start := as.start + 1
diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
index 8a5544089d..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
@@ -22,65 +23,9 @@ theorem forIn_eq_forIn_toList [Monad m]
 
 /-! ### zipWith / zip -/
 
-theorem toList_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
-    (as.zipWith bs f).toList = as.toList.zipWith f bs.toList := by
-  let rec loop : ∀ (i : Nat) cs, i ≤ as.size → i ≤ bs.size →
-      (zipWithAux f as bs i cs).toList =
-        cs.toList ++ (as.toList.drop i).zipWith f (bs.toList.drop i) := by
-    intro i cs hia hib
-    unfold zipWithAux
-    by_cases h : i = as.size ∨ i = bs.size
-    case pos =>
-      have : ¬(i < as.size) ∨ ¬(i < bs.size) := by
-        cases h <;> simp_all only [Nat.not_lt, Nat.le_refl, true_or, or_true]
-      -- Cleaned up aesop output below
-      simp_all only [Nat.not_lt]
-      cases h <;> [(cases this); (cases this)]
-      · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length,
-                      List.zipWith_nil_left, List.append_nil]
-      · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length,
-                      List.zipWith_nil_left, List.append_nil]
-      · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length,
-                      List.zipWith_nil_right, List.append_nil]
-        split <;> simp_all only [Nat.not_lt]
-      · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length,
-                      List.zipWith_nil_right, List.append_nil]
-        split <;> simp_all only [Nat.not_lt]
-    case neg =>
-      rw [not_or] at h
-      have has : i < as.size := Nat.lt_of_le_of_ne hia h.1
-      have hbs : i < bs.size := Nat.lt_of_le_of_ne hib h.2
-      simp only [has, hbs, dite_true]
-      rw [loop (i+1) _ has hbs, Array.push_toList]
-      have h₁ : [f as[i] bs[i]] = List.zipWith f [as[i]] [bs[i]] := rfl
-      let i_as : Fin as.toList.length := ⟨i, has⟩
-      let i_bs : Fin bs.toList.length := ⟨i, hbs⟩
-      rw [h₁, List.append_assoc]
-      congr
-      rw [← List.zipWith_append (h := by simp), getElem_eq_getElem_toList,
-        getElem_eq_getElem_toList]
-      show List.zipWith f (as.toList[i_as] :: List.drop (i_as + 1) as.toList)
-        ((List.get bs.toList i_bs) :: List.drop (i_bs + 1) bs.toList) =
-        List.zipWith f (List.drop i as.toList) (List.drop i bs.toList)
-      simp only [length_toList, Fin.getElem_fin, List.getElem_cons_drop, List.get_eq_getElem]
-  simp [zipWith, loop 0 #[] (by simp) (by simp)]
 @[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]
-
-theorem toList_zip (as : Array α) (bs : Array β) :
-    (as.zip bs).toList = as.toList.zip bs.toList :=
-  toList_zipWith Prod.mk as bs
-@[deprecated (since := "2024-09-09")] alias data_zip := toList_zip
-@[deprecated (since := "2024-08-13")] alias zip_eq_zip_data := data_zip
-
-@[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 α) :
@@ -119,12 +64,9 @@ where
 @[simp] proof_wanted toList_erase [BEq α] {l : Array α} {a : α} :
     (l.erase a).toList = l.toList.erase a
 
-@[simp] theorem eraseIdx!_eq_eraseIdx (a : Array α) (i : Nat) :
-    a.eraseIdx! i = a.eraseIdx i := rfl
-
-@[simp] theorem size_eraseIdx (a : Array α) (i : Nat) :
-    (a.eraseIdx i).size = if i < a.size then a.size-1 else a.size := by
-  simp only [eraseIdx]; split; simp; rfl
+@[simp] theorem size_eraseIdxIfInBounds (a : Array α) (i : Nat) :
+    (a.eraseIdxIfInBounds i).size = if i < a.size then a.size-1 else a.size := by
+  simp only [eraseIdxIfInBounds]; split; simp; rfl
 
 /-! ### set -/
 
@@ -132,111 +74,143 @@ 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
 
-/-! ### append -/
-
-alias append_empty := append_nil
-
-alias empty_append := nil_append
-
 /-! ### insertAt -/
 
-private theorem size_insertAt_loop (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size) :
-    (insertAt.loop as i bs j).size = bs.size := by
-  unfold insertAt.loop
+@[simp] private theorem size_insertIdx_loop (as : Array α) (i : Nat) (j : Fin as.size) :
+    (insertIdx.loop i as j).size = as.size := by
+  unfold insertIdx.loop
   split
-  · rw [size_insertAt_loop, size_swap]
+  · rw [size_insertIdx_loop, size_swap]
   · rfl
 
-@[simp] theorem size_insertAt (as : Array α) (i : Fin (as.size+1)) (v : α) :
-    (as.insertAt i v).size = as.size + 1 := by
-  rw [insertAt, size_insertAt_loop, size_push]
-
-private theorem get_insertAt_loop_lt (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size)
-    (k) (hk : k < (insertAt.loop as i bs j).size) (h : k < i) :
-    (insertAt.loop as i bs j)[k] = bs[k]'(size_insertAt_loop .. ▸ hk) := by
-  unfold insertAt.loop
-  split
-  · have h1 : k ≠ j - 1 := by omega
-    have h2 : k ≠ j := by omega
-    rw [get_insertAt_loop_lt, getElem_swap, if_neg h1, if_neg h2]
-    exact h
+@[simp] theorem size_insertIdx (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) :
+    (as.insertIdx i v).size = as.size + 1 := by
+  rw [insertIdx, size_insertIdx_loop, size_push]
+
+@[deprecated size_insertIdx (since := "2024-11-20")] alias size_insertAt := size_insertIdx
+
+theorem getElem_insertIdx_loop_lt {as : Array α} {i : Nat} {j : Fin as.size} {k : Nat} {h}
+    (w : k < i) :
+    (insertIdx.loop i as j)[k] = as[k]'(by simpa using h) := by
+  unfold insertIdx.loop
+  split <;> rename_i h₁
+  · simp only
+    rw [getElem_insertIdx_loop_lt w]
+    rw [getElem_swap]
+    split <;> rename_i h₂
+    · simp_all
+      omega
+    · split <;> rename_i h₃
+      · omega
+      · simp_all
   · rfl
 
-private theorem get_insertAt_loop_gt (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size)
-    (k) (hk : k < (insertAt.loop as i bs j).size) (hgt : j < k) :
-    (insertAt.loop as i bs j)[k] = bs[k]'(size_insertAt_loop .. ▸ hk) := by
-  unfold insertAt.loop
-  split
-  · have h1 : k ≠ j - 1 := by omega
-    have h2 : k ≠ j := by omega
-    rw [get_insertAt_loop_gt, getElem_swap, if_neg h1, if_neg h2]
-    exact Nat.lt_of_le_of_lt (Nat.pred_le _) hgt
-  · rfl
-
-private theorem get_insertAt_loop_eq (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size)
-    (k) (hk : k < (insertAt.loop as i bs j).size) (heq : i = k) (h : i.val ≤ j.val) :
-    (insertAt.loop as i bs j)[k] = bs[j] := by
-  unfold insertAt.loop
-  split
-  · next h =>
-    rw [get_insertAt_loop_eq, Fin.getElem_fin, getElem_swap, if_pos rfl]
-    exact heq
-    exact Nat.le_pred_of_lt h
-  · congr; omega
-
-private theorem get_insertAt_loop_gt_le (as : Array α) (i : Fin (as.size+1)) (j : Fin bs.size)
-    (k) (hk : k < (insertAt.loop as i bs j).size) (hgt : i < k) (hle : k ≤ j) :
-    (insertAt.loop as i bs j)[k] = bs[k-1] := by
-  unfold insertAt.loop
-  split
-  · next h =>
-    if h0 : k = j then
-      cases h0
-      have h1 : j.val ≠ j - 1 := by omega
-      rw [get_insertAt_loop_gt, getElem_swap, if_neg h1, if_pos rfl]; rfl
-      exact Nat.pred_lt_of_lt hgt
-    else
-      have h1 : k - 1 ≠ j - 1 := by omega
-      have h2 : k - 1 ≠ j := by omega
-      rw [get_insertAt_loop_gt_le, getElem_swap, if_neg h1, if_neg h2]
-      apply Nat.le_of_lt_add_one
-      rw [Nat.sub_one_add_one]
-      exact Nat.lt_of_le_of_ne hle h0
-      exact Nat.not_eq_zero_of_lt h
-      exact hgt
-  · next h =>
-    absurd h
-    exact Nat.lt_of_lt_of_le hgt hle
-
-theorem getElem_insertAt_lt (as : Array α) (i : Fin (as.size+1)) (v : α)
-    (k) (hlt : k < i.val) {hk : k < (as.insertAt i v).size} {hk' : k < as.size} :
-    (as.insertAt i v)[k] = as[k] := by
-  simp only [insertAt]
-  rw [get_insertAt_loop_lt, getElem_push, dif_pos hk']
-  exact hlt
-
-theorem getElem_insertAt_gt (as : Array α) (i : Fin (as.size+1)) (v : α)
-    (k) (hgt : k > i.val) {hk : k < (as.insertAt i v).size} {hk' : k - 1 < as.size} :
-    (as.insertAt i v)[k] = as[k - 1] := by
-  simp only [insertAt]
-  rw [get_insertAt_loop_gt_le, getElem_push, dif_pos hk']
-  exact hgt
-  rw [size_insertAt] at hk
-  exact Nat.le_of_lt_succ hk
-
-theorem getElem_insertAt_eq (as : Array α) (i : Fin (as.size+1)) (v : α)
-    (k) (heq : i.val = k) {hk : k < (as.insertAt i v).size} :
-    (as.insertAt i v)[k] = v := by
-  simp only [insertAt]
-  rw [get_insertAt_loop_eq, Fin.getElem_fin, getElem_push_eq]
-  exact heq
-  exact Nat.le_of_lt_succ i.is_lt
+theorem getElem_insertIdx_loop_eq {as : Array α} {i : Nat} {j : Nat} {hj : j < as.size} {h} :
+    (insertIdx.loop i as ⟨j, hj⟩)[i] = if i ≤ j then as[j] else as[i]'(by simpa using h) := by
+  unfold insertIdx.loop
+  split <;> rename_i h₁
+  · simp at h₁
+    have : j - 1 < j := by omega
+    rw [getElem_insertIdx_loop_eq]
+    rw [getElem_swap]
+    simp
+    split <;> rename_i h₂
+    · rw [if_pos (by omega)]
+    · omega
+  · simp at h₁
+    by_cases h' : i = j
+    · simp [h']
+    · have t : ¬ i ≤ j := by omega
+      simp [t]
+
+theorem getElem_insertIdx_loop_gt {as : Array α} {i : Nat} {j : Nat} {hj : j < as.size}
+    {k : Nat} {h} (w : i < k) :
+    (insertIdx.loop i as ⟨j, hj⟩)[k] =
+      if k ≤ j then as[k-1]'(by simp at h; omega) else as[k]'(by simpa using h) := by
+  unfold insertIdx.loop
+  split <;> rename_i h₁
+  · simp only
+    simp only at h₁
+    have : j - 1 < j := by omega
+    rw [getElem_insertIdx_loop_gt w]
+    rw [getElem_swap]
+    split <;> rename_i h₂
+    · rw [if_neg (by omega), if_neg (by omega)]
+      have t : k ≤ j := by omega
+      simp [t]
+    · rw [getElem_swap]
+      rw [if_neg (by omega)]
+      split <;> rename_i h₃
+      · simp [h₃]
+      · have t : ¬ k ≤ j := by omega
+        simp [t]
+  · simp only at h₁
+    have t : ¬ k ≤ j := by omega
+    simp [t]
+
+theorem getElem_insertIdx_loop {as : Array α} {i : Nat} {j : Nat} {hj : j < as.size} {k : Nat} {h} :
+    (insertIdx.loop i as ⟨j, hj⟩)[k] =
+      if h₁ : k < i then
+        as[k]'(by simpa using h)
+      else
+        if h₂ : k = i then
+          if i ≤ j then as[j] else as[i]'(by simpa [h₂] using h)
+        else
+          if k ≤ j then as[k-1]'(by simp at h; omega) else as[k]'(by simpa using h) := by
+  split <;> rename_i h₁
+  · rw [getElem_insertIdx_loop_lt h₁]
+  · split <;> rename_i h₂
+    · subst h₂
+      rw [getElem_insertIdx_loop_eq]
+    · rw [getElem_insertIdx_loop_gt (by omega)]
+
+theorem getElem_insertIdx (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α)
+    (k) (h' : k < (as.insertIdx i v).size) :
+    (as.insertIdx i v)[k] =
+      if h₁ : k < i then
+        as[k]'(by omega)
+      else
+        if h₂ : k = i then
+          v
+        else
+          as[k - 1]'(by simp at h'; omega) := by
+  unfold insertIdx
+  rw [getElem_insertIdx_loop]
+  simp only [size_insertIdx] at h'
+  replace h' : k ≤ as.size := by omega
+  simp only [getElem_push, h, ↓reduceIte, Nat.lt_irrefl, ↓reduceDIte, h', dite_eq_ite]
+  split <;> rename_i h₁
+  · rw [dif_pos (by omega)]
+  · split <;> rename_i h₂
+    · simp [h₂]
+    · split <;> rename_i h₃
+      · rfl
+      · omega
+
+theorem getElem_insertIdx_lt (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α)
+    (k) (h' : k < (as.insertIdx i v).size) (h : k < i) :
+    (as.insertIdx i v)[k] = as[k] := by
+  simp [getElem_insertIdx, h]
+
+@[deprecated getElem_insertIdx_lt (since := "2024-11-20")] alias getElem_insertAt_lt :=
+getElem_insertIdx_lt
+
+theorem getElem_insertIdx_eq (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) :
+    (as.insertIdx i v)[i]'(by simp; omega) = v := by
+  simp [getElem_insertIdx, h]
+
+@[deprecated getElem_insertIdx_eq (since := "2024-11-20")] alias getElem_insertAt_eq :=
+getElem_insertIdx_eq
+
+theorem getElem_insertIdx_gt (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α)
+    (k) (h' : k < (as.insertIdx i v).size) (h : i < k) :
+    (as.insertIdx i v)[k] = as[k-1]'(by simp at h'; omega) := by
+  rw [getElem_insertIdx]
+  rw [dif_neg (by omega), dif_neg (by omega)]
+
+@[deprecated getElem_insertIdx_gt (since := "2024-11-20")] alias getElem_insertAt_gt :=
+getElem_insertIdx_gt
diff --git a/Batteries/Data/Array/Merge.lean b/Batteries/Data/Array/Merge.lean
index 70034111ad..7f26fd0c3f 100644
--- a/Batteries/Data/Array/Merge.lean
+++ b/Batteries/Data/Array/Merge.lean
@@ -83,7 +83,7 @@ set_option linter.unusedVariables.funArgs false in
 `f ⋯ (f (f x₁ x₂) x₃) ⋯ xₙ`.
 -/
 def mergeAdjacentDups [eq : BEq α] (f : α → α → α) (xs : Array α) : Array α :=
-  if h : 0 < xs.size then go (mkEmpty xs.size) 1 (xs.get ⟨0, h⟩) else xs
+  if h : 0 < xs.size then go (mkEmpty xs.size) 1 xs[0] else xs
 where
   /-- Auxiliary definition for `mergeAdjacentDups`. -/
   go (acc : Array α) (i : Nat) (hd : α) :=
diff --git a/Batteries/Data/Array/Monadic.lean b/Batteries/Data/Array/Monadic.lean
index 934111e131..ba297a9f70 100644
--- a/Batteries/Data/Array/Monadic.lean
+++ b/Batteries/Data/Array/Monadic.lean
@@ -153,7 +153,7 @@ theorem SatisfiesM_mapIdxM [Monad m] [LawfulMonad m] (as : Array α) (f : Nat 
     (hs : ∀ i, motive i.1 → SatisfiesM (p i · ∧ motive (i + 1)) (f i as[i])) :
     SatisfiesM
       (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i])
-      (Array.mapIdxM as f) :=
+      (as.mapIdxM f) :=
   SatisfiesM_mapFinIdxM as (fun i => f i) motive h0 p hs
 
 theorem size_modifyM [Monad m] [LawfulMonad m] (a : Array α) (i : Nat) (f : α → m α) :
diff --git a/Batteries/Data/Array/OfFn.lean b/Batteries/Data/Array/OfFn.lean
index e02be7cba1..5233fd1f96 100644
--- a/Batteries/Data/Array/OfFn.lean
+++ b/Batteries/Data/Array/OfFn.lean
@@ -11,8 +11,4 @@ namespace Array
 
 /-! ### ofFn -/
 
-@[simp]
-theorem toList_ofFn (f : Fin n → α) : (ofFn f).toList = List.ofFn f := by
-  apply ext_getElem <;> simp
-
 end Array
diff --git a/Batteries/Data/Array/Pairwise.lean b/Batteries/Data/Array/Pairwise.lean
index 82ace9609f..498c070540 100644
--- a/Batteries/Data/Array/Pairwise.lean
+++ b/Batteries/Data/Array/Pairwise.lean
@@ -20,7 +20,7 @@ that `as` is strictly sorted and `as.Pairwise (· ≤ ·)` asserts that `as` is
 def Pairwise (R : α → α → Prop) (as : Array α) : Prop := as.toList.Pairwise R
 
 theorem pairwise_iff_get {as : Array α} : as.Pairwise R ↔
-    ∀ (i j : Fin as.size), i < j → R (as.get i) (as.get j) := by
+    ∀ (i j : Fin as.size), i < j → R (as.get i i.2) (as.get j j.2) := by
   unfold Pairwise; simp [List.pairwise_iff_get, getElem_fin_eq_getElem_toList]
 
 theorem pairwise_iff_getElem {as : Array α} : as.Pairwise R ↔
diff --git a/Batteries/Data/BinaryHeap.lean b/Batteries/Data/BinaryHeap.lean
index 29a273a9d0..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. -/
@@ -88,7 +88,7 @@ def size (self : BinaryHeap α lt) : Nat := self.1.size
 def vector (self : BinaryHeap α lt) : Vector α self.size := ⟨self.1, rfl⟩
 
 /-- `O(1)`. Get an element in the heap by index. -/
-def get (self : BinaryHeap α lt) (i : Fin self.size) : α := self.1.get i
+def get (self : BinaryHeap α lt) (i : Fin self.size) : α := self.1[i]'(i.2)
 
 /-- `O(log n)`. Insert an element into a `BinaryHeap`, preserving the max-heap property. -/
 def insert (self : BinaryHeap α lt) (x : α) : BinaryHeap α lt where
@@ -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/ByteArray.lean b/Batteries/Data/ByteArray.lean
index 6a95a241aa..86a495e2df 100644
--- a/Batteries/Data/ByteArray.lean
+++ b/Batteries/Data/ByteArray.lean
@@ -15,7 +15,7 @@ theorem getElem_eq_data_getElem (a : ByteArray) (h : i < a.size) : a[i] = a.data
 /-! ### uget/uset -/
 
 @[simp] theorem uset_eq_set (a : ByteArray) {i : USize} (h : i.toNat < a.size) (v : UInt8) :
-    a.uset i v h = a.set ⟨i.toNat, h⟩ v := rfl
+    a.uset i v h = a.set i.toNat v := rfl
 
 /-! ### empty -/
 
@@ -45,7 +45,7 @@ theorem get_push_lt (a : ByteArray) (x : UInt8) (i : Nat) (h : i < a.size) :
 /-! ### set -/
 
 @[simp] theorem data_set (a : ByteArray) (i : Fin a.size) (v : UInt8) :
-    (a.set i v).data = a.data.set i v := rfl
+    (a.set i v).data = a.data.set i v i.isLt := rfl
 @[deprecated (since := "2024-08-13")] alias set_data := data_set
 
 @[simp] theorem size_set (a : ByteArray) (i : Fin a.size) (v : UInt8) :
@@ -60,7 +60,7 @@ theorem get_set_ne (a : ByteArray) (i : Fin a.size) (v : UInt8) (hj : j < a.size
   Array.get_set_ne (h:=h) ..
 
 theorem set_set (a : ByteArray) (i : Fin a.size) (v v' : UInt8) :
-    (a.set i v).set ⟨i, by simp [i.2]⟩ v' = a.set i v' :=
+    (a.set i v).set i v' = a.set i v' :=
   ByteArray.ext <| Array.set_set ..
 
 /-! ### copySlice -/
@@ -132,7 +132,7 @@ def ofFn (f : Fin n → UInt8) : ByteArray where
   simp [get, Fin.cast]
 
 @[simp] theorem getElem_ofFn (f : Fin n → UInt8) (i) (h : i < (ofFn f).size) :
-    (ofFn f)[i] = f ⟨i, size_ofFn f ▸ h⟩ := get_ofFn ..
+    (ofFn f)[i] = f ⟨i, size_ofFn f ▸ h⟩ := get_ofFn f ⟨i, h⟩
 
 private def ofFnAux (f : Fin n → UInt8) : ByteArray := go 0 (mkEmpty n) where
   go (i : Nat) (acc : ByteArray) : ByteArray :=
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..800d7c7c87 100644
--- a/Batteries/Data/Fin/Basic.lean
+++ b/Batteries/Data/Fin/Basic.lean
@@ -1,70 +1,93 @@
 /-
 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
+Authors: Robert Y. Lewis, Keeley Hoek, Mario Carneiro, François G. Dorais, Quang Dao
 -/
+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:
+/-- Heterogeneous monadic fold over `Fin n` from right to left:
 ```
-Fin.foldlM n f x₀ = do
-  let x₁ ← f x₀ 0
-  let x₂ ← f x₁ 1
+Fin.foldrM n f xₙ = do
+  let xₙ₋₁ : α (n-1) ← f (n-1) xₙ
+  let xₙ₋₂ : α (n-2) ← f (n-2) xₙ₋₁
   ...
-  let xₙ ← f xₙ₋₁ (n-1)
-  pure xₙ
+  let x₀ : α 0 ← f 0 x₁
+  pure x₀
 ```
--/
-@[inline] def foldlM [Monad m] (n) (f : α → Fin n → m α) (init : α) : m α := loop init 0 where
+This is the dependent version of `Fin.foldrM`. -/
+@[inline] def dfoldrM [Monad m] (n : Nat) (α : Fin (n + 1) → Type _)
+    (f : ∀ (i : Fin n), α i.succ → m (α i.castSucc)) (init : α (last n)) : m (α 0) :=
+  loop n (Nat.lt_succ_self n) init where
   /--
-  Inner loop for `Fin.foldlM`.
+  Inner loop for `Fin.dfoldrM`.
   ```
-  Fin.foldlM.loop n f xᵢ i = do
-    let xᵢ₊₁ ← f xᵢ i
+  Fin.dfoldrM.loop n f i h xᵢ = do
+    let xᵢ₋₁ ← f (i-1) xᵢ
     ...
-    let xₙ ← f xₙ₋₁ (n-1)
-    pure xₙ
+    let x₁ ← f 1 x₂
+    let x₀ ← f 0 x₁
+    pure x₀
   ```
   -/
-  loop (x : α) (i : Nat) : m α := do
-    if h : i < n then f x ⟨i, h⟩ >>= (loop · (i+1)) else pure x
-  termination_by n - i
+  @[specialize] loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : m (α 0) :=
+    match i with
+    | i + 1 => (f ⟨i, Nat.lt_of_succ_lt_succ h⟩ x) >>= loop i (Nat.lt_of_succ_lt h)
+    | 0 => pure x
 
-/--
-Folds a monadic function over `Fin n` from right to left:
+/-- Heterogeneous fold over `Fin n` from the right: `foldr 3 f x = f 0 (f 1 (f 2 x))`, where
+`f 2 : α 3 → α 2`, `f 1 : α 2 → α 1`, etc.
+
+This is the dependent version of `Fin.foldr`. -/
+@[inline] def dfoldr (n : Nat) (α : Fin (n + 1) → Type _)
+    (f : ∀ (i : Fin n), α i.succ → α i.castSucc) (init : α (last n)) : α 0 :=
+  dfoldrM (m := Id) n α f init
+
+/-- Heterogeneous monadic fold over `Fin n` from left to right:
 ```
-Fin.foldrM n f xₙ = do
-  let xₙ₋₁ ← f (n-1) xₙ
-  let xₙ₋₂ ← f (n-2) xₙ₋₁
+Fin.foldlM n f x₀ = do
+  let x₁ : α 1 ← f 0 x₀
+  let x₂ : α 2 ← f 1 x₁
   ...
-  let x₀ ← f 0 x₁
-  pure x₀
+  let xₙ : α n ← f (n-1) xₙ₋₁
+  pure xₙ
 ```
--/
-@[inline] def foldrM [Monad m] (n) (f : Fin n → α → m α) (init : α) : m α :=
-  loop ⟨n, Nat.le_refl n⟩ init where
-  /--
-  Inner loop for `Fin.foldrM`.
-  ```
-  Fin.foldrM.loop n f i xᵢ = do
-    let xᵢ₋₁ ← f (i-1) xᵢ
+This is the dependent version of `Fin.foldlM`. -/
+@[inline] def dfoldlM [Monad m] (n : Nat) (α : Fin (n + 1) → Type _)
+    (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (init : α 0) : m (α (last n)) :=
+  loop 0 (Nat.zero_lt_succ n) init where
+  /-- Inner loop for `Fin.dfoldlM`.
+    ```
+  Fin.foldM.loop n α f i h xᵢ = do
+    let xᵢ₊₁ : α (i+1) ← f i xᵢ
     ...
-    let x₁ ← f 1 x₂
-    let x₀ ← f 0 x₁
-    pure x₀
+    let xₙ : α n ← f (n-1) xₙ₋₁
+    pure xₙ
   ```
   -/
-  loop : {i // i ≤ n} → α → m α
-  | ⟨0, _⟩, x => pure x
-  | ⟨i+1, h⟩, x => f ⟨i, h⟩ x >>= loop ⟨i, Nat.le_of_lt h⟩
+  @[semireducible, specialize] loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : m (α (last n)) :=
+    if h' : i < n then
+      (f ⟨i, h'⟩ x) >>= loop (i + 1) (Nat.succ_lt_succ h')
+    else
+      haveI : ⟨i, h⟩ = last n := by ext; simp; omega
+      _root_.cast (congrArg (fun i => m (α i)) this) (pure x)
+
+/-- Heterogeneous fold over `Fin n` from the left: `foldl 3 f x = f 0 (f 1 (f 2 x))`, where
+`f 0 : α 0 → α 1`, `f 1 : α 1 → α 2`, etc.
+
+This is the dependent version of `Fin.foldl`. -/
+@[inline] def dfoldl (n : Nat) (α : Fin (n + 1) → Type _)
+    (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (init : α 0) : α (last n) :=
+  dfoldlM (m := Id) n α f init
diff --git a/Batteries/Data/Fin/Fold.lean b/Batteries/Data/Fin/Fold.lean
new file mode 100644
index 0000000000..9d2d821c2f
--- /dev/null
+++ b/Batteries/Data/Fin/Fold.lean
@@ -0,0 +1,171 @@
+/-
+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, Quang Dao
+-/
+import Batteries.Data.List.FinRange
+import Batteries.Data.Fin.Basic
+
+namespace Fin
+
+/-! ### dfoldrM -/
+
+theorem dfoldrM_loop_zero [Monad m] (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (x) :
+    dfoldrM.loop n α f 0 h x = pure x := rfl
+
+theorem dfoldrM_loop_succ [Monad m] (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (x) :
+    dfoldrM.loop n α f (i+1) h x = f ⟨i, by omega⟩ x >>= dfoldrM.loop n α f i (by omega) := rfl
+
+theorem dfoldrM_loop [Monad m] [LawfulMonad m] (f : (i : Fin (n+1)) → α i.succ → m (α i.castSucc))
+    (x) : dfoldrM.loop (n+1) α f (i+1) h x =
+      dfoldrM.loop n (α ∘ succ) (f ·.succ) i (by omega) x >>= f 0 := by
+  induction i with
+  | zero =>
+    rw [dfoldrM_loop_zero, dfoldrM_loop_succ, pure_bind]
+    conv => rhs; rw [← bind_pure (f 0 x)]
+    rfl
+  | succ i ih =>
+    rw [dfoldrM_loop_succ, dfoldrM_loop_succ, bind_assoc]
+    congr; funext; exact ih ..
+
+@[simp] theorem dfoldrM_zero [Monad m] (f : (i : Fin 0) → α i.succ → m (α i.castSucc)) (x) :
+    dfoldrM 0 α f x = pure x := rfl
+
+theorem dfoldrM_succ [Monad m] [LawfulMonad m] (f : (i : Fin (n+1)) → α i.succ → m (α i.castSucc))
+    (x) : dfoldrM (n+1) α f x = dfoldrM n (α ∘ succ) (f ·.succ) x >>= f 0 := dfoldrM_loop ..
+
+theorem dfoldrM_eq_foldrM [Monad m] [LawfulMonad m] (f : (i : Fin n) → α → m α) (x) :
+    dfoldrM n (fun _ => α) f x = foldrM n f x := by
+  induction n with
+  | zero => simp only [dfoldrM_zero, foldrM_zero]
+  | succ n ih => simp only [dfoldrM_succ, foldrM_succ, Function.comp_def, ih]
+
+theorem dfoldr_eq_dfoldrM (f : (i : Fin n) → α i.succ → α i.castSucc) (x) :
+    dfoldr n α f x = dfoldrM (m:=Id) n α f x := rfl
+
+/-! ### dfoldr -/
+
+@[simp] theorem dfoldr_zero (f : (i : Fin 0) → α i.succ → α i.castSucc) (x) :
+    dfoldr 0 α f x = x := rfl
+
+theorem dfoldr_succ (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (x) :
+    dfoldr (n+1) α f x = f 0 (dfoldr n (α ∘ succ) (f ·.succ) x) := dfoldrM_succ ..
+
+theorem dfoldr_succ_last {n : Nat} {α : Fin (n+2) → Sort _}
+    (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (x : α (last (n+1))) :
+      dfoldr (n+1) α f x = dfoldr n (α ∘ castSucc) (f ·.castSucc) (f (last n) x) := by
+  induction n with
+  | zero => simp only [dfoldr_succ, dfoldr_zero, last, zero_eta]
+  | succ n ih => rw [dfoldr_succ, ih (α := α ∘ succ) (f ·.succ), dfoldr_succ]; congr
+
+theorem dfoldr_eq_foldr (f : (i : Fin n) → α → α) (x) :
+    dfoldr n (fun _ => α) f x = foldr n f x := by
+  induction n with
+  | zero => simp only [dfoldr_zero, foldr_zero]
+  | succ n ih => simp only [dfoldr_succ, foldr_succ, Function.comp_def, ih]
+
+/-! ### dfoldlM -/
+
+theorem dfoldlM_loop_lt [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (h : i < n) (x) :
+    dfoldlM.loop n α f i (Nat.lt_add_right 1 h) x =
+      (f ⟨i, h⟩ x) >>= (dfoldlM.loop n α f (i+1) (Nat.add_lt_add_right h 1)) := by
+  rw [dfoldlM.loop, dif_pos h]
+
+theorem dfoldlM_loop_eq [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (x) :
+    dfoldlM.loop n α f n (Nat.le_refl _) x = pure x := by
+  rw [dfoldlM.loop, dif_neg (Nat.lt_irrefl _), cast_eq]
+
+@[simp] theorem dfoldlM_zero [Monad m] (f : (i : Fin 0) → α i.castSucc → m (α i.succ)) (x) :
+    dfoldlM 0 α f x = pure x := rfl
+
+theorem dfoldlM_loop [Monad m] (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) (h : i < n+1)
+    (x) : dfoldlM.loop (n+1) α f i (Nat.lt_add_right 1 h) x =
+      f ⟨i, h⟩ x >>= (dfoldlM.loop n (α ∘ succ) (f ·.succ ·) i h .) := by
+  if h' : i < n then
+    rw [dfoldlM_loop_lt _ h _]
+    congr; funext
+    rw [dfoldlM_loop_lt _ h' _, dfoldlM_loop]; rfl
+  else
+    cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h')
+    rw [dfoldlM_loop_lt]
+    congr; funext
+    rw [dfoldlM_loop_eq, dfoldlM_loop_eq]
+
+theorem dfoldlM_succ [Monad m] (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) (x) :
+    dfoldlM (n+1) α f x = f 0 x >>= (dfoldlM n (α ∘ succ) (f ·.succ ·) .) :=
+  dfoldlM_loop ..
+
+theorem dfoldlM_eq_foldlM [Monad m] (f : (i : Fin n) → α → m α) (x : α) :
+    dfoldlM n (fun _ => α) f x = foldlM n (fun x i => f i x) x := by
+  induction n generalizing x with
+  | zero => simp only [dfoldlM_zero, foldlM_zero]
+  | succ n ih =>
+    simp only [dfoldlM_succ, foldlM_succ, Function.comp_apply, Function.comp_def]
+    congr; ext; simp only [ih]
+
+/-! ### dfoldl -/
+
+@[simp] theorem dfoldl_zero (f : (i : Fin 0) → α i.castSucc → α i.succ) (x) :
+    dfoldl 0 α f x = x := rfl
+
+theorem dfoldl_succ (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (x) :
+    dfoldl (n+1) α f x = dfoldl n (α ∘ succ) (f ·.succ ·) (f 0 x) := dfoldlM_succ ..
+
+theorem dfoldl_succ_last (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (x) :
+    dfoldl (n+1) α f x = f (last n) (dfoldl n (α ∘ castSucc) (f ·.castSucc ·) x) := by
+  rw [dfoldl_succ]
+  induction n with
+  | zero => simp [dfoldl_succ, last]
+  | succ n ih => rw [dfoldl_succ, @ih (α ∘ succ) (f ·.succ ·), dfoldl_succ]; congr
+
+theorem dfoldl_eq_dfoldlM (f : (i : Fin n) → α i.castSucc → α i.succ) (x) :
+    dfoldl n α f x = dfoldlM (m := Id) n α f x := rfl
+
+theorem dfoldl_eq_foldl (f : Fin n → α → α) (x : α) :
+    dfoldl n (fun _ => α) f x = foldl n (fun x i => f i x) x := by
+  induction n generalizing x with
+  | zero => simp only [dfoldl_zero, foldl_zero]
+  | succ n ih =>
+    simp only [dfoldl_succ, foldl_succ, Function.comp_apply, Function.comp_def]
+    congr; simp only [ih]
+
+/-! ### `Fin.fold{l/r}{M}` equals `List.fold{l/r}{M}` -/
+
+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..ddc7bbf1cf 100644
--- a/Batteries/Data/Fin/Lemmas.lean
+++ b/Batteries/Data/Fin/Lemmas.lean
@@ -13,204 +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_loop_lt [Monad m] (f : α → Fin n → m α) (x) (h : i < n) :
-    foldlM.loop n f x i = f x ⟨i, h⟩ >>= (foldlM.loop n f . (i+1)) := by
-  rw [foldlM.loop, dif_pos h]
-
-theorem foldlM_loop_eq [Monad m] (f : α → Fin n → m α) (x) : foldlM.loop n f x n = pure x := by
-  rw [foldlM.loop, dif_neg (Nat.lt_irrefl _)]
-
-theorem foldlM_loop [Monad m] (f : α → Fin (n+1) → m α) (x) (h : i < n+1) :
-    foldlM.loop (n+1) f x i = f x ⟨i, h⟩ >>= (foldlM.loop n (fun x j => f x j.succ) . i) := by
-  if h' : i < n then
-    rw [foldlM_loop_lt _ _ h]
-    congr; funext
-    rw [foldlM_loop_lt _ _ h', foldlM_loop]; rfl
-  else
-    cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h')
-    rw [foldlM_loop_lt]
-    congr; funext
-    rw [foldlM_loop_eq, foldlM_loop_eq]
-termination_by n - i
-
-@[simp] theorem foldlM_zero [Monad m] (f : α → Fin 0 → m α) (x) : foldlM 0 f x = pure x :=
-  foldlM_loop_eq ..
-
-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) :
-    foldrM.loop n f ⟨0, Nat.zero_le _⟩ x = pure x := by
-  rw [foldrM.loop]
-
-theorem foldrM_loop_succ [Monad m] (f : Fin n → α → m α) (x) (h : i < n) :
-    foldrM.loop n f ⟨i+1, h⟩ x = f ⟨i, h⟩ x >>= foldrM.loop n f ⟨i, Nat.le_of_lt h⟩ := by
-  rw [foldrM.loop]
-
-theorem foldrM_loop [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x) (h : i+1 ≤ n+1) :
-    foldrM.loop (n+1) f ⟨i+1, h⟩ x =
-      foldrM.loop n (fun j => f j.succ) ⟨i, Nat.le_of_succ_le_succ h⟩ x >>= f 0 := by
-  induction i generalizing x with
-  | zero =>
-    rw [foldrM_loop_zero, foldrM_loop_succ, pure_bind]
-    conv => rhs; rw [←bind_pure (f 0 x)]
-    congr; funext; exact foldrM_loop_zero ..
-  | succ i ih =>
-    rw [foldrM_loop_succ, foldrM_loop_succ, bind_assoc]
-    congr; funext; exact ih ..
-
-@[simp] theorem foldrM_zero [Monad m] (f : Fin 0 → α → m α) (x) : foldrM 0 f x = pure x :=
-  foldrM_loop_zero ..
-
-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) :
-    foldl.loop n f x i = foldl.loop n f (f x ⟨i, h⟩) (i+1) := by
-  rw [foldl.loop, dif_pos h]
-
-theorem foldl_loop_eq (f : α → Fin n → α) (x) : foldl.loop n f x n = x := by
-  rw [foldl.loop, dif_neg (Nat.lt_irrefl _)]
-
-theorem foldl_loop (f : α → Fin (n+1) → α) (x) (h : i < n+1) :
-    foldl.loop (n+1) f x i = foldl.loop n (fun x j => f x j.succ) (f x ⟨i, h⟩) i := by
-  if h' : i < n then
-    rw [foldl_loop_lt _ _ h]
-    rw [foldl_loop_lt _ _ h', foldl_loop]; rfl
-  else
-    cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h')
-    rw [foldl_loop_lt]
-    rw [foldl_loop_eq, foldl_loop_eq]
-
-@[simp] theorem foldl_zero (f : α → Fin 0 → α) (x) : foldl 0 f x = x :=
-  foldl_loop_eq ..
-
-theorem foldl_succ (f : α → Fin (n+1) → α) (x) :
-    foldl (n+1) f x = foldl n (fun x i => f x i.succ) (f x 0) :=
-  foldl_loop ..
-
-theorem foldl_succ_last (f : α → Fin (n+1) → α) (x) :
-    foldl (n+1) f x = f (foldl n (f · ·.castSucc) x) (last n) := by
-  rw [foldl_succ]
-  induction n generalizing x with
-  | zero => simp [foldl_succ, Fin.last]
-  | succ n ih => rw [foldl_succ, ih (f · ·.succ), foldl_succ]; simp [succ_castSucc]
-
-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) :
-    foldr.loop n f ⟨0, Nat.zero_le _⟩ x = x := by
-  rw [foldr.loop]
-
-theorem foldr_loop_succ (f : Fin n → α → α) (x) (h : i < n) :
-    foldr.loop n f ⟨i+1, h⟩ x = foldr.loop n f ⟨i, Nat.le_of_lt h⟩ (f ⟨i, h⟩ x) := by
-  rw [foldr.loop]
-
-theorem foldr_loop (f : Fin (n+1) → α → α) (x) (h : i+1 ≤ n+1) :
-    foldr.loop (n+1) f ⟨i+1, h⟩ x =
-      f 0 (foldr.loop n (fun j => f j.succ) ⟨i, Nat.le_of_succ_le_succ h⟩ x) := by
-  induction i generalizing x <;> simp [foldr_loop_zero, foldr_loop_succ, *]
-
-@[simp] theorem foldr_zero (f : Fin 0 → α → α) (x) : foldr 0 f x = x :=
-  foldr_loop_zero ..
-
-theorem foldr_succ (f : Fin (n+1) → α → α) (x) :
-    foldr (n+1) f x = f 0 (foldr n (fun i => f i.succ) x) := foldr_loop ..
-
-theorem foldr_succ_last (f : Fin (n+1) → α → α) (x) :
-    foldr (n+1) f x = foldr n (f ·.castSucc) (f (last n) x) := by
-  induction n generalizing x with
-  | zero => simp [foldr_succ, Fin.last]
-  | succ n ih => rw [foldr_succ, ih (f ·.succ), foldr_succ]; simp [succ_castSucc]
-
-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
-  | zero => simp
-  | succ n ih => rw [foldl_succ, foldr_succ_last, ← ih]; simp [rev_succ]
-
-theorem foldr_rev (f : α → Fin n → α) (x) :
-     foldr n (fun i x => f x i.rev) x = foldl n f x := by
-  induction n generalizing x with
-  | zero => simp
-  | succ n ih => rw [foldl_succ_last, foldr_succ, ← ih]; simp [rev_succ]
diff --git a/Batteries/Data/HashMap/Basic.lean b/Batteries/Data/HashMap/Basic.lean
index de029c4276..0d1b2b1fe1 100644
--- a/Batteries/Data/HashMap/Basic.lean
+++ b/Batteries/Data/HashMap/Basic.lean
@@ -40,7 +40,7 @@ Note: this is marked `noncomputable` because it is only intended for specificati
 noncomputable def size (data : Buckets α β) : Nat := (data.1.toList.map (·.toList.length)).sum
 
 @[simp] theorem update_size (self : Buckets α β) (i d h) :
-    (self.update i d h).1.size = self.1.size := Array.size_uset ..
+    (self.update i d h).1.size = self.1.size := Array.size_uset _ _ _ h
 
 /-- Map a function over the values in the map. -/
 @[specialize] def mapVal (f : α → β → γ) (self : Buckets α β) : Buckets α γ :=
@@ -143,11 +143,10 @@ where
   destroying `source` in the process. -/
   go (i : Nat) (source : Array (AssocList α β)) (target : Buckets α β) : Buckets α β :=
     if h : i < source.size then
-      let idx : Fin source.size := ⟨i, h⟩
-      let es := source.get idx
+      let es := source[i]
       -- We remove `es` from `source` to make sure we can reuse its memory cells
       -- when performing es.foldl
-      let source := source.set idx .nil
+      let source := source.set i .nil
       let target := es.foldl reinsertAux target
       go (i+1) source target
     else target
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 9c0ab14d46..1404315159 100644
--- a/Batteries/Data/List/Basic.lean
+++ b/Batteries/Data/List/Basic.lean
@@ -159,32 +159,8 @@ Split a list at every occurrence of a separator element. The separators are not
   | [x], acc => acc.toListAppend [f x]
   | x :: xs, acc => go xs (acc.push x)
 
-/--
-`insertIdx n a l` inserts `a` into the list `l` after the first `n` elements of `l`
-```
-insertIdx 2 1 [1, 2, 3, 4] = [1, 2, 1, 3, 4]
-```
--/
-def insertIdx (n : Nat) (a : α) : List α → List α :=
-  modifyTailIdx (cons a) n
-
 @[deprecated (since := "2024-10-21")] alias insertNth := insertIdx
 
-/-- Tail-recursive version of `insertIdx`. -/
-@[inline] def insertIdxTR (n : Nat) (a : α) (l : List α) : List α := go n l #[] where
-  /-- Auxiliary for `insertIdxTR`: `insertIdxTR.go a n l acc = acc.toList ++ insertIdx n a l`. -/
-  go : Nat → List α → Array α → List α
-  | 0, l, acc => acc.toListAppend (a :: l)
-  | _, [], acc => acc.toList
-  | n+1, a :: l, acc => go n l (acc.push a)
-
-theorem insertIdxTR_go_eq : ∀ n l, insertIdxTR.go a n l acc = acc.toList ++ insertIdx n a l
-  | 0, l | _+1, [] => by simp [insertIdxTR.go, insertIdx]
-  | n+1, a :: l => by simp [insertIdxTR.go, insertIdx, insertIdxTR_go_eq n l]
-
-@[csimp] theorem insertIdx_eq_insertIdxTR : @insertIdx = @insertIdxTR := by
-  funext α f n l; simp [insertIdxTR, insertIdxTR_go_eq]
-
 theorem headD_eq_head? (l) (a : α) : headD l a = (head? l).getD a := by cases l <;> rfl
 
 /--
@@ -487,7 +463,7 @@ theorem sections_eq_nil_of_isEmpty : ∀ {L}, L.any isEmpty → @sections α L =
   cases e : L.any isEmpty <;> simp [sections_eq_nil_of_isEmpty, *]
   clear e; induction L with | nil => rfl | cons l L IH => ?_
   simp [IH, sectionsTR.go]
-  rw [Array.foldl_eq_foldl_toList, Array.foldl_toList_eq_flatMap]; rfl
+  rw [← Array.foldl_toList, Array.foldl_toList_eq_flatMap]; rfl
   intros; apply Array.foldl_toList_eq_map
 
 /--
@@ -544,14 +520,6 @@ def sigmaTR {σ : α → Type _} (l₁ : List α) (l₂ : ∀ a, List (σ a)) :
   rw [Array.foldl_toList_eq_flatMap]; rfl
   intros; apply Array.foldl_toList_eq_map
 
-/--
-`ofFn f` with `f : fin n → α` returns the list whose ith element is `f i`
-```
-ofFn f = [f 0, f 1, ... , f (n - 1)]
-```
--/
-def ofFn {n} (f : Fin n → α) : List α := Fin.foldr n (f · :: ·) []
-
 /-- `ofFnNthVal f i` returns `some (f i)` if `i < n` and `none` otherwise. -/
 def ofFnNthVal {n} (f : Fin n → α) (i : Nat) : Option α :=
   if h : i < n then some (f ⟨i, h⟩) else none
@@ -1064,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/List/OfFn.lean b/Batteries/Data/List/OfFn.lean
index 93214cc99b..c66846e61a 100644
--- a/Batteries/Data/List/OfFn.lean
+++ b/Batteries/Data/List/OfFn.lean
@@ -12,38 +12,4 @@ import Batteries.Data.Fin.Lemmas
 
 namespace List
 
-@[simp]
-theorem length_ofFn (f : Fin n → α) : (ofFn f).length = n := by
-  simp only [ofFn]
-  induction n with
-  | zero => simp
-  | succ n ih => simp [Fin.foldr_succ, ih]
-
-@[simp]
-protected theorem getElem_ofFn (f : Fin n → α) (i : Nat) (h : i < (ofFn f).length) :
-    (ofFn f)[i] = f ⟨i, by simp_all⟩ := by
-  simp only [ofFn]
-  induction n generalizing i with
-  | zero => simp at h
-  | succ n ih =>
-    match i with
-    | 0 => simp [Fin.foldr_succ]
-    | i+1 =>
-      simp only [Fin.foldr_succ]
-      apply ih
-      simp_all
-
-@[simp]
-protected theorem getElem?_ofFn (f : Fin n → α) (i) : (ofFn f)[i]? = ofFnNthVal f i :=
-  if h : i < (ofFn f).length
-  then by
-    rw [getElem?_eq_getElem h, List.getElem_ofFn]
-    · simp only [length_ofFn] at h; simp [ofFnNthVal, h]
-  else by
-    rw [ofFnNthVal, dif_neg] <;>
-    simpa using h
-
-@[simp] theorem toArray_ofFn (f : Fin n → α) : (ofFn f).toArray = Array.ofFn f := by
-  ext <;> simp
-
 end List
diff --git a/Batteries/Data/MLList/Basic.lean b/Batteries/Data/MLList/Basic.lean
index 1ed6d7e256..1553f29061 100644
--- a/Batteries/Data/MLList/Basic.lean
+++ b/Batteries/Data/MLList/Basic.lean
@@ -174,7 +174,7 @@ def fixl [Monad m] {α β : Type u} (f : α → m (α × List β)) (s : α) : ML
 
 /-- Compute, inside the monad, whether a `MLList` is empty. -/
 def isEmpty [Monad m] (xs : MLList m α) : m (ULift Bool) :=
-  (ULift.up ∘ Option.isSome) <$> uncons xs
+  (ULift.up ∘ Option.isNone) <$> uncons xs
 
 /-- Convert a `List` to a `MLList`. -/
 def ofList : List α → MLList m α
@@ -334,7 +334,7 @@ partial def fin (n : Nat) : MLList m (Fin n) := go 0 where
 partial def ofArray {α : Type} (L : Array α) : MLList m α := go 0 where
   /-- Implementation of `MLList.ofArray`. -/
   go (i : Nat) : MLList m α :=
-    if h : i < L.size then cons (L.get ⟨i, h⟩) (thunk fun _ => go (i+1)) else nil
+    if h : i < L.size then cons L[i] (thunk fun _ => go (i+1)) else nil
 
 /-- Group the elements of a lazy list into chunks of a given size.
 If the lazy list is finite, the last chunk may be smaller (possibly even length 0). -/
diff --git a/Batteries/Data/Range/Lemmas.lean b/Batteries/Data/Range/Lemmas.lean
index a075e0b6b4..3fd893daa9 100644
--- a/Batteries/Data/Range/Lemmas.lean
+++ b/Batteries/Data/Range/Lemmas.lean
@@ -57,12 +57,15 @@ theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range)
   suffices ∀ H, forIn' [start:stop:step] init f = forIn (L.pmap Subtype.mk H) init f' from this _
   intro H; dsimp only [forIn', Range.forIn']
   if h : start < stop then
-    simp [numElems, Nat.not_le.2 h, L]; split
+    simp only [numElems, Nat.not_le.2 h, ↓reduceIte, L]; split
     · subst step
       suffices ∀ n H init,
           forIn'.loop start stop 0 f n start (Nat.le_refl _) init =
           forIn ((List.range' start n 0).pmap Subtype.mk H) init f' from this _ ..
-      intro n; induction n with (intro H init; unfold forIn'.loop; simp [*])
+      intro n; induction n with
+        (intro H init
+         unfold forIn'.loop
+         simp only [↓reduceDIte, Nat.add_zero, List.pmap, List.forIn_cons, List.forIn_nil, h])
       | succ n ih => simp [ih (List.forall_mem_cons.1 H).2]; rfl
     · next step0 =>
       have hstep := Nat.pos_of_ne_zero step0
@@ -84,10 +87,15 @@ theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range)
           have ih := ih _ _ (Nat.le_trans hle (Nat.le_add_right ..))
             (List.forall_mem_cons.1 H).2 (Nat.le_of_succ_le_succ h1) fun i => by
               rw [Nat.add_right_comm, Nat.add_assoc, ← Nat.mul_succ, h2, Nat.succ_le_succ_iff]
-          have := h2 0; simp at this
-          rw [forIn'.loop]; simp [this, ih]; rfl
+          have := h2 0
+          simp only [Nat.mul_zero, Nat.add_zero, Nat.le_zero_eq, Nat.add_one_ne_zero, iff_false,
+            Nat.not_le] at this
+          rw [forIn'.loop]
+          simp only [this, ↓reduceDIte, ih, List.pmap, List.forIn_cons]
+          rfl
   else
-    simp [List.range', h, numElems_stop_le_start ⟨start, stop, step⟩ (Nat.not_lt.1 h), L]
+    simp only [numElems_stop_le_start ⟨start, stop, step⟩ (Nat.not_lt.1 h), List.range'_zero,
+      List.pmap, List.forIn_nil, L]
     cases stop <;> unfold forIn'.loop <;> simp [List.forIn', h]
 
 theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
diff --git a/Batteries/Data/String/Lemmas.lean b/Batteries/Data/String/Lemmas.lean
index 431591ebc1..642029cdd1 100644
--- a/Batteries/Data/String/Lemmas.lean
+++ b/Batteries/Data/String/Lemmas.lean
@@ -573,7 +573,7 @@ theorem extract (h₁ : ValidFor l (m ++ r) it₁) (h₂ : ValidFor (m.reverse +
     it₁.extract it₂ = ⟨m⟩ := by
   cases h₁.out; cases h₂.out
   simp only [Iterator.extract, List.reverseAux_eq, List.reverse_append, List.reverse_reverse,
-    List.append_assoc, ne_eq, not_true_eq_false, decide_False, utf8Len_append, utf8Len_reverse,
+    List.append_assoc, ne_eq, not_true_eq_false, decide_false, utf8Len_append, utf8Len_reverse,
     gt_iff_lt, pos_lt_eq, Nat.not_lt.2 (Nat.le_add_left ..), Bool.or_self, Bool.false_eq_true,
     ↓reduceIte]
   simpa [Nat.add_comm] using extract_of_valid l.reverse m r
diff --git a/Batteries/Data/UInt.lean b/Batteries/Data/UInt.lean
index 3f9b495629..007a57d75d 100644
--- a/Batteries/Data/UInt.lean
+++ b/Batteries/Data/UInt.lean
@@ -10,11 +10,6 @@ import Batteries.Classes.Order
 @[ext] theorem UInt8.ext : {x y : UInt8} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-@[simp] theorem UInt8.val_val_eq_toNat (x : UInt8) : x.val.val = x.toNat := rfl
-
-@[simp] theorem UInt8.toNat_ofNat (n) :
-    (no_index (OfNat.ofNat n) : UInt8).toNat = n % UInt8.size := rfl
-
 theorem UInt8.toNat_lt (x : UInt8) : x.toNat < 2 ^ 8 := x.val.isLt
 
 @[simp] theorem UInt8.toUInt16_toNat (x : UInt8) : x.toUInt16.toNat = x.toNat := rfl
@@ -23,19 +18,6 @@ theorem UInt8.toNat_lt (x : UInt8) : x.toNat < 2 ^ 8 := x.val.isLt
 
 @[simp] theorem UInt8.toUInt64_toNat (x : UInt8) : x.toUInt64.toNat = x.toNat := rfl
 
-theorem UInt8.toNat_add (x y : UInt8) : (x + y).toNat = (x.toNat + y.toNat) % UInt8.size := rfl
-
-theorem UInt8.toNat_sub (x y : UInt8) :
-    (x - y).toNat = (UInt8.size - y.toNat + x.toNat) % UInt8.size := rfl
-
-theorem UInt8.toNat_mul (x y : UInt8) : (x * y).toNat = (x.toNat * y.toNat) % UInt8.size := rfl
-
-theorem UInt8.le_antisymm_iff {x y : UInt8} : x = y ↔ x ≤ y ∧ y ≤ x :=
-  UInt8.ext_iff.trans Nat.le_antisymm_iff
-
-theorem UInt8.le_antisymm {x y : UInt8} (h1 : x ≤ y) (h2 : y ≤ x) : x = y :=
-  UInt8.le_antisymm_iff.2 ⟨h1, h2⟩
-
 instance : Batteries.LawfulOrd UInt8 := .compareOfLessAndEq
   (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt8.le_antisymm
 
@@ -44,11 +26,6 @@ instance : Batteries.LawfulOrd UInt8 := .compareOfLessAndEq
 @[ext] theorem UInt16.ext : {x y : UInt16} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-@[simp] theorem UInt16.val_val_eq_toNat (x : UInt16) : x.val.val = x.toNat := rfl
-
-@[simp] theorem UInt16.toNat_ofNat (n) :
-    (no_index (OfNat.ofNat n) : UInt16).toNat = n % UInt16.size := rfl
-
 theorem UInt16.toNat_lt (x : UInt16) : x.toNat < 2 ^ 16 := x.val.isLt
 
 @[simp] theorem UInt16.toUInt8_toNat (x : UInt16) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
@@ -57,19 +34,6 @@ theorem UInt16.toNat_lt (x : UInt16) : x.toNat < 2 ^ 16 := x.val.isLt
 
 @[simp] theorem UInt16.toUInt64_toNat (x : UInt16) : x.toUInt64.toNat = x.toNat := rfl
 
-theorem UInt16.toNat_add (x y : UInt16) : (x + y).toNat = (x.toNat + y.toNat) % UInt16.size := rfl
-
-theorem UInt16.toNat_sub (x y : UInt16) :
-    (x - y).toNat = (UInt16.size - y.toNat + x.toNat) % UInt16.size := rfl
-
-theorem UInt16.toNat_mul (x y : UInt16) : (x * y).toNat = (x.toNat * y.toNat) % UInt16.size := rfl
-
-theorem UInt16.le_antisymm_iff {x y : UInt16} : x = y ↔ x ≤ y ∧ y ≤ x :=
-  UInt16.ext_iff.trans Nat.le_antisymm_iff
-
-theorem UInt16.le_antisymm {x y : UInt16} (h1 : x ≤ y) (h2 : y ≤ x) : x = y :=
-  UInt16.le_antisymm_iff.2 ⟨h1, h2⟩
-
 instance : Batteries.LawfulOrd UInt16 := .compareOfLessAndEq
   (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt16.le_antisymm
 
@@ -78,11 +42,6 @@ instance : Batteries.LawfulOrd UInt16 := .compareOfLessAndEq
 @[ext] theorem UInt32.ext : {x y : UInt32} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-@[simp] theorem UInt32.val_val_eq_toNat (x : UInt32) : x.val.val = x.toNat := rfl
-
-@[simp] theorem UInt32.toNat_ofNat (n) :
-    (no_index (OfNat.ofNat n) : UInt32).toNat = n % UInt32.size := rfl
-
 theorem UInt32.toNat_lt (x : UInt32) : x.toNat < 2 ^ 32 := x.val.isLt
 
 @[simp] theorem UInt32.toUInt8_toNat (x : UInt32) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
@@ -91,19 +50,6 @@ theorem UInt32.toNat_lt (x : UInt32) : x.toNat < 2 ^ 32 := x.val.isLt
 
 @[simp] theorem UInt32.toUInt64_toNat (x : UInt32) : x.toUInt64.toNat = x.toNat := rfl
 
-theorem UInt32.toNat_add (x y : UInt32) : (x + y).toNat = (x.toNat + y.toNat) % UInt32.size := rfl
-
-theorem UInt32.toNat_sub (x y : UInt32) :
-    (x - y).toNat = (UInt32.size - y.toNat + x.toNat) % UInt32.size := rfl
-
-theorem UInt32.toNat_mul (x y : UInt32) : (x * y).toNat = (x.toNat * y.toNat) % UInt32.size := rfl
-
-theorem UInt32.le_antisymm_iff {x y : UInt32} : x = y ↔ x ≤ y ∧ y ≤ x :=
-  UInt32.ext_iff.trans Nat.le_antisymm_iff
-
-theorem UInt32.le_antisymm {x y : UInt32} (h1 : x ≤ y) (h2 : y ≤ x) : x = y :=
-  UInt32.le_antisymm_iff.2 ⟨h1, h2⟩
-
 instance : Batteries.LawfulOrd UInt32 := .compareOfLessAndEq
   (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt32.le_antisymm
 
@@ -112,11 +58,6 @@ instance : Batteries.LawfulOrd UInt32 := .compareOfLessAndEq
 @[ext] theorem UInt64.ext : {x y : UInt64} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-@[simp] theorem UInt64.val_val_eq_toNat (x : UInt64) : x.val.val = x.toNat := rfl
-
-@[simp] theorem UInt64.toNat_ofNat (n) :
-    (no_index (OfNat.ofNat n) : UInt64).toNat = n % UInt64.size := rfl
-
 theorem UInt64.toNat_lt (x : UInt64) : x.toNat < 2 ^ 64 := x.val.isLt
 
 @[simp] theorem UInt64.toUInt8_toNat (x : UInt64) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
@@ -125,19 +66,6 @@ theorem UInt64.toNat_lt (x : UInt64) : x.toNat < 2 ^ 64 := x.val.isLt
 
 @[simp] theorem UInt64.toUInt32_toNat (x : UInt64) : x.toUInt32.toNat = x.toNat % 2 ^ 32 := rfl
 
-theorem UInt64.toNat_add (x y : UInt64) : (x + y).toNat = (x.toNat + y.toNat) % UInt64.size := rfl
-
-theorem UInt64.toNat_sub (x y : UInt64) :
-    (x - y).toNat = (UInt64.size - y.toNat + x.toNat) % UInt64.size := rfl
-
-theorem UInt64.toNat_mul (x y : UInt64) : (x * y).toNat = (x.toNat * y.toNat) % UInt64.size := rfl
-
-theorem UInt64.le_antisymm_iff {x y : UInt64} : x = y ↔ x ≤ y ∧ y ≤ x :=
-  UInt64.ext_iff.trans Nat.le_antisymm_iff
-
-theorem UInt64.le_antisymm {x y : UInt64} (h1 : x ≤ y) (h2 : y ≤ x) : x = y :=
-  UInt64.le_antisymm_iff.2 ⟨h1, h2⟩
-
 instance : Batteries.LawfulOrd UInt64 := .compareOfLessAndEq
   (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt64.le_antisymm
 
@@ -146,11 +74,6 @@ instance : Batteries.LawfulOrd UInt64 := .compareOfLessAndEq
 @[ext] theorem USize.ext : {x y : USize} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-@[simp] theorem USize.val_val_eq_toNat (x : USize) : x.val.val = x.toNat := rfl
-
-@[simp] theorem USize.toNat_ofNat (n) :
-    (no_index (OfNat.ofNat n) : USize).toNat = n % USize.size := rfl
-
 theorem USize.size_eq : USize.size = 2 ^ System.Platform.numBits := by
   rw [USize.size]
 
@@ -172,18 +95,5 @@ theorem USize.toNat_lt (x : USize) : x.toNat < 2 ^ System.Platform.numBits := by
 
 @[simp] theorem UInt32.toUSize_toNat (x : UInt32) : x.toUSize.toNat = x.toNat := rfl
 
-theorem USize.toNat_add (x y : USize) : (x + y).toNat = (x.toNat + y.toNat) % USize.size := rfl
-
-theorem USize.toNat_sub (x y : USize) :
-    (x - y).toNat = (USize.size - y.toNat + x.toNat) % USize.size := rfl
-
-theorem USize.toNat_mul (x y : USize) : (x * y).toNat = (x.toNat * y.toNat) % USize.size := rfl
-
-theorem USize.le_antisymm_iff {x y : USize} : x = y ↔ x ≤ y ∧ y ≤ x :=
-  USize.ext_iff.trans Nat.le_antisymm_iff
-
-theorem USize.le_antisymm {x y : USize} (h1 : x ≤ y) (h2 : y ≤ x) : x = y :=
-  USize.le_antisymm_iff.2 ⟨h1, h2⟩
-
 instance : Batteries.LawfulOrd USize := .compareOfLessAndEq
   (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt USize.le_antisymm
diff --git a/Batteries/Data/UnionFind/Basic.lean b/Batteries/Data/UnionFind/Basic.lean
index c48bb5bda1..3328834ec2 100644
--- a/Batteries/Data/UnionFind/Basic.lean
+++ b/Batteries/Data/UnionFind/Basic.lean
@@ -25,39 +25,35 @@ namespace UnionFind
 
 /-- Parent of a union-find node, defaults to self when the node is a root -/
 def parentD (arr : Array UFNode) (i : Nat) : Nat :=
-  if h : i < arr.size then (arr.get ⟨i, h⟩).parent else i
+  if h : i < arr.size then arr[i].parent else i
 
 /-- Rank of a union-find node, defaults to 0 when the node is a root -/
 def rankD (arr : Array UFNode) (i : Nat) : Nat :=
-  if h : i < arr.size then (arr.get ⟨i, h⟩).rank else 0
+  if h : i < arr.size then arr[i].rank else 0
 
-theorem parentD_eq {arr : Array UFNode} {i} : parentD arr i.1 = (arr.get i).parent := dif_pos _
+theorem parentD_eq {arr : Array UFNode} {i} (h) :
+    parentD arr i = arr[i].parent := dif_pos _
 
-theorem parentD_eq' {arr : Array UFNode} {i} (h) :
-    parentD arr i = (arr.get ⟨i, h⟩).parent := dif_pos _
-
-theorem rankD_eq {arr : Array UFNode} {i} : rankD arr i.1 = (arr.get i).rank := dif_pos _
-
-theorem rankD_eq' {arr : Array UFNode} {i} (h) : rankD arr i = (arr.get ⟨i, h⟩).rank := dif_pos _
+theorem rankD_eq {arr : Array UFNode} {i} (h) : rankD arr i = arr[i].rank := dif_pos _
 
 theorem parentD_of_not_lt : ¬i < arr.size → parentD arr i = i := (dif_neg ·)
 
 theorem lt_of_parentD : parentD arr i ≠ i → i < arr.size :=
   Decidable.not_imp_comm.1 parentD_of_not_lt
 
-theorem parentD_set {arr : Array UFNode} {x v i} :
-    parentD (arr.set x v) i = if x.1 = i then v.parent else parentD arr i := by
+theorem parentD_set {arr : Array UFNode} {x v i h} :
+    parentD (arr.set x v h) i = if x = i then v.parent else parentD arr i := by
   rw [parentD]; simp only [Array.size_set, Array.get_eq_getElem, parentD]
   split
   · split <;> simp_all
-  · split <;> [(subst i; cases ‹¬_› x.2); rfl]
+  · split <;> [(subst i; cases ‹¬_› h); rfl]
 
-theorem rankD_set {arr : Array UFNode} {x v i} :
-    rankD (arr.set x v) i = if x.1 = i then v.rank else rankD arr i := by
+theorem rankD_set {arr : Array UFNode} {x v i h} :
+    rankD (arr.set x v h) i = if x = i then v.rank else rankD arr i := by
   rw [rankD]; simp only [Array.size_set, Array.get_eq_getElem, rankD]
   split
   · split <;> simp_all
-  · split <;> [(subst i; cases ‹¬_› x.2); rfl]
+  · split <;> [(subst i; cases ‹¬_› h); rfl]
 
 end UnionFind
 
@@ -126,9 +122,8 @@ instance : EmptyCollection UnionFind := ⟨.empty⟩
 /-- Parent of union-find node -/
 abbrev parent (self : UnionFind) (i : Nat) : Nat := parentD self.arr i
 
-theorem parent'_lt (self : UnionFind) (i : Fin self.size) :
-    (self.arr.get i).parent < self.size := by
-  simp only [← parentD_eq, parentD_lt, Fin.is_lt, Array.length_toList]
+theorem parent'_lt (self : UnionFind) (i : Nat) (h) : self.arr[i].parent < self.size := by
+  simp [← parentD_eq, parentD_lt, Fin.is_lt, Array.length_toList, h]
 
 theorem parent_lt (self : UnionFind) (i : Nat) : self.parent i < self.size ↔ i < self.size := by
   simp only [parentD]; split <;> simp only [*, parent'_lt]
@@ -139,20 +134,19 @@ abbrev rank (self : UnionFind) (i : Nat) : Nat := rankD self.arr i
 theorem rank_lt {self : UnionFind} {i : Nat} : self.parent i ≠ i →
     self.rank i < self.rank (self.parent i) := by simpa only [rank] using self.rankD_lt
 
-theorem rank'_lt (self : UnionFind) (i : Fin self.size) : (self.arr.get i).parent ≠ i →
-    self.rank i < self.rank (self.arr.get i).parent := by
+theorem rank'_lt (self : UnionFind) (i h) : self.arr[i].parent ≠ i →
+    self.rank i < self.rank (self.arr[i]).parent := by
   simpa only [← parentD_eq] using self.rankD_lt
 
 /-- Maximum rank of nodes in a union-find structure -/
 noncomputable def rankMax (self : UnionFind) := self.arr.foldr (max ·.rank) 0 + 1
 
-theorem rank'_lt_rankMax (self : UnionFind) (i : Fin self.size) :
-    (self.arr.get i).rank < self.rankMax := by
+theorem rank'_lt_rankMax (self : UnionFind) (i : Nat) (h) : (self.arr[i]).rank < self.rankMax := by
   let rec go : ∀ {l} {x : UFNode}, x ∈ l → x.rank ≤ List.foldr (max ·.rank) 0 l
     | a::l, _, List.Mem.head _ => by dsimp; apply Nat.le_max_left
     | a::l, _, .tail _ h => by dsimp; exact Nat.le_trans (go h) (Nat.le_max_right ..)
-  simp only [Array.get_eq_getElem, rankMax, Array.foldr_eq_foldr_toList]
-  exact Nat.lt_succ.2 <| go (self.arr.toList.get_mem i.1 i.2)
+  simp only [Array.get_eq_getElem, rankMax, ← Array.foldr_toList]
+  exact Nat.lt_succ.2 <| go (self.arr.toList.getElem_mem _)
 
 theorem rankD_lt_rankMax (self : UnionFind) (i : Nat) :
     rankD self.arr i < self.rankMax := by
@@ -175,17 +169,17 @@ def push (self : UnionFind) : UnionFind where
   arr := self.arr.push ⟨self.arr.size, 0⟩
   parentD_lt {i} := by
     simp only [Array.size_push, push_parentD]; simp only [parentD, Array.get_eq_getElem]
-    split <;> [exact fun _ => Nat.lt_succ_of_lt (self.parent'_lt _); exact id]
+    split <;> [exact fun _ => Nat.lt_succ_of_lt (self.parent'_lt ..); exact id]
   rankD_lt := by simp only [push_parentD, ne_eq, push_rankD]; exact self.rank_lt
 
 /-- Root of a union-find node. -/
 def root (self : UnionFind) (x : Fin self.size) : Fin self.size :=
-  let y := (self.arr.get x).parent
+  let y := self.arr[x.1].parent
   if h : y = x then
     x
   else
-    have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ h)
-    self.root ⟨y, self.parent'_lt x⟩
+    have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ h)
+    self.root ⟨y, self.parent'_lt x _⟩
 termination_by self.rankMax - self.rank x
 
 @[inherit_doc root]
@@ -202,9 +196,9 @@ def rootD (self : UnionFind) (x : Nat) : Nat :=
 
 @[nolint unusedHavesSuffices]
 theorem parent_root (self : UnionFind) (x : Fin self.size) :
-    (self.arr.get (self.root x)).parent = self.root x := by
+    (self.arr[(self.root x).1]).parent = self.root x := by
   rw [root]; split <;> [assumption; skip]
-  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›)
   apply parent_root
 termination_by self.rankMax - self.rank x
 
@@ -231,7 +225,7 @@ theorem rootD_lt {self : UnionFind} {x : Nat} : self.rootD x < self.size ↔ x <
 @[nolint unusedHavesSuffices]
 theorem rootD_eq_self {self : UnionFind} {x : Nat} : self.rootD x = x ↔ self.parent x = x := by
   refine ⟨fun h => by rw [← h, parent_rootD], fun h => ?_⟩
-  rw [rootD]; split <;> [rw [root, dif_pos (by rwa [parent, parentD_eq' ‹_›] at h)]; rfl]
+  rw [rootD]; split <;> [rw [root, dif_pos (by rwa [parent, parentD_eq ‹_›] at h)]; rfl]
 
 theorem rootD_rootD {self : UnionFind} {x : Nat} : self.rootD (self.rootD x) = self.rootD x :=
   rootD_eq_self.2 (parent_rootD ..)
@@ -271,12 +265,12 @@ structure FindAux (n : Nat) where
 
 /-- Auxiliary function for find operation -/
 def findAux (self : UnionFind) (x : Fin self.size) : FindAux self.size :=
-  let y := (self.arr.get x).parent
+  let y := self.arr[x.1].parent
   if h : y = x then
     ⟨self.arr, x, rfl⟩
   else
-    have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ h)
-    let ⟨arr₁, root, H⟩ := self.findAux ⟨y, self.parent'_lt x⟩
+    have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ h)
+    let ⟨arr₁, root, H⟩ := self.findAux ⟨y, self.parent'_lt _ x.2⟩
     ⟨arr₁.modify x fun s => { s with parent := root }, root, by simp [H]⟩
 termination_by self.rankMax - self.rank x
 
@@ -286,16 +280,16 @@ theorem findAux_root {self : UnionFind} {x : Fin self.size} :
   rw [findAux, root]
   simp only [Array.length_toList, Array.get_eq_getElem, dite_eq_ite]
   split <;> simp only
-  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›)
   exact findAux_root
 termination_by self.rankMax - self.rank x
 
 @[nolint unusedHavesSuffices]
 theorem findAux_s {self : UnionFind} {x : Fin self.size} :
-    (findAux self x).s = if (self.arr.get x).parent = x then self.arr else
-      (self.findAux ⟨_, self.parent'_lt x⟩).s.modify x fun s =>
+    (findAux self x).s = if self.arr[x.1].parent = x then self.arr else
+      (self.findAux ⟨_, self.parent'_lt x x.2⟩).s.modify x fun s =>
         { s with parent := self.rootD x } := by
-  rw [show self.rootD _ = (self.findAux ⟨_, self.parent'_lt x⟩).root from _]
+  rw [show self.rootD _ = (self.findAux ⟨_, self.parent'_lt x x.2⟩).root from _]
   · rw [findAux]; split <;> rfl
   · rw [← rootD_parent, parent, parentD_eq]
     simp only [rootD, Array.get_eq_getElem, Array.length_toList, findAux_root]
@@ -307,10 +301,11 @@ theorem rankD_findAux {self : UnionFind} {x : Fin self.size} :
     rankD (findAux self x).s i = self.rank i := by
   if h : i < self.size then
     rw [findAux_s]; split <;> [rfl; skip]
-    have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+    have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›)
     have := lt_of_parentD (by rwa [parentD_eq])
-    rw [rankD_eq' (by simp [FindAux.size_eq, h]), Array.get_modify]
-    split <;> simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt x⟩), -Array.get_eq_getElem]
+    rw [rankD_eq (by simp [FindAux.size_eq, h]), Array.getElem_modify]
+    split <;>
+      simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt _ x.2⟩), -Array.get_eq_getElem]
   else
     simp only [rankD, Array.data_length, Array.get_eq_getElem, rank]
     rw [dif_neg (by rwa [FindAux.size_eq]), dif_neg h]
@@ -319,13 +314,13 @@ termination_by self.rankMax - self.rank x
 set_option linter.deprecated false in
 theorem parentD_findAux {self : UnionFind} {x : Fin self.size} :
     parentD (findAux self x).s i =
-    if i = x then self.rootD x else parentD (self.findAux ⟨_, self.parent'_lt x⟩).s i := by
+    if i = x then self.rootD x else parentD (self.findAux ⟨_, self.parent'_lt _ x.2⟩).s i := by
   rw [findAux_s]; split <;> [split; skip]
   · subst i; rw [rootD_eq_self.2 _] <;> simp [parentD_eq, *, -Array.get_eq_getElem]
   · rw [findAux_s]; simp [*, -Array.get_eq_getElem]
   · next h =>
     rw [parentD]; split <;> rename_i h'
-    · rw [Array.get_modify (by simpa using h')]
+    · rw [Array.getElem_modify (by simpa using h')]
       simp only [Array.data_length, @eq_comm _ i]
       split <;> simp [← parentD_eq, -Array.get_eq_getElem]
     · rw [if_neg (mt (by rintro rfl; simp [FindAux.size_eq]) h')]
@@ -334,47 +329,48 @@ theorem parentD_findAux {self : UnionFind} {x : Fin self.size} :
 theorem parentD_findAux_rootD {self : UnionFind} {x : Fin self.size} :
     parentD (findAux self x).s (self.rootD x) = self.rootD x := by
   rw [parentD_findAux]; split <;> [rfl; rename_i h]
-  rw [rootD_eq_self, parent, parentD_eq] at h
-  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
-  rw [← rootD_parent, parent, parentD_eq]
-  exact parentD_findAux_rootD (x := ⟨_, self.parent'_lt x⟩)
+  rw [rootD_eq_self, parent, parentD_eq x.2] at h
+  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›)
+  rw [← rootD_parent, parent, parentD_eq x.2]
+  exact parentD_findAux_rootD (x := ⟨_, self.parent'_lt _ x.2⟩)
 termination_by self.rankMax - self.rank x
 
 theorem parentD_findAux_lt {self : UnionFind} {x : Fin self.size} (h : i < self.size) :
     parentD (findAux self x).s i < self.size := by
-  if h' : (self.arr.get x).parent = x then
+  if h' : self.arr[x.1].parent = x then
     rw [findAux_s, if_pos h']; apply self.parentD_lt h
   else
     rw [parentD_findAux]
     split
     · simp [rootD_lt]
-    · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+    · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›)
       apply parentD_findAux_lt h
 termination_by self.rankMax - self.rank x
 
 theorem parentD_findAux_or (self : UnionFind) (x : Fin self.size) (i) :
     parentD (findAux self x).s i = self.rootD i ∧ self.rootD i = self.rootD x ∨
     parentD (findAux self x).s i = self.parent i := by
-  if h' : (self.arr.get x).parent = x then
+  if h' : self.arr[x.1].parent = x then
     rw [findAux_s, if_pos h']; exact .inr rfl
   else
     rw [parentD_findAux]
     split
     · simp [*]
-    · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
-      exact (parentD_findAux_or self ⟨_, self.parent'_lt x⟩ i).imp_left <| .imp_right fun h => by
-        simp only [h, ← parentD_eq, rootD_parent, Array.length_toList]
+    · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›)
+      refine (parentD_findAux_or self ⟨_, self.parent'_lt _ x.2⟩ i)
+        |>.imp_left (.imp_right fun h => ?_)
+      simp only [h, ← parentD_eq, rootD_parent, Array.length_toList]
 termination_by self.rankMax - self.rank x
 
 theorem lt_rankD_findAux {self : UnionFind} {x : Fin self.size} :
     parentD (findAux self x).s i ≠ i →
     self.rank i < self.rank (parentD (findAux self x).s i) := by
-  if h' : (self.arr.get x).parent = x then
+  if h' : self.arr[x.1].parent = x then
     rw [findAux_s, if_pos h']; apply self.rank_lt
   else
     rw [parentD_findAux]; split <;> rename_i h <;> intro h'
     · subst i; rwa [lt_rank_root, Ne, ← rootD_eq_self]
-    · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
+    · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›)
       apply lt_rankD_findAux h'
 termination_by self.rankMax - self.rank x
 
@@ -447,46 +443,46 @@ def linkAux (self : Array UFNode) (x y : Fin self.size) : Array UFNode :=
   if x.1 = y then
     self
   else
-    let nx := self.get x
-    let ny := self.get y
+    let nx := self[x.1]
+    let ny := self[y.1]
     if ny.rank < nx.rank then
       self.set y {ny with parent := x}
     else
       let arr₁ := self.set x {nx with parent := y}
       if nx.rank = ny.rank then
-        arr₁.set ⟨y, by simp [arr₁]⟩ {ny with rank := ny.rank + 1}
+        arr₁.set y {ny with rank := ny.rank + 1} (by simp [arr₁])
       else
         arr₁
 
 theorem setParentBump_rankD_lt {arr : Array UFNode} {x y : Fin arr.size}
-    (hroot : (arr.get x).rank < (arr.get y).rank ∨ (arr.get y).parent = y)
-    (H : (arr.get x).rank ≤ (arr.get y).rank) {i : Nat}
+    (hroot : arr[x.1].rank < arr[y.1].rank ∨ arr[y.1].parent = y)
+    (H : arr[x.1].rank ≤ arr[y.1].rank) {i : Nat}
     (rankD_lt : parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i))
     (hP : parentD arr' i = if x.1 = i then y.1 else parentD arr i)
     (hR : ∀ {i}, rankD arr' i =
-      if y.1 = i ∧ (arr.get x).rank = (arr.get y).rank then
-        (arr.get y).rank + 1
+      if y.1 = i ∧ arr[x.1].rank = arr[y.1].rank then
+        arr[y.1].rank + 1
       else rankD arr i) :
     ¬parentD arr' i = i → rankD arr' i < rankD arr' (parentD arr' i) := by
   simp [hP, hR, -Array.get_eq_getElem] at *; split <;> rename_i h₁ <;> [simp [← h₁]; skip] <;>
     split <;> rename_i h₂ <;> intro h
   · simp [h₂] at h
-  · simp only [rankD_eq, Array.get_eq_getElem]
+  · simp only [rankD_eq, x.2, y.2, Array.get_eq_getElem]
     split <;> rename_i h₃
     · rw [← h₃]; apply Nat.lt_succ_self
     · exact Nat.lt_of_le_of_ne H h₃
   · cases h₂.1
     simp only [h₂.2, false_or, Nat.lt_irrefl] at hroot
-    simp only [hroot, parentD_eq, not_true_eq_false] at h
+    simp only [hroot, parentD_eq y.2, not_true_eq_false] at h
   · have := rankD_lt h
     split <;> rename_i h₃
     · rw [← rankD_eq, h₃.1]; exact Nat.lt_succ_of_lt this
     · exact this
 
 theorem setParent_rankD_lt {arr : Array UFNode} {x y : Fin arr.size}
-    (h : (arr.get x).rank < (arr.get y).rank) {i : Nat}
+    (h : arr[x.1].rank < arr[y.1].rank) {i : Nat}
     (rankD_lt : parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i)) :
-    let arr' := arr.set x ⟨y, (arr.get x).rank⟩
+    let arr' := arr.set x ⟨y, arr[x].rank⟩
     parentD arr' i ≠ i → rankD arr' i < rankD arr' (parentD arr' i) :=
   setParentBump_rankD_lt (.inl h) (Nat.le_of_lt h) rankD_lt parentD_set
     (by simp [rankD_set, Nat.ne_of_lt h, rankD_eq, -Array.get_eq_getElem])
@@ -505,7 +501,7 @@ def link (self : UnionFind) (x y : Fin self.size) (yroot : self.parent y = y) :
     · exact self.parentD_lt h
     · rw [parentD_set]; split <;> [exact x.2; exact self.parentD_lt h]
     · rw [parentD_set]; split
-      · exact self.parent'_lt _
+      · exact self.parent'_lt ..
       · rw [parentD_set]; split <;> [exact y.2; exact self.parentD_lt h]
     · rw [parentD_set]; split <;> [exact y.2; exact self.parentD_lt h]
   rankD_lt := by
diff --git a/Batteries/Data/UnionFind/Lemmas.lean b/Batteries/Data/UnionFind/Lemmas.lean
index 9a7b0dac58..f070a6d4f1 100644
--- a/Batteries/Data/UnionFind/Lemmas.lean
+++ b/Batteries/Data/UnionFind/Lemmas.lean
@@ -43,7 +43,7 @@ theorem parentD_linkAux {self} {x y : Fin self.size} :
     if x.1 = y then
       parentD self i
     else
-      if (self.get y).rank < (self.get x).rank then
+      if self[y.1].rank < self[x.1].rank then
         if y = i then x else parentD self i
       else
         if x = i then y else parentD self i := by
diff --git a/Batteries/Data/Vector/Basic.lean b/Batteries/Data/Vector/Basic.lean
index 0ae5871356..7b2581c852 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,292 +17,30 @@ 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.get (i.cast v.size_toArray.symm)
-
-/-- 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⟩
-
-/-- 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⟩
-
-/-- Maps elements of a vector using the function `f`. -/
-@[inline] def map (f : α → β) (v : Vector α n) : Vector β n :=
-  ⟨v.toArray.map f, by simp⟩
-
-/-- 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⟩
-
-/-- 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]⟩
+@[deprecated (since := "2024-11-25")] alias setN := set
 
-/--
-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.
+@[deprecated (since := "2024-11-25")] alias setD := setIfInBounds
 
-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]⟩
+@[deprecated (since := "2024-11-24")] alias swapN := swap
 
-/-- The vector `#v[0,1,2,...,n-1]`. -/
-@[inline] def range (n : Nat) : Vector Nat n := ⟨Array.range n, by simp⟩
+@[deprecated (since := "2024-11-24")] alias swap! := swapIfInBounds
 
-/--
-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)
+@[deprecated (since := "2024-11-20")] alias eraseIdxN := eraseIdx
 
-instance [BEq α] : BEq (Vector α n) where
-  beq a b := isEqv a b (· == ·)
+/-- Use `#v[]` instead. -/
+@[deprecated "Use `#v[]`." (since := "2024-11-27")]
+def empty (α : Type u) : Vector α 0 := #v[]
 
 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 `Fin` index. -/
-@[inline] def feraseIdx (v : Vector α n) (i : Fin n) : Vector α (n-1) :=
-  ⟨v.toArray.feraseIdx (Fin.cast v.size_toArray.symm i), by simp [Array.size_feraseIdx]⟩
-
-/-- 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.toArray.eraseIdx i, by simp [*]⟩
-  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.toArray.eraseIdx 0, by simp [*]⟩
-  else
-    v.cast (by omega)
-
-/--
-Delete an element of a vector using a `Nat` index. By default, the `get_elem_tactic` is used to
-synthesise a proof that the index is within bounds.
--/
-@[inline] def eraseIdxN (v : Vector α n) (i : Nat) (h : i < n := by get_elem_tactic) :
-  Vector α (n - 1) := ⟨v.toArray.eraseIdxN i (by simp [*]), by simp⟩
-
-/--
-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
-
 /--
 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/Batteries/Lean/Meta/Simp.lean b/Batteries/Lean/Meta/Simp.lean
index 7ea81e87fa..085472c934 100644
--- a/Batteries/Lean/Meta/Simp.lean
+++ b/Batteries/Lean/Meta/Simp.lean
@@ -55,10 +55,8 @@ def mkSimpContext' (simpTheorems : SimpTheorems) (stx : Syntax) (eraseLocal : Bo
     pure simpTheorems
   let simprocs ← if simpOnly then pure {} else Simp.getSimprocs
   let congrTheorems ← Meta.getSimpCongrTheorems
-  let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) (simprocs := #[simprocs]) {
-    config       := (← elabSimpConfig stx[1] (kind := kind))
-    simpTheorems := #[simpTheorems], congrTheorems
-  }
+  let ctx ← Simp.mkContext (← elabSimpConfig stx[1] (kind := kind)) #[simpTheorems] congrTheorems
+  let r ← elabSimpArgs stx[4] (simprocs := #[simprocs]) ctx eraseLocal kind
   if !r.starArg || ignoreStarArg then
     return { r with dischargeWrapper }
   else
@@ -73,7 +71,7 @@ def mkSimpContext' (simpTheorems : SimpTheorems) (stx : Syntax) (eraseLocal : Bo
     for h in hs do
       unless simpTheorems.isErased (.fvar h) do
         simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr
-    let ctx := { ctx with simpTheorems }
+    let ctx := ctx.setSimpTheorems simpTheorems
     return { ctx, simprocs, dischargeWrapper }
 
 
diff --git a/Batteries/Lean/NameMap.lean b/Batteries/Lean/NameMap.lean
deleted file mode 100644
index 0c6d341925..0000000000
--- a/Batteries/Lean/NameMap.lean
+++ /dev/null
@@ -1,40 +0,0 @@
-/-
-Copyright (c) 2023 Jon Eugster. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jon Eugster
--/
-import Lean.Data.NameMap
-
-/-!
-# Additional functions on `Lean.NameMap`.
-
-We provide `NameMap.filter` and `NameMap.filterMap`.
--/
-
-namespace Lean.NameMap
-
-/--
-`filter f m` returns the `NameMap` consisting of all
-"`key`/`val`"-pairs in `m` where `f key val` returns `true`.
--/
-def filter (f : Name → α → Bool) (m : NameMap α) : NameMap α :=
-  m.fold process {}
-where
-  /-- see `Lean.NameMap.filter` -/
-  process (r : NameMap α) (n : Name) (i : α) :=
-    if f n i then r.insert n i else r
-
-/--
-`filterMap f m` allows to filter a `NameMap` and simultaneously modify the filtered values.
-
-It takes a function `f : Name → α → Option β` and applies `f name` to the value with key `name`.
-The resulting entries with non-`none` value are collected to form the output `NameMap`.
--/
-def filterMap (f : Name → α → Option β) (m : NameMap α) : NameMap β :=
-  m.fold process {}
-where
-  /-- see `Lean.NameMap.filterMap` -/
-  process (r : NameMap β) (n : Name) (i : α) :=
-    match f n i with
-    | none => r
-    | some b => r.insert n b
diff --git a/Batteries/Tactic/Instances.lean b/Batteries/Tactic/Instances.lean
index b243c4f153..7e7ea30d8f 100644
--- a/Batteries/Tactic/Instances.lean
+++ b/Batteries/Tactic/Instances.lean
@@ -35,7 +35,7 @@ elab (name := instancesCmd) tk:"#instances " stx:term : command => runTermElabM
     let some className ← isClass? type
       | throwErrorAt stx "type class instance expected{indentExpr type}"
     let globalInstances ← getGlobalInstancesIndex
-    let result ← globalInstances.getUnify type tcDtConfig
+    let result ← globalInstances.getUnify type
     let erasedInstances ← getErasedInstances
     let mut msgs := #[]
     for e in result.insertionSort fun e₁ e₂ => e₁.priority < e₂.priority do
diff --git a/Batteries/Tactic/Lint/Frontend.lean b/Batteries/Tactic/Lint/Frontend.lean
index cb0369db5f..7f39e6759c 100644
--- a/Batteries/Tactic/Lint/Frontend.lean
+++ b/Batteries/Tactic/Lint/Frontend.lean
@@ -53,7 +53,7 @@ sanity check, lint, cleanup, command, tactic
 -/
 
 namespace Batteries.Tactic.Lint
-open Lean
+open Lean Elab Command
 
 /-- Verbosity for the linter output. -/
 inductive LintVerbosity
@@ -89,9 +89,6 @@ def getChecks (slow : Bool) (runOnly : Option (List Name)) (runAlways : Option (
         result := result.binInsert (·.name.lt ·.name) linter
   pure result
 
--- Note: we have to use the same context as `runTermElabM` here so that the `simpNF`
--- linter works the same as the `simp` tactic itself. See #671
-open private mkMetaContext from Lean.Elab.Command in
 /--
 Runs all the specified linters on all the specified declarations in parallel,
 producing a list of results.
@@ -107,7 +104,7 @@ def lintCore (decls : Array Name) (linters : Array NamedLinter) :
       (linter, ·) <$> decls.mapM fun decl => (decl, ·) <$> do
         BaseIO.asTask do
           match ← withCurrHeartbeats (linter.test decl)
-              |>.run' mkMetaContext
+              |>.run' mkMetaContext -- We use the context used by `Command.liftTermElabM`
               |>.run' {options, fileName := "", fileMap := default} {env}
               |>.toBaseIO with
           | Except.ok msg? => pure msg?
diff --git a/Batteries/Tactic/Lint/Simp.lean b/Batteries/Tactic/Lint/Simp.lean
index c6c0ad8828..3e83431dcc 100644
--- a/Batteries/Tactic/Lint/Simp.lean
+++ b/Batteries/Tactic/Lint/Simp.lean
@@ -108,7 +108,7 @@ see note [simp-normal form] for tips how to debug this.
 https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form"
   test := fun declName => do
     unless ← isSimpTheorem declName do return none
-    let ctx := { ← Simp.Context.mkDefault with config.decide := false }
+    let ctx ← Simp.Context.mkDefault
     checkAllSimpTheoremInfos (← getConstInfo declName).type fun {lhs, rhs, isConditional, ..} => do
       let isRfl ← isRflTheorem declName
       let ({ expr := lhs', proof? := prf1, .. }, prf1Stats) ←
@@ -228,7 +228,7 @@ private def Expr.eqOrIff? : Expr → Option (Expr × Expr)
   noErrorsFound := "No commutativity lemma is marked simp."
   errorsFound := "COMMUTATIVITY LEMMA IS SIMP.
 Some commutativity lemmas are simp lemmas:"
-  test := fun declName => withReducible do
+  test := fun declName => withSimpGlobalConfig do withReducible do
     unless ← isSimpTheorem declName do return none
     let ty := (← getConstInfo declName).type
     forallTelescopeReducing ty fun _ ty' => do
@@ -239,7 +239,7 @@ Some commutativity lemmas are simp lemmas:"
     unless ← isDefEq rhs lhs' do return none
     unless ← withNewMCtxDepth (isDefEq rhs lhs') do return none
     -- make sure that the discrimination tree will actually find this match (see #69)
-    if (← (← DiscrTree.empty.insert rhs () simpDtConfig).getMatch lhs' simpDtConfig).isEmpty then
+    if (← (← DiscrTree.empty.insert rhs ()).getMatch lhs').isEmpty then
       return none
     -- ensure that the second application makes progress:
     if ← isDefEq lhs' rhs' then return none
diff --git a/Batteries/Tactic/Trans.lean b/Batteries/Tactic/Trans.lean
index 7070c843ac..903796bc5d 100644
--- a/Batteries/Tactic/Trans.lean
+++ b/Batteries/Tactic/Trans.lean
@@ -24,9 +24,6 @@ open Lean Meta Elab
 
 initialize registerTraceClass `Tactic.trans
 
-/-- Discrimation tree settings for the `trans` extension. -/
-def transExt.config : WhnfCoreConfig := {}
-
 /-- Environment extension storing transitivity lemmas -/
 initialize transExt :
     SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name) ←
@@ -49,7 +46,7 @@ initialize registerBuiltinAttribute {
     let some xyHyp := xs.pop.back? | fail
     let .app (.app _ _) _ ← inferType yzHyp | fail
     let .app (.app _ _) _ ← inferType xyHyp | fail
-    let key ← withReducible <| DiscrTree.mkPath rel transExt.config
+    let key ← withReducible <| DiscrTree.mkPath rel
     transExt.add (decl, key) kind
 }
 
@@ -162,7 +159,7 @@ elab "trans" t?:(ppSpace colGt term)? : tactic => withMainContext do
       let s ← saveState
       trace[Tactic.trans]"trying homogeneous case"
       let lemmas :=
-        (← (transExt.getState (← getEnv)).getUnify rel transExt.config).push ``Trans.simple
+        (← (transExt.getState (← getEnv)).getUnify rel).push ``Trans.simple
       for lem in lemmas do
         trace[Tactic.trans]"trying lemma {lem}"
         try
@@ -182,7 +179,7 @@ elab "trans" t?:(ppSpace colGt term)? : tactic => withMainContext do
     trace[Tactic.trans]"trying heterogeneous case"
     let t'? ← t?.mapM (elabTermWithHoles · none (← getMainTag))
     let s ← saveState
-    for lem in (← (transExt.getState (← getEnv)).getUnify rel transExt.config).push
+    for lem in (← (transExt.getState (← getEnv)).getUnify rel).push
         ``HEq.trans |>.push ``Trans.trans do
       try
         liftMetaTactic fun g => do
diff --git a/Batteries/Util/Cache.lean b/Batteries/Util/Cache.lean
index 866325df5a..de6beb846b 100644
--- a/Batteries/Util/Cache.lean
+++ b/Batteries/Util/Cache.lean
@@ -132,9 +132,6 @@ the second will store declarations from imports (and will hopefully be "read-onl
 -/
 @[reducible] def DiscrTreeCache (α : Type) : Type := DeclCache (DiscrTree α × DiscrTree α)
 
-/-- Discrimination tree settings for the `DiscrTreeCache`. -/
-def DiscrTreeCache.config : WhnfCoreConfig := {}
-
 /--
 Build a `DiscrTreeCache`,
 from a function that returns a collection of keys and values for each declaration.
@@ -170,4 +167,4 @@ def DiscrTreeCache.getMatch (c : DiscrTreeCache α) (e : Expr) : MetaM (Array α
   let (locals, imports) ← c.get
   -- `DiscrTree.getMatch` returns results in batches, with more specific lemmas coming later.
   -- Hence we reverse this list, so we try out more specific lemmas earlier.
-  return (← locals.getMatch e config).reverse ++ (← imports.getMatch e config).reverse
+  return (← locals.getMatch e).reverse ++ (← imports.getMatch e).reverse
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 89f784293e..e94478ddb6 100644
--- a/BatteriesTest/array.lean
+++ b/BatteriesTest/array.lean
@@ -9,14 +9,14 @@ variable (v d : α)
 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 g ~> v
+#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/BatteriesTest/lint_simpNF.lean b/BatteriesTest/lint_simpNF.lean
index c9c8f9d307..771e47c65a 100644
--- a/BatteriesTest/lint_simpNF.lean
+++ b/BatteriesTest/lint_simpNF.lean
@@ -38,4 +38,17 @@ theorem foo_eq_ite (n : Nat) : foo n = if n = n then n else 0 := by
 
 end Equiv
 
+namespace List
+
+private axiom test_sorry : ∀ {α}, α
+
+@[simp]
+theorem ofFn_getElem_eq_map {β : Type _} (l : List α) (f : α → β) :
+    ofFn (fun i : Fin l.length => f <| l[(i : Nat)]) = l.map f := test_sorry
+
+example {β : Type _} (l : List α) (f : α → β) :
+    ofFn (fun i : Fin l.length => f <| l[(i : Nat)]) = l.map f := by simp only [ofFn_getElem_eq_map]
+
+end List
+
 #lint- only simpNF
diff --git a/BatteriesTest/show_term.lean b/BatteriesTest/show_term.lean
index 7288c369e9..1986fc06ee 100644
--- a/BatteriesTest/show_term.lean
+++ b/BatteriesTest/show_term.lean
@@ -11,7 +11,7 @@ Authors: Kim Morrison
     exact n
     exact 37
 
-/-- info: Try this: refine (?fst, ?snd) -/
+/-- info: Try this: refine (?_, ?_) -/
 #guard_msgs in example : Nat × Nat := by
   show_term constructor
   repeat exact 42
diff --git a/README.md b/README.md
index 2873f65536..36d46eee4d 100644
--- a/README.md
+++ b/README.md
@@ -6,14 +6,14 @@ 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
 [[require]]
 name = "batteries"
 scope = "leanprover-community"
-version = "main"
+rev = "main"
 ```
 
 Additionally, please make sure that you're using the version of Lean that the current version of `batteries` expects. The easiest way to do this is to copy the [`lean-toolchain`](./lean-toolchain) file from this repository to your project. Once you've added the dependency declaration, the command `lake update` checks out the current version of `batteries` and writes it the Lake manifest file. Don't run this command again unless you're prepared to potentially also update your Lean compiler version, as it will retrieve the latest version of dependencies and add them to the manifest.
diff --git a/lean-toolchain b/lean-toolchain
index 0bef727630..cf25a9816f 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc1
+leanprover/lean4:v4.15.0-rc1