From cade9753218c5a53627861a492f76a692f61863b Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 14 Nov 2024 10:23:11 +1100
Subject: [PATCH 01/42] chore: adaptations for nightly-2024-11-12 (#1040)

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
---
 Batteries/Data/Array/Basic.lean      |   8 +-
 Batteries/Data/Array/Lemmas.lean     |  48 ----------
 Batteries/Data/Array/Merge.lean      |   2 +-
 Batteries/Data/Array/Monadic.lean    |   2 +-
 Batteries/Data/Array/OfFn.lean       |   4 -
 Batteries/Data/Array/Pairwise.lean   |   2 +-
 Batteries/Data/BinaryHeap.lean       |   2 +-
 Batteries/Data/ByteArray.lean        |   8 +-
 Batteries/Data/Fin/Basic.lean        |  54 -----------
 Batteries/Data/Fin/Lemmas.lean       | 128 ---------------------------
 Batteries/Data/HashMap/Basic.lean    |   7 +-
 Batteries/Data/List/Basic.lean       |  32 -------
 Batteries/Data/List/OfFn.lean        |  34 -------
 Batteries/Data/MLList/Basic.lean     |   2 +-
 Batteries/Data/String/Lemmas.lean    |   2 +-
 Batteries/Data/UnionFind/Basic.lean  | 128 +++++++++++++--------------
 Batteries/Data/UnionFind/Lemmas.lean |   2 +-
 Batteries/Data/Vector/Basic.lean     |   2 +-
 BatteriesTest/array.lean             |   2 +-
 lean-toolchain                       |   2 +-
 20 files changed, 83 insertions(+), 388 deletions(-)

diff --git a/Batteries/Data/Array/Basic.lean b/Batteries/Data/Array/Basic.lean
index 403c42d9e2..8be0bc967d 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,7 +135,7 @@ 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 α`.
@@ -201,7 +201,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..daf0493b88 100644
--- a/Batteries/Data/Array/Lemmas.lean
+++ b/Batteries/Data/Array/Lemmas.lean
@@ -22,48 +22,6 @@ 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
 
@@ -71,12 +29,6 @@ theorem toList_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
     (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
diff --git a/Batteries/Data/Array/Merge.lean b/Batteries/Data/Array/Merge.lean
index 4b806a35d6..252f7a6364 100644
--- a/Batteries/Data/Array/Merge.lean
+++ b/Batteries/Data/Array/Merge.lean
@@ -94,7 +94,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..897cca1c2a 100644
--- a/Batteries/Data/BinaryHeap.lean
+++ b/Batteries/Data/BinaryHeap.lean
@@ -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
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/Basic.lean b/Batteries/Data/Fin/Basic.lean
index b61481e33a..346f3006e5 100644
--- a/Batteries/Data/Fin/Basic.lean
+++ b/Batteries/Data/Fin/Basic.lean
@@ -14,57 +14,3 @@ def enum (n) : Array (Fin n) := Array.ofFn id
 
 /-- `list n` is the list of all elements of `Fin n` in order -/
 def list (n) : List (Fin n) := (enum n).toList
-
-/--
-Folds a monadic function over `Fin n` from left to right:
-```
-Fin.foldlM n f x₀ = do
-  let x₁ ← f x₀ 0
-  let x₂ ← f x₁ 1
-  ...
-  let xₙ ← f xₙ₋₁ (n-1)
-  pure xₙ
-```
--/
-@[inline] def foldlM [Monad m] (n) (f : α → Fin n → m α) (init : α) : m α := loop init 0 where
-  /--
-  Inner loop for `Fin.foldlM`.
-  ```
-  Fin.foldlM.loop n f xᵢ i = do
-    let xᵢ₊₁ ← f xᵢ i
-    ...
-    let xₙ ← f xₙ₋₁ (n-1)
-    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
-
-/--
-Folds a monadic function over `Fin n` from right to left:
-```
-Fin.foldrM n f xₙ = do
-  let xₙ₋₁ ← f (n-1) xₙ
-  let xₙ₋₂ ← f (n-2) xₙ₋₁
-  ...
-  let x₀ ← f 0 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ᵢ
-    ...
-    let x₁ ← f 1 x₂
-    let x₀ ← f 0 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⟩
diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean
index 5010e1310f..d799e2e6f3 100644
--- a/Batteries/Data/Fin/Lemmas.lean
+++ b/Batteries/Data/Fin/Lemmas.lean
@@ -56,32 +56,6 @@ theorem list_reverse (n) : (list n).reverse = (list n).map rev := by
 
 /-! ### 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
@@ -93,32 +67,6 @@ theorem foldlM_eq_foldlM_list [Monad m] (f : α → Fin n → m α) (x) :
 
 /-! ### 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
@@ -127,41 +75,6 @@ theorem foldrM_eq_foldrM_list [Monad m] [LawfulMonad m] (f : Fin n → α → m
 
 /-! ### 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]
@@ -169,48 +82,7 @@ theorem foldl_eq_foldl_list (f : α → Fin n → α) (x) : foldl n f x = (list
 
 /-! ### 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 3fd1d3350d..a8a93dd197 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/Basic.lean b/Batteries/Data/List/Basic.lean
index 3e2460f18c..77adfc783b 100644
--- a/Batteries/Data/List/Basic.lean
+++ b/Batteries/Data/List/Basic.lean
@@ -163,32 +163,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
 
 /--
@@ -548,14 +524,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
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 8f58c11fb8..5de23f0b53 100644
--- a/Batteries/Data/MLList/Basic.lean
+++ b/Batteries/Data/MLList/Basic.lean
@@ -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/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/UnionFind/Basic.lean b/Batteries/Data/UnionFind/Basic.lean
index c48bb5bda1..a607dc2284 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)
+  exact Nat.lt_succ.2 <| go (self.arr.toList.get_mem i h)
 
 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..73a4a41aee 100644
--- a/Batteries/Data/Vector/Basic.lean
+++ b/Batteries/Data/Vector/Basic.lean
@@ -68,7 +68,7 @@ instance [Inhabited α] : Inhabited (Vector α n) where
 
 /-- 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)
+  v.toArray[(i.cast v.size_toArray.symm).1]
 
 /-- Get an element of a vector using a `USize` index and a proof that the index is within bounds. -/
 @[inline] def uget (v : Vector α n) (i : USize) (h : i.toNat < n) : α :=
diff --git a/BatteriesTest/array.lean b/BatteriesTest/array.lean
index 89f784293e..58bb65b713 100644
--- a/BatteriesTest/array.lean
+++ b/BatteriesTest/array.lean
@@ -9,7 +9,7 @@ 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 g ~> v
 #check_simp (a.set! i v).get! i ~> (a.setD 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
diff --git a/lean-toolchain b/lean-toolchain
index 0bef727630..9e0b2f2e74 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc1
+leanprover/lean4:nightly-2024-11-12

From d0fc2bcb44b6f123d3021b4a0c741e8377756f74 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 14 Nov 2024 19:48:39 +1100
Subject: [PATCH 02/42] chore: adaptations for nightly-2024-11-13 (#1048)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Henrik Böving <hargonix@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
---
 Batteries/Lean/Meta/Simp.lean   | 8 +++-----
 Batteries/Tactic/Lint/Simp.lean | 2 +-
 lean-toolchain                  | 2 +-
 3 files changed, 5 insertions(+), 7 deletions(-)

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/Tactic/Lint/Simp.lean b/Batteries/Tactic/Lint/Simp.lean
index c6c0ad8828..88ad7a1bc2 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) ←
diff --git a/lean-toolchain b/lean-toolchain
index 9e0b2f2e74..d6cb529aed 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-12
+leanprover/lean4:nightly-2024-11-13

From d414a3c80d4debb688c5d82b123b5ffc9fa9ac6f Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 18 Nov 2024 17:03:46 +1100
Subject: [PATCH 03/42] chore: adaptations for nightly-2024-11-14 (#1049)

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
---
 Batteries.lean                      |  1 -
 Batteries/Data/List/Basic.lean      |  2 +-
 Batteries/Data/UnionFind/Basic.lean |  2 +-
 Batteries/Lean/NameMap.lean         | 40 -----------------------------
 lean-toolchain                      |  2 +-
 5 files changed, 3 insertions(+), 44 deletions(-)
 delete mode 100644 Batteries/Lean/NameMap.lean

diff --git a/Batteries.lean b/Batteries.lean
index b645334bf4..6c24d239bc 100644
--- a/Batteries.lean
+++ b/Batteries.lean
@@ -55,7 +55,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/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean
index 31a7d5a661..e62ef1f3c2 100644
--- a/Batteries/Data/List/Basic.lean
+++ b/Batteries/Data/List/Basic.lean
@@ -463,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
 
 /--
diff --git a/Batteries/Data/UnionFind/Basic.lean b/Batteries/Data/UnionFind/Basic.lean
index a607dc2284..cefa85bf3c 100644
--- a/Batteries/Data/UnionFind/Basic.lean
+++ b/Batteries/Data/UnionFind/Basic.lean
@@ -145,7 +145,7 @@ theorem rank'_lt_rankMax (self : UnionFind) (i : Nat) (h) : (self.arr[i]).rank <
   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]
+  simp only [Array.get_eq_getElem, rankMax, ← Array.foldr_toList]
   exact Nat.lt_succ.2 <| go (self.arr.toList.get_mem i h)
 
 theorem rankD_lt_rankMax (self : UnionFind) (i : Nat) :
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/lean-toolchain b/lean-toolchain
index d6cb529aed..97bb2ffae1 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-13
+leanprover/lean4:nightly-2024-11-14

From a8815f0d111d6cea6c9301dfdebf32b92e7b8641 Mon Sep 17 00:00:00 2001
From: leanprover-community-mathlib4-bot
 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Date: Tue, 19 Nov 2024 05:47:22 +0000
Subject: [PATCH 04/42] Update lean-toolchain for testing
 https://github.com/leanprover/lean4/pull/6095

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

diff --git a/lean-toolchain b/lean-toolchain
index 585547139e..33df9a1695 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-18
+leanprover/lean4-pr-releases:pr-release-6095

From 6336d636051c3fbe945113fae80553982f09a87e Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 19 Nov 2024 19:22:45 +1100
Subject: [PATCH 05/42] fix

---
 Batteries/Data/UnionFind/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Batteries/Data/UnionFind/Basic.lean b/Batteries/Data/UnionFind/Basic.lean
index cefa85bf3c..3a523e4f9d 100644
--- a/Batteries/Data/UnionFind/Basic.lean
+++ b/Batteries/Data/UnionFind/Basic.lean
@@ -146,7 +146,7 @@ theorem rank'_lt_rankMax (self : UnionFind) (i : Nat) (h) : (self.arr[i]).rank <
     | 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_toList]
-  exact Nat.lt_succ.2 <| go (self.arr.toList.get_mem i h)
+  exact Nat.lt_succ.2 <| go (self.arr.toList.getElem_mem h)
 
 theorem rankD_lt_rankMax (self : UnionFind) (i : Nat) :
     rankD self.arr i < self.rankMax := by

From 58b15585c1480b5e9afcded83a36b8ea0a7d4a24 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 21 Nov 2024 08:31:05 +1100
Subject: [PATCH 06/42] fix, mostly by commenting out

---
 Batteries/Data/Array/Basic.lean     |  20 +--
 Batteries/Data/Array/Lemmas.lean    | 198 ++++++++++++++--------------
 Batteries/Data/Range/Lemmas.lean    | 105 ++++++++-------
 Batteries/Data/UnionFind/Basic.lean |   2 +-
 Batteries/Data/Vector/Basic.lean    |  53 ++++----
 lean-toolchain                      |   2 +-
 6 files changed, 184 insertions(+), 196 deletions(-)

diff --git a/Batteries/Data/Array/Basic.lean b/Batteries/Data/Array/Basic.lean
index 8be0bc967d..5631aa3628 100644
--- a/Batteries/Data/Array/Basic.lean
+++ b/Batteries/Data/Array/Basic.lean
@@ -155,25 +155,7 @@ Automatically generates proof of `i < a.size` with `get_elem_tactic` where feasi
 abbrev swapAtN (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) :
     α × Array α := swapAt a ⟨i,h⟩ x
 
-/--
-`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
 
diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
index 2613cbc4f3..7b17fc17fb 100644
--- a/Batteries/Data/Array/Lemmas.lean
+++ b/Batteries/Data/Array/Lemmas.lean
@@ -71,12 +71,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 -/
 
@@ -93,96 +90,99 @@ theorem map_empty (f : α → β) : map f #[] = #[] := mapM_empty f
 
 theorem mem_singleton : a ∈ #[b] ↔ a = b := by simp
 
-/-! ### 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
-  split
-  · rw [size_insertAt_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
-  · 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
+-- FIXME: temporarily commented out; I've broken this on nightly-2024-11-20,
+-- and am hoping it is not necessary to get Mathlib working again
+
+-- /-! ### 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
+--   split
+--   · rw [size_insertAt_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
+--   · 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
diff --git a/Batteries/Data/Range/Lemmas.lean b/Batteries/Data/Range/Lemmas.lean
index a075e0b6b4..c25ace6c31 100644
--- a/Batteries/Data/Range/Lemmas.lean
+++ b/Batteries/Data/Range/Lemmas.lean
@@ -45,55 +45,58 @@ theorem mem_range'_elems (r : Range) (h : x ∈ List.range' r.start r.numElems r
     refine Nat.not_le.1 fun h =>
       Nat.not_le.2 h' <| (numElems_le_iff (Nat.pos_of_ne_zero step0)).2 h
 
-theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range)
-    (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) :
-    forIn' r init f =
-    forIn
-      ((List.range' r.start r.numElems r.step).pmap Subtype.mk fun _ => mem_range'_elems r)
-      init (fun ⟨a, h⟩ => f a h) := by
-  let ⟨start, stop, step⟩ := r
-  let L := List.range' start (numElems ⟨start, stop, step⟩) step
-  let f' : { a // start ≤ a ∧ a < stop } → _ := fun ⟨a, h⟩ => f a h
-  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
-    · 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 [*])
-      | succ n ih => simp [ih (List.forall_mem_cons.1 H).2]; rfl
-    · next step0 =>
-      have hstep := Nat.pos_of_ne_zero step0
-      suffices ∀ fuel l i hle H, l ≤ fuel →
-          (∀ j, stop ≤ i + step * j ↔ l ≤ j) → ∀ init,
-          forIn'.loop start stop step f fuel i hle init =
-          forIn ((List.range' i l step).pmap Subtype.mk H) init f' by
-        refine this _ _ _ _ _
-          ((numElems_le_iff hstep).2 (Nat.le_trans ?_ (Nat.le_add_left ..)))
-          (fun _ => (numElems_le_iff hstep).symm) _
-        conv => lhs; rw [← Nat.one_mul stop]
-        exact Nat.mul_le_mul_right stop hstep
-      intro fuel; induction fuel with intro l i hle H h1 h2 init
-      | zero => simp [forIn'.loop, Nat.le_zero.1 h1]
-      | succ fuel ih =>
-        cases l with
-        | zero => rw [forIn'.loop]; simp [Nat.not_lt.2 <| by simpa using (h2 0).2 (Nat.le_refl _)]
-        | succ l =>
-          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
-  else
-    simp [List.range', h, numElems_stop_le_start ⟨start, stop, step⟩ (Nat.not_lt.1 h), L]
-    cases stop <;> unfold forIn'.loop <;> simp [List.forIn', h]
+-- FIXME: temporarily commented out; I've broken this on nightly-2024-11-20,
+-- and am hoping it is not necessary to get Mathlib working again
+
+-- theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range)
+--     (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) :
+--     forIn' r init f =
+--     forIn
+--       ((List.range' r.start r.numElems r.step).pmap Subtype.mk fun _ => mem_range'_elems r)
+--       init (fun ⟨a, h⟩ => f a h) := by
+--   let ⟨start, stop, step⟩ := r
+--   let L := List.range' start (numElems ⟨start, stop, step⟩) step
+--   let f' : { a // start ≤ a ∧ a < stop } → _ := fun ⟨a, h⟩ => f a h
+--   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
+--     · 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 [*])
+--       | succ n ih => simp [ih (List.forall_mem_cons.1 H).2]; rfl
+--     · next step0 =>
+--       have hstep := Nat.pos_of_ne_zero step0
+--       suffices ∀ fuel l i hle H, l ≤ fuel →
+--           (∀ j, stop ≤ i + step * j ↔ l ≤ j) → ∀ init,
+--           forIn'.loop start stop step f fuel i hle init =
+--           forIn ((List.range' i l step).pmap Subtype.mk H) init f' by
+--         refine this _ _ _ _ _
+--           ((numElems_le_iff hstep).2 (Nat.le_trans ?_ (Nat.le_add_left ..)))
+--           (fun _ => (numElems_le_iff hstep).symm) _
+--         conv => lhs; rw [← Nat.one_mul stop]
+--         exact Nat.mul_le_mul_right stop hstep
+--       intro fuel; induction fuel with intro l i hle H h1 h2 init
+--       | zero => simp [forIn'.loop, Nat.le_zero.1 h1]
+--       | succ fuel ih =>
+--         cases l with
+--         | zero => rw [forIn'.loop]; simp [Nat.not_lt.2 <| by simpa using (h2 0).2 (Nat.le_refl _)]
+--         | succ l =>
+--           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
+--   else
+--     simp [List.range', h, numElems_stop_le_start ⟨start, stop, step⟩ (Nat.not_lt.1 h), L]
+--     cases stop <;> unfold forIn'.loop <;> simp [List.forIn', h]
 
-theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
-    (init : β) (f : Nat → β → m (ForInStep β)) :
-    forIn r init f = forIn (List.range' r.start r.numElems r.step) init f := by
-  refine Eq.trans ?_ <| (forIn'_eq_forIn_range' r init (fun x _ => f x)).trans ?_
-  · simp [forIn, forIn']
-  · suffices ∀ L H, forIn (List.pmap Subtype.mk L H) init (f ·.1) = forIn L init f from this _ ..
-    intro L; induction L generalizing init <;> intro H <;> simp [*]
+-- theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
+--     (init : β) (f : Nat → β → m (ForInStep β)) :
+--     forIn r init f = forIn (List.range' r.start r.numElems r.step) init f := by
+--   refine Eq.trans ?_ <| (forIn'_eq_forIn_range' r init (fun x _ => f x)).trans ?_
+--   · simp [forIn, forIn']
+--   · suffices ∀ L H, forIn (List.pmap Subtype.mk L H) init (f ·.1) = forIn L init f from this _ ..
+--     intro L; induction L generalizing init <;> intro H <;> simp [*]
diff --git a/Batteries/Data/UnionFind/Basic.lean b/Batteries/Data/UnionFind/Basic.lean
index cefa85bf3c..3a523e4f9d 100644
--- a/Batteries/Data/UnionFind/Basic.lean
+++ b/Batteries/Data/UnionFind/Basic.lean
@@ -146,7 +146,7 @@ theorem rank'_lt_rankMax (self : UnionFind) (i : Nat) (h) : (self.arr[i]).rank <
     | 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_toList]
-  exact Nat.lt_succ.2 <| go (self.arr.toList.get_mem i h)
+  exact Nat.lt_succ.2 <| go (self.arr.toList.getElem_mem h)
 
 theorem rankD_lt_rankMax (self : UnionFind) (i : Nat) :
     rankD self.arr i < self.rankMax := by
diff --git a/Batteries/Data/Vector/Basic.lean b/Batteries/Data/Vector/Basic.lean
index 73a4a41aee..7dd2abc78c 100644
--- a/Batteries/Data/Vector/Basic.lean
+++ b/Batteries/Data/Vector/Basic.lean
@@ -263,31 +263,34 @@ proof_wanted instLawfulBEq (α n) [BEq α] [LawfulBEq α] : LawfulBEq (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⟩
+-- FIXME: temporarily commented out; I've broken this on nightly-2024-11-20,
+-- and am hoping it is not necessary to get Mathlib working again
+
+-- /-- 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
diff --git a/lean-toolchain b/lean-toolchain
index 80611d83b2..118d9e578a 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-19
+leanprover/lean4:nightly-2024-11-20

From 9b9f4d0406d00baaae62d1a717b5aa854a2ae51d Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 21 Nov 2024 08:36:48 +1100
Subject: [PATCH 07/42] long lines

---
 Batteries/Data/Range/Lemmas.lean | 106 ++++++++++++++++---------------
 Batteries/Data/Vector/Basic.lean |  54 ++++++++--------
 2 files changed, 84 insertions(+), 76 deletions(-)

diff --git a/Batteries/Data/Range/Lemmas.lean b/Batteries/Data/Range/Lemmas.lean
index c25ace6c31..cba6bae84c 100644
--- a/Batteries/Data/Range/Lemmas.lean
+++ b/Batteries/Data/Range/Lemmas.lean
@@ -48,55 +48,59 @@ theorem mem_range'_elems (r : Range) (h : x ∈ List.range' r.start r.numElems r
 -- FIXME: temporarily commented out; I've broken this on nightly-2024-11-20,
 -- and am hoping it is not necessary to get Mathlib working again
 
--- theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range)
---     (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) :
---     forIn' r init f =
---     forIn
---       ((List.range' r.start r.numElems r.step).pmap Subtype.mk fun _ => mem_range'_elems r)
---       init (fun ⟨a, h⟩ => f a h) := by
---   let ⟨start, stop, step⟩ := r
---   let L := List.range' start (numElems ⟨start, stop, step⟩) step
---   let f' : { a // start ≤ a ∧ a < stop } → _ := fun ⟨a, h⟩ => f a h
---   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
---     · 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 [*])
---       | succ n ih => simp [ih (List.forall_mem_cons.1 H).2]; rfl
---     · next step0 =>
---       have hstep := Nat.pos_of_ne_zero step0
---       suffices ∀ fuel l i hle H, l ≤ fuel →
---           (∀ j, stop ≤ i + step * j ↔ l ≤ j) → ∀ init,
---           forIn'.loop start stop step f fuel i hle init =
---           forIn ((List.range' i l step).pmap Subtype.mk H) init f' by
---         refine this _ _ _ _ _
---           ((numElems_le_iff hstep).2 (Nat.le_trans ?_ (Nat.le_add_left ..)))
---           (fun _ => (numElems_le_iff hstep).symm) _
---         conv => lhs; rw [← Nat.one_mul stop]
---         exact Nat.mul_le_mul_right stop hstep
---       intro fuel; induction fuel with intro l i hle H h1 h2 init
---       | zero => simp [forIn'.loop, Nat.le_zero.1 h1]
---       | succ fuel ih =>
---         cases l with
---         | zero => rw [forIn'.loop]; simp [Nat.not_lt.2 <| by simpa using (h2 0).2 (Nat.le_refl _)]
---         | succ l =>
---           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
---   else
---     simp [List.range', h, numElems_stop_le_start ⟨start, stop, step⟩ (Nat.not_lt.1 h), L]
---     cases stop <;> unfold forIn'.loop <;> simp [List.forIn', h]
+/-
+
+theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range)
+    (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) :
+    forIn' r init f =
+    forIn
+      ((List.range' r.start r.numElems r.step).pmap Subtype.mk fun _ => mem_range'_elems r)
+      init (fun ⟨a, h⟩ => f a h) := by
+  let ⟨start, stop, step⟩ := r
+  let L := List.range' start (numElems ⟨start, stop, step⟩) step
+  let f' : { a // start ≤ a ∧ a < stop } → _ := fun ⟨a, h⟩ => f a h
+  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
+    · 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 [*])
+      | succ n ih => simp [ih (List.forall_mem_cons.1 H).2]; rfl
+    · next step0 =>
+      have hstep := Nat.pos_of_ne_zero step0
+      suffices ∀ fuel l i hle H, l ≤ fuel →
+          (∀ j, stop ≤ i + step * j ↔ l ≤ j) → ∀ init,
+          forIn'.loop start stop step f fuel i hle init =
+          forIn ((List.range' i l step).pmap Subtype.mk H) init f' by
+        refine this _ _ _ _ _
+          ((numElems_le_iff hstep).2 (Nat.le_trans ?_ (Nat.le_add_left ..)))
+          (fun _ => (numElems_le_iff hstep).symm) _
+        conv => lhs; rw [← Nat.one_mul stop]
+        exact Nat.mul_le_mul_right stop hstep
+      intro fuel; induction fuel with intro l i hle H h1 h2 init
+      | zero => simp [forIn'.loop, Nat.le_zero.1 h1]
+      | succ fuel ih =>
+        cases l with
+        | zero => rw [forIn'.loop]; simp [Nat.not_lt.2 <| by simpa using (h2 0).2 (Nat.le_refl _)]
+        | succ l =>
+          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
+  else
+    simp [List.range', h, numElems_stop_le_start ⟨start, stop, step⟩ (Nat.not_lt.1 h), L]
+    cases stop <;> unfold forIn'.loop <;> simp [List.forIn', h]
 
--- theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
---     (init : β) (f : Nat → β → m (ForInStep β)) :
---     forIn r init f = forIn (List.range' r.start r.numElems r.step) init f := by
---   refine Eq.trans ?_ <| (forIn'_eq_forIn_range' r init (fun x _ => f x)).trans ?_
---   · simp [forIn, forIn']
---   · suffices ∀ L H, forIn (List.pmap Subtype.mk L H) init (f ·.1) = forIn L init f from this _ ..
---     intro L; induction L generalizing init <;> intro H <;> simp [*]
+theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
+    (init : β) (f : Nat → β → m (ForInStep β)) :
+    forIn r init f = forIn (List.range' r.start r.numElems r.step) init f := by
+  refine Eq.trans ?_ <| (forIn'_eq_forIn_range' r init (fun x _ => f x)).trans ?_
+  · simp [forIn, forIn']
+  · suffices ∀ L H, forIn (List.pmap Subtype.mk L H) init (f ·.1) = forIn L init f from this _ ..
+    intro L; induction L generalizing init <;> intro H <;> simp [*]
+
+-/
diff --git a/Batteries/Data/Vector/Basic.lean b/Batteries/Data/Vector/Basic.lean
index 7dd2abc78c..f87dc73523 100644
--- a/Batteries/Data/Vector/Basic.lean
+++ b/Batteries/Data/Vector/Basic.lean
@@ -266,31 +266,35 @@ proof_wanted instLawfulBEq (α n) [BEq α] [LawfulBEq α] : LawfulBEq (Vector α
 -- FIXME: temporarily commented out; I've broken this on nightly-2024-11-20,
 -- and am hoping it is not necessary to get Mathlib working again
 
--- /-- 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⟩
+/-
+
+/-- 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

From d65361579d743e5f201d980b165faf4eadda67b1 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 21 Nov 2024 09:10:32 +1100
Subject: [PATCH 08/42] fix up vector

---
 Batteries/Data/Vector/Basic.lean | 22 +++++++---------------
 1 file changed, 7 insertions(+), 15 deletions(-)

diff --git a/Batteries/Data/Vector/Basic.lean b/Batteries/Data/Vector/Basic.lean
index f87dc73523..41bbffda8f 100644
--- a/Batteries/Data/Vector/Basic.lean
+++ b/Batteries/Data/Vector/Basic.lean
@@ -266,16 +266,15 @@ proof_wanted instLawfulBEq (α n) [BEq α] [LawfulBEq α] : LawfulBEq (Vector α
 -- FIXME: temporarily commented out; I've broken this on nightly-2024-11-20,
 -- and am hoping it is not necessary to get Mathlib working again
 
-/-
-
-/-- 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 and a tactic provided proof. -/
+@[inline] def eraseIdx (v : Vector α n) (i : Nat) (h : i < n := by get_elem_tactic) :
+    Vector α (n-1) :=
+  ⟨v.toArray.eraseIdx i (v.size_toArray.symm ▸ h), by simp [Array.size_eraseIdx]⟩
 
 /-- Delete an element of a vector using a `Nat` index. Panics if the index is out of bounds. -/
 @[inline] def eraseIdx! (v : Vector α n) (i : Nat) : Vector α (n-1) :=
   if _ : i < n then
-    ⟨v.toArray.eraseIdx i, by simp [*]⟩
+    v.eraseIdx i
   else
     have : Inhabited (Vector α (n-1)) := ⟨v.pop⟩
     panic! "index out of bounds"
@@ -283,18 +282,11 @@ proof_wanted instLawfulBEq (α n) [BEq α] [LawfulBEq α] : LawfulBEq (Vector α
 /-- 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 [*]⟩
+    v.eraseIdx 0
   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⟩
-
--/
+@[deprecated (since := "2024-11-20")] alias eraseIdxN := eraseIdx
 
 /--
 Finds the first index of a given value in a vector using `==` for comparison. Returns `none` if the

From 0f31de78320c48f58277e00db99676f114e90ccd Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 21 Nov 2024 15:34:08 +1100
Subject: [PATCH 09/42] .

---
 Batteries/Data/Array/Lemmas.lean | 288 +++++++++++++++++++++----------
 Batteries/Data/Vector/Basic.lean |   3 -
 2 files changed, 195 insertions(+), 96 deletions(-)

diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
index 7b17fc17fb..2ffc4a1229 100644
--- a/Batteries/Data/Array/Lemmas.lean
+++ b/Batteries/Data/Array/Lemmas.lean
@@ -93,96 +93,198 @@ theorem mem_singleton : a ∈ #[b] ↔ a = b := by simp
 -- FIXME: temporarily commented out; I've broken this on nightly-2024-11-20,
 -- and am hoping it is not necessary to get Mathlib working again
 
--- /-! ### 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
---   split
---   · rw [size_insertAt_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
---   · 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
+/-! ### insertAt -/
+
+@[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_insertIdx_loop, size_swap]
+  · rfl
+
+@[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]
+
+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
+
+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]
+    simp only [Fin.getElem_fin]
+    split <;> rename_i h₂
+    · rw [if_neg (by omega), if_neg (by omega)]
+      have t : k ≤ j := by omega
+      simp [t]
+    · rw [getElem_swap]
+      simp only [Fin.getElem_fin]
+      rw [if_neg (by omega)]
+      split <;> rename_i h₃
+      · simp [h₃]
+      · 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 ∨ k - 1 ≥ as.size then
+          v
+        else
+          as[k - 1] := by
+  unfold insertIdx
+  rw [getElem_insertIdx_loop]
+  simp at h'
+  replace h' : k ≤ as.size := by omega
+  simp [h, h', getElem_push]
+  split <;> rename_i h₁
+  · rw [dif_pos (by omega)]
+  · split <;> rename_i h₂
+    · simp [h₂]
+    · split <;> rename_i h₃
+      · rw [dif_neg]
+        omega
+      · rw [dif_pos]
+        omega
+
+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
+  · 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
diff --git a/Batteries/Data/Vector/Basic.lean b/Batteries/Data/Vector/Basic.lean
index 41bbffda8f..315e8b932f 100644
--- a/Batteries/Data/Vector/Basic.lean
+++ b/Batteries/Data/Vector/Basic.lean
@@ -263,9 +263,6 @@ proof_wanted instLawfulBEq (α n) [BEq α] [LawfulBEq α] : LawfulBEq (Vector α
 @[inline] def reverse (v : Vector α n) : Vector α n :=
   ⟨v.toArray.reverse, by simp⟩
 
--- FIXME: temporarily commented out; I've broken this on nightly-2024-11-20,
--- and am hoping it is not necessary to get Mathlib working again
-
 /-- Delete an element of a vector using a `Nat` index and a tactic provided proof. -/
 @[inline] def eraseIdx (v : Vector α n) (i : Nat) (h : i < n := by get_elem_tactic) :
     Vector α (n-1) :=

From a46ce3df7fe4a66f3bbbdcaf43acdf063da0b304 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 21 Nov 2024 15:41:41 +1100
Subject: [PATCH 10/42] rewrite insertIdx theorems

---
 Batteries/Data/Array/Lemmas.lean | 120 ++++++++-----------------------
 1 file changed, 30 insertions(+), 90 deletions(-)

diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
index 2ffc4a1229..a86a6107f9 100644
--- a/Batteries/Data/Array/Lemmas.lean
+++ b/Batteries/Data/Array/Lemmas.lean
@@ -90,9 +90,6 @@ theorem map_empty (f : α → β) : map f #[] = #[] := mapM_empty f
 
 theorem mem_singleton : a ∈ #[b] ↔ a = b := by simp
 
--- FIXME: temporarily commented out; I've broken this on nightly-2024-11-20,
--- and am hoping it is not necessary to get Mathlib working again
-
 /-! ### insertAt -/
 
 @[simp] private theorem size_insertIdx_loop (as : Array α) (i : Nat) (j : Fin as.size) :
@@ -106,6 +103,8 @@ theorem mem_singleton : a ∈ #[b] ↔ a = b := by simp
     (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
@@ -189,102 +188,43 @@ theorem getElem_insertIdx (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α)
       if h₁ : k < i then
         as[k]'(by omega)
       else
-        if h₂ : k = i ∨ k - 1 ≥ as.size then
+        if h₂ : k = i then
           v
         else
-          as[k - 1] := by
+          as[k - 1]'(by simp at h'; omega) := by
   unfold insertIdx
   rw [getElem_insertIdx_loop]
-  simp at h'
+  simp only [size_insertIdx] at h'
   replace h' : k ≤ as.size := by omega
-  simp [h, h', getElem_push]
+  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₃
-      · rw [dif_neg]
-        omega
-      · rw [dif_pos]
-        omega
-
-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
-  · rfl
+      · rfl
+      · omega
 
-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
+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]
 
-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
+@[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

From ecb1399feb18d6d1cca39467fde5a101b4ce43d4 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 21 Nov 2024 15:45:42 +1100
Subject: [PATCH 11/42] long line

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

diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
index a86a6107f9..58509c2fb9 100644
--- a/Batteries/Data/Array/Lemmas.lean
+++ b/Batteries/Data/Array/Lemmas.lean
@@ -139,8 +139,8 @@ theorem getElem_insertIdx_loop_eq {as : Array α} {i : Nat} {j : Nat} {hj : j <
     · 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) :
+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

From 71894b60a7141fc616dbc80eb84f1d6adc2e8468 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 21 Nov 2024 15:50:02 +1100
Subject: [PATCH 12/42] fix

---
 Batteries/Tactic/Lint/Simp.lean | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/Batteries/Tactic/Lint/Simp.lean b/Batteries/Tactic/Lint/Simp.lean
index c2122689cf..3e83431dcc 100644
--- a/Batteries/Tactic/Lint/Simp.lean
+++ b/Batteries/Tactic/Lint/Simp.lean
@@ -108,11 +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
-<<<<<<< HEAD
-    let ctx := ← Simp.Context.mkDefault
-=======
     let ctx ← Simp.Context.mkDefault
->>>>>>> nightly-testing
     checkAllSimpTheoremInfos (← getConstInfo declName).type fun {lhs, rhs, isConditional, ..} => do
       let isRfl ← isRflTheorem declName
       let ({ expr := lhs', proof? := prf1, .. }, prf1Stats) ←

From 61a9b88e24abb28c8cd2fdce4eee1eca3960480d Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 21 Nov 2024 15:51:26 +1100
Subject: [PATCH 13/42] chore: adaptations for nightly-2024-11-18 (#1053)

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
---
 Batteries/Data/Array/Lemmas.lean    |  6 ------
 Batteries/Tactic/Instances.lean     |  2 +-
 Batteries/Tactic/Lint/Frontend.lean |  7 ++-----
 Batteries/Tactic/Lint/Simp.lean     |  6 +++---
 Batteries/Tactic/Trans.lean         |  9 +++------
 Batteries/Util/Cache.lean           |  5 +----
 BatteriesTest/lint_simpNF.lean      | 13 +++++++++++++
 lean-toolchain                      |  2 +-
 8 files changed, 24 insertions(+), 26 deletions(-)

diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
index daf0493b88..2613cbc4f3 100644
--- a/Batteries/Data/Array/Lemmas.lean
+++ b/Batteries/Data/Array/Lemmas.lean
@@ -93,12 +93,6 @@ theorem map_empty (f : α → β) : map f #[] = #[] := mapM_empty f
 
 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) :
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 88ad7a1bc2..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
+    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/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/lean-toolchain b/lean-toolchain
index 97bb2ffae1..585547139e 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-14
+leanprover/lean4:nightly-2024-11-18

From a822446d61ad7e7f5e843365c7041c326553050a Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 21 Nov 2024 15:53:39 +1100
Subject: [PATCH 14/42] chore: cleanup breaking non-terminal simps (#1057)

---
 Batteries/Data/Range/Lemmas.lean | 18 +++++++++++++-----
 1 file changed, 13 insertions(+), 5 deletions(-)

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)

From b3935d53ce8dad5665af7ac41f06f0f6de4d942f Mon Sep 17 00:00:00 2001
From: leanprover-community-mathlib4-bot
 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Date: Thu, 21 Nov 2024 09:05:56 +0000
Subject: [PATCH 15/42] chore: bump to nightly-2024-11-21

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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