diff --git a/src/Init/Data/Array/Bootstrap.lean b/src/Init/Data/Array/Bootstrap.lean
index b44e458800..998e90c377 100644
--- a/src/Init/Data/Array/Bootstrap.lean
+++ b/src/Init/Data/Array/Bootstrap.lean
@@ -73,7 +73,7 @@ theorem foldr_eq_foldr_toList (f : α → β → β) (init : β) (arr : Array α
 
 @[simp] theorem append_eq_append (arr arr' : Array α) : arr.append arr' = arr ++ arr' := rfl
 
-@[simp] theorem append_toList (arr arr' : Array α) :
+@[simp] theorem toList_append (arr arr' : Array α) :
     (arr ++ arr').toList = arr.toList ++ arr'.toList := by
   rw [← append_eq_append]; unfold Array.append
   rw [foldl_eq_foldl_toList]
@@ -111,8 +111,8 @@ abbrev toList_eq := @toListImpl_eq
 @[deprecated pop_toList (since := "2024-09-09")]
 abbrev pop_data := @pop_toList
 
-@[deprecated append_toList (since := "2024-09-09")]
-abbrev append_data := @append_toList
+@[deprecated toList_append (since := "2024-09-09")]
+abbrev append_data := @toList_append
 
 @[deprecated appendList_toList (since := "2024-09-09")]
 abbrev appendList_data := @appendList_toList
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index a84dd923e2..64c8cc6d0b 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -91,6 +91,8 @@ 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
@@ -123,6 +125,11 @@ theorem toArray_concat {as : List α} {x : α} :
     l.toArray.foldl f init = l.foldl f init := by
   rw [foldl_eq_foldl_toList]
 
+@[simp] theorem append_toArray (l₁ l₂ : List α) :
+    l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
+  apply ext'
+  simp
+
 end List
 
 namespace Array
@@ -450,6 +457,10 @@ abbrev get?_eq_data_get? := @get?_eq_toList_get?
 theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
   simp [get!_eq_getD]
 
+theorem getElem?_eq_some_iff {as : Array α} : as[n]? = some a ↔ ∃ h : n < as.size, as[n] = a := by
+  cases as
+  simp [List.getElem?_eq_some_iff]
+
 @[simp] theorem back_eq_back? [Inhabited α] (a : Array α) : a.back = a.back?.getD default := by
   simp [back, back?]
 
@@ -725,13 +736,17 @@ theorem foldr_induction
   simp only [mem_def, toList_map, List.mem_map]
 
 theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
-    arr.mapM f = return mk (← arr.toList.mapM f) := by
+    arr.mapM f = List.toArray <$> (arr.toList.mapM f) := by
   rw [mapM_eq_foldlM, foldlM_eq_foldlM_toList, ← List.foldrM_reverse]
   conv => rhs; rw [← List.reverse_reverse arr.toList]
   induction arr.toList.reverse with
   | nil => simp
   | cons a l ih => simp [ih]
 
+@[simp] theorem toList_mapM [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
+    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
 
@@ -788,16 +803,20 @@ theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Pro
   simpa using map_induction as f (fun _ => True) trivial p (by simp_all)
 
 @[simp] theorem getElem_map (f : α → β) (as : Array α) (i : Nat) (h) :
-    ((as.map f)[i]) = f (as[i]'(size_map .. ▸ h)) := by
+    (as.map f)[i] = f (as[i]'(size_map .. ▸ h)) := by
   have := map_spec as f (fun i b => b = f (as[i]))
   simp only [implies_true, true_implies] at this
   obtain ⟨eq, w⟩ := this
   apply w
   simp_all
 
+@[simp] theorem getElem?_map (f : α → β) (as : Array α) (i : Nat) :
+    (as.map f)[i]? = as[i]?.map f := by
+  simp [getElem?_def]
+
 /-! ### mapIdx -/
 
--- This could also be prove from `SatisfiesM_mapIdxM`.
+-- This could also be proved from `SatisfiesM_mapIdxM` in Batteries.
 theorem mapIdx_induction (as : Array α) (f : Fin as.size → α → β)
     (motive : Nat → Prop) (h0 : motive 0)
     (p : Fin as.size → β → Prop)
@@ -837,10 +856,15 @@ theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β)
 
 @[simp] theorem getElem_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat)
     (h : i < (mapIdx a f).size) :
-    haveI : i < a.size := by simp_all
-    (a.mapIdx f)[i] = f ⟨i, this⟩ a[i] :=
+    (a.mapIdx f)[i] = f ⟨i, by simp_all⟩ (a[i]'(by simp_all)) :=
   (mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
 
+@[simp] theorem getElem?_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat) :
+    (a.mapIdx f)[i]? =
+      a[i]?.pbind fun b h => f ⟨i, (getElem?_eq_some_iff.1 h).1⟩ b := by
+  simp only [getElem?_def, size_mapIdx, getElem_mapIdx]
+  split <;> simp_all
+
 /-! ### modify -/
 
 @[simp] theorem size_modify (a : Array α) (i : Nat) (f : α → α) : (a.modify i f).size = a.size := by
@@ -932,34 +956,45 @@ abbrev empty_data := @toList_empty
 theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] := rfl
 
 @[simp] theorem mem_append {a : α} {s t : Array α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
-  simp only [mem_def, append_toList, List.mem_append]
+  simp only [mem_def, toList_append, List.mem_append]
 
-theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
-  simp only [size, append_toList, List.length_append]
+@[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
+  simp only [size, toList_append, List.length_append]
 
-theorem get_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
+theorem getElem_append {as bs : Array α} (h : i < (as ++ bs).size) :
+    (as ++ bs)[i] = if h' : i < as.size then as[i] else bs[i - as.size]'(by simp at h; omega) := by
+  cases as; cases bs
+  simp [List.getElem_append]
+
+theorem getElem_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
     (as ++ bs)[i] = as[i] := by
   simp only [getElem_eq_getElem_toList]
-  have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, append_toList] at h
+  have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, toList_append] at h
   conv => rhs; rw [← List.getElem_append_left (bs := bs.toList) (h' := h')]
-  apply List.get_of_eq; rw [append_toList]
+  apply List.get_of_eq; rw [toList_append]
 
-theorem get_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i)
+@[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
   simp only [getElem_eq_getElem_toList]
-  have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, append_toList] at h
+  have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, toList_append] at h
   conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
-  apply List.get_of_eq; rw [append_toList]
+  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 [append_toList, toList_empty, List.append_nil]
+  apply ext'; simp only [toList_append, toList_empty, List.append_nil]
 
 @[simp] theorem nil_append (as : Array α) : #[] ++ as = as := by
-  apply ext'; simp only [append_toList, toList_empty, List.nil_append]
+  apply ext'; simp only [toList_append, toList_empty, List.nil_append]
 
 theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) := by
-  apply ext'; simp only [append_toList, List.append_assoc]
+  apply ext'; simp only [toList_append, List.append_assoc]
 
 /-! ### extract -/
 
@@ -1009,20 +1044,20 @@ theorem size_extract_loop (as bs : Array α) (size start : Nat) :
   simp [extract]; rw [size_extract_loop, size_empty, Nat.zero_add, Nat.sub_min_sub_right,
     Nat.min_assoc, Nat.min_self]
 
-theorem get_extract_loop_lt_aux (as bs : Array α) (size start : Nat) (hlt : i < bs.size) :
+theorem getElem_extract_loop_lt_aux (as bs : Array α) (size start : Nat) (hlt : i < bs.size) :
     i < (extract.loop as size start bs).size := by
   rw [size_extract_loop]
   apply Nat.lt_of_lt_of_le hlt
   exact Nat.le_add_right ..
 
-theorem get_extract_loop_lt (as bs : Array α) (size start : Nat) (hlt : i < bs.size)
-    (h := get_extract_loop_lt_aux as bs size start hlt) :
+theorem getElem_extract_loop_lt (as bs : Array α) (size start : Nat) (hlt : i < bs.size)
+    (h := getElem_extract_loop_lt_aux as bs size start hlt) :
     (extract.loop as size start bs)[i] = bs[i] := by
-  apply Eq.trans _ (get_append_left (bs:=extract.loop as size start #[]) hlt)
+  apply Eq.trans _ (getElem_append_left (bs:=extract.loop as size start #[]) hlt)
   · rw [size_append]; exact Nat.lt_of_lt_of_le hlt (Nat.le_add_right ..)
   · congr; rw [extract_loop_eq_aux]
 
-theorem get_extract_loop_ge_aux (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
+theorem getElem_extract_loop_ge_aux (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
     (h : i < (extract.loop as size start bs).size) : start + i - bs.size < as.size := by
   have h : i < bs.size + (as.size - start) := by
       apply Nat.lt_of_lt_of_le h
@@ -1033,9 +1068,9 @@ theorem get_extract_loop_ge_aux (as bs : Array α) (size start : Nat) (hge : i 
   apply Nat.add_lt_of_lt_sub'
   exact Nat.sub_lt_left_of_lt_add hge h
 
-theorem get_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
+theorem getElem_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
     (h : i < (extract.loop as size start bs).size)
-    (h' := get_extract_loop_ge_aux as bs size start hge h) :
+    (h' := getElem_extract_loop_ge_aux as bs size start hge h) :
     (extract.loop as size start bs)[i] = as[start + i - bs.size] := by
   induction size using Nat.recAux generalizing start bs with
   | zero =>
@@ -1057,28 +1092,37 @@ theorem get_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i ≥ b
       have h₂ : bs.size < (extract.loop as size (start+1) (bs.push as[start])).size := by
         rw [size_extract_loop]; apply Nat.lt_of_lt_of_le h₁; exact Nat.le_add_right ..
       have h : (extract.loop as size (start + 1) (push bs as[start]))[bs.size] = as[start] := by
-        rw [get_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, get_push_eq]
+        rw [getElem_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, get_push_eq]
       rw [h]; congr; rw [Nat.add_sub_cancel]
     else
       have hge : bs.size + 1 ≤ i := Nat.lt_of_le_of_ne hge hi
       rw [ih (bs.push as[start]) (start+1) ((size_push ..).symm ▸ hge)]
       congr 1; rw [size_push, Nat.add_right_comm, Nat.add_sub_add_right]
 
-theorem get_extract_aux {as : Array α} {start stop : Nat} (h : i < (as.extract start stop).size) :
+theorem getElem_extract_aux {as : Array α} {start stop : Nat} (h : i < (as.extract start stop).size) :
     start + i < as.size := by
   rw [size_extract] at h; apply Nat.add_lt_of_lt_sub'; apply Nat.lt_of_lt_of_le h
   apply Nat.sub_le_sub_right; apply Nat.min_le_right
 
-@[simp] theorem get_extract {as : Array α} {start stop : Nat}
+@[simp] theorem getElem_extract {as : Array α} {start stop : Nat}
     (h : i < (as.extract start stop).size) :
-    (as.extract start stop)[i] = as[start + i]'(get_extract_aux h) :=
+    (as.extract start stop)[i] = as[start + i]'(getElem_extract_aux h) :=
   show (extract.loop as (min stop as.size - start) start #[])[i]
-    = as[start + i]'(get_extract_aux h) by rw [get_extract_loop_ge]; rfl; exact Nat.zero_le _
+    = as[start + i]'(getElem_extract_aux h) by rw [getElem_extract_loop_ge]; rfl; exact Nat.zero_le _
+
+theorem getElem?_extract {as : Array α} {start stop : Nat} :
+    (as.extract start stop)[i]? = if i < min stop as.size - start then as[start + i]? else none := by
+  simp only [getElem?_def, size_extract, getElem_extract]
+  split
+  · split
+    · rfl
+    · omega
+  · rfl
 
 @[simp] theorem extract_all (as : Array α) : as.extract 0 as.size = as := by
   apply ext
   · rw [size_extract, Nat.min_self, Nat.sub_zero]
-  · intros; rw [get_extract]; congr; rw [Nat.zero_add]
+  · intros; rw [getElem_extract]; congr; rw [Nat.zero_add]
 
 theorem extract_empty_of_stop_le_start (as : Array α) {start stop : Nat} (h : stop ≤ start) :
     as.extract start stop = #[] := by
@@ -1160,9 +1204,12 @@ theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
 theorem any_eq_true {p : α → Bool} {as : Array α} :
     any as p ↔ ∃ i : Fin as.size, p as[i] := by simp [any_iff_exists, Fin.isLt]
 
-theorem any_def {p : α → Bool} (as : Array α) : as.any p = as.toList.any p := by
+theorem any_toList {p : α → Bool} (as : Array α) : as.toList.any p = as.any p := by
   rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]; simp only [List.mem_iff_get]
-  exact ⟨fun ⟨i, h⟩ => ⟨_, ⟨i, rfl⟩, h⟩, fun ⟨_, ⟨i, rfl⟩, h⟩ => ⟨i, h⟩⟩
+  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 -/
 
@@ -1194,22 +1241,25 @@ theorem all_iff_forall {p : α → Bool} {as : Array α} {start stop} :
 theorem all_eq_true {p : α → Bool} {as : Array α} : all as p ↔ ∀ i : Fin as.size, p as[i] := by
   simp [all_iff_forall, Fin.isLt]
 
-theorem all_def {p : α → Bool} (as : Array α) : as.all p = as.toList.all p := by
+theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all p := by
   rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]; simp only [List.mem_iff_getElem]
   constructor
+  · intro w i
+    exact w as[i] ⟨i, i.2, (getElem_eq_getElem_toList i.2).symm⟩
   · rintro w x ⟨r, h, rfl⟩
     rw [← getElem_eq_getElem_toList]
     exact w ⟨r, h⟩
-  · intro w i
-    exact w as[i] ⟨i, i.2, (getElem_eq_getElem_toList i.2).symm⟩
+
+@[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_def, List.all_eq_true, mem_def]
+  simp only [← all_toList, List.all_eq_true, mem_def]
 
 /-! ### contains -/
 
 theorem contains_def [DecidableEq α] {a : α} {as : Array α} : as.contains a ↔ a ∈ as := by
-  rw [mem_def, contains, any_def, List.any_eq_true]; simp [and_comm]
+  rw [mem_def, contains, ← any_toList, List.any_eq_true]; simp [and_comm]
 
 instance [DecidableEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
   decidable_of_iff _ contains_def
@@ -1218,12 +1268,12 @@ instance [DecidableEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
 
 open Fin
 
-@[simp] theorem get_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.val] = a[i] :=
+@[simp] theorem getElem_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.val] = a[i] :=
   by simp only [swap, fin_cast_val, get_eq_getElem, getElem_set_eq, getElem_fin]
 
-@[simp] theorem get_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.val] = a[j] :=
+@[simp] theorem getElem_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.val] = a[j] :=
   if he : ((Array.size_set _ _ _).symm ▸ j).val = i.val then by
-    simp only [←he, fin_cast_val, get_swap_right, getElem_fin]
+    simp only [←he, fin_cast_val, getElem_swap_right, getElem_fin]
   else by
     apply Eq.trans
     · apply Array.get_set_ne
@@ -1231,7 +1281,7 @@ open Fin
       · assumption
     · simp [get_set_ne]
 
-@[simp] theorem get_swap_of_ne (a : Array α) {i j : Fin a.size} (hp : p < a.size)
+@[simp] theorem getElem_swap_of_ne (a : Array α) {i j : Fin a.size} (hp : p < a.size)
     (hi : p ≠ i) (hj : p ≠ j) : (a.swap i j)[p]'(a.size_swap .. |>.symm ▸ hp) = a[p] := by
   apply Eq.trans
   · have : ((a.size_set i (a.get j)).symm ▸ j).val = j.val := by simp only [fin_cast_val]
@@ -1243,22 +1293,22 @@ open Fin
     · apply Ne.symm
       · assumption
 
-theorem get_swap (a : Array α) (i j : Fin a.size) (k : Nat) (hk: k < a.size) :
+theorem getElem_swap' (a : Array α) (i j : Fin a.size) (k : Nat) (hk : k < a.size) :
     (a.swap i j)[k]'(by simp_all) = if k = i then a[j] else if k = j then a[i]  else a[k] := by
   split
-  · simp_all only [get_swap_left]
+  · simp_all only [getElem_swap_left]
   · split <;> simp_all
 
-theorem get_swap' (a : Array α) (i j : Fin a.size) (k : Nat) (hk' : k < (a.swap i j).size) :
+theorem getElem_swap (a : Array α) (i j : Fin a.size) (k : Nat) (hk : k < (a.swap i j).size) :
     (a.swap i j)[k] = if k = i then a[j] else if k = j then a[i] else a[k]'(by simp_all) := by
-  apply get_swap
+  apply getElem_swap'
 
 @[simp] theorem swap_swap (a : Array α) {i j : Fin a.size} :
     (a.swap i j).swap ⟨i.1, (a.size_swap ..).symm ▸i.2⟩ ⟨j.1, (a.size_swap ..).symm ▸j.2⟩ = a := by
   apply ext
   · simp only [size_swap]
   · intros
-    simp only [get_swap']
+    simp only [getElem_swap]
     split
     · simp_all
     · split <;> simp_all
@@ -1267,11 +1317,35 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
   apply ext
   · simp only [size_swap]
   · intros
-    simp only [get_swap']
+    simp only [getElem_swap]
     split
     · 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
 
 
@@ -1288,9 +1362,6 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
 @[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
   simp [mem_def]
 
-@[simp] theorem getElem?_toArray (l : List α) (i : Nat) : l.toArray[i]? = l[i]? := by
-  simp [getElem?_eq_getElem?_toList]
-
 @[simp] theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse := by
   simp
 
@@ -1345,14 +1416,14 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
   rw [← anyM_toList]
 
 @[simp] theorem any_toArray (p : α → Bool) (l : List α) : l.toArray.any p = l.any p := by
-  rw [Array.any_def]
+  rw [any_toList]
 
 @[simp] theorem allM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
     l.toArray.allM p = l.allM p := by
   rw [← allM_toList]
 
 @[simp] theorem all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p := by
-  rw [Array.all_def]
+  rw [all_toList]
 
 @[simp] theorem swap_toArray (l : List α) (i j : Fin l.toArray.size) :
     l.toArray.swap i j = ((l.set i l[j]).set j l[i]).toArray := by
@@ -1377,11 +1448,6 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
   apply ext'
   erw [toList_filterMap] -- `erw` required to unify `l.length` with `l.toArray.size`.
 
-@[simp] theorem append_toArray (l₁ l₂ : List α) :
-    l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
-  apply ext'
-  simp
-
 @[simp] theorem toArray_range (n : Nat) : (range n).toArray = Array.range n := by
   apply ext'
   simp
diff --git a/src/Std/Sat/AIG/RefVec.lean b/src/Std/Sat/AIG/RefVec.lean
index 73c71d4784..0d1099fc43 100644
--- a/src/Std/Sat/AIG/RefVec.lean
+++ b/src/Std/Sat/AIG/RefVec.lean
@@ -104,10 +104,10 @@ def append (lhs : RefVec aig lw) (rhs : RefVec aig rw) : RefVec aig (lw + rw) :=
     by
       intro i h
       by_cases hsplit : i < lrefs.size
-      · rw [Array.get_append_left]
+      · rw [Array.getElem_append_left]
         apply hl2
         omega
-      · rw [Array.get_append_right]
+      · rw [Array.getElem_append_right]
         · apply hr2
           omega
         · omega
@@ -124,9 +124,9 @@ theorem get_append (lhs : RefVec aig lw) (rhs : RefVec aig rw) (idx : Nat)
   simp only [get, append]
   split
   · simp [Ref.mk.injEq]
-    rw [Array.get_append_left]
+    rw [Array.getElem_append_left]
   · simp only [Ref.mk.injEq]
-    rw [Array.get_append_right]
+    rw [Array.getElem_append_right]
     · simp [lhs.hlen]
     · rw [lhs.hlen]
       omega