diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index badd90415b..0fd20c4e0e 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -45,16 +45,6 @@ theorem getElem?_eq_getElem?_toList (a : Array α) (i : Nat) : a[i]? = a.toList[
   rw [getElem?_eq]
   split <;> simp_all
 
-@[deprecated getElem_eq_getElem_toList (since := "2024-09-25")]
-abbrev getElem_eq_toList_getElem := @getElem_eq_getElem_toList
-
-@[deprecated getElem_eq_toList_getElem (since := "2024-09-09")]
-abbrev getElem_eq_data_getElem := @getElem_eq_getElem_toList
-
-@[deprecated getElem_eq_toList_getElem (since := "2024-06-12")]
-theorem getElem_eq_toList_get (a : Array α) (h : i < a.size) : a[i] = a.toList.get ⟨i, h⟩ := by
-  simp
-
 theorem get_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
     have : i < (a.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
     (a.push x)[i] = a[i] := by
@@ -77,7 +67,10 @@ namespace List
 
 open Array
 
-/-! ### Lemmas about `List.toArray`. -/
+/-! ### Lemmas about `List.toArray`.
+
+We prefer to pull `List.toArray` outwards.
+-/
 
 @[simp] theorem size_toArrayAux {a : List α} {b : Array α} :
     (a.toArrayAux b).size = b.size + a.length := by
@@ -85,20 +78,11 @@ open Array
 
 @[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
 
-@[deprecated toArray_toList (since := "2024-09-09")]
-abbrev toArray_data := @toArray_toList
-
 @[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
     a.toArray[i] = a[i]'(by simpa using h) := rfl
 
 @[simp] theorem getElem?_toArray {a : List α} {i : Nat} : a.toArray[i]? = a[i]? := rfl
 
-@[deprecated "Use the reverse direction of `List.push_toArray`." (since := "2024-09-27")]
-theorem toArray_concat {as : List α} {x : α} :
-    (as ++ [x]).toArray = as.toArray.push x := by
-  apply ext'
-  simp
-
 @[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
   apply ext'
   simp
@@ -163,20 +147,12 @@ end List
 
 namespace Array
 
-attribute [simp] uset
-
 @[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
 
 @[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
 
-@[deprecated toArray_toList (since := "2024-09-09")]
-abbrev toArray_data := @toArray_toList
-
 @[simp] theorem length_toList {l : Array α} : l.toList.length = l.size := rfl
 
-@[deprecated length_toList (since := "2024-09-09")]
-abbrev data_length := @length_toList
-
 @[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
 
 @[simp] theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
@@ -225,9 +201,6 @@ where
     induction l generalizing arr <;> simp [*]
   simp [H]
 
-@[deprecated toList_map (since := "2024-09-09")]
-abbrev map_data := @toList_map
-
 @[simp] theorem size_map (f : α → β) (arr : Array α) : (arr.map f).size = arr.size := by
   simp only [← length_toList]
   simp
@@ -248,21 +221,10 @@ theorem foldl_toList_eq_flatMap (l : List α) (acc : Array β)
     (l.foldl F acc).toList = acc.toList ++ l.flatMap G := by
   induction l generalizing acc <;> simp [*, List.flatMap]
 
-@[deprecated foldl_toList_eq_flatMap (since := "2024-10-16")]
-abbrev foldl_toList_eq_bind := @foldl_toList_eq_flatMap
-
-@[deprecated foldl_toList_eq_flatMap (since := "2024-10-16")]
-abbrev foldl_data_eq_bind := @foldl_toList_eq_flatMap
-
 theorem foldl_toList_eq_map (l : List α) (acc : Array β) (G : α → β) :
     (l.foldl (fun acc a => acc.push (G a)) acc).toList = acc.toList ++ l.map G := by
   induction l generalizing acc <;> simp [*]
 
-@[deprecated foldl_toList_eq_map (since := "2024-09-09")]
-abbrev foldl_data_eq_map := @foldl_toList_eq_map
-
-theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by simp
-
 theorem anyM_eq_anyM_loop [Monad m] (p : α → m Bool) (as : Array α) (start stop) :
     anyM p as start stop = anyM.loop p as (min stop as.size) (Nat.min_le_right ..) start := by
   simp only [anyM, Nat.min_def]; split <;> rfl
@@ -277,6 +239,12 @@ theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
 @[simp] theorem not_mem_empty (a : α) : ¬(a ∈ #[]) := by
   simp [mem_def]
 
+/-! # uset -/
+
+attribute [simp] uset
+
+theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by simp
+
 /-! # get -/
 
 @[simp] theorem get_eq_getElem (a : Array α) (i : Fin _) : a.get i = a[i.1] := rfl
@@ -396,6 +364,10 @@ termination_by n - i
     (ofFn f)[i] = f ⟨i, size_ofFn f ▸ h⟩ :=
   getElem_ofFn_go _ _ _ (by simp) (by simp) nofun
 
+theorem getElem?_ofFn (f : Fin n → α) (i : Nat) :
+    (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none := by
+  simp [getElem?_def]
+
 /-- # mkArray -/
 
 @[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
@@ -403,19 +375,17 @@ termination_by n - i
 
 @[simp] theorem toList_mkArray (n : Nat) (v : α) : (mkArray n v).toList = List.replicate n v := rfl
 
-@[deprecated toList_mkArray (since := "2024-09-09")]
-abbrev mkArray_data := @toList_mkArray
-
 @[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
     (mkArray n v)[i] = v := by simp [Array.getElem_eq_getElem_toList]
 
+theorem getElem?_mkArray (n : Nat) (v : α) (i : Nat) :
+    (mkArray n v)[i]? = if i < n then some v else none := by
+  simp [getElem?_def]
+
 /-- # mem -/
 
 theorem mem_toList {a : α} {l : Array α} : a ∈ l.toList ↔ a ∈ l := mem_def.symm
 
-@[deprecated mem_toList (since := "2024-09-09")]
-abbrev mem_data := @mem_toList
-
 theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun
 
 theorem getElem_of_mem {a : α} {as : Array α} :
@@ -425,6 +395,12 @@ theorem getElem_of_mem {a : α} {as : Array α} :
   exists i
   exists hbound
 
+theorem getElem?_of_mem {a : α} {as : Array α} :
+    a ∈ as → ∃ (n : Nat), as[n]? = some a := by
+  intro ha
+  rcases List.getElem?_of_mem ha.val with ⟨i, hi⟩
+  exists i
+
 @[simp] theorem mem_dite_empty_left {x : α} [Decidable p] {l : ¬ p → Array α} :
     (x ∈ if h : p then #[] else l h) ↔ ∃ h : ¬ p, x ∈ l h := by
   split <;> simp_all [mem_def]
@@ -447,14 +423,11 @@ theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size}
     idx < a.size :=
   hidx
 
-theorem getElem?_mem {l : Array α} {i : Fin l.size} : l[i] ∈ l := by
+theorem getElem_mem {l : Array α} {i : Nat} (h : i < l.size) : l[i] ∈ l := by
   erw [Array.mem_def, getElem_eq_getElem_toList]
   apply List.get_mem
 
-theorem getElem_fin_eq_toList_get (a : Array α) (i : Fin _) : a[i] = a.toList.get i := rfl
-
-@[deprecated getElem_fin_eq_toList_get (since := "2024-09-09")]
-abbrev getElem_fin_eq_data_get := @getElem_fin_eq_toList_get
+theorem getElem_fin_eq_getElem_toList (a : Array α) (i : Fin a.size) : a[i] = a.toList[i] := rfl
 
 @[simp] theorem ugetElem_eq_getElem (a : Array α) {i : USize} (h : i.toNat < a.size) :
   a[i] = a[i.toNat] := rfl
@@ -465,26 +438,8 @@ theorem get?_len_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none :
 theorem getElem_mem_toList (a : Array α) (h : i < a.size) : a[i] ∈ a.toList := by
   simp only [getElem_eq_getElem_toList, List.getElem_mem]
 
-@[deprecated getElem_mem_toList (since := "2024-09-09")]
-abbrev getElem_mem_data := @getElem_mem_toList
-
-theorem getElem?_eq_toList_getElem? (a : Array α) (i : Nat) : a[i]? = a.toList[i]? := by
-  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg]
-
-@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-30")]
-theorem getElem?_eq_toList_get? (a : Array α) (i : Nat) : a[i]? = a.toList.get? i := by
-  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]
-
-set_option linter.deprecated false in
-@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-09")]
-abbrev getElem?_eq_data_get? := @getElem?_eq_toList_get?
-
-set_option linter.deprecated false in
-theorem get?_eq_toList_get? (a : Array α) (i : Nat) : a.get? i = a.toList.get? i :=
-  getElem?_eq_toList_get? ..
-
-@[deprecated get?_eq_toList_get? (since := "2024-09-09")]
-abbrev get?_eq_data_get? := @get?_eq_toList_get?
+theorem get?_eq_get?_toList (a : Array α) (i : Nat) : a.get? i = a.toList.get? i := by
+  simp [getElem?_eq_getElem?_toList]
 
 theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
   simp [get!_eq_getD]
@@ -497,7 +452,7 @@ theorem getElem?_eq_some_iff {as : Array α} : as[n]? = some a ↔ ∃ h : n < a
   simp [back, back?]
 
 @[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
-  simp [back?, getElem?_eq_toList_getElem?]
+  simp [back?, getElem?_eq_getElem?_toList]
 
 theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp
 
@@ -528,9 +483,6 @@ theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x el
 
 @[simp] theorem toList_set (a : Array α) (i v) : (a.set i v).toList = a.toList.set i.1 v := rfl
 
-@[deprecated toList_set (since := "2024-09-09")]
-abbrev data_set := @toList_set
-
 theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
     (a.set i v)[i.1] = v := by
   simp only [set, getElem_eq_getElem_toList, List.getElem_set_self]
@@ -571,12 +523,9 @@ theorem swap_def (a : Array α) (i j : Fin a.size) :
 @[simp] theorem toList_swap (a : Array α) (i j : Fin a.size) :
     (a.swap i j).toList = (a.toList.set i (a.get j)).set j (a.get i) := by simp [swap_def]
 
-@[deprecated toList_swap (since := "2024-09-09")]
-abbrev data_swap := @toList_swap
-
-theorem get?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]? =
+theorem getElem?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]? =
     if j = k then some a[i.1] else if i = k then some a[j.1] else a[k]? := by
-  simp [swap_def, get?_set, ← getElem_fin_eq_toList_get]
+  simp [swap_def, get?_set, ← getElem_fin_eq_getElem_toList]
 
 @[simp] theorem swapAt_def (a : Array α) (i : Fin a.size) (v : α) :
     a.swapAt i v = (a[i.1], a.set i v) := rfl
@@ -594,9 +543,6 @@ theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
 
 @[simp] theorem toList_pop (a : Array α) : a.pop.toList = a.toList.dropLast := by simp [pop]
 
-@[deprecated toList_pop (since := "2024-09-09")]
-abbrev data_pop := @toList_pop
-
 @[simp] theorem pop_empty : (#[] : Array α).pop = #[] := rfl
 
 @[simp] theorem pop_push (a : Array α) : (a.push x).pop = a := by simp [pop]
@@ -629,9 +575,6 @@ theorem eq_push_of_size_ne_zero {as : Array α} (h : as.size ≠ 0) :
 
 theorem size_eq_length_toList (as : Array α) : as.size = as.toList.length := rfl
 
-@[deprecated size_eq_length_toList (since := "2024-09-09")]
-abbrev size_eq_length_data := @size_eq_length_toList
-
 @[simp] theorem size_swap! (a : Array α) (i j) :
     (a.swap! i j).size = a.size := by unfold swap!; split <;> (try split) <;> simp [size_swap]
 
@@ -656,14 +599,10 @@ abbrev size_eq_length_data := @size_eq_length_toList
 @[simp] theorem toList_range (n : Nat) : (range n).toList = List.range n := by
   induction n <;> simp_all [range, Nat.fold, flip, List.range_succ]
 
-@[deprecated toList_range (since := "2024-09-09")]
-abbrev data_range := @toList_range
-
 @[simp]
 theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Array.range n)[x] = x := by
   simp [getElem_eq_getElem_toList]
 
-set_option linter.deprecated false in
 @[simp] theorem toList_reverse (a : Array α) : a.reverse.toList = a.toList.reverse := by
   let rec go (as : Array α) (i j hj)
       (h : i + j + 1 = a.size) (h₂ : as.size = a.size)
@@ -676,9 +615,9 @@ set_option linter.deprecated false in
       · rwa [Nat.add_right_comm i]
       · simp [size_swap, h₂]
       · intro k
-        rw [← getElem?_eq_toList_getElem?, get?_swap]
+        rw [← getElem?_eq_getElem?_toList, getElem?_swap]
         simp only [H, getElem_eq_getElem_toList, ← List.getElem?_eq_getElem, Nat.le_of_lt h₁,
-          getElem?_eq_toList_getElem?]
+          getElem?_eq_getElem?_toList]
         split <;> rename_i h₂
         · simp only [← h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false]
           exact (List.getElem?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
@@ -705,9 +644,6 @@ set_option linter.deprecated false in
         true_and, Nat.not_lt] at h
       rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (a.toList.length_reverse ▸ ‹_›)]
 
-@[deprecated toList_reverse (since := "2024-09-30")]
-abbrev reverse_toList := @toList_reverse
-
 /-! ### foldl / foldr -/
 
 @[simp] theorem foldlM_loop_empty [Monad m] (f : β → α → m β) (init : β) (i j : Nat) :
@@ -736,7 +672,7 @@ abbrev reverse_toList := @toList_reverse
     foldrM f init #[] start stop = return init := by
   simp [foldrM]
 
--- This proof is the pure version of `Array.SatisfiesM_foldlM`,
+-- This proof is the pure version of `Array.SatisfiesM_foldlM` in Batteries,
 -- reproduced to avoid a dependency on `SatisfiesM`.
 theorem foldl_induction
     {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive 0 init) {f : β → α → β}
@@ -752,7 +688,7 @@ theorem foldl_induction
     · next hj => exact Nat.le_antisymm h₁ (Nat.ge_of_not_lt hj) ▸ H
   simpa [foldl, foldlM] using go (Nat.zero_le _) (Nat.le_refl _) h0
 
--- This proof is the pure version of `Array.SatisfiesM_foldrM`,
+-- This proof is the pure version of `Array.SatisfiesM_foldrM` in Batteries,
 -- reproduced to avoid a dependency on `SatisfiesM`.
 theorem foldr_induction
     {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive as.size init) {f : α → β → β}
@@ -798,9 +734,6 @@ theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : A
     toList <$> arr.mapM f = arr.toList.mapM f := by
   simp [mapM_eq_mapM_toList]
 
-@[deprecated mapM_eq_mapM_toList (since := "2024-09-09")]
-abbrev mapM_eq_mapM_data := @mapM_eq_mapM_toList
-
 theorem mapM_map_eq_foldl (as : Array α) (f : α → β) (i) :
     mapM.map (m := Id) f as i b = as.foldl (start := i) (fun r a => r.push (f a)) b := by
   unfold mapM.map
@@ -872,6 +805,12 @@ theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Pro
   · simp only [getElem_map, get_push, size_map]
     split <;> rfl
 
+@[simp] theorem map_pop {f : α → β} {as : Array α} :
+    as.pop.map f = (as.map f).pop := by
+  ext
+  · simp
+  · simp only [getElem_map, getElem_pop, size_map]
+
 /-! ### mapIdx -/
 
 -- This could also be proved from `SatisfiesM_mapIdxM` in Batteries.
@@ -945,12 +884,6 @@ theorem getElem_modify_of_ne {as : Array α} {i : Nat} (h : i ≠ j)
     (as.modify i f)[j] = as[j]'(by simpa using hj) := by
   simp [getElem_modify hj, h]
 
-@[deprecated getElem_modify (since := "2024-08-08")]
-theorem get_modify {arr : Array α} {x i} (h : i < (arr.modify x f).size) :
-    (arr.modify x f).get ⟨i, h⟩ =
-    if x = i then f (arr.get ⟨i, by simpa using h⟩) else arr.get ⟨i, by simpa using h⟩ := by
-  simp [getElem_modify h]
-
 /-! ### filter -/
 
 @[simp] theorem toList_filter (p : α → Bool) (l : Array α) :
@@ -964,9 +897,6 @@ theorem get_modify {arr : Array α} {x i} (h : i < (arr.modify x f).size) :
   induction l with simp
   | cons => split <;> simp [*]
 
-@[deprecated toList_filter (since := "2024-09-09")]
-abbrev filter_data := @toList_filter
-
 @[simp] theorem filter_filter (q) (l : Array α) :
     filter p (filter q l) = filter (fun a => p a && q a) l := by
   apply ext'
@@ -1000,9 +930,6 @@ theorem filter_congr {as bs : Array α} (h : as = bs)
   · simp_all [Id.run, List.filterMap_cons]
     split <;> simp_all
 
-@[deprecated toList_filterMap (since := "2024-09-09")]
-abbrev filterMap_data := @toList_filterMap
-
 @[simp] theorem mem_filterMap {f : α → Option β} {l : Array α} {b : β} :
     b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b := by
   simp only [mem_def, toList_filterMap, List.mem_filterMap]
@@ -1020,9 +947,6 @@ theorem size_empty : (#[] : Array α).size = 0 := rfl
 
 theorem toList_empty : (#[] : Array α).toList = [] := rfl
 
-@[deprecated toList_empty (since := "2024-09-09")]
-abbrev empty_data := @toList_empty
-
 /-! ### append -/
 
 theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] := rfl
@@ -1045,9 +969,6 @@ theorem getElem_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt :
   conv => rhs; rw [← List.getElem_append_left (bs := bs.toList) (h' := h')]
   apply List.get_of_eq; rw [toList_append]
 
-@[deprecated getElem_append_left (since := "2024-09-30")]
-abbrev get_append_left := @getElem_append_left
-
 theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i)
     (hlt : i - as.size < bs.size := Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) :
     (as ++ bs)[i] = bs[i - as.size] := by
@@ -1056,9 +977,6 @@ theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle :
   conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
   apply List.get_of_eq; rw [toList_append]
 
-@[deprecated getElem_append_right (since := "2024-09-30")]
-abbrev get_append_right := @getElem_append_right
-
 @[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by
   apply ext'; simp only [toList_append, toList_empty, List.append_nil]
 
@@ -1301,9 +1219,6 @@ theorem any_toList {p : α → Bool} (as : Array α) : as.toList.any p = as.any
   rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]; simp only [List.mem_iff_get]
   exact ⟨fun ⟨_, ⟨i, rfl⟩, h⟩ => ⟨i, h⟩, fun ⟨i, h⟩ => ⟨_, ⟨i, rfl⟩, h⟩⟩
 
-@[deprecated "Use the reverse direction of `Array.any_toList`" (since := "2024-09-30")]
-abbrev any_def := @any_toList
-
 /-! ### all -/
 
 theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) :
@@ -1343,9 +1258,6 @@ theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all
     rw [← getElem_eq_getElem_toList]
     exact w ⟨r, h⟩
 
-@[deprecated "Use the reverse direction of `Array.all_toList`" (since := "2024-09-30")]
-abbrev all_def := @all_toList
-
 theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by
   simp only [← all_toList, List.all_eq_true, mem_def]
 
@@ -1415,33 +1327,8 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
     · split <;> simp_all
     · split <;> simp_all
 
-@[deprecated getElem_extract_loop_lt_aux (since := "2024-09-30")]
-abbrev get_extract_loop_lt_aux := @getElem_extract_loop_lt_aux
-@[deprecated getElem_extract_loop_lt (since := "2024-09-30")]
-abbrev get_extract_loop_lt := @getElem_extract_loop_lt
-@[deprecated getElem_extract_loop_ge_aux (since := "2024-09-30")]
-abbrev get_extract_loop_ge_aux := @getElem_extract_loop_ge_aux
-@[deprecated getElem_extract_loop_ge (since := "2024-09-30")]
-abbrev get_extract_loop_ge := @getElem_extract_loop_ge
-@[deprecated getElem_extract_aux (since := "2024-09-30")]
-abbrev get_extract_aux := @getElem_extract_aux
-@[deprecated getElem_extract (since := "2024-09-30")]
-abbrev get_extract := @getElem_extract
-
-@[deprecated getElem_swap_right (since := "2024-09-30")]
-abbrev get_swap_right := @getElem_swap_right
-@[deprecated getElem_swap_left (since := "2024-09-30")]
-abbrev get_swap_left := @getElem_swap_left
-@[deprecated getElem_swap_of_ne (since := "2024-09-30")]
-abbrev get_swap_of_ne := @getElem_swap_of_ne
-@[deprecated getElem_swap (since := "2024-09-30")]
-abbrev get_swap := @getElem_swap
-@[deprecated getElem_swap' (since := "2024-09-30")]
-abbrev get_swap' := @getElem_swap'
-
 end Array
 
-
 open Array
 
 namespace List
@@ -1586,3 +1473,158 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
   simp
 
 end List
+
+/-! ### Deprecations -/
+
+namespace List
+
+@[deprecated toArray_toList (since := "2024-09-09")]
+abbrev toArray_data := @toArray_toList
+
+@[deprecated "Use the reverse direction of `List.push_toArray`." (since := "2024-09-27")]
+theorem toArray_concat {as : List α} {x : α} :
+    (as ++ [x]).toArray = as.toArray.push x := by
+  apply ext'
+  simp
+
+end List
+
+namespace Array
+
+@[deprecated getElem_eq_getElem_toList (since := "2024-09-25")]
+abbrev getElem_eq_toList_getElem := @getElem_eq_getElem_toList
+
+@[deprecated getElem_eq_toList_getElem (since := "2024-09-09")]
+abbrev getElem_eq_data_getElem := @getElem_eq_getElem_toList
+
+@[deprecated getElem_eq_toList_getElem (since := "2024-06-12")]
+theorem getElem_eq_toList_get (a : Array α) (h : i < a.size) : a[i] = a.toList.get ⟨i, h⟩ := by
+  simp
+
+@[deprecated toArray_toList (since := "2024-09-09")]
+abbrev toArray_data := @toArray_toList
+
+@[deprecated length_toList (since := "2024-09-09")]
+abbrev data_length := @length_toList
+
+@[deprecated toList_map (since := "2024-09-09")]
+abbrev map_data := @toList_map
+
+@[deprecated foldl_toList_eq_flatMap (since := "2024-10-16")]
+abbrev foldl_toList_eq_bind := @foldl_toList_eq_flatMap
+
+@[deprecated foldl_toList_eq_flatMap (since := "2024-10-16")]
+abbrev foldl_data_eq_bind := @foldl_toList_eq_flatMap
+
+@[deprecated foldl_toList_eq_map (since := "2024-09-09")]
+abbrev foldl_data_eq_map := @foldl_toList_eq_map
+
+@[deprecated toList_mkArray (since := "2024-09-09")]
+abbrev mkArray_data := @toList_mkArray
+
+@[deprecated mem_toList (since := "2024-09-09")]
+abbrev mem_data := @mem_toList
+
+@[deprecated getElem_mem (since := "2024-10-17")]
+abbrev getElem?_mem := @getElem_mem
+
+@[deprecated getElem_fin_eq_getElem_toList (since := "2024-10-17")]
+abbrev getElem_fin_eq_toList_get := @getElem_fin_eq_getElem_toList
+
+@[deprecated getElem_fin_eq_getElem_toList (since := "2024-09-09")]
+abbrev getElem_fin_eq_data_get := @getElem_fin_eq_getElem_toList
+
+@[deprecated getElem_mem_toList (since := "2024-09-09")]
+abbrev getElem_mem_data := @getElem_mem_toList
+
+@[deprecated getElem?_eq_getElem?_toList (since := "2024-10-17")]
+abbrev getElem?_eq_toList_getElem? := @getElem?_eq_getElem?_toList
+
+@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-30")]
+theorem getElem?_eq_toList_get? (a : Array α) (i : Nat) : a[i]? = a.toList.get? i := by
+  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]
+
+set_option linter.deprecated false in
+@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-09")]
+abbrev getElem?_eq_data_get? := @getElem?_eq_toList_get?
+
+@[deprecated get?_eq_get?_toList (since := "2024-10-17")]
+abbrev get?_eq_toList_get? := @get?_eq_get?_toList
+
+@[deprecated get?_eq_toList_get? (since := "2024-09-09")]
+abbrev get?_eq_data_get? := @get?_eq_get?_toList
+
+@[deprecated toList_set (since := "2024-09-09")]
+abbrev data_set := @toList_set
+
+@[deprecated toList_swap (since := "2024-09-09")]
+abbrev data_swap := @toList_swap
+
+@[deprecated getElem?_swap (since := "2024-10-17")] abbrev get?_swap := @getElem?_swap
+
+@[deprecated toList_pop (since := "2024-09-09")] abbrev data_pop := @toList_pop
+
+@[deprecated size_eq_length_toList (since := "2024-09-09")]
+abbrev size_eq_length_data := @size_eq_length_toList
+
+@[deprecated toList_range (since := "2024-09-09")]
+abbrev data_range := @toList_range
+
+@[deprecated toList_reverse (since := "2024-09-30")]
+abbrev reverse_toList := @toList_reverse
+
+@[deprecated mapM_eq_mapM_toList (since := "2024-09-09")]
+abbrev mapM_eq_mapM_data := @mapM_eq_mapM_toList
+
+@[deprecated getElem_modify (since := "2024-08-08")]
+theorem get_modify {arr : Array α} {x i} (h : i < (arr.modify x f).size) :
+    (arr.modify x f).get ⟨i, h⟩ =
+    if x = i then f (arr.get ⟨i, by simpa using h⟩) else arr.get ⟨i, by simpa using h⟩ := by
+  simp [getElem_modify h]
+
+@[deprecated toList_filter (since := "2024-09-09")]
+abbrev filter_data := @toList_filter
+
+@[deprecated toList_filterMap (since := "2024-09-09")]
+abbrev filterMap_data := @toList_filterMap
+
+@[deprecated toList_empty (since := "2024-09-09")]
+abbrev empty_data := @toList_empty
+
+@[deprecated getElem_append_left (since := "2024-09-30")]
+abbrev get_append_left := @getElem_append_left
+
+@[deprecated getElem_append_right (since := "2024-09-30")]
+abbrev get_append_right := @getElem_append_right
+
+@[deprecated "Use the reverse direction of `Array.any_toList`" (since := "2024-09-30")]
+abbrev any_def := @any_toList
+
+@[deprecated "Use the reverse direction of `Array.all_toList`" (since := "2024-09-30")]
+abbrev all_def := @all_toList
+
+@[deprecated getElem_extract_loop_lt_aux (since := "2024-09-30")]
+abbrev get_extract_loop_lt_aux := @getElem_extract_loop_lt_aux
+@[deprecated getElem_extract_loop_lt (since := "2024-09-30")]
+abbrev get_extract_loop_lt := @getElem_extract_loop_lt
+@[deprecated getElem_extract_loop_ge_aux (since := "2024-09-30")]
+abbrev get_extract_loop_ge_aux := @getElem_extract_loop_ge_aux
+@[deprecated getElem_extract_loop_ge (since := "2024-09-30")]
+abbrev get_extract_loop_ge := @getElem_extract_loop_ge
+@[deprecated getElem_extract_aux (since := "2024-09-30")]
+abbrev get_extract_aux := @getElem_extract_aux
+@[deprecated getElem_extract (since := "2024-09-30")]
+abbrev get_extract := @getElem_extract
+
+@[deprecated getElem_swap_right (since := "2024-09-30")]
+abbrev get_swap_right := @getElem_swap_right
+@[deprecated getElem_swap_left (since := "2024-09-30")]
+abbrev get_swap_left := @getElem_swap_left
+@[deprecated getElem_swap_of_ne (since := "2024-09-30")]
+abbrev get_swap_of_ne := @getElem_swap_of_ne
+@[deprecated getElem_swap (since := "2024-09-30")]
+abbrev get_swap := @getElem_swap
+@[deprecated getElem_swap' (since := "2024-09-30")]
+abbrev get_swap' := @getElem_swap'
+
+end Array
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
index b5994b39f8..9f8b50a9c1 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
@@ -1112,7 +1112,7 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
   let li := derivedLits_arr[i]
   have li_in_derivedLits : li ∈ derivedLits := by
     rw [Array.mem_toList, ← derivedLits_arr_def]
-    simp only [li, Array.getElem?_mem]
+    simp [li, Array.getElem_mem]
   have i_in_bounds : i.1 < derivedLits.length := by
     have i_property := i.2
     simp only [derivedLits_arr_def, Array.size_mk] at i_property
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
index 518d0f4552..1395829505 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
@@ -570,7 +570,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
         rw [c_clause_rw] at pc1
         have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, false) := by
           rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
-          rw [← Array.getElem_fin_eq_toList_get] at hidx
+          simp only [List.get_eq_getElem] at hidx
           exact Exists.intro idx hidx
         rcases idx_exists with ⟨idx, hidx⟩
         specialize h1 idx idx.2
@@ -580,7 +580,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
         rw [c_clause_rw] at pc1
         have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, true) := by
           rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
-          rw [← Array.getElem_fin_eq_toList_get] at hidx
+          simp only [List.get_eq_getElem] at hidx
           exact Exists.intro idx hidx
         rcases idx_exists with ⟨idx, hidx⟩
         specialize h1 idx idx.2
@@ -595,7 +595,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
       rw [c_clause_rw] at pc1
       have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, false) := by
         rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
-        rw [← Array.getElem_fin_eq_toList_get] at hidx
+        simp only [List.get_eq_getElem] at hidx
         exact Exists.intro idx hidx
       rcases idx_exists with ⟨idx, hidx⟩
       apply Exists.intro idx ∘ And.intro idx.2
@@ -606,7 +606,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
       rw [c_clause_rw] at pc1
       have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, true) := by
         rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
-        rw [← Array.getElem_fin_eq_toList_get] at hidx
+        simp only [List.get_eq_getElem] at hidx
         exact Exists.intro idx hidx
       rcases idx_exists with ⟨idx, hidx⟩
       apply Exists.intro idx ∘ And.intro idx.2