diff --git a/src/Init/Data/Array/Attach.lean b/src/Init/Data/Array/Attach.lean
index ed489b012b..caabd1b993 100644
--- a/src/Init/Data/Array/Attach.lean
+++ b/src/Init/Data/Array/Attach.lean
@@ -20,7 +20,7 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
   with the same elements but in the type `{x // P x}`. -/
 @[implemented_by attachWithImpl] def attachWith
     (xs : Array α) (P : α → Prop) (H : ∀ x ∈ xs, P x) : Array {x // P x} :=
-  ⟨xs.data.attachWith P fun x h => H x (Array.Mem.mk h)⟩
+  ⟨xs.toList.attachWith P fun x h => H x (Array.Mem.mk h)⟩
 
 /-- `O(1)`. "Attach" the proof that the elements of `xs` are in `xs` to produce a new array
   with the same elements but in the type `{x // x ∈ xs}`. -/
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 29135dc8b5..5ed4c9ffd5 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -16,10 +16,11 @@ universe u v w
 namespace Array
 variable {α : Type u}
 
+@[deprecated Array.toList (since := "2024-09-10")] abbrev Array.data := @Array.toList
+
 @[extern "lean_mk_array"]
-def mkArray {α : Type u} (n : Nat) (v : α) : Array α := {
-  data := List.replicate n v
-}
+def mkArray {α : Type u} (n : Nat) (v : α) : Array α where
+  toList := List.replicate n v
 
 /--
 `ofFn f` with `f : Fin n → α` returns the list whose ith element is `f i`.
@@ -134,9 +135,8 @@ def swapAt! (a : Array α) (i : Nat) (v : α) : α × Array α :=
     panic! ("index " ++ toString i ++ " out of bounds")
 
 @[extern "lean_array_pop"]
-def pop (a : Array α) : Array α := {
-  data := a.data.dropLast
-}
+def pop (a : Array α) : Array α where
+  toList := a.toList.dropLast
 
 def shrink (a : Array α) (n : Nat) : Array α :=
   let rec loop
@@ -499,10 +499,10 @@ def elem [BEq α] (a : α) (as : Array α) : Bool :=
       (true, r)
 
 /-- Convert a `Array α` into an `List α`. This is O(n) in the size of the array.  -/
--- This function is exported to C, where it is called by `Array.data`
+-- This function is exported to C, where it is called by `Array.toList`
 -- (the projection) to implement this functionality.
-@[export lean_array_to_list]
-def toList (as : Array α) : List α :=
+@[export lean_array_to_list_impl]
+def toListImpl (as : Array α) : List α :=
   as.foldr List.cons []
 
 /-- Prepends an `Array α` onto the front of a list.  Equivalent to `as.toList ++ l`. -/
@@ -793,30 +793,32 @@ def toListLitAux (a : Array α) (n : Nat) (hsz : a.size = n) : ∀ (i : Nat), i
 def toArrayLit (a : Array α) (n : Nat) (hsz : a.size = n) : Array α :=
   List.toArray <| toListLitAux a n hsz n (hsz ▸ Nat.le_refl _) []
 
-theorem ext' {as bs : Array α} (h : as.data = bs.data) : as = bs := by
+theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
   cases as; cases bs; simp at h; rw [h]
 
-@[simp] theorem toArrayAux_eq (as : List α) (acc : Array α) : (as.toArrayAux acc).data = acc.data ++ as := by
+@[simp] theorem toArrayAux_eq (as : List α) (acc : Array α) : (as.toArrayAux acc).toList = acc.toList ++ as := by
   induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append]
 
-@[simp] theorem data_toArray (as : List α) : as.toArray.data = as := by
+@[simp] theorem toList_toArray (as : List α) : as.toArray.toList = as := by
   simp [List.toArray, Array.mkEmpty]
 
+@[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @toList_toArray
+
 @[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
 
 theorem toArrayLit_eq (as : Array α) (n : Nat) (hsz : as.size = n) : as = toArrayLit as n hsz := by
   apply ext'
-  simp [toArrayLit, data_toArray]
+  simp [toArrayLit, toList_toArray]
   have hle : n ≤ as.size := hsz ▸ Nat.le_refl _
   have hge : as.size ≤ n := hsz ▸ Nat.le_refl _
   have := go n hle
   rw [List.drop_eq_nil_of_le hge] at this
   rw [this]
 where
-  getLit_eq (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = getElem as.data i ((id (α := as.data.length = n) h₁) ▸ h₂) :=
+  getLit_eq (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = getElem as.toList i ((id (α := as.toList.length = n) h₁) ▸ h₂) :=
     rfl
 
-  go (i : Nat) (hi : i ≤ as.size) : toListLitAux as n hsz i hi (as.data.drop i) = as.data := by
+  go (i : Nat) (hi : i ≤ as.size) : toListLitAux as n hsz i hi (as.toList.drop i) = as.toList := by
     induction i <;> simp [getLit_eq, List.get_drop_eq_drop, toListLitAux, List.drop, *]
 
 def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : Nat) : Bool :=
diff --git a/src/Init/Data/Array/Bootstrap.lean b/src/Init/Data/Array/Bootstrap.lean
index 26c37951c2..b44e458800 100644
--- a/src/Init/Data/Array/Bootstrap.lean
+++ b/src/Init/Data/Array/Bootstrap.lean
@@ -15,76 +15,106 @@ This file contains some theorems about `Array` and `List` needed for `Init.Data.
 
 namespace Array
 
-theorem foldlM_eq_foldlM_data.aux [Monad m]
+theorem foldlM_eq_foldlM_toList.aux [Monad m]
     (f : β → α → m β) (arr : Array α) (i j) (H : arr.size ≤ i + j) (b) :
-    foldlM.loop f arr arr.size (Nat.le_refl _) i j b = (arr.data.drop j).foldlM f b := by
+    foldlM.loop f arr arr.size (Nat.le_refl _) i j b = (arr.toList.drop j).foldlM f b := by
   unfold foldlM.loop
   split; split
   · cases Nat.not_le_of_gt ‹_› (Nat.zero_add _ ▸ H)
   · rename_i i; rw [Nat.succ_add] at H
-    simp [foldlM_eq_foldlM_data.aux f arr i (j+1) H]
+    simp [foldlM_eq_foldlM_toList.aux f arr i (j+1) H]
     rw (config := {occs := .pos [2]}) [← List.get_drop_eq_drop _ _ ‹_›]
     rfl
   · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
 
-theorem foldlM_eq_foldlM_data [Monad m]
+theorem foldlM_eq_foldlM_toList [Monad m]
     (f : β → α → m β) (init : β) (arr : Array α) :
-    arr.foldlM f init = arr.data.foldlM f init := by
-  simp [foldlM, foldlM_eq_foldlM_data.aux]
+    arr.foldlM f init = arr.toList.foldlM f init := by
+  simp [foldlM, foldlM_eq_foldlM_toList.aux]
 
-theorem foldl_eq_foldl_data (f : β → α → β) (init : β) (arr : Array α) :
-    arr.foldl f init = arr.data.foldl f init :=
-  List.foldl_eq_foldlM .. ▸ foldlM_eq_foldlM_data ..
+theorem foldl_eq_foldl_toList (f : β → α → β) (init : β) (arr : Array α) :
+    arr.foldl f init = arr.toList.foldl f init :=
+  List.foldl_eq_foldlM .. ▸ foldlM_eq_foldlM_toList ..
 
-theorem foldrM_eq_reverse_foldlM_data.aux [Monad m]
+theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
     (f : α → β → m β) (arr : Array α) (init : β) (i h) :
-    (arr.data.take i).reverse.foldlM (fun x y => f y x) init = foldrM.fold f arr 0 i h init := by
+    (arr.toList.take i).reverse.foldlM (fun x y => f y x) init = foldrM.fold f arr 0 i h init := by
   unfold foldrM.fold
   match i with
   | 0 => simp [List.foldlM, List.take]
   | i+1 => rw [← List.take_concat_get _ _ h]; simp [← (aux f arr · i)]; rfl
 
-theorem foldrM_eq_reverse_foldlM_data [Monad m] (f : α → β → m β) (init : β) (arr : Array α) :
-    arr.foldrM f init = arr.data.reverse.foldlM (fun x y => f y x) init := by
+theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init : β) (arr : Array α) :
+    arr.foldrM f init = arr.toList.reverse.foldlM (fun x y => f y x) init := by
   have : arr = #[] ∨ 0 < arr.size :=
     match arr with | ⟨[]⟩ => .inl rfl | ⟨a::l⟩ => .inr (Nat.zero_lt_succ _)
   match arr, this with | _, .inl rfl => rfl | arr, .inr h => ?_
-  simp [foldrM, h, ← foldrM_eq_reverse_foldlM_data.aux, List.take_length]
+  simp [foldrM, h, ← foldrM_eq_reverse_foldlM_toList.aux, List.take_length]
 
-theorem foldrM_eq_foldrM_data [Monad m]
+theorem foldrM_eq_foldrM_toList [Monad m]
     (f : α → β → m β) (init : β) (arr : Array α) :
-    arr.foldrM f init = arr.data.foldrM f init := by
-  rw [foldrM_eq_reverse_foldlM_data, List.foldlM_reverse]
+    arr.foldrM f init = arr.toList.foldrM f init := by
+  rw [foldrM_eq_reverse_foldlM_toList, List.foldlM_reverse]
 
-theorem foldr_eq_foldr_data (f : α → β → β) (init : β) (arr : Array α) :
-    arr.foldr f init = arr.data.foldr f init :=
-  List.foldr_eq_foldrM .. ▸ foldrM_eq_foldrM_data ..
+theorem foldr_eq_foldr_toList (f : α → β → β) (init : β) (arr : Array α) :
+    arr.foldr f init = arr.toList.foldr f init :=
+  List.foldr_eq_foldrM .. ▸ foldrM_eq_foldrM_toList ..
 
-@[simp] theorem push_data (arr : Array α) (a : α) : (arr.push a).data = arr.data ++ [a] := by
+@[simp] theorem push_toList (arr : Array α) (a : α) : (arr.push a).toList = arr.toList ++ [a] := by
   simp [push, List.concat_eq_append]
 
-@[simp] theorem toListAppend_eq (arr : Array α) (l) : arr.toListAppend l = arr.data ++ l := by
-  simp [toListAppend, foldr_eq_foldr_data]
+@[simp] theorem toListAppend_eq (arr : Array α) (l) : arr.toListAppend l = arr.toList ++ l := by
+  simp [toListAppend, foldr_eq_foldr_toList]
 
-@[simp] theorem toList_eq (arr : Array α) : arr.toList = arr.data := by
-  simp [toList, foldr_eq_foldr_data]
+@[simp] theorem toListImpl_eq (arr : Array α) : arr.toListImpl = arr.toList := by
+  simp [toListImpl, foldr_eq_foldr_toList]
 
-@[simp] theorem pop_data (arr : Array α) : arr.pop.data = arr.data.dropLast := rfl
+@[simp] theorem pop_toList (arr : Array α) : arr.pop.toList = arr.toList.dropLast := rfl
 
 @[simp] theorem append_eq_append (arr arr' : Array α) : arr.append arr' = arr ++ arr' := rfl
 
-@[simp] theorem append_data (arr arr' : Array α) :
-    (arr ++ arr').data = arr.data ++ arr'.data := by
+@[simp] theorem append_toList (arr arr' : Array α) :
+    (arr ++ arr').toList = arr.toList ++ arr'.toList := by
   rw [← append_eq_append]; unfold Array.append
-  rw [foldl_eq_foldl_data]
-  induction arr'.data generalizing arr <;> simp [*]
+  rw [foldl_eq_foldl_toList]
+  induction arr'.toList generalizing arr <;> simp [*]
 
 @[simp] theorem appendList_eq_append
     (arr : Array α) (l : List α) : arr.appendList l = arr ++ l := rfl
 
-@[simp] theorem appendList_data (arr : Array α) (l : List α) :
-    (arr ++ l).data = arr.data ++ l := by
+@[simp] theorem appendList_toList (arr : Array α) (l : List α) :
+    (arr ++ l).toList = arr.toList ++ l := by
   rw [← appendList_eq_append]; unfold Array.appendList
   induction l generalizing arr <;> simp [*]
 
+@[deprecated foldlM_eq_foldlM_toList (since := "2024-09-09")]
+abbrev foldlM_eq_foldlM_data := @foldlM_eq_foldlM_toList
+
+@[deprecated foldl_eq_foldl_toList (since := "2024-09-09")]
+abbrev foldl_eq_foldl_data := @foldl_eq_foldl_toList
+
+@[deprecated foldrM_eq_reverse_foldlM_toList (since := "2024-09-09")]
+abbrev foldrM_eq_reverse_foldlM_data := @foldrM_eq_reverse_foldlM_toList
+
+@[deprecated foldrM_eq_foldrM_toList (since := "2024-09-09")]
+abbrev foldrM_eq_foldrM_data := @foldrM_eq_foldrM_toList
+
+@[deprecated foldr_eq_foldr_toList (since := "2024-09-09")]
+abbrev foldr_eq_foldr_data := @foldr_eq_foldr_toList
+
+@[deprecated push_toList (since := "2024-09-09")]
+abbrev push_data := @push_toList
+
+@[deprecated toListImpl_eq (since := "2024-09-09")]
+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 appendList_toList (since := "2024-09-09")]
+abbrev appendList_data := @appendList_toList
+
 end Array
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index d83f20f27b..b3effb0867 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -23,25 +23,34 @@ attribute [simp] data_toArray uset
 
 @[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
 
-@[simp] theorem toArray_data : (a : Array α) → a.data.toArray = a
-  | ⟨l⟩ => ext' (data_toArray l)
+@[simp] theorem toArray_toList : (a : Array α) → a.toList.toArray = a
+  | ⟨l⟩ => ext' (toList_toArray l)
 
-@[simp] theorem data_length {l : Array α} : l.data.length = l.size := rfl
+@[deprecated toArray_toList (since := "2024-09-09")]
+abbrev toArray_data := @toArray_toList
+
+@[simp] theorem toList_length {l : Array α} : l.toList.length = l.size := rfl
+
+@[deprecated toList_length (since := "2024-09-09")]
+abbrev data_length := @toList_length
 
 @[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
 
 @[simp] theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
 
-theorem getElem_eq_data_getElem (a : Array α) (h : i < a.size) : a[i] = a.data[i] := by
+theorem getElem_eq_toList_getElem (a : Array α) (h : i < a.size) : a[i] = a.toList[i] := by
   by_cases i < a.size <;> (try simp [*]) <;> rfl
 
-@[deprecated getElem_eq_data_getElem (since := "2024-06-12")]
-theorem getElem_eq_data_get (a : Array α) (h : i < a.size) : a[i] = a.data.get ⟨i, h⟩ := by
-  simp [getElem_eq_data_getElem]
+@[deprecated getElem_eq_toList_getElem (since := "2024-09-09")]
+abbrev getElem_eq_data_getElem := @getElem_eq_toList_getElem
+
+@[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 [getElem_eq_toList_getElem]
 
 theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
     (arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
-  simp [foldrM_eq_reverse_foldlM_data, -size_push]
+  simp [foldrM_eq_reverse_foldlM_toList, -size_push]
 
 @[simp] theorem foldrM_push' [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
     (arr.push a).foldrM f init (start := arr.size + 1) = f a init >>= arr.foldrM f := by
@@ -56,17 +65,17 @@ theorem foldr_push (f : α → β → β) (init : β) (arr : Array α) (a : α)
 /-- A more efficient version of `arr.toList.reverse`. -/
 @[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) []
 
-@[simp] theorem toListRev_eq (arr : Array α) : arr.toListRev = arr.data.reverse := by
-  rw [toListRev, foldl_eq_foldl_data, ← List.foldr_reverse, List.foldr_cons_nil]
+@[simp] theorem toListRev_eq (arr : Array α) : arr.toListRev = arr.toList.reverse := by
+  rw [toListRev, foldl_eq_foldl_toList, ← List.foldr_reverse, List.foldr_cons_nil]
 
 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
-  simp only [push, getElem_eq_data_getElem, List.concat_eq_append, List.getElem_append_left, h]
+  simp only [push, getElem_eq_toList_getElem, List.concat_eq_append, List.getElem_append_left, h]
 
 @[simp] theorem get_push_eq (a : Array α) (x : α) : (a.push x)[a.size] = x := by
-  simp only [push, getElem_eq_data_getElem, List.concat_eq_append]
-  rw [List.getElem_append_right] <;> simp [getElem_eq_data_getElem, Nat.zero_lt_one]
+  simp only [push, getElem_eq_toList_getElem, List.concat_eq_append]
+  rw [List.getElem_append_right] <;> simp [getElem_eq_toList_getElem, Nat.zero_lt_one]
 
 theorem get_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
     (a.push x)[i] = if h : i < a.size then a[i] else x := by
@@ -77,27 +86,31 @@ theorem get_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
 
 theorem mapM_eq_foldlM [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
     arr.mapM f = arr.foldlM (fun bs a => bs.push <$> f a) #[] := by
-  rw [mapM, aux, foldlM_eq_foldlM_data]; rfl
+  rw [mapM, aux, foldlM_eq_foldlM_toList]; rfl
 where
   aux (i r) :
-      mapM.map f arr i r = (arr.data.drop i).foldlM (fun bs a => bs.push <$> f a) r := by
+      mapM.map f arr i r = (arr.toList.drop i).foldlM (fun bs a => bs.push <$> f a) r := by
     unfold mapM.map; split
     · rw [← List.get_drop_eq_drop _ i ‹_›]
-      simp only [aux (i + 1), map_eq_pure_bind, data_length, List.foldlM_cons, bind_assoc, pure_bind]
+      simp only [aux (i + 1), map_eq_pure_bind, toList_length, List.foldlM_cons, bind_assoc,
+        pure_bind]
       rfl
     · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
   termination_by arr.size - i
   decreasing_by decreasing_trivial_pre_omega
 
-@[simp] theorem map_data (f : α → β) (arr : Array α) : (arr.map f).data = arr.data.map f := by
+@[simp] theorem map_toList (f : α → β) (arr : Array α) : (arr.map f).toList = arr.toList.map f := by
   rw [map, mapM_eq_foldlM]
-  apply congrArg data (foldl_eq_foldl_data (fun bs a => push bs (f a)) #[] arr) |>.trans
-  have H (l arr) : List.foldl (fun bs a => push bs (f a)) arr l = ⟨arr.data ++ l.map f⟩ := by
+  apply congrArg toList (foldl_eq_foldl_toList (fun bs a => push bs (f a)) #[] arr) |>.trans
+  have H (l arr) : List.foldl (fun bs a => push bs (f a)) arr l = ⟨arr.toList ++ l.map f⟩ := by
     induction l generalizing arr <;> simp [*]
   simp [H]
 
+@[deprecated map_toList (since := "2024-09-09")]
+abbrev map_data := @map_toList
+
 @[simp] theorem size_map (f : α → β) (arr : Array α) : (arr.map f).size = arr.size := by
-  simp only [← data_length]
+  simp only [← toList_length]
   simp
 
 @[simp] theorem appendList_nil (arr : Array α) : arr ++ ([] : List α) = arr := Array.ext' (by simp)
@@ -105,16 +118,22 @@ where
 @[simp] theorem appendList_cons (arr : Array α) (a : α) (l : List α) :
     arr ++ (a :: l) = arr.push a ++ l := Array.ext' (by simp)
 
-theorem foldl_data_eq_bind (l : List α) (acc : Array β)
+theorem foldl_toList_eq_bind (l : List α) (acc : Array β)
     (F : Array β → α → Array β) (G : α → List β)
-    (H : ∀ acc a, (F acc a).data = acc.data ++ G a) :
-    (l.foldl F acc).data = acc.data ++ l.bind G := by
+    (H : ∀ acc a, (F acc a).toList = acc.toList ++ G a) :
+    (l.foldl F acc).toList = acc.toList ++ l.bind G := by
   induction l generalizing acc <;> simp [*, List.bind]
 
-theorem foldl_data_eq_map (l : List α) (acc : Array β) (G : α → β) :
-    (l.foldl (fun acc a => acc.push (G a)) acc).data = acc.data ++ l.map G := by
+@[deprecated foldl_toList_eq_bind (since := "2024-09-09")]
+abbrev foldl_data_eq_bind := @foldl_toList_eq_bind
+
+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) :
@@ -125,7 +144,7 @@ theorem anyM_stop_le_start [Monad m] (p : α → m Bool) (as : Array α) (start
     (h : min stop as.size ≤ start) : anyM p as start stop = pure false := by
   rw [anyM_eq_anyM_loop, anyM.loop, dif_neg (Nat.not_lt.2 h)]
 
-theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.data :=
+theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
   ⟨fun | .mk h => h, Array.Mem.mk⟩
 
 /-! # get -/
@@ -164,11 +183,11 @@ theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default
 @[simp] theorem getElem_set_eq (a : Array α) (i : Fin a.size) (v : α) {j : Nat}
       (eq : i.val = j) (p : j < (a.set i v).size) :
     (a.set i v)[j]'p = v := by
-  simp [set, getElem_eq_data_getElem, ←eq]
+  simp [set, getElem_eq_toList_getElem, ←eq]
 
 @[simp] theorem getElem_set_ne (a : Array α) (i : Fin a.size) (v : α) {j : Nat} (pj : j < (a.set i v).size)
     (h : i.val ≠ j) : (a.set i v)[j]'pj = a[j]'(size_set a i v ▸ pj) := by
-  simp only [set, getElem_eq_data_getElem, List.getElem_set_ne h]
+  simp only [set, getElem_eq_toList_getElem, List.getElem_set_ne h]
 
 theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
     (h : j < (a.set i v).size) :
@@ -249,14 +268,20 @@ termination_by n - i
 
 /-- # mkArray -/
 
-@[simp] theorem mkArray_data (n : Nat) (v : α) : (mkArray n v).data = List.replicate n v := rfl
+@[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_data_getElem]
+    (mkArray n v)[i] = v := by simp [Array.getElem_eq_toList_getElem]
 
 /-- # mem -/
 
-theorem mem_data {a : α} {l : Array α} : a ∈ l.data ↔ a ∈ l := mem_def.symm
+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
 
@@ -290,10 +315,13 @@ theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size}
   hidx
 
 theorem getElem?_mem {l : Array α} {i : Fin l.size} : l[i] ∈ l := by
-  erw [Array.mem_def, getElem_eq_data_getElem]
+  erw [Array.mem_def, getElem_eq_toList_getElem]
   apply List.get_mem
 
-theorem getElem_fin_eq_data_get (a : Array α) (i : Fin _) : a[i] = a.data.get i := rfl
+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
 
 @[simp] theorem ugetElem_eq_getElem (a : Array α) {i : USize} (h : i.toNat < a.size) :
   a[i] = a[i.toNat] := rfl
@@ -304,14 +332,23 @@ theorem getElem?_eq_getElem (a : Array α) (i : Nat) (h : i < a.size) : a[i]? =
 theorem get?_len_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none := by
   simp [getElem?_neg, h]
 
-theorem getElem_mem_data (a : Array α) (h : i < a.size) : a[i] ∈ a.data := by
-  simp only [getElem_eq_data_getElem, List.getElem_mem]
+theorem getElem_mem_toList (a : Array α) (h : i < a.size) : a[i] ∈ a.toList := by
+  simp only [getElem_eq_toList_getElem, List.getElem_mem]
 
-theorem getElem?_eq_data_get? (a : Array α) (i : Nat) : a[i]? = a.data.get? i := by
+@[deprecated getElem_mem_toList (since := "2024-09-09")]
+abbrev getElem_mem_data := @getElem_mem_toList
+
+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]; rfl
 
-theorem get?_eq_data_get? (a : Array α) (i : Nat) : a.get? i = a.data.get? i :=
-  getElem?_eq_data_get? ..
+@[deprecated getElem?_eq_toList_get? (since := "2024-09-09")]
+abbrev getElem?_eq_data_get? := @getElem?_eq_toList_get?
+
+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? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
   simp [get!_eq_getD]
@@ -320,7 +357,7 @@ theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD
   simp [back, back?]
 
 @[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
-  simp [back?, getElem?_eq_data_get?]
+  simp [back?, getElem?_eq_toList_get?]
 
 theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp
 
@@ -349,11 +386,14 @@ theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x el
 @[simp] theorem get?_size {a : Array α} : a[a.size]? = none := by
   simp only [getElem?_def, Nat.lt_irrefl, dite_false]
 
-@[simp] theorem data_set (a : Array α) (i v) : (a.set i v).data = a.data.set i.1 v := rfl
+@[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_data_getElem, List.getElem_set_self]
+  simp only [set, getElem_eq_toList_getElem, List.getElem_set_self]
 
 theorem get?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
     (a.set i v)[i.1]? = v := by simp [getElem?_pos, i.2]
@@ -372,7 +412,7 @@ theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v :
 
 @[simp] theorem get_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α) (hj : j < a.size)
     (h : i.1 ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
-  simp only [set, getElem_eq_data_getElem, List.getElem_set_ne h]
+  simp only [set, getElem_eq_toList_getElem, List.getElem_set_ne h]
 
 theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
   (setD a i v)[i] = v := by
@@ -388,12 +428,15 @@ theorem swap_def (a : Array α) (i j : Fin a.size) :
     a.swap i j = (a.set i (a.get j)).set ⟨j.1, by simp [j.2]⟩ (a.get i) := by
   simp [swap, fin_cast_val]
 
-theorem data_swap (a : Array α) (i j : Fin a.size) :
-    (a.swap i j).data = (a.data.set i (a.get j)).set j (a.get i) := by simp [swap_def]
+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]? =
     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_data_get]
+  simp [swap_def, get?_set, ← getElem_fin_eq_toList_get]
 
 @[simp] theorem swapAt_def (a : Array α) (i : Fin a.size) (v : α) :
     a.swapAt i v = (a[i.1], a.set i v) := rfl
@@ -402,7 +445,10 @@ theorem get?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]?
 theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
     a.swapAt! i v = (a[i], a.set ⟨i, h⟩ v) := by simp [swapAt!, h]
 
-@[simp] theorem data_pop (a : Array α) : a.pop.data = a.data.dropLast := by simp [pop]
+@[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
 
@@ -434,7 +480,10 @@ theorem eq_push_of_size_ne_zero {as : Array α} (h : as.size ≠ 0) :
   let _ : Inhabited α := ⟨as[0]⟩
   ⟨as.pop, as.back, eq_push_pop_back_of_size_ne_zero h⟩
 
-theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl
+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]
@@ -458,19 +507,22 @@ theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl
     simp only [mkEmpty_eq, size_push] at *
     omega
 
-@[simp] theorem data_range (n : Nat) : (range n).data = List.range n := by
+@[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_data_getElem]
+  simp [getElem_eq_toList_getElem]
 
 set_option linter.deprecated false in
-@[simp] theorem reverse_data (a : Array α) : a.reverse.data = a.data.reverse := by
+@[simp] theorem reverse_toList (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)
-      (H : ∀ k, as.data.get? k = if i ≤ k ∧ k ≤ j then a.data.get? k else a.data.reverse.get? k)
-      (k) : (reverse.loop as i ⟨j, hj⟩).data.get? k = a.data.reverse.get? k := by
+      (H : ∀ k, as.toList.get? k = if i ≤ k ∧ k ≤ j then a.toList.get? k else a.toList.reverse.get? k)
+      (k) : (reverse.loop as i ⟨j, hj⟩).toList.get? k = a.toList.reverse.get? k := by
     rw [reverse.loop]; dsimp; split <;> rename_i h₁
     · have p := reverse.termination h₁
       match j with | j+1 => ?_
@@ -479,8 +531,9 @@ set_option linter.deprecated false in
       · rwa [Nat.add_right_comm i]
       · simp [size_swap, h₂]
       · intro k
-        rw [← getElem?_eq_data_get?, get?_swap]
-        simp only [H, getElem_eq_data_get, ← List.get?_eq_get, Nat.le_of_lt h₁, getElem?_eq_data_get?]
+        rw [← getElem?_eq_toList_get?, get?_swap]
+        simp only [H, getElem_eq_toList_get, ← List.get?_eq_get, Nat.le_of_lt h₁,
+          getElem?_eq_toList_get?]
         split <;> rename_i h₂
         · simp only [← h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false]
           exact (List.get?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
@@ -505,7 +558,7 @@ set_option linter.deprecated false in
     · rename_i h
       simp only [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := a.size - 1), this, Nat.zero_le,
         true_and, Nat.not_lt] at h
-      rw [List.get?_eq_none.2 ‹_›, List.get?_eq_none.2 (a.data.length_reverse ▸ ‹_›)]
+      rw [List.get?_eq_none.2 ‹_›, List.get?_eq_none.2 (a.toList.length_reverse ▸ ‹_›)]
 
 /-! ### foldl / foldr -/
 
@@ -545,16 +598,19 @@ theorem foldr_induction
 /-! ### map -/
 
 @[simp] theorem mem_map {f : α → β} {l : Array α} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b := by
-  simp only [mem_def, map_data, List.mem_map]
+  simp only [mem_def, map_toList, List.mem_map]
 
-theorem mapM_eq_mapM_data [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
-    arr.mapM f = return mk (← arr.data.mapM f) := by
-  rw [mapM_eq_foldlM, foldlM_eq_foldlM_data, ← List.foldrM_reverse]
-  conv => rhs; rw [← List.reverse_reverse arr.data]
-  induction arr.data.reverse with
+theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
+    arr.mapM f = return mk (← 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; rfl
   | cons a l ih => simp [ih]; simp [map_eq_pure_bind, push]
 
+@[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
@@ -691,86 +747,95 @@ theorem get_modify {arr : Array α} {x i} (h : i < arr.size) :
 
 /-! ### filter -/
 
-@[simp] theorem filter_data (p : α → Bool) (l : Array α) :
-    (l.filter p).data = l.data.filter p := by
+@[simp] theorem filter_toList (p : α → Bool) (l : Array α) :
+    (l.filter p).toList = l.toList.filter p := by
   dsimp only [filter]
-  rw [foldl_eq_foldl_data]
-  generalize l.data = l
-  suffices ∀ a, (List.foldl (fun r a => if p a = true then push r a else r) a l).data =
-      a.data ++ List.filter p l by
+  rw [foldl_eq_foldl_toList]
+  generalize l.toList = l
+  suffices ∀ a, (List.foldl (fun r a => if p a = true then push r a else r) a l).toList =
+      a.toList ++ List.filter p l by
     simpa using this #[]
   induction l with simp
   | cons => split <;> simp [*]
 
+@[deprecated filter_toList (since := "2024-09-09")]
+abbrev filter_data := @filter_toList
+
 @[simp] theorem filter_filter (q) (l : Array α) :
     filter p (filter q l) = filter (fun a => p a && q a) l := by
   apply ext'
-  simp only [filter_data, List.filter_filter]
+  simp only [filter_toList, List.filter_filter]
 
 @[simp] theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x := by
-  simp only [mem_def, filter_data, List.mem_filter]
+  simp only [mem_def, filter_toList, List.mem_filter]
 
 theorem mem_of_mem_filter {a : α} {l} (h : a ∈ filter p l) : a ∈ l :=
   (mem_filter.mp h).1
 
 /-! ### filterMap -/
 
-@[simp] theorem filterMap_data (f : α → Option β) (l : Array α) :
-    (l.filterMap f).data = l.data.filterMap f := by
+@[simp] theorem filterMap_toList (f : α → Option β) (l : Array α) :
+    (l.filterMap f).toList = l.toList.filterMap f := by
   dsimp only [filterMap, filterMapM]
-  rw [foldlM_eq_foldlM_data]
-  generalize l.data = l
-  have this : ∀ a : Array β, (Id.run (List.foldlM (m := Id) ?_ a l)).data =
-    a.data ++ List.filterMap f l := ?_
+  rw [foldlM_eq_foldlM_toList]
+  generalize l.toList = l
+  have this : ∀ a : Array β, (Id.run (List.foldlM (m := Id) ?_ a l)).toList =
+    a.toList ++ List.filterMap f l := ?_
   exact this #[]
   induction l
   · simp_all [Id.run]
   · simp_all [Id.run, List.filterMap_cons]
     split <;> simp_all
 
+@[deprecated filterMap_toList (since := "2024-09-09")]
+abbrev filterMap_data := @filterMap_toList
+
 @[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, filterMap_data, List.mem_filterMap]
+  simp only [mem_def, filterMap_toList, List.mem_filterMap]
 
 /-! ### empty -/
 
 theorem size_empty : (#[] : Array α).size = 0 := rfl
 
-theorem empty_data : (#[] : Array α).data = [] := 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
 
 @[simp] theorem mem_append {a : α} {s t : Array α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
-  simp only [mem_def, append_data, List.mem_append]
+  simp only [mem_def, append_toList, List.mem_append]
 
 theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
-  simp only [size, append_data, List.length_append]
+  simp only [size, append_toList, List.length_append]
 
 theorem get_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
     (as ++ bs)[i] = as[i] := by
-  simp only [getElem_eq_data_getElem]
-  have h' : i < (as.data ++ bs.data).length := by rwa [← data_length, append_data] at h
-  conv => rhs; rw [← List.getElem_append_left (bs := bs.data) (h' := h')]
-  apply List.get_of_eq; rw [append_data]
+  simp only [getElem_eq_toList_getElem]
+  have h' : i < (as.toList ++ bs.toList).length := by rwa [← toList_length, append_toList] at h
+  conv => rhs; rw [← List.getElem_append_left (bs := bs.toList) (h' := h')]
+  apply List.get_of_eq; rw [append_toList]
 
 theorem get_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_data_getElem]
-  have h' : i < (as.data ++ bs.data).length := by rwa [← data_length, append_data] at h
+  simp only [getElem_eq_toList_getElem]
+  have h' : i < (as.toList ++ bs.toList).length := by rwa [← toList_length, append_toList] at h
   conv => rhs; rw [← List.getElem_append_right (h' := h') (h := Nat.not_lt_of_ge hle)]
-  apply List.get_of_eq; rw [append_data]
+  apply List.get_of_eq; rw [append_toList]
 
 @[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by
-  apply ext'; simp only [append_data, empty_data, List.append_nil]
+  apply ext'; simp only [append_toList, toList_empty, List.append_nil]
 
 @[simp] theorem nil_append (as : Array α) : #[] ++ as = as := by
-  apply ext'; simp only [append_data, empty_data, List.nil_append]
+  apply ext'; simp only [append_toList, toList_empty, List.nil_append]
 
 theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) := by
-  apply ext'; simp only [append_data, List.append_assoc]
+  apply ext'; simp only [append_toList, List.append_assoc]
 
 /-! ### extract -/
 
@@ -944,7 +1009,7 @@ 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.data.any p := by
+theorem any_def {p : α → Bool} (as : Array α) : as.any p = as.toList.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⟩⟩
 
@@ -967,14 +1032,14 @@ 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.data.all p := by
+theorem all_def {p : α → Bool} (as : Array α) : as.all p = as.toList.all p := by
   rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]; simp only [List.mem_iff_getElem]
   constructor
   · rintro w x ⟨r, h, rfl⟩
-    rw [← getElem_eq_data_getElem]
+    rw [← getElem_eq_toList_getElem]
     exact w ⟨r, h⟩
   · intro w i
-    exact w as[i] ⟨i, i.2, (getElem_eq_data_getElem as i.2).symm⟩
+    exact w as[i] ⟨i, i.2, (getElem_eq_toList_getElem as i.2).symm⟩
 
 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]
diff --git a/src/Init/Data/Array/Mem.lean b/src/Init/Data/Array/Mem.lean
index 32b68e19f7..c33251ba39 100644
--- a/src/Init/Data/Array/Mem.lean
+++ b/src/Init/Data/Array/Mem.lean
@@ -14,7 +14,7 @@ namespace Array
 -- NB: This is defined as a structure rather than a plain def so that a lemma
 -- like `sizeOf_lt_of_mem` will not apply with no actual arrays around.
 structure Mem (as : Array α) (a : α) : Prop where
-  val : a ∈ as.data
+  val : a ∈ as.toList
 
 instance : Membership α (Array α) where
   mem := Mem
diff --git a/src/Init/Data/Array/TakeDrop.lean b/src/Init/Data/Array/TakeDrop.lean
index 7bfd25d11d..56b73a66aa 100644
--- a/src/Init/Data/Array/TakeDrop.lean
+++ b/src/Init/Data/Array/TakeDrop.lean
@@ -10,8 +10,8 @@ import Init.Data.List.Nat.TakeDrop
 namespace Array
 
 theorem exists_of_uset (self : Array α) (i d h) :
-    ∃ l₁ l₂, self.data = l₁ ++ self[i] :: l₂ ∧ List.length l₁ = i.toNat ∧
-      (self.uset i d h).data = l₁ ++ d :: l₂ := by
-  simpa [Array.getElem_eq_data_getElem] using List.exists_of_set _
+    ∃ l₁ l₂, self.toList = l₁ ++ self[i] :: l₂ ∧ List.length l₁ = i.toNat ∧
+      (self.uset i d h).toList = l₁ ++ d :: l₂ := by
+  simpa [Array.getElem_eq_toList_getElem] using List.exists_of_set _
 
 end Array
diff --git a/src/Init/Data/List/Impl.lean b/src/Init/Data/List/Impl.lean
index 192a8f7da7..c07ac71c8c 100644
--- a/src/Init/Data/List/Impl.lean
+++ b/src/Init/Data/List/Impl.lean
@@ -57,8 +57,8 @@ The following operations are given `@[csimp]` replacements below:
 
 @[csimp] theorem set_eq_setTR : @set = @setTR := by
   funext α l n a; simp [setTR]
-  let rec go (acc) : ∀ xs n, l = acc.data ++ xs →
-    setTR.go l a xs n acc = acc.data ++ xs.set n a
+  let rec go (acc) : ∀ xs n, l = acc.toList ++ xs →
+    setTR.go l a xs n acc = acc.toList ++ xs.set n a
   | [], _ => fun h => by simp [setTR.go, set, h]
   | x::xs, 0 => by simp [setTR.go, set]
   | x::xs, n+1 => fun h => by simp only [setTR.go, set]; rw [go _ xs] <;> simp [h]
@@ -77,10 +77,11 @@ The following operations are given `@[csimp]` replacements below:
 
 @[csimp] theorem filterMap_eq_filterMapTR : @List.filterMap = @filterMapTR := by
   funext α β f l
-  let rec go : ∀ as acc, filterMapTR.go f as acc = acc.data ++ as.filterMap f
+  let rec go : ∀ as acc, filterMapTR.go f as acc = acc.toList ++ as.filterMap f
     | [], acc => by simp [filterMapTR.go, filterMap]
     | a::as, acc => by
-      simp only [filterMapTR.go, go as, Array.push_data, append_assoc, singleton_append, filterMap]
+      simp only [filterMapTR.go, go as, Array.push_toList, append_assoc, singleton_append,
+        filterMap]
       split <;> simp [*]
   exact (go l #[]).symm
 
@@ -90,7 +91,7 @@ The following operations are given `@[csimp]` replacements below:
 @[specialize] def foldrTR (f : α → β → β) (init : β) (l : List α) : β := l.toArray.foldr f init
 
 @[csimp] theorem foldr_eq_foldrTR : @foldr = @foldrTR := by
-  funext α β f init l; simp [foldrTR, Array.foldr_eq_foldr_data, -Array.size_toArray]
+  funext α β f init l; simp [foldrTR, Array.foldr_eq_foldr_toList, -Array.size_toArray]
 
 /-! ### bind  -/
 
@@ -103,7 +104,7 @@ The following operations are given `@[csimp]` replacements below:
 
 @[csimp] theorem bind_eq_bindTR : @List.bind = @bindTR := by
   funext α β as f
-  let rec go : ∀ as acc, bindTR.go f as acc = acc.data ++ as.bind f
+  let rec go : ∀ as acc, bindTR.go f as acc = acc.toList ++ as.bind f
     | [], acc => by simp [bindTR.go, bind]
     | x::xs, acc => by simp [bindTR.go, bind, go xs]
   exact (go as #[]).symm
@@ -131,7 +132,7 @@ The following operations are given `@[csimp]` replacements below:
 
 @[csimp] theorem take_eq_takeTR : @take = @takeTR := by
   funext α n l; simp [takeTR]
-  suffices ∀ xs acc, l = acc.data ++ xs → takeTR.go l xs n acc = acc.data ++ xs.take n from
+  suffices ∀ xs acc, l = acc.toList ++ xs → takeTR.go l xs n acc = acc.toList ++ xs.take n from
     (this l #[] (by simp)).symm
   intro xs; induction xs generalizing n with intro acc
   | nil => cases n <;> simp [take, takeTR.go]
@@ -152,13 +153,13 @@ The following operations are given `@[csimp]` replacements below:
 
 @[csimp] theorem takeWhile_eq_takeWhileTR : @takeWhile = @takeWhileTR := by
   funext α p l; simp [takeWhileTR]
-  suffices ∀ xs acc, l = acc.data ++ xs →
-      takeWhileTR.go p l xs acc = acc.data ++ xs.takeWhile p from
+  suffices ∀ xs acc, l = acc.toList ++ xs →
+      takeWhileTR.go p l xs acc = acc.toList ++ xs.takeWhile p from
     (this l #[] (by simp)).symm
   intro xs; induction xs with intro acc
   | nil => simp [takeWhile, takeWhileTR.go]
   | cons x xs IH =>
-    simp only [takeWhileTR.go, Array.toList_eq, takeWhile]
+    simp only [takeWhileTR.go, Array.toListImpl_eq, takeWhile]
     split
     · intro h; rw [IH] <;> simp_all
     · simp [*]
@@ -185,8 +186,8 @@ The following operations are given `@[csimp]` replacements below:
 
 @[csimp] theorem replace_eq_replaceTR : @List.replace = @replaceTR := by
   funext α _ l b c; simp [replaceTR]
-  suffices ∀ xs acc, l = acc.data ++ xs →
-      replaceTR.go l b c xs acc = acc.data ++ xs.replace b c from
+  suffices ∀ xs acc, l = acc.toList ++ xs →
+      replaceTR.go l b c xs acc = acc.toList ++ xs.replace b c from
     (this l #[] (by simp)).symm
   intro xs; induction xs with intro acc
   | nil => simp [replace, replaceTR.go]
@@ -208,7 +209,7 @@ The following operations are given `@[csimp]` replacements below:
 
 @[csimp] theorem erase_eq_eraseTR : @List.erase = @eraseTR := by
   funext α _ l a; simp [eraseTR]
-  suffices ∀ xs acc, l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ xs.erase a from
+  suffices ∀ xs acc, l = acc.toList ++ xs → eraseTR.go l a xs acc = acc.toList ++ xs.erase a from
     (this l #[] (by simp)).symm
   intro xs; induction xs with intro acc h
   | nil => simp [List.erase, eraseTR.go, h]
@@ -228,8 +229,8 @@ The following operations are given `@[csimp]` replacements below:
 
 @[csimp] theorem eraseP_eq_erasePTR : @eraseP = @erasePTR := by
   funext α p l; simp [erasePTR]
-  let rec go (acc) : ∀ xs, l = acc.data ++ xs →
-    erasePTR.go p l xs acc = acc.data ++ xs.eraseP p
+  let rec go (acc) : ∀ xs, l = acc.toList ++ xs →
+    erasePTR.go p l xs acc = acc.toList ++ xs.eraseP p
   | [] => fun h => by simp [erasePTR.go, eraseP, h]
   | x::xs => by
     simp [erasePTR.go, eraseP]; cases p x <;> simp
@@ -249,7 +250,7 @@ The following operations are given `@[csimp]` replacements below:
 
 @[csimp] theorem eraseIdx_eq_eraseIdxTR : @eraseIdx = @eraseIdxTR := by
   funext α l n; simp [eraseIdxTR]
-  suffices ∀ xs acc, l = acc.data ++ xs → eraseIdxTR.go l xs n acc = acc.data ++ xs.eraseIdx n from
+  suffices ∀ xs acc, l = acc.toList ++ xs → eraseIdxTR.go l xs n acc = acc.toList ++ xs.eraseIdx n from
     (this l #[] (by simp)).symm
   intro xs; induction xs generalizing n with intro acc h
   | nil => simp [eraseIdx, eraseIdxTR.go, h]
@@ -273,7 +274,7 @@ The following operations are given `@[csimp]` replacements below:
 
 @[csimp] theorem zipWith_eq_zipWithTR : @zipWith = @zipWithTR := by
   funext α β γ f as bs
-  let rec go : ∀ as bs acc, zipWithTR.go f as bs acc = acc.data ++ as.zipWith f bs
+  let rec go : ∀ as bs acc, zipWithTR.go f as bs acc = acc.toList ++ as.zipWith f bs
     | [], _, acc | _::_, [], acc => by simp [zipWithTR.go, zipWith]
     | a::as, b::bs, acc => by simp [zipWithTR.go, zipWith, go as bs]
   exact (go as bs #[]).symm
@@ -295,7 +296,7 @@ def enumFromTR (n : Nat) (l : List α) : List (Nat × α) :=
     | a::as, n => by
       rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as]
       simp [enumFrom, f]
-  rw [Array.foldr_eq_foldr_data]
+  rw [Array.foldr_eq_foldr_toList]
   simp [go]
 
 /-! ## Other list operations -/
@@ -321,7 +322,7 @@ where
   | [_] => simp
   | x::y::xs =>
     let rec go {acc x} : ∀ xs,
-      intercalateTR.go sep.toArray x xs acc = acc.data ++ join (intersperse sep (x::xs))
+      intercalateTR.go sep.toArray x xs acc = acc.toList ++ join (intersperse sep (x::xs))
     | [] => by simp [intercalateTR.go]
     | _::_ => by simp [intercalateTR.go, go]
     simp [intersperse, go]
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index aa2a25ad5d..a690c5c399 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -2568,17 +2568,17 @@ structure Array (α : Type u) where
   /--
   Converts a `Array α` into an `List α`.
 
-  At runtime, this projection is implemented by `Array.toList` and is O(n) in the length of the
+  At runtime, this projection is implemented by `Array.toListImpl` and is O(n) in the length of the
   array. -/
-  data : List α
+  toList : List α
 
-attribute [extern "lean_array_data"] Array.data
+attribute [extern "lean_array_to_list"] Array.toList
 attribute [extern "lean_array_mk"] Array.mk
 
 /-- Construct a new empty array with initial capacity `c`. -/
 @[extern "lean_mk_empty_array_with_capacity"]
 def Array.mkEmpty {α : Type u} (c : @& Nat) : Array α where
-  data := List.nil
+  toList := List.nil
 
 /-- Construct a new empty array. -/
 def Array.empty {α : Type u} : Array α := mkEmpty 0
@@ -2586,12 +2586,12 @@ def Array.empty {α : Type u} : Array α := mkEmpty 0
 /-- Get the size of an array. This is a cached value, so it is O(1) to access. -/
 @[reducible, extern "lean_array_get_size"]
 def Array.size {α : Type u} (a : @& Array α) : Nat :=
- a.data.length
+ a.toList.length
 
 /-- Access an element from an array without bounds checks, using a `Fin` index. -/
 @[extern "lean_array_fget"]
 def Array.get {α : Type u} (a : @& Array α) (i : @& Fin a.size) : α :=
-  a.data.get i
+  a.toList.get i
 
 /-- Access an element from an array, or return `v₀` if the index is out of bounds. -/
 @[inline] abbrev Array.getD (a : Array α) (i : Nat) (v₀ : α) : α :=
@@ -2608,7 +2608,7 @@ Push an element onto the end of an array. This is amortized O(1) because
 -/
 @[extern "lean_array_push"]
 def Array.push {α : Type u} (a : Array α) (v : α) : Array α where
-  data := List.concat a.data v
+  toList := List.concat a.toList v
 
 /-- Create array `#[]` -/
 def Array.mkArray0 {α : Type u} : Array α :=
@@ -2654,7 +2654,7 @@ count of 1 when called.
 -/
 @[extern "lean_array_fset"]
 def Array.set (a : Array α) (i : @& Fin a.size) (v : α) : Array α where
-  data := a.data.set i.val v
+  toList := a.toList.set i.val v
 
 /--
 Set an element in an array, or do nothing if the index is out of bounds.
diff --git a/src/Std/Data/DHashMap/Internal/Defs.lean b/src/Std/Data/DHashMap/Internal/Defs.lean
index 5c27e31bca..c7a18fd167 100644
--- a/src/Std/Data/DHashMap/Internal/Defs.lean
+++ b/src/Std/Data/DHashMap/Internal/Defs.lean
@@ -156,7 +156,7 @@ namespace DHashMap.Internal
 
 /-- Internal implementation detail of the hash map -/
 def toListModel (buckets : Array (AssocList α β)) : List ((a : α) × β a) :=
-  buckets.data.bind AssocList.toList
+  buckets.toList.bind AssocList.toList
 
 /-- Internal implementation detail of the hash map -/
 @[inline] def computeSize (buckets : Array (AssocList α β)) : Nat :=
diff --git a/src/Std/Data/DHashMap/Internal/Model.lean b/src/Std/Data/DHashMap/Internal/Model.lean
index fd95bc4b51..e6d25ef7a4 100644
--- a/src/Std/Data/DHashMap/Internal/Model.lean
+++ b/src/Std/Data/DHashMap/Internal/Model.lean
@@ -121,7 +121,7 @@ theorem exists_bucket_of_update [BEq α] [Hashable α] (m : Array (AssocList α
 
 theorem exists_bucket' [BEq α] [Hashable α]
     (self : Array (AssocList α β)) (i : USize) (hi : i.toNat < self.size) :
-      ∃ l, Perm (self.data.bind AssocList.toList) (self[i.toNat].toList ++ l) ∧
+      ∃ l, Perm (self.toList.bind AssocList.toList) (self[i.toNat].toList ++ l) ∧
         (∀ [LawfulHashable α], IsHashSelf self → ∀ k,
           (mkIdx self.size (by omega) (hash k)).1.toNat = i.toNat → containsKey k l = false) := by
   obtain ⟨l, h₁, -, h₂⟩ := exists_bucket_of_uset self i hi .nil
@@ -186,13 +186,13 @@ theorem toListModel_updateAllBuckets {m : Raw₀ α β} {f : AssocList α β →
     have := (hg (l := []) (l' := [])).length_eq
     rw [List.length_append, List.append_nil] at this
     omega
-  rw [updateAllBuckets, toListModel, Array.map_data, List.bind_eq_foldl, List.foldl_map,
+  rw [updateAllBuckets, toListModel, Array.map_toList, List.bind_eq_foldl, List.foldl_map,
     toListModel, List.bind_eq_foldl]
   suffices ∀ (l : List (AssocList α β)) (l' : List ((a: α) × δ a)) (l'' : List ((a : α) × β a)),
       Perm (g l'') l' →
       Perm (l.foldl (fun acc a => acc ++ (f a).toList) l')
         (g (l.foldl (fun acc a => acc ++ a.toList) l'')) by
-    simpa using this m.1.buckets.data [] [] (by simp [hg₀])
+    simpa using this m.1.buckets.toList [] [] (by simp [hg₀])
   rintro l l' l'' h
   induction l generalizing l' l''
   · simpa using h.symm
diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean
index 989d6a6cbc..3d52b7a1fc 100644
--- a/src/Std/Data/DHashMap/Internal/WF.lean
+++ b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -38,11 +38,11 @@ theorem toListModel_mkArray_nil {c} :
 @[simp]
 theorem computeSize_eq {buckets : Array (AssocList α β)} :
     computeSize buckets = (toListModel buckets).length := by
-  rw [computeSize, toListModel, List.bind_eq_foldl, Array.foldl_eq_foldl_data]
+  rw [computeSize, toListModel, List.bind_eq_foldl, Array.foldl_eq_foldl_toList]
   suffices ∀ (l : List (AssocList α β)) (l' : List ((a : α) × β a)),
       l.foldl (fun d b => d + b.toList.length) l'.length =
         (l.foldl (fun acc a => acc ++ a.toList) l').length
-    by simpa using this buckets.data []
+    by simpa using this buckets.toList []
   intro l l'
   induction l generalizing l'
   · simp
@@ -129,7 +129,7 @@ theorem expand.go_eq [BEq α] [Hashable α] [PartialEquivBEq α] (source : Array
     (target : {d : Array (AssocList α β) // 0 < d.size}) : expand.go 0 source target =
       (toListModel source).foldl (fun acc p => reinsertAux hash acc p.1 p.2) target := by
   suffices ∀ i, expand.go i source target =
-    ((source.data.drop i).bind AssocList.toList).foldl
+    ((source.toList.drop i).bind AssocList.toList).foldl
       (fun acc p => reinsertAux hash acc p.1 p.2) target by
     simpa using this 0
   intro i
@@ -138,12 +138,12 @@ theorem expand.go_eq [BEq α] [Hashable α] [PartialEquivBEq α] (source : Array
     simp only [newSource, newTarget, es] at *
     rw [expand.go_pos hi]
     refine ih.trans ?_
-    simp only [Array.get_eq_getElem, AssocList.foldl_eq, Array.data_set]
+    simp only [Array.get_eq_getElem, AssocList.foldl_eq, Array.toList_set]
     rw [List.drop_eq_getElem_cons hi, List.bind_cons, List.foldl_append,
-      List.drop_set_of_lt _ _ (by omega), Array.getElem_eq_data_getElem]
+      List.drop_set_of_lt _ _ (by omega), Array.getElem_eq_toList_getElem]
   · next i source target hi =>
     rw [expand.go_neg hi, List.drop_eq_nil_of_le, bind_nil, foldl_nil]
-    rwa [Array.size_eq_length_data, Nat.not_lt] at hi
+    rwa [Array.size_eq_length_toList, Nat.not_lt] at hi
 
 theorem isHashSelf_expand [BEq α] [Hashable α] [LawfulHashable α] [EquivBEq α]
     {buckets : {d : Array (AssocList α β) // 0 < d.size}} : IsHashSelf (expand buckets).1 := by
diff --git a/src/Std/Sat/AIG/Lemmas.lean b/src/Std/Sat/AIG/Lemmas.lean
index b294d16ff3..85d81f4642 100644
--- a/src/Std/Sat/AIG/Lemmas.lean
+++ b/src/Std/Sat/AIG/Lemmas.lean
@@ -277,7 +277,7 @@ theorem denote_congr (assign1 assign2 : α → Bool) (aig : AIG α) (idx : Nat)
     simp only [denote_idx_atom heq]
     apply h
     rw [mem_def, ← heq, Array.mem_def]
-    apply Array.getElem_mem_data
+    apply Array.getElem_mem_toList
   · intro lhs rhs linv rinv heq
     simp only [denote_idx_gate heq]
     have := aig.invariant hidx heq
diff --git a/src/Std/Tactic/BVDecide/LRAT/Checker.lean b/src/Std/Tactic/BVDecide/LRAT/Checker.lean
index 5c3d39a1b7..5bed41df13 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Checker.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Checker.lean
@@ -62,7 +62,7 @@ theorem check_sound (lratProof : Array IntAction) (cnf : CNF Nat) :
       _
       (by
         intro action h
-        simp only [Array.toList_eq, List.filterMap_map, List.mem_filterMap, Function.comp_apply] at h
+        simp only [List.filterMap_map, List.mem_filterMap, Function.comp_apply] at h
         rcases h with ⟨WellFormedActions, _, h2⟩
         split at h2
         . contradiction
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean
index c60edb14af..bd318fc498 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean
@@ -113,7 +113,7 @@ theorem limplies_insert [Clause α β] [Entails α σ] [Formula α β σ] {c : 
   simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq]
   intro h c' c'_in_f
   have c'_in_fc : c' ∈ toList (insert f c) := by
-    simp only [insert_iff, Array.toList_eq, Array.data_toArray, List.mem_singleton]
+    simp only [insert_iff, Array.toList_toArray, List.mem_singleton]
     exact Or.inr c'_in_f
   exact h c' c'_in_fc
 
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean
index d274687ae4..9d41210870 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean
@@ -223,7 +223,7 @@ theorem ofArray_eq (arr : Array (Literal (PosFin n)))
     ofArray arr = some c → toList c = Array.toList arr := by
   intro h
   simp only [ofArray] at h
-  rw [toList, Array.toList_eq]
+  rw [toList]
   let motive (idx : Nat) (acc : Option (DefaultClause n)) : Prop :=
     ∃ idx_le_arr_size : idx ≤ arr.size, ∀ c' : DefaultClause n, acc = some c' →
       ∃ hsize : c'.clause.length = arr.size - idx, ∀ i : Fin c'.clause.length,
@@ -293,13 +293,13 @@ theorem ofArray_eq (arr : Array (Literal (PosFin n)))
   next i l =>
   by_cases i_in_bounds : i < c.clause.length
   · specialize h ⟨i, i_in_bounds⟩
-    have i_in_bounds' : i < arr.data.length := by
+    have i_in_bounds' : i < arr.toList.length := by
       dsimp; omega
     rw [List.getElem?_eq_getElem i_in_bounds, List.getElem?_eq_getElem i_in_bounds']
     simp only [List.get_eq_getElem, Nat.zero_add] at h
-    rw [← Array.getElem_eq_data_getElem]
+    rw [← Array.getElem_eq_toList_getElem]
     simp [h]
-  · have arr_data_length_le_i : arr.data.length ≤ i := by
+  · have arr_data_length_le_i : arr.toList.length ≤ i := by
       dsimp; omega
     simp only [Nat.not_lt, ← List.getElem?_eq_none_iff] at i_in_bounds arr_data_length_le_i
     rw [i_in_bounds, arr_data_length_le_i]
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
index 7da58ac52f..d08241e95b 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
@@ -61,7 +61,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
   | nil => cases h1
   | cons hd tl ih =>
     unfold DefaultClause.ofArray at h2
-    rw [Array.foldr_eq_foldr_data, Array.toArray_data] at h2
+    rw [Array.foldr_eq_foldr_toList, Array.toArray_toList] at h2
     dsimp only [List.foldr] at h2
     split at h2
     · cases h2
@@ -77,7 +77,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
             · assumption
             · next heq _ _ =>
               unfold DefaultClause.ofArray
-              rw [Array.foldr_eq_foldr_data, Array.toArray_data]
+              rw [Array.foldr_eq_foldr_toList, Array.toArray_toList]
               exact heq
         · cases h1
           · simp only [← Option.some.inj h2]
@@ -89,7 +89,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
             apply ih
             assumption
             unfold DefaultClause.ofArray
-            rw [Array.foldr_eq_foldr_data, Array.toArray_data]
+            rw [Array.foldr_eq_foldr_toList, Array.toArray_toList]
             exact heq
 
 theorem CNF.Clause.convertLRAT_sat_of_sat (clause : CNF.Clause (PosFin n))
@@ -155,7 +155,7 @@ theorem CNF.unsat_of_convertLRAT_unsat (cnf : CNF Nat) :
   simp only [Formula.formulaEntails_def, List.all_eq_true, decide_eq_true_eq]
   intro lratClause hlclause
   simp only [Formula.toList, DefaultFormula.toList, DefaultFormula.ofArray,
-    CNF.convertLRAT', Array.size_toArray, List.length_map, Array.toList_eq, Array.data_toArray,
+    CNF.convertLRAT', Array.size_toArray, List.length_map, Array.toList_toArray,
     List.map_nil, List.append_nil, List.mem_filterMap, List.mem_map, id_eq, exists_eq_right] at hlclause
   rcases hlclause with ⟨reflectClause, ⟨hrclause1, hrclause2⟩⟩
   simp only [CNF.eval, List.all_eq_true] at h2
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
index a9146eed96..a87390e5d4 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
@@ -106,11 +106,11 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
   constructor
   · simp only [ofArray]
   · have hsize : (ofArray arr).assignments.size = n := by
-      simp only [ofArray, Array.foldl_eq_foldl_data]
+      simp only [ofArray, Array.foldl_eq_foldl_toList]
       have hb : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
-      have hl (acc : Array Assignment) (ih : acc.size = n) (cOpt : Option (DefaultClause n)) (_cOpt_in_arr : cOpt ∈ arr.data) :
+      have hl (acc : Array Assignment) (ih : acc.size = n) (cOpt : Option (DefaultClause n)) (_cOpt_in_arr : cOpt ∈ arr.toList) :
         (ofArray_fold_fn acc cOpt).size = n := by rw [size_ofArray_fold_fn acc cOpt, ih]
-      exact List.foldlRecOn arr.data ofArray_fold_fn (mkArray n unassigned) hb hl
+      exact List.foldlRecOn arr.toList ofArray_fold_fn (mkArray n unassigned) hb hl
     apply Exists.intro hsize
     let ModifiedAssignmentsInvariant (assignments : Array Assignment) : Prop :=
       ∃ hsize : assignments.size = n,
@@ -122,7 +122,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
       intro i b h
       by_cases hb : b <;> simp [hasAssignment, hb, hasPosAssignment, hasNegAssignment] at h
     have hl (acc : Array Assignment) (ih : ModifiedAssignmentsInvariant acc) (cOpt : Option (DefaultClause n))
-      (cOpt_in_arr : cOpt ∈ arr.data) : ModifiedAssignmentsInvariant (ofArray_fold_fn acc cOpt) := by
+      (cOpt_in_arr : cOpt ∈ arr.toList) : ModifiedAssignmentsInvariant (ofArray_fold_fn acc cOpt) := by
       have hsize : (ofArray_fold_fn acc cOpt).size = n := by rw [size_ofArray_fold_fn, ih.1]
       apply Exists.intro hsize
       intro i b h
@@ -145,7 +145,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
             by_cases b
             · next b_eq_true =>
               rw [isUnit_iff, DefaultClause.toList] at heq
-              simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
+              simp only [toList, ofArray, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
               have i_eq_l : i = l := Subtype.ext i_eq_l
               simp only [unit, b_eq_true, i_eq_l]
               have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
@@ -179,7 +179,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
               exact ih h
             · next b_eq_false =>
               rw [isUnit_iff, DefaultClause.toList] at heq
-              simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
+              simp only [toList, ofArray, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
               have i_eq_l : i = l := Subtype.ext i_eq_l
               simp only [unit, b_eq_false, i_eq_l]
               have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
@@ -189,9 +189,9 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
           · next i_ne_l =>
             simp only [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l)] at h
             exact ih i b h
-    rcases List.foldlRecOn arr.data ofArray_fold_fn (mkArray n unassigned) hb hl with ⟨_h_size, h'⟩
+    rcases List.foldlRecOn arr.toList ofArray_fold_fn (mkArray n unassigned) hb hl with ⟨_h_size, h'⟩
     intro i b h
-    simp only [ofArray, Array.foldl_eq_foldl_data] at h
+    simp only [ofArray, Array.foldl_eq_foldl_toList] at h
     exact h' i b h
 
 theorem readyForRatAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))) :
@@ -202,7 +202,7 @@ theorem readyForRatAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
 
 theorem insert_iff {n : Nat} (f : DefaultFormula n) (c1 : DefaultClause n) (c2 : DefaultClause n) :
     c2 ∈ toList (insert f c1) ↔ c2 = c1 ∨ c2 ∈ toList f := by
-  simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right,
+  simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right,
     List.mem_map, Prod.exists, Bool.exists_bool]
   by_cases c2 = c1
   · next c2_eq_c1 =>
@@ -222,7 +222,7 @@ theorem insert_iff {n : Nat} (f : DefaultFormula n) (c1 : DefaultClause n) (c2 :
         simp only [insert] at h
         split at h
         all_goals
-          simp only [Array.push_data, List.mem_append, List.mem_singleton, Option.some.injEq] at h
+          simp only [Array.push_toList, List.mem_append, List.mem_singleton, Option.some.injEq] at h
           rcases h with h | h
           · exact h
           · exact False.elim <| c2_ne_c1 h
@@ -237,7 +237,7 @@ theorem insert_iff {n : Nat} (f : DefaultFormula n) (c1 : DefaultClause n) (c2 :
         simp only [insert]
         split
         all_goals
-          simp only [Array.push_data, List.mem_append, List.mem_singleton, Option.some.injEq]
+          simp only [Array.push_toList, List.mem_append, List.mem_singleton, Option.some.injEq]
           exact Or.inl h
       · rw [rupUnits_insert]
         exact Or.inr <| Or.inl h
@@ -250,7 +250,7 @@ theorem limplies_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
   simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq]
   intro h c' c'_in_f
   have c'_in_fc : c' ∈ toList (insert f c) := by
-    simp only [insert_iff, Array.toList_eq, Array.data_toArray, List.mem_singleton]
+    simp only [insert_iff, Array.toList_toArray, List.mem_singleton]
     exact Or.inr c'_in_f
   exact h c' c'_in_fc
 
@@ -267,9 +267,9 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
   · refine ⟨f_readyForRupAdd.1, f_readyForRupAdd.2.1, ?_⟩
     intro i b hb
     have hf := f_readyForRupAdd.2.2 i b hb
-    simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right,
+    simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right,
       List.mem_map, Prod.exists, Bool.exists_bool] at hf
-    simp only [toList, Array.toList_eq, Array.push_data, List.append_assoc, List.mem_append, List.mem_filterMap,
+    simp only [toList, Array.push_toList, List.append_assoc, List.mem_append, List.mem_filterMap,
       List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]
     rcases hf with hf | hf
     · exact (Or.inl ∘ Or.inl) hf
@@ -285,7 +285,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
     simp only at hb
     by_cases (i, b) = (l, true)
     · next ib_eq_c =>
-      simp only [toList, Array.toList_eq, Array.push_data, List.append_assoc, List.mem_append, List.mem_filterMap,
+      simp only [toList, Array.push_toList, List.append_assoc, List.mem_append, List.mem_filterMap,
         List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]
       apply Or.inl ∘ Or.inr
       rw [isUnit_iff, DefaultClause.toList, ← ib_eq_c] at hc
@@ -308,9 +308,9 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
           simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
           exact hb
       specialize hf hb'
-      simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
+      simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
         exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
-      simp only [toList, Array.toList_eq, Array.push_data, List.append_assoc, List.mem_append, List.mem_filterMap,
+      simp only [toList, Array.push_toList, List.append_assoc, List.mem_append, List.mem_filterMap,
         List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]
       rcases hf with hf | hf
       · exact Or.inl <| Or.inl hf
@@ -326,7 +326,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
     simp only at hb
     by_cases (i, b) = (l, false)
     · next ib_eq_c =>
-      simp only [toList, Array.toList_eq, Array.push_data, List.append_assoc, List.mem_append, List.mem_filterMap,
+      simp only [toList, Array.push_toList, List.append_assoc, List.mem_append, List.mem_filterMap,
         List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]
       apply Or.inl ∘ Or.inr
       rw [isUnit_iff, DefaultClause.toList, ← ib_eq_c] at hc
@@ -347,9 +347,9 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
           simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
           exact hb
       specialize hf hb'
-      simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
+      simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
         exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
-      simp only [toList, Array.toList_eq, Array.push_data, List.append_assoc, List.mem_append, List.mem_filterMap,
+      simp only [toList, Array.push_toList, List.append_assoc, List.mem_append, List.mem_filterMap,
         List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]
       rcases hf with hf | hf
       · exact Or.inl <| Or.inl hf
@@ -365,22 +365,22 @@ theorem readyForRatAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
 theorem mem_of_insertRupUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clause (PosFin n))
     (c : DefaultClause n) :
     c ∈ toList (insertRupUnits f units).1 → c ∈ units.map Clause.unit ∨ c ∈ toList f := by
-  simp only [toList, insertRupUnits, Array.toList_eq, List.append_assoc, List.mem_append,
+  simp only [toList, insertRupUnits, List.append_assoc, List.mem_append,
     List.mem_filterMap, id_eq, exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
   intro h
-  have hb : ∀ l : Literal (PosFin n), l ∈ (f.rupUnits, f.assignments, false).1.data → (l ∈ f.rupUnits.data ∨ l ∈ units) := by
+  have hb : ∀ l : Literal (PosFin n), l ∈ (f.rupUnits, f.assignments, false).1.toList → (l ∈ f.rupUnits.toList ∨ l ∈ units) := by
     intro l hl
     exact Or.inl hl
   have hl (acc : Array (Literal (PosFin n)) × Array Assignment × Bool)
-    (ih : ∀ l : Literal (PosFin n), l ∈ acc.1.data → l ∈ f.rupUnits.data ∨ l ∈ units)
+    (ih : ∀ l : Literal (PosFin n), l ∈ acc.1.toList → l ∈ f.rupUnits.toList ∨ l ∈ units)
     (unit : Literal (PosFin n)) (unit_in_units : unit ∈ units) :
-    ∀ l : Literal (PosFin n), l ∈ (insertUnit acc unit).1.data → (l ∈ f.rupUnits.data ∨ l ∈ units) := by
+    ∀ l : Literal (PosFin n), l ∈ (insertUnit acc unit).1.toList → (l ∈ f.rupUnits.toList ∨ l ∈ units) := by
     intro l hl
     rw [insertUnit.eq_def] at hl
     dsimp at hl
     split at hl
     · exact ih l hl
-    · simp only [Array.push_data, List.mem_append, List.mem_singleton] at hl
+    · simp only [Array.push_toList, List.mem_append, List.mem_singleton] at hl
       rcases hl with l_in_acc | l_eq_unit
       · exact ih l l_in_acc
       · rw [l_eq_unit]
@@ -403,21 +403,21 @@ theorem mem_of_insertRupUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clau
 theorem mem_of_insertRatUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clause (PosFin n))
     (c : DefaultClause n) :
     c ∈ toList (insertRatUnits f units).1 → c ∈ units.map Clause.unit ∨ c ∈ toList f := by
-  simp only [toList, insertRatUnits, Array.toList_eq, List.append_assoc, List.mem_append,
+  simp only [toList, insertRatUnits, List.append_assoc, List.mem_append,
     List.mem_filterMap, id_eq, exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
   intro h
-  have hb : ∀ l : Literal (PosFin n), l ∈ (f.ratUnits, f.assignments, false).1.data → (l ∈ f.ratUnits.data ∨ l ∈ units) :=
+  have hb : ∀ l : Literal (PosFin n), l ∈ (f.ratUnits, f.assignments, false).1.toList → (l ∈ f.ratUnits.toList ∨ l ∈ units) :=
     fun _ => Or.inl
   have hl (acc : Array (Literal (PosFin n)) × Array Assignment × Bool)
-    (ih : ∀ l : Literal (PosFin n), l ∈ acc.1.data → l ∈ f.ratUnits.data ∨ l ∈ units)
+    (ih : ∀ l : Literal (PosFin n), l ∈ acc.1.toList → l ∈ f.ratUnits.toList ∨ l ∈ units)
     (unit : Literal (PosFin n)) (unit_in_units : unit ∈ units) :
-    ∀ l : Literal (PosFin n), l ∈ (insertUnit acc unit).1.data → (l ∈ f.ratUnits.data ∨ l ∈ units) := by
+    ∀ l : Literal (PosFin n), l ∈ (insertUnit acc unit).1.toList → (l ∈ f.ratUnits.toList ∨ l ∈ units) := by
     intro l hl
     rw [insertUnit.eq_def] at hl
     dsimp at hl
     split at hl
     · exact ih l hl
-    · simp only [Array.push_data, List.mem_append, List.mem_singleton] at hl
+    · simp only [Array.push_toList, List.mem_append, List.mem_singleton] at hl
       rcases hl with l_in_acc | l_eq_unit
       · exact ih l l_in_acc
       · rw [l_eq_unit]
@@ -481,18 +481,18 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
         rw [l_ne_b] at hb
         have hb := has_remove_irrelevant f.assignments[i.1] b hb
         specialize hf i b hb
-        simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
+        simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
           exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
-        simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
+        simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
           exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
         rcases hf with hf | hf
         · apply Or.inl
           simp only [Array.set!, Array.setD]
           split
           · rcases List.getElem_of_mem hf with ⟨idx, hbound, hidx⟩
-            simp only [← hidx, Array.data_set]
+            simp only [← hidx, Array.toList_set]
             rw [List.mem_iff_get]
-            have idx_in_bounds : idx < List.length (List.set f.clauses.data id none) := by
+            have idx_in_bounds : idx < List.length (List.set f.clauses.toList id none) := by
               simp only [List.length_set]
               exact hbound
             apply Exists.intro ⟨idx, idx_in_bounds⟩
@@ -500,11 +500,11 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
             · next id_eq_idx =>
               exfalso
               have idx_in_bounds2 : idx < f.clauses.size := by
-                have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
+                have f_clauses_rw : f.clauses = { toList := f.clauses.toList } := rfl
                 conv => rhs; rw [f_clauses_rw, Array.size_mk]
                 exact hbound
-              simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDIte,
-                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_getElem, decidableGetElem?] at heq
+              simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
+                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, decidableGetElem?] at heq
               rw [hidx, hl] at heq
               simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
               simp only [← heq, not] at l_ne_b
@@ -515,18 +515,18 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
       · next l_ne_i =>
         simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
         specialize hf i b hb
-        simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
+        simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
           exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
-        simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
+        simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
           exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
         rcases hf with hf | hf
         · apply Or.inl
           simp only [Array.set!, Array.setD]
           split
           · rcases List.getElem_of_mem hf with ⟨idx, hbound, hidx⟩
-            simp only [← hidx, Array.data_set]
+            simp only [← hidx, Array.toList_set]
             rw [List.mem_iff_get]
-            have idx_in_bounds : idx < List.length (List.set f.clauses.data id none) := by
+            have idx_in_bounds : idx < List.length (List.set f.clauses.toList id none) := by
               simp only [List.length_set]
               exact hbound
             apply Exists.intro ⟨idx, idx_in_bounds⟩
@@ -534,11 +534,11 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
             · next id_eq_idx =>
               exfalso
               have idx_in_bounds2 : idx < f.clauses.size := by
-                have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
+                have f_clauses_rw : f.clauses = { toList := f.clauses.toList } := rfl
                 conv => rhs; rw [f_clauses_rw, Array.size_mk]
                 exact hbound
-              simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDIte,
-                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_getElem, decidableGetElem?] at heq
+              simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
+                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, decidableGetElem?] at heq
               rw [hidx, hl] at heq
               simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
               have i_eq_l : i = l.1 := by rw [← heq]
@@ -576,18 +576,18 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
           · rfl
         simp only [deleteOne_f_rw] at hb
         specialize hf i b hb
-        simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
+        simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
           exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
-        simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
+        simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
           exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
         rcases hf with hf | hf
         · apply Or.inl
           simp only [Array.set!, Array.setD]
           split
           · rcases List.getElem_of_mem hf with ⟨idx, hbound, hidx⟩
-            simp only [← hidx, Array.data_set]
+            simp only [← hidx, Array.toList_set]
             rw [List.mem_iff_get]
-            have idx_in_bounds : idx < List.length (List.set f.clauses.data id none) := by
+            have idx_in_bounds : idx < List.length (List.set f.clauses.toList id none) := by
               simp only [List.length_set]
               exact hbound
             apply Exists.intro ⟨idx, idx_in_bounds⟩
@@ -595,11 +595,11 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
             · next id_eq_idx =>
               exfalso
               have idx_in_bounds2 : idx < f.clauses.size := by
-                have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
+                have f_clauses_rw : f.clauses = { toList := f.clauses.toList } := rfl
                 conv => rhs; rw [f_clauses_rw, Array.size_mk]
                 exact hbound
-              simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDIte,
-                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_getElem, decidableGetElem?] at heq
+              simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
+                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, decidableGetElem?] at heq
               rw [hidx] at heq
               simp only [Option.some.injEq] at heq
               rw [← heq] at hl
@@ -614,16 +614,16 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
 theorem readyForRupAdd_delete {n : Nat} (f : DefaultFormula n) (arr : Array Nat) :
     ReadyForRupAdd f → ReadyForRupAdd (delete f arr) := by
   intro h
-  rw [delete, Array.foldl_eq_foldl_data]
+  rw [delete, Array.foldl_eq_foldl_toList]
   constructor
   · have hb : f.rupUnits = #[] := h.1
-    have hl (acc : DefaultFormula n) (ih : acc.rupUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.data) :
+    have hl (acc : DefaultFormula n) (ih : acc.rupUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.toList) :
       (deleteOne acc id).rupUnits = #[] := by rw [deleteOne_preserves_rupUnits, ih]
-    exact List.foldlRecOn arr.data deleteOne f hb hl
+    exact List.foldlRecOn arr.toList deleteOne f hb hl
   · have hb : StrongAssignmentsInvariant f := h.2
-    have hl (acc : DefaultFormula n) (ih : StrongAssignmentsInvariant acc) (id : Nat) (_id_in_arr : id ∈ arr.data) :
+    have hl (acc : DefaultFormula n) (ih : StrongAssignmentsInvariant acc) (id : Nat) (_id_in_arr : id ∈ arr.toList) :
       StrongAssignmentsInvariant (deleteOne acc id) := deleteOne_preserves_strongAssignmentsInvariant acc id ih
-    exact List.foldlRecOn arr.data deleteOne f hb hl
+    exact List.foldlRecOn arr.toList deleteOne f hb hl
 
 theorem deleteOne_preserves_ratUnits {n : Nat} (f : DefaultFormula n) (id : Nat) :
     (deleteOne f id).ratUnits = f.ratUnits := by
@@ -634,11 +634,11 @@ theorem readyForRatAdd_delete {n : Nat} (f : DefaultFormula n) (arr : Array Nat)
     ReadyForRatAdd f → ReadyForRatAdd (delete f arr) := by
   intro h
   constructor
-  · rw [delete, Array.foldl_eq_foldl_data]
+  · rw [delete, Array.foldl_eq_foldl_toList]
     have hb : f.ratUnits = #[] := h.1
-    have hl (acc : DefaultFormula n) (ih : acc.ratUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.data) :
+    have hl (acc : DefaultFormula n) (ih : acc.ratUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.toList) :
       (deleteOne acc id).ratUnits = #[] := by rw [deleteOne_preserves_ratUnits, ih]
-    exact List.foldlRecOn arr.data deleteOne f hb hl
+    exact List.foldlRecOn arr.toList deleteOne f hb hl
   · exact readyForRupAdd_delete f arr h.2
 
 theorem deleteOne_subset (f : DefaultFormula n) (id : Nat) (c : DefaultClause n) :
@@ -651,11 +651,11 @@ theorem deleteOne_subset (f : DefaultFormula n) (id : Nat) (c : DefaultClause n)
     rw [toList, List.mem_append, List.mem_append, or_assoc]
     rcases h1 with h1 | h1 | h1
     · apply Or.inl
-      simp only [Array.toList_eq, List.mem_filterMap, id_eq, exists_eq_right] at h1
-      simp only [Array.toList_eq, List.mem_filterMap, id_eq, exists_eq_right]
+      simp only [List.mem_filterMap, id_eq, exists_eq_right] at h1
+      simp only [List.mem_filterMap, id_eq, exists_eq_right]
       rw [Array.set!, Array.setD] at h1
       split at h1
-      · simp only [Array.data_set] at h1
+      · simp only [Array.toList_set] at h1
         rcases List.getElem_of_mem h1 with ⟨i, h, h4⟩
         rw [List.getElem_set] at h4
         split at h4
@@ -668,11 +668,11 @@ theorem deleteOne_subset (f : DefaultFormula n) (id : Nat) (c : DefaultClause n)
 
 theorem delete_subset (f : DefaultFormula n) (arr : Array Nat) (c : DefaultClause n) :
     c ∈ toList (delete f arr) → c ∈ toList f := by
-  simp only [delete, Array.foldl_eq_foldl_data]
+  simp only [delete, Array.foldl_eq_foldl_toList]
   have hb : c ∈ toList f → c ∈ toList f := id
-  have hl (f' : DefaultFormula n) (ih : c ∈ toList f' → c ∈ toList f) (id : Nat) (_ : id ∈ arr.data) :
+  have hl (f' : DefaultFormula n) (ih : c ∈ toList f' → c ∈ toList f) (id : Nat) (_ : id ∈ arr.toList) :
     c ∈ toList (deleteOne f' id) → c ∈ toList f := by intro h; exact ih <| deleteOne_subset f' id c h
-  exact List.foldlRecOn arr.data deleteOne f hb hl
+  exact List.foldlRecOn arr.toList deleteOne f hb hl
 
 end DefaultFormula
 
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
index b6a9beac2b..9eb4d90d99 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
@@ -80,12 +80,12 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
   apply Exists.intro hsize
   intro i b hb p hp
   simp only [(· ⊨ ·), Clause.eval] at hp
-  simp only [toList, Array.toList_eq, List.append_assoc,
+  simp only [toList, List.append_assoc,
     Entails.eval, List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe,
     List.all_eq_true, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, List.mem_map] at hp
   have pf : p ⊨ f := by
     simp only [(· ⊨ ·), Clause.eval]
-    simp only [toList, Array.toList_eq, List.append_assoc,
+    simp only [toList, List.append_assoc,
       Entails.eval, List.any_eq_true, Prod.exists, Bool.exists_bool,
       Bool.decide_coe, List.all_eq_true, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, List.mem_map]
     intro c cf
@@ -105,8 +105,8 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
       have j_unit_def : j_unit = unit (insertRatUnits f units).1.ratUnits[j] := rfl
       have j_unit_in_insertRatUnits_res :
         ∃ i : PosFin n,
-          (i, false) ∈ (insertRatUnits f units).1.ratUnits.data ∧ unit (i, false) = j_unit ∨
-          (i, true) ∈ (insertRatUnits f units).1.ratUnits.data ∧ unit (i, true) = j_unit := by
+          (i, false) ∈ (insertRatUnits f units).1.ratUnits.toList ∧ unit (i, false) = j_unit ∨
+          (i, true) ∈ (insertRatUnits f units).1.ratUnits.toList ∧ unit (i, true) = j_unit := by
         apply Exists.intro i
         rw [j_unit_def, h1]
         by_cases hb' : b'
@@ -118,7 +118,7 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
               simp only [h1, Prod.mk.injEq, and_true]
               rfl
             rw [← h1]
-            apply Array.getElem_mem_data
+            apply Array.getElem_mem_toList
           · rfl
         · simp only [Bool.not_eq_true] at hb'
           rw [hb']
@@ -129,7 +129,7 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
               simp only [h1, Prod.mk.injEq, and_true]
               rfl
             rw [← h1]
-            apply Array.getElem_mem_data
+            apply Array.getElem_mem_toList
           · rfl
       specialize hp j_unit ((Or.inr ∘ Or.inr) j_unit_in_insertRatUnits_res)
       simp only [List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe, Fin.getElem_fin, List.find?, j_unit] at hp
@@ -151,8 +151,8 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
     have j1_unit_def : j1_unit = unit (insertRatUnits f units).1.ratUnits[j1] := rfl
     have j1_unit_in_insertRatUnits_res :
       ∃ i : PosFin n,
-        (i, false) ∈ (insertRatUnits f units).1.ratUnits.data ∧ unit (i, false) = j1_unit ∨
-        (i, true) ∈ (insertRatUnits f units).1.ratUnits.data ∧ unit (i, true) = j1_unit := by
+        (i, false) ∈ (insertRatUnits f units).1.ratUnits.toList ∧ unit (i, false) = j1_unit ∨
+        (i, true) ∈ (insertRatUnits f units).1.ratUnits.toList ∧ unit (i, true) = j1_unit := by
       apply Exists.intro i ∘ Or.inr
       rw [j1_unit_def, h1]
       constructor
@@ -161,14 +161,14 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
           simp only [Prod.mk.injEq, and_true]
           rfl
         rw [← h1]
-        apply Array.getElem_mem_data
+        apply Array.getElem_mem_toList
       · rfl
     let j2_unit := unit (insertRatUnits f units).1.ratUnits[j2]
     have j2_unit_def : j2_unit = unit (insertRatUnits f units).1.ratUnits[j2] := rfl
     have j2_unit_in_insertRatUnits_res :
       ∃ i : PosFin n,
-        (i, false) ∈ (insertRatUnits f units).1.ratUnits.data ∧ unit (i, false) = j2_unit ∨
-        (i, true) ∈ (insertRatUnits f units).1.ratUnits.data ∧ unit (i, true) = j2_unit := by
+        (i, false) ∈ (insertRatUnits f units).1.ratUnits.toList ∧ unit (i, false) = j2_unit ∨
+        (i, true) ∈ (insertRatUnits f units).1.ratUnits.toList ∧ unit (i, true) = j2_unit := by
       apply Exists.intro i ∘ Or.inl
       rw [j2_unit_def, h2]
       constructor
@@ -177,7 +177,7 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
           simp only [Prod.mk.injEq, and_true]
           rfl
         rw [← h2]
-        apply Array.getElem_mem_data
+        apply Array.getElem_mem_toList
       · rfl
     have hp1 := hp j1_unit ((Or.inr ∘ Or.inr) j1_unit_in_insertRatUnits_res)
     have hp2 := hp j2_unit ((Or.inr ∘ Or.inr) j2_unit_in_insertRatUnits_res)
@@ -219,7 +219,7 @@ theorem sat_of_confirmRupHint_of_insertRat_fold {n : Nat} (f : DefaultFormula n)
       not_imp] at fc_unsat
     rcases fc_unsat with ⟨unsat_c, unsat_c_in_fc, p_unsat_c⟩
     have unsat_c_in_fc := mem_of_insertRatUnits f (negate c) unsat_c unsat_c_in_fc
-    simp only [Array.toList_eq, List.mem_map, Prod.exists, Bool.exists_bool] at unsat_c_in_fc
+    simp only [List.mem_map, Prod.exists, Bool.exists_bool] at unsat_c_in_fc
     rcases unsat_c_in_fc with ⟨v, ⟨v_in_neg_c, unsat_c_eq⟩ | ⟨v_in_neg_c, unsat_c_eq⟩⟩ | unsat_c_in_f
     · simp only [negate_eq, List.mem_map, Prod.exists, Bool.exists_bool] at v_in_neg_c
       rcases v_in_neg_c with ⟨v', ⟨_, v'_eq_v⟩ | ⟨v'_in_c, v'_eq_v⟩⟩
@@ -285,13 +285,13 @@ theorem sat_of_insertRat {n : Nat} (f : DefaultFormula n)
     simp [p_entails_i_true] at p_entails_i_false
   · simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe]
     apply Exists.intro i
-    have ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) (negate c)).1.data := by
+    have ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) (negate c)).1.toList := by
       have i_rw : i = ⟨i.1, i.2⟩ := rfl
       rw [i_rw, ← h1]
       apply List.get_mem
     have ib_in_insertUnit_fold := mem_insertUnit_fold_units f.ratUnits f.assignments false (negate c) (i, b) ib_in_insertUnit_fold
     simp only [negate, Literal.negate, List.mem_map, Prod.mk.injEq, Prod.exists, Bool.exists_bool,
-      Bool.not_false, Bool.not_true, hf.1, Array.data_toArray, List.find?, List.not_mem_nil, or_false]
+      Bool.not_false, Bool.not_true, hf.1, Array.toList_toArray, List.find?, List.not_mem_nil, or_false]
       at ib_in_insertUnit_fold
     rw [hboth] at h2
     rcases ib_in_insertUnit_fold with ⟨i', ⟨i_false_in_c, i'_eq_i, b_eq_true⟩ | ⟨i_true_in_c, i'_eq_i, b_eq_false⟩⟩
@@ -330,11 +330,11 @@ theorem sat_of_insertRat {n : Nat} (f : DefaultFormula n)
         exact h3 (has_both b)
       · simp at h2
   · exfalso
-    have i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) (negate c)).1.data := by
+    have i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) (negate c)).1.toList := by
       have i_rw : i = ⟨i.1, i.2⟩ := rfl
       rw [i_rw, ← h1]
       apply List.get_mem
-    have i_false_in_insertUnit_fold : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) (negate c)).1.data := by
+    have i_false_in_insertUnit_fold : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) (negate c)).1.toList := by
       have i_rw : i = ⟨i.1, i.2⟩ := rfl
       rw [i_rw, ← h2]
       apply List.get_mem
@@ -344,7 +344,7 @@ theorem sat_of_insertRat {n : Nat} (f : DefaultFormula n)
     have i_false_in_insertUnit_fold :=
       mem_insertUnit_fold_units #[] f.assignments false (c.clause.map Literal.negate) (i, false) i_false_in_insertUnit_fold
     simp only [Literal.negate, List.mem_map, Prod.mk.injEq, Bool.not_eq_true', Prod.exists,
-      exists_eq_right_right, exists_eq_right, Array.data_toArray, List.find?, List.not_mem_nil, or_false,
+      exists_eq_right_right, exists_eq_right, Array.toList_toArray, List.find?, List.not_mem_nil, or_false,
       Bool.not_eq_false'] at i_true_in_insertUnit_fold i_false_in_insertUnit_fold
     have c_not_tautology := Clause.not_tautology c (i, true)
     simp only [Clause.toList] at c_not_tautology
@@ -440,7 +440,7 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
     (ratHintsExhaustive_eq_true : ratHintsExhaustive f pivot ratHints = true) (c' : DefaultClause n)
     (c'_in_f : c' ∈ toList f) (negPivot_in_c' : Literal.negate pivot ∈ Clause.toList c') :
     ∃ i : Fin ratHints.size, f.clauses[ratHints[i].1]! = some c' := by
-  simp only [toList, Array.toList_eq, f_readyForRatAdd.2.1, Array.data_toArray, List.map, List.append_nil, f_readyForRatAdd.1,
+  simp only [toList, f_readyForRatAdd.2.1, Array.toList_toArray, List.map, List.append_nil, f_readyForRatAdd.1,
     List.mem_filterMap, id_eq, exists_eq_right] at c'_in_f
   rw [List.mem_iff_getElem] at c'_in_f
   rcases c'_in_f with ⟨i, hi, c'_in_f⟩
@@ -451,29 +451,29 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
   have i_lt_f_clauses_size : i < f.clauses.size := by
     rw [Array.size_range] at i_in_bounds
     exact i_in_bounds
-  have h : i ∈ (ratHints.map (fun x => x.1)).data := by
+  have h : i ∈ (ratHints.map (fun x => x.1)).toList := by
     rw [← of_decide_eq_true ratHintsExhaustive_eq_true]
     have i_eq_range_i : i = (Array.range f.clauses.size)[i]'i_in_bounds := by
       rw [Array.getElem_range]
     rw [i_eq_range_i]
-    rw [Array.mem_data]
+    rw [Array.mem_toList]
     rw [Array.mem_filter]
     constructor
-    · rw [← Array.mem_data]
-      apply Array.getElem_mem_data
-    · rw [← Array.getElem_eq_data_getElem] at c'_in_f
+    · rw [← Array.mem_toList]
+      apply Array.getElem_mem_toList
+    · rw [← Array.getElem_eq_toList_getElem] at c'_in_f
       simp only [getElem!, Array.getElem_range, i_lt_f_clauses_size, dite_true,
         c'_in_f, DefaultClause.contains_iff, Array.get_eq_getElem, decidableGetElem?]
       simpa [Clause.toList] using negPivot_in_c'
   rcases List.get_of_mem h with ⟨j, h'⟩
   have j_in_bounds : j < ratHints.size := by
     have j_property := j.2
-    simp only [Array.map_data, List.length_map] at j_property
+    simp only [Array.map_toList, List.length_map] at j_property
     dsimp at *
     omega
-  simp only [List.get_eq_getElem, Array.map_data, Array.data_length, List.getElem_map] at h'
-  rw [← Array.getElem_eq_data_getElem] at h'
-  rw [← Array.getElem_eq_data_getElem] at c'_in_f
+  simp only [List.get_eq_getElem, Array.map_toList, Array.toList_length, List.getElem_map] at h'
+  rw [← Array.getElem_eq_toList_getElem] at h'
+  rw [← Array.getElem_eq_toList_getElem] at c'_in_f
   exists ⟨j.1, j_in_bounds⟩
   simp [getElem!, h', i_lt_f_clauses_size, dite_true, c'_in_f, decidableGetElem?]
 
@@ -559,7 +559,7 @@ theorem safe_insert_of_performRatCheck_fold_success {n : Nat} (f : DefaultFormul
       simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq, Classical.not_forall,
         not_imp] at fc_unsat
       rcases fc_unsat with ⟨c', c'_in_fc, p'_not_entails_c'⟩
-      simp only [insert_iff, Array.toList_eq, Array.data_toArray, List.mem_singleton] at c'_in_fc
+      simp only [insert_iff, Array.toList_toArray, List.mem_singleton] at c'_in_fc
       rcases c'_in_fc with c'_eq_c | c'_in_f
       · rw [← c'_eq_c] at p'_entails_c
         exact p'_not_entails_c' p'_entails_c
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
index 797fa17714..c5c2bb088f 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
@@ -746,13 +746,13 @@ theorem size_assignemnts_confirmRupHint {n : Nat} (clauses : Array (Option (Defa
 theorem size_assignments_performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) :
     (performRupCheck f rupHints).1.assignments.size = f.assignments.size := by
   simp only [performRupCheck]
-  rw [Array.foldl_eq_foldl_data]
+  rw [Array.foldl_eq_foldl_toList]
   have hb : (f.assignments, ([] : CNF.Clause (PosFin n)), false, false).1.size = f.assignments.size := rfl
   have hl (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool) (hsize : acc.1.size = f.assignments.size)
-    (id : Nat) (_ : id ∈ rupHints.data) : (confirmRupHint f.clauses acc id).1.size = f.assignments.size := by
+    (id : Nat) (_ : id ∈ rupHints.toList) : (confirmRupHint f.clauses acc id).1.size = f.assignments.size := by
     have h := size_assignemnts_confirmRupHint f.clauses acc.1 acc.2.1 acc.2.2.1 acc.2.2.2 id
     rw [h, hsize]
-  exact List.foldlRecOn rupHints.data (confirmRupHint f.clauses) (f.assignments, [], false, false) hb hl
+  exact List.foldlRecOn rupHints.toList (confirmRupHint f.clauses) (f.assignments, [], false, false) hb hl
 
 def DerivedLitsInvariant {n : Nat} (f : DefaultFormula n)
     (fassignments_size : f.assignments.size = n) (assignments : Array Assignment)
@@ -1112,13 +1112,13 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
     (derivedLits : CNF.Clause (PosFin n))
     (derivedLits_satisfies_invariant:
       DerivedLitsInvariant f f_assignments_size (performRupCheck f rupHints).fst.assignments f'_assignments_size derivedLits)
-    (derivedLits_arr : Array (Literal (PosFin n))) (derivedLits_arr_def: derivedLits_arr = { data := derivedLits })
+    (derivedLits_arr : Array (Literal (PosFin n))) (derivedLits_arr_def: derivedLits_arr = { toList := derivedLits })
     (i j : Fin (Array.size derivedLits_arr)) (i_ne_j : i ≠ j) :
     derivedLits_arr[i] ≠ derivedLits_arr[j] := by
   intro li_eq_lj
   let li := derivedLits_arr[i]
   have li_in_derivedLits : li ∈ derivedLits := by
-    rw [Array.mem_data, ← derivedLits_arr_def]
+    rw [Array.mem_toList, ← derivedLits_arr_def]
     simp only [li, Array.getElem?_mem]
   have i_in_bounds : i.1 < derivedLits.length := by
     have i_property := i.2
@@ -1140,25 +1140,25 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
       specialize h3 ⟨j.1, j_in_bounds⟩ j_ne_k
       simp only [derivedLits_arr_def, Fin.getElem_fin] at li_eq_lj
       simp only [Fin.getElem_fin, derivedLits_arr_def, ne_eq, li, li_eq_lj] at h3
-      simp only [List.get_eq_getElem, Array.getElem_eq_data_getElem, not_true_eq_false] at h3
+      simp only [List.get_eq_getElem, Array.getElem_eq_toList_getElem, not_true_eq_false] at h3
     · next k_ne_i =>
       have i_ne_k : ⟨i.1, i_in_bounds⟩ ≠ k := by intro i_eq_k; simp only [← i_eq_k, not_true] at k_ne_i
       specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k
       simp (config := { decide := true }) [Fin.getElem_fin, derivedLits_arr_def, ne_eq,
-        Array.getElem_eq_data_getElem, li] at h3
+        Array.getElem_eq_toList_getElem, li] at h3
   · by_cases li.2 = true
     · next li_eq_true =>
       have i_ne_k2 : ⟨i.1, i_in_bounds⟩ ≠ k2 := by
         intro i_eq_k2
         rw [← i_eq_k2] at k2_eq_false
         simp only [List.get_eq_getElem] at k2_eq_false
-        simp [derivedLits_arr_def, Array.getElem_eq_data_getElem, k2_eq_false, li] at li_eq_true
+        simp [derivedLits_arr_def, Array.getElem_eq_toList_getElem, k2_eq_false, li] at li_eq_true
       have j_ne_k2 : ⟨j.1, j_in_bounds⟩ ≠ k2 := by
         intro j_eq_k2
         rw [← j_eq_k2] at k2_eq_false
         simp only [List.get_eq_getElem] at k2_eq_false
-        simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_data_getElem] at li_eq_lj
-        simp [derivedLits_arr_def, Array.getElem_eq_data_getElem, k2_eq_false, li_eq_lj, li] at li_eq_true
+        simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem] at li_eq_lj
+        simp [derivedLits_arr_def, Array.getElem_eq_toList_getElem, k2_eq_false, li_eq_lj, li] at li_eq_true
       by_cases ⟨i.1, i_in_bounds⟩ = k1
       · next i_eq_k1 =>
         have j_ne_k1 : ⟨j.1, j_in_bounds⟩ ≠ k1 := by
@@ -1167,11 +1167,11 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
           simp only [Fin.mk.injEq] at i_eq_k1
           exact i_ne_j (Fin.eq_of_val_eq i_eq_k1)
         specialize h3 ⟨j.1, j_in_bounds⟩ j_ne_k1 j_ne_k2
-        simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_data_getElem] at h3
+        simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_toList_getElem] at h3
       · next i_ne_k1 =>
         specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k1 i_ne_k2
         apply h3
-        simp (config := { decide := true }) only [Fin.getElem_fin, Array.getElem_eq_data_getElem,
+        simp (config := { decide := true }) only [Fin.getElem_fin, Array.getElem_eq_toList_getElem,
           ne_eq, derivedLits_arr_def, li]
         rfl
     · next li_eq_false =>
@@ -1180,13 +1180,13 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
         intro i_eq_k1
         rw [← i_eq_k1] at k1_eq_true
         simp only [List.get_eq_getElem] at k1_eq_true
-        simp [derivedLits_arr_def, Array.getElem_eq_data_getElem, k1_eq_true, li] at li_eq_false
+        simp [derivedLits_arr_def, Array.getElem_eq_toList_getElem, k1_eq_true, li] at li_eq_false
       have j_ne_k1 : ⟨j.1, j_in_bounds⟩ ≠ k1 := by
         intro j_eq_k1
         rw [← j_eq_k1] at k1_eq_true
         simp only [List.get_eq_getElem] at k1_eq_true
-        simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_data_getElem] at li_eq_lj
-        simp [derivedLits_arr_def, Array.getElem_eq_data_getElem, k1_eq_true, li_eq_lj, li] at li_eq_false
+        simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem] at li_eq_lj
+        simp [derivedLits_arr_def, Array.getElem_eq_toList_getElem, k1_eq_true, li_eq_lj, li] at li_eq_false
       by_cases ⟨i.1, i_in_bounds⟩ = k2
       · next i_eq_k2 =>
         have j_ne_k2 : ⟨j.1, j_in_bounds⟩ ≠ k2 := by
@@ -1195,17 +1195,17 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
           simp only [Fin.mk.injEq] at i_eq_k2
           exact i_ne_j (Fin.eq_of_val_eq i_eq_k2)
         specialize h3 ⟨j.1, j_in_bounds⟩ j_ne_k1 j_ne_k2
-        simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_data_getElem] at h3
+        simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_toList_getElem] at h3
       · next i_ne_k2 =>
         specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k1 i_ne_k2
-        simp (config := { decide := true }) [Array.getElem_eq_data_getElem, derivedLits_arr_def, li] at h3
+        simp (config := { decide := true }) [Array.getElem_eq_toList_getElem, derivedLits_arr_def, li] at h3
 
 theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormula n)
     (f_assignments_size : f.assignments.size = n)
     (f' : DefaultFormula n) (_f'_def : f' = (performRupCheck f rupHints).1)
     (f'_assignments_size : f'.assignments.size = n) (derivedLits : CNF.Clause (PosFin n))
     (derivedLits_arr : Array (Literal (PosFin n)))
-    (derivedLits_arr_def : derivedLits_arr = {data := derivedLits})
+    (derivedLits_arr_def : derivedLits_arr = {toList := derivedLits})
     (derivedLits_satisfies_invariant :
       DerivedLitsInvariant f f_assignments_size f'.assignments f'_assignments_size derivedLits)
     (_derivedLits_arr_nodup : ∀ (i j : Fin (Array.size derivedLits_arr)), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]) :
@@ -1221,7 +1221,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
     · intro j _
       have idx_in_list : derivedLits_arr[j] ∈ derivedLits := by
         simp only [derivedLits_arr_def, Fin.getElem_fin]
-        apply Array.getElem_mem_data
+        apply Array.getElem_mem_toList
       exact h2 derivedLits_arr[j] idx_in_list
   · apply Or.inr ∘ Or.inl
     have j_lt_derivedLits_arr_size : j.1 < derivedLits_arr.size := by
@@ -1232,7 +1232,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
     constructor
     · apply Nat.zero_le
     · constructor
-      · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_data_getElem, ← j_eq_i]
+      · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem, ← j_eq_i]
         rfl
       · apply And.intro h1 ∘ And.intro h2
         intro k _ k_ne_j
@@ -1244,7 +1244,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
           apply Fin.ne_of_val_ne
           simp only
           exact Fin.val_ne_of_ne k_ne_j
-        simp only [Fin.getElem_fin, Array.getElem_eq_data_getElem, ne_eq, derivedLits_arr_def]
+        simp only [Fin.getElem_fin, Array.getElem_eq_toList_getElem, ne_eq, derivedLits_arr_def]
         exact h3 ⟨k.1, k_in_bounds⟩ k_ne_j
   · apply Or.inr ∘ Or.inr
     have j1_lt_derivedLits_arr_size : j1.1 < derivedLits_arr.size := by
@@ -1258,11 +1258,11 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
             ⟨j2.1, j2_lt_derivedLits_arr_size⟩,
             i_gt_zero, Nat.zero_le j1.1, Nat.zero_le j2.1, ?_⟩
     constructor
-    · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_data_getElem, ← j1_eq_i]
+    · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem, ← j1_eq_i]
       rw [← j1_eq_true]
       rfl
     · constructor
-      · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_data_getElem, ← j2_eq_i]
+      · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem, ← j2_eq_i]
         rw [← j2_eq_false]
         rfl
       · apply And.intro h1 ∘ And.intro h2
@@ -1279,7 +1279,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
           apply Fin.ne_of_val_ne
           simp only
           exact Fin.val_ne_of_ne k_ne_j2
-        simp only [Fin.getElem_fin, Array.getElem_eq_data_getElem, ne_eq, derivedLits_arr_def]
+        simp only [Fin.getElem_fin, Array.getElem_eq_toList_getElem, ne_eq, derivedLits_arr_def]
         exact h3 ⟨k.1, k_in_bounds⟩ k_ne_j1 k_ne_j2
 
 theorem restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n)
@@ -1295,9 +1295,9 @@ theorem restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_a
   have derivedLits_satisfies_invariant := derivedLitsInvariant_performRupCheck f f_assignments_size rupHints f'_assignments_size
   simp only at derivedLits_satisfies_invariant
   generalize (performRupCheck f rupHints).2.1 = derivedLits at *
-  rw [← f'_def, ← Array.foldl_eq_foldl_data]
-  let derivedLits_arr : Array (Literal (PosFin n)) := {data := derivedLits}
-  have derivedLits_arr_def : derivedLits_arr = {data := derivedLits} := rfl
+  rw [← f'_def, ← Array.foldl_eq_foldl_toList]
+  let derivedLits_arr : Array (Literal (PosFin n)) := {toList := derivedLits}
+  have derivedLits_arr_def : derivedLits_arr = {toList := derivedLits} := rfl
   have derivedLits_arr_nodup := nodup_derivedLits f f_assignments_size rupHints f'_assignments_size derivedLits
     derivedLits_satisfies_invariant derivedLits_arr derivedLits_arr_def
   let motive := ClearInsertInductionMotive f f_assignments_size derivedLits_arr
@@ -1308,7 +1308,7 @@ theorem restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_a
     clear_insert_inductive_case f f_assignments_size derivedLits_arr derivedLits_arr_nodup idx assignments ih
   rcases Array.foldl_induction motive h_base h_inductive with ⟨h_size, h⟩
   apply Array.ext
-  · rw [Array.foldl_eq_foldl_data, size_clearUnit_foldl f'.assignments clearUnit size_clearUnit derivedLits,
+  · rw [Array.foldl_eq_foldl_toList, size_clearUnit_foldl f'.assignments clearUnit size_clearUnit derivedLits,
       f'_assignments_size, f_assignments_size]
   · intro i hi1 hi2
     rw [f_assignments_size] at hi2
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
index 2c2a864a57..17c703bd7b 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
@@ -92,25 +92,25 @@ theorem contradiction_of_insertUnit_fold_success {n : Nat} (assignments : Array
 theorem mem_insertUnit_units {n : Nat} (units : Array (Literal (PosFin n))) (assignments : Array Assignment)
     (foundContradiction : Bool) (l : Literal (PosFin n)) :
     let insertUnit_res := insertUnit (units, assignments, foundContradiction) l
-    ∀ l' : Literal (PosFin n), l' ∈ insertUnit_res.1.data → l' = l ∨ l' ∈ units.data := by
+    ∀ l' : Literal (PosFin n), l' ∈ insertUnit_res.1.toList → l' = l ∨ l' ∈ units.toList := by
   intro insertUnit_res l' l'_in_insertUnit_res
   simp only [insertUnit_res] at *
   simp only [insertUnit] at l'_in_insertUnit_res
   split at l'_in_insertUnit_res
   · exact Or.inr l'_in_insertUnit_res
-  · simp only [Array.push_data, List.mem_append, List.mem_singleton] at l'_in_insertUnit_res
+  · simp only [Array.push_toList, List.mem_append, List.mem_singleton] at l'_in_insertUnit_res
     exact Or.symm l'_in_insertUnit_res
 
 theorem mem_insertUnit_fold_units {n : Nat} (units : Array (Literal (PosFin n))) (assignments : Array Assignment)
     (foundContradiction : Bool) (l : CNF.Clause (PosFin n)) :
     let insertUnit_fold_res := List.foldl insertUnit (units, assignments, foundContradiction) l
-    ∀ l' : Literal (PosFin n), l' ∈ insertUnit_fold_res.1.data → l' ∈ l ∨ l' ∈ units.data := by
-  have hb (l' : Literal (PosFin n)) : l' ∈ (units, assignments, foundContradiction).1.data → l' ∈ l ∨ l' ∈ units.data := by
+    ∀ l' : Literal (PosFin n), l' ∈ insertUnit_fold_res.1.toList → l' ∈ l ∨ l' ∈ units.toList := by
+  have hb (l' : Literal (PosFin n)) : l' ∈ (units, assignments, foundContradiction).1.toList → l' ∈ l ∨ l' ∈ units.toList := by
     intro h
     exact Or.inr h
   have hl (acc : Array (Literal (PosFin n)) × Array Assignment × Bool)
-    (h : ∀ l' : Literal (PosFin n), l' ∈ acc.1.data → l' ∈ l ∨ l' ∈ units.data) (l'' : Literal (PosFin n))
-    (l''_in_l : l'' ∈ l) : ∀ l' : Literal (PosFin n), l' ∈ (insertUnit acc l'').1.data → l' ∈ l ∨ l' ∈ units.data := by
+    (h : ∀ l' : Literal (PosFin n), l' ∈ acc.1.toList → l' ∈ l ∨ l' ∈ units.toList) (l'' : Literal (PosFin n))
+    (l''_in_l : l'' ∈ l) : ∀ l' : Literal (PosFin n), l' ∈ (insertUnit acc l'').1.toList → l' ∈ l ∨ l' ∈ units.toList := by
     intro l' l'_in_res
     rcases mem_insertUnit_units  acc.1 acc.2.1 acc.2.2 l'' l' l'_in_res with l'_eq_l'' | l'_in_acc
     · rw [l'_eq_l'']
@@ -150,13 +150,13 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re
     simp [p_entails_i_true] at p_entails_i_false
   · simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe]
     apply Exists.intro i
-    have ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) (negate c)).1.data := by
+    have ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) (negate c)).1.toList := by
       have i_rw : i = ⟨i.1, i.2⟩ := rfl
       rw [i_rw, ← h1]
       apply List.get_mem
     have ib_in_insertUnit_fold := mem_insertUnit_fold_units f.rupUnits f.assignments false (negate c) (i, b) ib_in_insertUnit_fold
     simp only [negate, Literal.negate, List.mem_map, Prod.mk.injEq, Prod.exists, Bool.exists_bool,
-      Bool.not_false, Bool.not_true, f_readyForRupAdd.1, Array.data_toArray, List.find?, List.not_mem_nil, or_false]
+      Bool.not_false, Bool.not_true, f_readyForRupAdd.1, Array.toList_toArray, List.find?, List.not_mem_nil, or_false]
       at ib_in_insertUnit_fold
     rw [hboth] at h2
     rcases ib_in_insertUnit_fold with ⟨i', ⟨i_false_in_c, i'_eq_i, b_eq_true⟩ | ⟨i_true_in_c, i'_eq_i, b_eq_false⟩⟩
@@ -196,11 +196,11 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re
         exact h3 (has_both b)
       · simp at h2
   · exfalso
-    have i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) (negate c)).1.data := by
+    have i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) (negate c)).1.toList := by
       have i_rw : i = ⟨i.1, i.2⟩ := rfl
       rw [i_rw, ← h1]
       apply List.get_mem
-    have i_false_in_insertUnit_fold : (i, false) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) (negate c)).1.data := by
+    have i_false_in_insertUnit_fold : (i, false) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) (negate c)).1.toList := by
       have i_rw : i = ⟨i.1, i.2⟩ := rfl
       rw [i_rw, ← h2]
       apply List.get_mem
@@ -210,7 +210,7 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re
     have i_false_in_insertUnit_fold :=
       mem_insertUnit_fold_units #[] f.assignments false (c.clause.map Literal.negate) (i, false) i_false_in_insertUnit_fold
     simp only [Literal.negate, List.mem_map, Prod.mk.injEq, Bool.not_eq_true', Prod.exists,
-      exists_eq_right_right, exists_eq_right, Array.data_toArray, List.find?, List.not_mem_nil, or_false,
+      exists_eq_right_right, exists_eq_right, Array.toList_toArray, List.find?, List.not_mem_nil, or_false,
       Bool.not_eq_false'] at i_true_in_insertUnit_fold i_false_in_insertUnit_fold
     have c_not_tautology := Clause.not_tautology c (i, true)
     simp only [Clause.toList, (· ⊨ ·)] at c_not_tautology
@@ -240,18 +240,18 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
   apply Exists.intro hsize
   intro i b hb p hp
   simp only [(· ⊨ ·), Clause.eval] at hp
-  simp only [toList, Array.toList_eq, List.append_assoc, List.any_eq_true, Prod.exists,
+  simp only [toList, List.append_assoc, List.any_eq_true, Prod.exists,
     Bool.exists_bool, Bool.decide_coe, List.all_eq_true, List.mem_append, List.mem_filterMap, id_eq,
     exists_eq_right, List.mem_map] at hp
   have pf : p ⊨ f := by
     simp only [(· ⊨ ·), Clause.eval]
-    simp only [toList, Array.toList_eq, List.append_assoc, List.any_eq_true, Prod.exists, Bool.exists_bool,
+    simp only [toList, List.append_assoc, List.any_eq_true, Prod.exists, Bool.exists_bool,
       Bool.decide_coe, List.all_eq_true, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, List.mem_map]
     intro c cf
     rcases cf with cf | cf | cf
     · specialize hp c (Or.inl cf)
       exact hp
-    · simp only [f_readyForRupAdd.1, Array.data_toArray, List.find?, List.not_mem_nil, false_and, or_self, exists_false] at cf
+    · simp only [f_readyForRupAdd.1, Array.toList_toArray, List.find?, List.not_mem_nil, false_and, or_self, exists_false] at cf
     · specialize hp c <| (Or.inr ∘ Or.inr) cf
       exact hp
   rcases h ⟨i.1, i.2.2⟩ with ⟨h1, h2⟩ | ⟨j, b', i_gt_zero, h1, h2, h3, h4⟩ | ⟨j1, j2, i_gt_zero, h1, h2, _, _, _⟩
@@ -264,8 +264,8 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
       have j_unit_def : j_unit = unit (insertRupUnits f units).1.rupUnits[j] := rfl
       have j_unit_in_insertRupUnits_res :
         ∃ i : PosFin n,
-          (i, false) ∈ (insertRupUnits f units).1.rupUnits.data ∧ unit (i, false) = j_unit ∨
-          (i, true) ∈ (insertRupUnits f units).1.rupUnits.data ∧ unit (i, true) = j_unit := by
+          (i, false) ∈ (insertRupUnits f units).1.rupUnits.toList ∧ unit (i, false) = j_unit ∨
+          (i, true) ∈ (insertRupUnits f units).1.rupUnits.toList ∧ unit (i, true) = j_unit := by
         apply Exists.intro i
         rw [j_unit_def, h1]
         by_cases hb' : b'
@@ -278,7 +278,7 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
               simp only [Prod.mk.injEq, and_true]
               rfl
             rw [← h1]
-            apply Array.getElem_mem_data
+            apply Array.getElem_mem_toList
           · rfl
         · simp only [Bool.not_eq_true] at hb'
           rw [hb']
@@ -290,7 +290,7 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
               simp only [Prod.mk.injEq, and_true]
               rfl
             rw [← h1]
-            apply Array.getElem_mem_data
+            apply Array.getElem_mem_toList
           · rfl
       specialize hp j_unit ((Or.inr ∘ Or.inl) j_unit_in_insertRupUnits_res)
       simp only [List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe, Fin.getElem_fin, List.find?, j_unit] at hp
@@ -314,8 +314,8 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
     have j1_unit_def : j1_unit = unit (insertRupUnits f units).1.rupUnits[j1] := rfl
     have j1_unit_in_insertRupUnits_res :
       ∃ i : PosFin n,
-        (i, false) ∈ (insertRupUnits f units).1.rupUnits.data ∧ unit (i, false) = j1_unit ∨
-        (i, true) ∈ (insertRupUnits f units).1.rupUnits.data ∧ unit (i, true) = j1_unit := by
+        (i, false) ∈ (insertRupUnits f units).1.rupUnits.toList ∧ unit (i, false) = j1_unit ∨
+        (i, true) ∈ (insertRupUnits f units).1.rupUnits.toList ∧ unit (i, true) = j1_unit := by
       apply Exists.intro i ∘ Or.inr
       rw [j1_unit_def, h1]
       constructor
@@ -324,14 +324,14 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
           simp only [Prod.mk.injEq, and_true]
           rfl
         rw [← h1]
-        apply Array.getElem_mem_data
+        apply Array.getElem_mem_toList
       · rfl
     let j2_unit := unit (insertRupUnits f units).1.rupUnits[j2]
     have j2_unit_def : j2_unit = unit (insertRupUnits f units).1.rupUnits[j2] := rfl
     have j2_unit_in_insertRupUnits_res :
       ∃ i : PosFin n,
-        (i, false) ∈ (insertRupUnits f units).1.rupUnits.data ∧ unit (i, false) = j2_unit ∨
-        (i, true) ∈ (insertRupUnits f units).1.rupUnits.data ∧ unit (i, true) = j2_unit := by
+        (i, false) ∈ (insertRupUnits f units).1.rupUnits.toList ∧ unit (i, false) = j2_unit ∨
+        (i, true) ∈ (insertRupUnits f units).1.rupUnits.toList ∧ unit (i, true) = j2_unit := by
       apply Exists.intro i ∘ Or.inl
       rw [j2_unit_def, h2]
       constructor
@@ -340,7 +340,7 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
           simp only [Prod.mk.injEq, and_true]
           rfl
         rw [← h2]
-        apply Array.getElem_mem_data
+        apply Array.getElem_mem_toList
       · rfl
     have hp1 := hp j1_unit ((Or.inr ∘ Or.inl) j1_unit_in_insertRupUnits_res)
     have hp2 := hp j2_unit ((Or.inr ∘ Or.inl) j2_unit_in_insertRupUnits_res)
@@ -544,8 +544,8 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
     (reduce c assignment = reducedToEmpty → Incompatible (PosFin n) c assignment) ∧
     (∀ l : Literal (PosFin n), reduce c assignment = reducedToUnit l → ∀ (p : (PosFin n) → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l) := by
   let c_arr := Array.mk c.clause
-  have c_clause_rw : c.clause = c_arr.data := rfl
-  rw [reduce, c_clause_rw, ← Array.foldl_eq_foldl_data]
+  have c_clause_rw : c.clause = c_arr.toList := rfl
+  rw [reduce, c_clause_rw, ← Array.foldl_eq_foldl_toList]
   let motive := ReducePostconditionInductionMotive c_arr assignment
   have h_base : motive 0 reducedToEmpty := by
     have : ∀ (a : PosFin n) (b : Bool), (reducedToEmpty = reducedToUnit (a, b)) = False := by intros; simp
@@ -571,7 +571,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_data_get] at hidx
+          rw [← Array.getElem_fin_eq_toList_get] at hidx
           exact Exists.intro idx hidx
         rcases idx_exists with ⟨idx, hidx⟩
         specialize h1 idx idx.2
@@ -581,7 +581,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_data_get] at hidx
+          rw [← Array.getElem_fin_eq_toList_get] at hidx
           exact Exists.intro idx hidx
         rcases idx_exists with ⟨idx, hidx⟩
         specialize h1 idx idx.2
@@ -596,7 +596,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_data_get] at hidx
+        rw [← Array.getElem_fin_eq_toList_get] at hidx
         exact Exists.intro idx hidx
       rcases idx_exists with ⟨idx, hidx⟩
       apply Exists.intro idx ∘ And.intro idx.2
@@ -607,7 +607,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_data_get] at hidx
+        rw [← Array.getElem_fin_eq_toList_get] at hidx
         exact Exists.intro idx hidx
       rcases idx_exists with ⟨idx, hidx⟩
       apply Exists.intro idx ∘ And.intro idx.2
@@ -638,14 +638,14 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
     split
     · next c hc =>
       have c_in_f : c ∈ toList f := by
-        simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
+        simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
           exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
         apply Or.inl
         simp only [getElem?, decidableGetElem?] at hc
         split at hc
         · simp only [Option.some.injEq] at hc
           rw [← hc]
-          apply Array.getElem_mem_data
+          apply Array.getElem_mem_toList
         · simp at hc
       split
       · next heq =>
@@ -745,7 +745,7 @@ theorem sat_of_confirmRupHint_insertRup_fold {n : Nat} (f : DefaultFormula n)
       not_imp] at fc_unsat
     rcases fc_unsat with ⟨unsat_c, unsat_c_in_fc, p_unsat_c⟩
     have unsat_c_in_fc := mem_of_insertRupUnits f (negate c) unsat_c unsat_c_in_fc
-    simp only [Array.toList_eq, List.mem_map, Prod.exists, Bool.exists_bool] at unsat_c_in_fc
+    simp only [List.mem_map, Prod.exists, Bool.exists_bool] at unsat_c_in_fc
     rcases unsat_c_in_fc with ⟨v, ⟨v_in_neg_c, unsat_c_eq⟩ | ⟨v_in_neg_c, unsat_c_eq⟩⟩ | unsat_c_in_f
     · simp only [negate_eq, List.mem_map, Prod.exists, Bool.exists_bool] at v_in_neg_c
       rcases v_in_neg_c with ⟨v', ⟨_, v'_eq_v⟩ | ⟨v'_in_c, v'_eq_v⟩⟩
diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
index e2f704a80d..4272c61041 100644
--- a/src/include/lean/lean.h
+++ b/src/include/lean/lean.h
@@ -703,7 +703,7 @@ static inline void lean_array_set_core(u_lean_obj_arg o, size_t i, lean_obj_arg
     lean_to_array(o)->m_data[i] = v;
 }
 LEAN_EXPORT lean_object * lean_array_mk(lean_obj_arg l);
-LEAN_EXPORT lean_object * lean_array_data(lean_obj_arg a);
+LEAN_EXPORT lean_object * lean_array_to_list(lean_obj_arg a);
 
 /* Arrays of objects (high level API) */
 
diff --git a/src/lake/Lake/CLI/Actions.lean b/src/lake/Lake/CLI/Actions.lean
index b92ea5488b..92a435c595 100644
--- a/src/lake/Lake/CLI/Actions.lean
+++ b/src/lake/Lake/CLI/Actions.lean
@@ -78,7 +78,7 @@ def Package.lint (pkg : Package) (args : List String := []) (buildConfig : Build
   let cfgArgs := pkg.lintDriverArgs
   let (pkg, driver) ← pkg.resolveDriver "lint" pkg.lintDriver
   if let some script := pkg.scripts.find? driver.toName then
-    script.run (cfgArgs.data ++ args)
+    script.run (cfgArgs.toList ++ args)
   else if let some exe := pkg.findLeanExe? driver.toName  then
     let exeFile ← runBuild exe.fetch buildConfig
     env exeFile.toString (cfgArgs ++ args.toArray)
diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp
index 01569e1bf4..42057654f3 100644
--- a/src/library/compiler/erase_irrelevant.cpp
+++ b/src/library/compiler/erase_irrelevant.cpp
@@ -215,7 +215,7 @@ class erase_irrelevant_fn {
         expr minor       = visit_minor(args[3]);
         lean_always_assert(is_lambda(minor));
         return
-            ::lean::mk_let(next_name(), mk_enf_object_type(), mk_app(mk_constant(get_array_data_name()), mk_enf_neutral(), major),
+            ::lean::mk_let(next_name(), mk_enf_object_type(), mk_app(mk_constant(get_array_to_list_name()), mk_enf_neutral(), major),
                            binding_body(minor));
     }
 
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 2aa91ce25e..63d027ab67 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -12,7 +12,7 @@ name const * g_and_rec = nullptr;
 name const * g_and_cases_on = nullptr;
 name const * g_array = nullptr;
 name const * g_array_sz = nullptr;
-name const * g_array_data = nullptr;
+name const * g_array_to_list = nullptr;
 name const * g_auto_param = nullptr;
 name const * g_bit0 = nullptr;
 name const * g_bit1 = nullptr;
@@ -127,8 +127,8 @@ void initialize_constants() {
     mark_persistent(g_array->raw());
     g_array_sz = new name{"Array", "sz"};
     mark_persistent(g_array_sz->raw());
-    g_array_data = new name{"Array", "data"};
-    mark_persistent(g_array_data->raw());
+    g_array_to_list = new name{"Array", "toList"};
+    mark_persistent(g_array_to_list->raw());
     g_auto_param = new name{"autoParam"};
     mark_persistent(g_auto_param->raw());
     g_bit0 = new name{"bit0"};
@@ -330,7 +330,7 @@ void finalize_constants() {
     delete g_and_cases_on;
     delete g_array;
     delete g_array_sz;
-    delete g_array_data;
+    delete g_array_to_list;
     delete g_auto_param;
     delete g_bit0;
     delete g_bit1;
@@ -436,7 +436,7 @@ name const & get_and_rec_name() { return *g_and_rec; }
 name const & get_and_cases_on_name() { return *g_and_cases_on; }
 name const & get_array_name() { return *g_array; }
 name const & get_array_sz_name() { return *g_array_sz; }
-name const & get_array_data_name() { return *g_array_data; }
+name const & get_array_to_list_name() { return *g_array_to_list; }
 name const & get_auto_param_name() { return *g_auto_param; }
 name const & get_bit0_name() { return *g_bit0; }
 name const & get_bit1_name() { return *g_bit1; }
diff --git a/src/library/constants.h b/src/library/constants.h
index 6bdde99609..7693928801 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -14,7 +14,7 @@ name const & get_and_rec_name();
 name const & get_and_cases_on_name();
 name const & get_array_name();
 name const & get_array_sz_name();
-name const & get_array_data_name();
+name const & get_array_to_list_name();
 name const & get_auto_param_name();
 name const & get_bit0_name();
 name const & get_bit1_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index 481a20aa57..973c231dab 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -7,7 +7,7 @@ And.rec
 And.casesOn
 Array
 Array.sz
-Array.data
+Array.toList
 autoParam
 bit0
 bit1
diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index 06128fafe5..eb6461f7cf 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -364,14 +364,14 @@ object * array_mk_empty() {
 }
 
 extern "C" object * lean_list_to_array(object *, object *);
-extern "C" object * lean_array_to_list(object *, object *);
+extern "C" object * lean_array_to_list_impl(object *, object *);
 
 extern "C" LEAN_EXPORT object * lean_array_mk(lean_obj_arg lst) {
     return lean_list_to_array(lean_box(0), lst);
 }
 
-extern "C" LEAN_EXPORT lean_object * lean_array_data(lean_obj_arg a) {
-    return lean_array_to_list(lean_box(0), a);
+extern "C" LEAN_EXPORT lean_object * lean_array_to_list(lean_obj_arg a) {
+    return lean_array_to_list_impl(lean_box(0), a);
 }
 
 extern "C" LEAN_EXPORT lean_obj_res lean_array_get_panic(lean_obj_arg def_val) {
diff --git a/tests/bench/liasolver.lean b/tests/bench/liasolver.lean
index afd1cae244..8a5633b8e2 100644
--- a/tests/bench/liasolver.lean
+++ b/tests/bench/liasolver.lean
@@ -392,5 +392,5 @@ def main (args : List String) : IO UInt32 := do
       IO.println "UNSAT"
     | Solution.sat assignment =>
       IO.println "SAT"
-      IO.println <| String.intercalate " " <| assignment.data.map toString
+      IO.println <| String.intercalate " " <| assignment.toList.map toString
   return 0
diff --git a/tests/compiler/array.lean b/tests/compiler/array.lean
index d0bfc5e0a8..75d80cedd6 100644
--- a/tests/compiler/array.lean
+++ b/tests/compiler/array.lean
@@ -2,7 +2,7 @@
   Array.casesOn (motive := fun _ => Nat) a (fun data => data.length)
 
 @[noinline] def g (a : Array Nat) : List Nat :=
-  a.data
+  a.toList
 
 @[noinline] def h (a : List Nat) : List Nat :=
   g (Array.mk a)
diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean
index 42e166ca08..1a93555361 100644
--- a/tests/lean/run/PPTopDownAnalyze.lean
+++ b/tests/lean/run/PPTopDownAnalyze.lean
@@ -275,8 +275,8 @@ set_option pp.proofs.withType false in
 
 end proofs
 
-#testDelab ∀ (α : Type u) (vals vals_1 : List α), { data := vals : Array α } = { data := vals_1 : Array α }
-  expecting ∀ (α : Type u) (vals vals_1 : List α), { data := vals : Array α } = { data := vals_1 }
+#testDelab ∀ (α : Type u) (vals vals_1 : List α), { toList := vals : Array α } = { toList := vals_1 : Array α }
+  expecting ∀ (α : Type u) (vals vals_1 : List α), { toList := vals : Array α } = { toList := vals_1 }
 
 #testDelab (do let ctxCore ← readThe Core.Context; pure ctxCore.currNamespace : MetaM Name)
   expecting do
diff --git a/tests/lean/run/structInstFast.lean b/tests/lean/run/structInstFast.lean
index ecc40bc43f..6992ebf549 100644
--- a/tests/lean/run/structInstFast.lean
+++ b/tests/lean/run/structInstFast.lean
@@ -63,7 +63,7 @@ where go (val : TSyntax `ident) (width depth : Nat) (cmds : Array <| TSyntax `co
     let cmd : TSyntax `command := ⟨mkNullNode cmds⟩
     `($cmd:command)
   | m+1 =>
-    let len := cmds.data.length
+    let len := cmds.toList.length
     let newTerm (s : String) := if len = 1 then baseTypeIdent else mkIdent' s (m+1)
     let newTerm' (s : String) := if len = 1 then baseIdent else mkIdent' s (m+1)
     let fieldsStx ← mkFieldsStx type (s!"x{m}_") width
diff --git a/tests/lean/run/structuralMutual.lean b/tests/lean/run/structuralMutual.lean
index 6d227e8e50..cae9891de1 100644
--- a/tests/lean/run/structuralMutual.lean
+++ b/tests/lean/run/structuralMutual.lean
@@ -696,7 +696,7 @@ info: WithTuple.Tree.map.induct {α β : Type} (f : α → β) (motive_1 : WithT
 info: WithArray.Tree.map.induct {α β : Type} (f : α → β) (motive_1 : WithArray.Tree α → Prop)
   (motive_2 : Array (WithArray.Tree α) → Prop) (motive_3 : List (WithArray.Tree α) → Prop)
   (case1 : ∀ (x : α) (arr₁ : Array (WithArray.Tree α)), motive_2 arr₁ → motive_1 (WithArray.Tree.node x arr₁))
-  (case2 : ∀ (arr₁ : List (WithArray.Tree α)), motive_3 arr₁ → motive_2 { data := arr₁ }) (case3 : motive_3 [])
+  (case2 : ∀ (arr₁ : List (WithArray.Tree α)), motive_3 arr₁ → motive_2 { toList := arr₁ }) (case3 : motive_3 [])
   (case4 : ∀ (h₁ : WithArray.Tree α) (t₁ : List (WithArray.Tree α)), motive_1 h₁ → motive_3 t₁ → motive_3 (h₁ :: t₁))
   (x : WithArray.Tree α) : motive_1 x
 -/