diff --git a/Batteries.lean b/Batteries.lean
index 37d88fa3fb..3bd1f4ef79 100644
--- a/Batteries.lean
+++ b/Batteries.lean
@@ -16,8 +16,6 @@ import Batteries.Data.Array
 import Batteries.Data.AssocList
 import Batteries.Data.BinaryHeap
 import Batteries.Data.BinomialHeap
-import Batteries.Data.BitVec
-import Batteries.Data.Bool
 import Batteries.Data.ByteArray
 import Batteries.Data.ByteSubarray
 import Batteries.Data.Char
@@ -25,12 +23,10 @@ import Batteries.Data.DList
 import Batteries.Data.Fin
 import Batteries.Data.FloatArray
 import Batteries.Data.HashMap
-import Batteries.Data.Int
 import Batteries.Data.LazyList
 import Batteries.Data.List
 import Batteries.Data.MLList
 import Batteries.Data.Nat
-import Batteries.Data.Option
 import Batteries.Data.PairingHeap
 import Batteries.Data.RBMap
 import Batteries.Data.Range
diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
index 02293aa349..303e0b8ea5 100644
--- a/Batteries/Data/Array/Lemmas.lean
+++ b/Batteries/Data/Array/Lemmas.lean
@@ -11,30 +11,33 @@ import Batteries.Util.ProofWanted
 
 namespace Array
 
-theorem forIn_eq_forIn_data [Monad m]
+theorem forIn_eq_forIn_toList [Monad m]
     (as : Array α) (b : β) (f : α → β → m (ForInStep β)) :
-    forIn as b f = forIn as.data b f := by
+    forIn as b f = forIn as.toList b f := by
   let rec loop : ∀ {i h b j}, j + i = as.size →
-      Array.forIn.loop as f i h b = forIn (as.data.drop j) b f
+      Array.forIn.loop as f i h b = forIn (as.toList.drop j) b f
     | 0, _, _, _, rfl => by rw [List.drop_length]; rfl
     | i+1, _, _, j, ij => by
       simp only [forIn.loop, Nat.add]
       have j_eq : j = size as - 1 - i := by simp [← ij, ← Nat.add_assoc]
       have : as.size - 1 - i < as.size := j_eq ▸ ij ▸ Nat.lt_succ_of_le (Nat.le_add_right ..)
-      have : as[size as - 1 - i] :: as.data.drop (j + 1) = as.data.drop j := by
+      have : as[size as - 1 - i] :: as.toList.drop (j + 1) = as.toList.drop j := by
         rw [j_eq]; exact List.getElem_cons_drop _ _ this
       simp only [← this, List.forIn_cons]; congr; funext x; congr; funext b
       rw [loop (i := i)]; rw [← ij, Nat.succ_add]; rfl
   conv => lhs; simp only [forIn, Array.forIn]
   rw [loop (Nat.zero_add _)]; rfl
+
+@[deprecated (since := "2024-09-09")] alias forIn_eq_forIn_data := forIn_eq_forIn_toList
 @[deprecated (since := "2024-08-13")] alias forIn_eq_data_forIn := forIn_eq_forIn_data
 
 /-! ### zipWith / zip -/
 
-theorem data_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
-    (as.zipWith bs f).data = as.data.zipWith f bs.data := by
+theorem toList_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
+    (as.zipWith bs f).toList = as.toList.zipWith f bs.toList := by
   let rec loop : ∀ (i : Nat) cs, i ≤ as.size → i ≤ bs.size →
-      (zipWithAux f as bs i cs).data = cs.data ++ (as.data.drop i).zipWith f (bs.data.drop i) := by
+      (zipWithAux f as bs i cs).toList =
+        cs.toList ++ (as.toList.drop i).zipWith f (bs.toList.drop i) := by
     intro i cs hia hib
     unfold zipWithAux
     by_cases h : i = as.size ∨ i = bs.size
@@ -59,27 +62,30 @@ theorem data_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
       have has : i < as.size := Nat.lt_of_le_of_ne hia h.1
       have hbs : i < bs.size := Nat.lt_of_le_of_ne hib h.2
       simp only [has, hbs, dite_true]
-      rw [loop (i+1) _ has hbs, Array.push_data]
+      rw [loop (i+1) _ has hbs, Array.push_toList]
       have h₁ : [f as[i] bs[i]] = List.zipWith f [as[i]] [bs[i]] := rfl
-      let i_as : Fin as.data.length := ⟨i, has⟩
-      let i_bs : Fin bs.data.length := ⟨i, hbs⟩
+      let i_as : Fin as.toList.length := ⟨i, has⟩
+      let i_bs : Fin bs.toList.length := ⟨i, hbs⟩
       rw [h₁, List.append_assoc]
       congr
-      rw [← List.zipWith_append (h := by simp), getElem_eq_data_getElem, getElem_eq_data_getElem]
-      show List.zipWith f (as.data[i_as] :: List.drop (i_as + 1) as.data)
-        ((List.get bs.data i_bs) :: List.drop (i_bs + 1) bs.data) =
-        List.zipWith f (List.drop i as.data) (List.drop i bs.data)
-      simp only [data_length, Fin.getElem_fin, List.getElem_cons_drop, List.get_eq_getElem]
+      rw [← List.zipWith_append (h := by simp), getElem_eq_toList_getElem,
+        getElem_eq_toList_getElem]
+      show List.zipWith f (as.toList[i_as] :: List.drop (i_as + 1) as.toList)
+        ((List.get bs.toList i_bs) :: List.drop (i_bs + 1) bs.toList) =
+        List.zipWith f (List.drop i as.toList) (List.drop i bs.toList)
+      simp only [toList_length, Fin.getElem_fin, List.getElem_cons_drop, List.get_eq_getElem]
   simp [zipWith, loop 0 #[] (by simp) (by simp)]
+@[deprecated (since := "2024-09-09")] alias data_zipWith := toList_zipWith
 @[deprecated (since := "2024-08-13")] alias zipWith_eq_zipWith_data := data_zipWith
 
 theorem size_zipWith (as : Array α) (bs : Array β) (f : α → β → γ) :
     (as.zipWith bs f).size = min as.size bs.size := by
-  rw [size_eq_length_data, data_zipWith, List.length_zipWith]
+  rw [size_eq_length_toList, toList_zipWith, List.length_zipWith]
 
-theorem data_zip (as : Array α) (bs : Array β) :
-    (as.zip bs).data = as.data.zip bs.data :=
-  data_zipWith Prod.mk as bs
+theorem toList_zip (as : Array α) (bs : Array β) :
+    (as.zip bs).toList = as.toList.zip bs.toList :=
+  toList_zipWith Prod.mk as bs
+@[deprecated (since := "2024-09-09")] alias data_zip := toList_zip
 @[deprecated (since := "2024-08-13")] alias zip_eq_zip_data := data_zip
 
 theorem size_zip (as : Array α) (bs : Array β) :
@@ -90,34 +96,36 @@ theorem size_zip (as : Array α) (bs : Array β) :
 
 theorem size_filter_le (p : α → Bool) (l : Array α) :
     (l.filter p).size ≤ l.size := by
-  simp only [← data_length, filter_data]
+  simp only [← toList_length, filter_toList]
   apply List.length_filter_le
 
 /-! ### join -/
 
-@[simp] theorem data_join {l : Array (Array α)} : l.join.data = (l.data.map data).join := by
+@[simp] theorem toList_join {l : Array (Array α)} : l.join.toList = (l.toList.map toList).join := by
   dsimp [join]
-  simp only [foldl_eq_foldl_data]
-  generalize l.data = l
-  have : ∀ a : Array α, (List.foldl ?_ a l).data = a.data ++ ?_ := ?_
+  simp only [foldl_eq_foldl_toList]
+  generalize l.toList = l
+  have : ∀ a : Array α, (List.foldl ?_ a l).toList = a.toList ++ ?_ := ?_
   exact this #[]
   induction l with
   | nil => simp
-  | cons h => induction h.data <;> simp [*]
+  | cons h => induction h.toList <;> simp [*]
+@[deprecated (since := "2024-09-09")] alias data_join := toList_join
 @[deprecated (since := "2024-08-13")] alias join_data := data_join
 
 theorem mem_join : ∀ {L : Array (Array α)}, a ∈ L.join ↔ ∃ l, l ∈ L ∧ a ∈ l := by
-  simp only [mem_def, data_join, List.mem_join, List.mem_map]
+  simp only [mem_def, toList_join, List.mem_join, List.mem_map]
   intro l
   constructor
   · rintro ⟨_, ⟨s, m, rfl⟩, h⟩
     exact ⟨s, m, h⟩
   · rintro ⟨s, h₁, h₂⟩
-    refine ⟨s.data, ⟨⟨s, h₁, rfl⟩, h₂⟩⟩
+    refine ⟨s.toList, ⟨⟨s, h₁, rfl⟩, h₂⟩⟩
 
 /-! ### erase -/
 
-@[simp] proof_wanted data_erase [BEq α] {l : Array α} {a : α} : (l.erase a).data = l.data.erase a
+@[simp] proof_wanted toList_erase [BEq α] {l : Array α} {a : α} :
+    (l.erase a).toList = l.toList.erase a
 
 /-! ### shrink -/
 
@@ -145,8 +153,6 @@ theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by
 
 /-! ### mem -/
 
-alias not_mem_empty := not_mem_nil
-
 theorem mem_singleton : a ∈ #[b] ↔ a = b := by simp
 
 /-! ### append -/
diff --git a/Batteries/Data/Array/Pairwise.lean b/Batteries/Data/Array/Pairwise.lean
index 84dff1f680..1a71924c1c 100644
--- a/Batteries/Data/Array/Pairwise.lean
+++ b/Batteries/Data/Array/Pairwise.lean
@@ -17,15 +17,15 @@ larger indices.
 For example `as.Pairwise (· ≠ ·)` asserts that `as` has no duplicates, `as.Pairwise (· < ·)` asserts
 that `as` is strictly sorted and `as.Pairwise (· ≤ ·)` asserts that `as` is weakly sorted.
 -/
-def Pairwise (R : α → α → Prop) (as : Array α) : Prop := as.data.Pairwise R
+def Pairwise (R : α → α → Prop) (as : Array α) : Prop := as.toList.Pairwise R
 
 theorem pairwise_iff_get {as : Array α} : as.Pairwise R ↔
     ∀ (i j : Fin as.size), i < j → R (as.get i) (as.get j) := by
-  unfold Pairwise; simp [List.pairwise_iff_get, getElem_fin_eq_data_get]; rfl
+  unfold Pairwise; simp [List.pairwise_iff_get, getElem_fin_eq_toList_get]; rfl
 
 theorem pairwise_iff_getElem {as : Array α} : as.Pairwise R ↔
     ∀ (i j : Nat) (_ : i < as.size) (_ : j < as.size), i < j → R as[i] as[j] := by
-  unfold Pairwise; simp [List.pairwise_iff_getElem, data_length]; rfl
+  unfold Pairwise; simp [List.pairwise_iff_getElem, toList_length]; rfl
 
 instance (R : α → α → Prop) [DecidableRel R] (as) : Decidable (Pairwise R as) :=
   have : (∀ (j : Fin as.size) (i : Fin j.val), R as[i.val] (as[j.val])) ↔ Pairwise R as := by
@@ -46,12 +46,13 @@ theorem pairwise_pair : #[a, b].Pairwise R ↔ R a b := by
 
 theorem pairwise_append {as bs : Array α} :
     (as ++ bs).Pairwise R ↔ as.Pairwise R ∧ bs.Pairwise R ∧ (∀ x ∈ as, ∀ y ∈ bs, R x y) := by
-  unfold Pairwise; simp [← mem_data, append_data, ← List.pairwise_append]
+  unfold Pairwise; simp [← mem_toList, append_toList, ← List.pairwise_append]
 
 theorem pairwise_push {as : Array α} :
     (as.push a).Pairwise R ↔ as.Pairwise R ∧ (∀ x ∈ as, R x a) := by
   unfold Pairwise
-  simp [← mem_data, push_data, List.pairwise_append, List.pairwise_singleton, List.mem_singleton]
+  simp [← mem_toList, push_toList, List.pairwise_append, List.pairwise_singleton,
+    List.mem_singleton]
 
 theorem pairwise_extract {as : Array α} (h : as.Pairwise R) (start stop) :
     (as.extract start stop).Pairwise R := by
diff --git a/Batteries/Data/AssocList.lean b/Batteries/Data/AssocList.lean
index 1492304efa..1e94b1d2f6 100644
--- a/Batteries/Data/AssocList.lean
+++ b/Batteries/Data/AssocList.lean
@@ -78,7 +78,7 @@ def toListTR (as : AssocList α β) : List (α × β) :=
 
 @[csimp] theorem toList_eq_toListTR : @toList = @toListTR := by
   funext α β as; simp [toListTR]
-  exact .symm <| (Array.foldl_data_eq_map (toList as) _ id).trans (List.map_id _)
+  exact .symm <| (Array.foldl_toList_eq_map (toList as) _ id).trans (List.map_id _)
 
 /-- `O(n)`. Run monadic function `f` on all elements in the list, from head to tail. -/
 @[specialize] def forM [Monad m] (f : α → β → m PUnit) : AssocList α β → m PUnit
diff --git a/Batteries/Data/BitVec.lean b/Batteries/Data/BitVec.lean
deleted file mode 100644
index ff4358f07d..0000000000
--- a/Batteries/Data/BitVec.lean
+++ /dev/null
@@ -1 +0,0 @@
-import Batteries.Data.BitVec.Lemmas
diff --git a/Batteries/Data/BitVec/Lemmas.lean b/Batteries/Data/BitVec/Lemmas.lean
deleted file mode 100644
index 2bcd3ce4aa..0000000000
--- a/Batteries/Data/BitVec/Lemmas.lean
+++ /dev/null
@@ -1,16 +0,0 @@
-/-
-Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joe Hendrix
--/
-import Batteries.Tactic.Alias
-
-namespace BitVec
-
-@[deprecated (since := "2024-02-07")] alias zero_is_unique := eq_nil
-
-/-! ### sub/neg -/
-
-@[deprecated (since := "2024-02-07")] alias sub_toNat := toNat_sub
-
-@[deprecated (since := "2024-02-07")] alias neg_toNat := toNat_neg
diff --git a/Batteries/Data/Bool.lean b/Batteries/Data/Bool.lean
deleted file mode 100644
index b6c0c9b4e7..0000000000
--- a/Batteries/Data/Bool.lean
+++ /dev/null
@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2023 F. G. Dorais. No rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: F. G. Dorais
--/
-
-import Batteries.Tactic.Alias
-
-namespace Bool
-
-/-! ### injectivity lemmas -/
-
-@[deprecated (since := "2023-10-27")] alias not_inj' := not_inj_iff
-
-@[deprecated (since := "2023-10-27")] alias and_or_inj_right' := and_or_inj_right_iff
-
-@[deprecated (since := "2023-10-27")] alias and_or_inj_left' := and_or_inj_left_iff
-
-end Bool
diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean
index 3632d4f254..346f3006e5 100644
--- a/Batteries/Data/Fin/Basic.lean
+++ b/Batteries/Data/Fin/Basic.lean
@@ -13,4 +13,4 @@ def clamp (n m : Nat) : Fin (m + 1) := ⟨min n m, Nat.lt_succ_of_le (Nat.min_le
 def enum (n) : Array (Fin n) := Array.ofFn id
 
 /-- `list n` is the list of all elements of `Fin n` in order -/
-def list (n) : List (Fin n) := (enum n).data
+def list (n) : List (Fin n) := (enum n).toList
diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean
index d0a0ce91f5..6707b6b4f5 100644
--- a/Batteries/Data/Fin/Lemmas.lean
+++ b/Batteries/Data/Fin/Lemmas.lean
@@ -30,7 +30,7 @@ attribute [norm_cast] val_last
 
 @[simp] theorem getElem_list (i : Nat) (h : i < (list n).length) :
     (list n)[i] = cast (length_list n) ⟨i, h⟩ := by
-  simp only [list]; rw [← Array.getElem_eq_data_getElem, getElem_enum, cast_mk]
+  simp only [list]; rw [← Array.getElem_eq_toList_getElem, getElem_enum, cast_mk]
 
 @[deprecated getElem_list (since := "2024-06-12")]
 theorem get_list (i : Fin (list n).length) : (list n).get i = i.cast (length_list n) := by
diff --git a/Batteries/Data/HashMap/Basic.lean b/Batteries/Data/HashMap/Basic.lean
index 12279d89d1..98905c3343 100644
--- a/Batteries/Data/HashMap/Basic.lean
+++ b/Batteries/Data/HashMap/Basic.lean
@@ -37,7 +37,7 @@ def update (data : Buckets α β) (i : USize)
 The number of elements in the bucket array.
 Note: this is marked `noncomputable` because it is only intended for specification.
 -/
-noncomputable def size (data : Buckets α β) : Nat := .sum (data.1.data.map (·.toList.length))
+noncomputable def size (data : Buckets α β) : Nat := .sum (data.1.toList.map (·.toList.length))
 
 @[simp] theorem update_size (self : Buckets α β) (i d h) :
     (self.update i d h).1.size = self.1.size := Array.size_uset ..
@@ -52,7 +52,7 @@ The well-formedness invariant for the bucket array says that every element hashe
 -/
 structure WF [BEq α] [Hashable α] (buckets : Buckets α β) : Prop where
   /-- The elements of a bucket are all distinct according to the `BEq` relation. -/
-  distinct [LawfulHashable α] [PartialEquivBEq α] : ∀ bucket ∈ buckets.1.data,
+  distinct [LawfulHashable α] [PartialEquivBEq α] : ∀ bucket ∈ buckets.1.toList,
     bucket.toList.Pairwise fun a b => ¬(a.1 == b.1)
   /-- Every element in a bucket should hash to its location. -/
   hash_self (i : Nat) (h : i < buckets.1.size) :
diff --git a/Batteries/Data/HashMap/WF.lean b/Batteries/Data/HashMap/WF.lean
index 9f69994638..993e9e10d4 100644
--- a/Batteries/Data/HashMap/WF.lean
+++ b/Batteries/Data/HashMap/WF.lean
@@ -15,26 +15,28 @@ attribute [-simp] Bool.not_eq_true
 
 namespace Buckets
 
-@[ext] protected theorem ext : ∀ {b₁ b₂ : Buckets α β}, b₁.1.data = b₂.1.data → b₁ = b₂
+@[ext] protected theorem ext : ∀ {b₁ b₂ : Buckets α β}, b₁.1.toList = b₂.1.toList → b₁ = b₂
   | ⟨⟨_⟩, _⟩, ⟨⟨_⟩, _⟩, rfl => rfl
 
-theorem update_data (self : Buckets α β) (i d h) :
-    (self.update i d h).1.data = self.1.data.set i.toNat d := rfl
+theorem toList_update (self : Buckets α β) (i d h) :
+    (self.update i d h).1.toList = self.1.toList.set i.toNat d := rfl
+
+@[deprecated (since := "2024-09-09")] alias update_data := toList_update
 
 theorem exists_of_update (self : Buckets α β) (i d h) :
-    ∃ l₁ l₂, self.1.data = l₁ ++ self.1[i] :: l₂ ∧ List.length l₁ = i.toNat ∧
-      (self.update i d h).1.data = l₁ ++ d :: l₂ := by
-  simp only [Array.data_length, Array.ugetElem_eq_getElem, Array.getElem_eq_data_getElem]
+    ∃ l₁ l₂, self.1.toList = l₁ ++ self.1[i] :: l₂ ∧ List.length l₁ = i.toNat ∧
+      (self.update i d h).1.toList = l₁ ++ d :: l₂ := by
+  simp only [Array.toList_length, Array.ugetElem_eq_getElem, Array.getElem_eq_toList_getElem]
   exact List.exists_of_set h
 
 theorem update_update (self : Buckets α β) (i d d' h h') :
     (self.update i d h).update i d' h' = self.update i d' h := by
-  simp only [update, Array.uset, Array.data_length]
+  simp only [update, Array.uset, Array.toList_length]
   congr 1
   rw [Array.set_set]
 
 theorem size_eq (data : Buckets α β) :
-  size data = .sum (data.1.data.map (·.toList.length)) := rfl
+  size data = .sum (data.1.toList.map (·.toList.length)) := rfl
 
 theorem mk_size (h) : (mk n h : Buckets α β).size = 0 := by
   simp only [mk, mkArray, size_eq]; clear h
@@ -44,7 +46,7 @@ theorem WF.mk' [BEq α] [Hashable α] (h) : (Buckets.mk n h : Buckets α β).WF
   refine ⟨fun _ h => ?_, fun i h => ?_⟩
   · simp only [Buckets.mk, mkArray, List.mem_replicate, ne_eq] at h
     simp [h, List.Pairwise.nil]
-  · simp [Buckets.mk, empty', mkArray, Array.getElem_eq_data_getElem, AssocList.All]
+  · simp [Buckets.mk, empty', mkArray, Array.getElem_eq_toList_getElem, AssocList.All]
 
 theorem WF.update [BEq α] [Hashable α] {buckets : Buckets α β} {i d h} (H : buckets.WF)
     (h₁ : ∀ [PartialEquivBEq α] [LawfulHashable α],
@@ -56,20 +58,20 @@ theorem WF.update [BEq α] [Hashable α] {buckets : Buckets α β} {i d h} (H :
   refine ⟨fun l hl => ?_, fun i hi p hp => ?_⟩
   · exact match List.mem_or_eq_of_mem_set hl with
     | .inl hl => H.1 _ hl
-    | .inr rfl => h₁ (H.1 _ (Array.getElem_mem_data ..))
+    | .inr rfl => h₁ (H.1 _ (Array.getElem_mem_toList ..))
   · revert hp
-    simp only [Array.getElem_eq_data_getElem, update_data, List.getElem_set, Array.data_length,
-      update_size]
+    simp only [Array.getElem_eq_toList_getElem, toList_update, List.getElem_set,
+      Array.toList_length, update_size]
     split <;> intro hp
     · next eq => exact eq ▸ h₂ (H.2 _ _) _ hp
-    · simp only [update_size, Array.data_length] at hi
+    · simp only [update_size, Array.toList_length] at hi
       exact H.2 i hi _ hp
 
 end Buckets
 
 theorem reinsertAux_size [Hashable α] (data : Buckets α β) (a : α) (b : β) :
     (reinsertAux data a b).size = data.size.succ := by
-  simp only [reinsertAux, Array.data_length, Array.ugetElem_eq_getElem, Buckets.size_eq,
+  simp only [reinsertAux, Array.toList_length, Array.ugetElem_eq_getElem, Buckets.size_eq,
     Nat.succ_eq_add_one]
   refine have ⟨l₁, l₂, h₁, _, eq⟩ := Buckets.exists_of_update ..; eq ▸ ?_
   simp [h₁, Nat.succ_add]; rfl
@@ -89,33 +91,33 @@ theorem expand_size [Hashable α] {buckets : Buckets α β} :
   · rw [Buckets.mk_size]; simp [Buckets.size]
   · nofun
 where
-  go (i source) (target : Buckets α β) (hs : ∀ j < i, source.data[j]?.getD .nil = .nil) :
+  go (i source) (target : Buckets α β) (hs : ∀ j < i, source.toList[j]?.getD .nil = .nil) :
       (expand.go i source target).size =
-        .sum (source.data.map (·.toList.length)) + target.size := by
+        .sum (source.toList.map (·.toList.length)) + target.size := by
     unfold expand.go; split
     · next H =>
       refine (go (i+1) _ _ fun j hj => ?a).trans ?b <;> simp
       · case a =>
         simp [List.getD_eq_getElem?_getD, List.getElem?_set, Option.map_eq_map]; split
-        · cases source.data[j]? <;> rfl
+        · cases source.toList[j]? <;> rfl
         · next H => exact hs _ (Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hj) (Ne.symm H))
       · case b =>
         refine have ⟨l₁, l₂, h₁, _, eq⟩ := List.exists_of_set H; eq ▸ ?_
         rw [h₁]
         simp only [Buckets.size_eq, List.map_append, List.map_cons, AssocList.toList,
-          List.length_nil, Nat.sum_append, Nat.sum_cons, Nat.zero_add, Array.data_length]
+          List.length_nil, Nat.sum_append, Nat.sum_cons, Nat.zero_add, Array.toList_length]
         rw [Nat.add_assoc, Nat.add_assoc, Nat.add_assoc]; congr 1
         (conv => rhs; rw [Nat.add_left_comm]); congr 1
-        rw [← Array.getElem_eq_data_getElem]
+        rw [← Array.getElem_eq_toList_getElem]
         have := @reinsertAux_size α β _; simp [Buckets.size] at this
         induction source[i].toList generalizing target <;> simp [*, Nat.succ_add]; rfl
     · next H =>
       rw [(_ : Nat.sum _ = 0), Nat.zero_add]
-      rw [← (_ : source.data.map (fun _ => .nil) = source.data)]
+      rw [← (_ : source.toList.map (fun _ => .nil) = source.toList)]
       · simp only [List.map_map]
-        induction source.data <;> simp [*]
+        induction source.toList <;> simp [*]
       refine List.ext_getElem (by simp) fun j h₁ h₂ => ?_
-      simp only [List.getElem_map, Array.data_length]
+      simp only [List.getElem_map, Array.toList_length]
       have := (hs j (Nat.lt_of_lt_of_le h₂ (Nat.not_lt.1 H))).symm
       rwa [List.getElem?_eq_getElem] at this
   termination_by source.size - i
@@ -124,21 +126,21 @@ theorem expand_WF.foldl [BEq α] [Hashable α] (rank : α → Nat) {l : List (α
     (hl₁ : ∀ [PartialEquivBEq α] [LawfulHashable α], l.Pairwise fun a b => ¬(a.1 == b.1))
     (hl₂ : ∀ x ∈ l, rank x.1 = i)
     {target : Buckets α β} (ht₁ : target.WF)
-    (ht₂ : ∀ bucket ∈ target.1.data,
+    (ht₂ : ∀ bucket ∈ target.1.toList,
       bucket.All fun k _ => rank k ≤ i ∧
         ∀ [PartialEquivBEq α] [LawfulHashable α], ∀ x ∈ l, ¬(x.1 == k)) :
     (l.foldl (fun d x => reinsertAux d x.1 x.2) target).WF ∧
-    ∀ bucket ∈ (l.foldl (fun d x => reinsertAux d x.1 x.2) target).1.data,
+    ∀ bucket ∈ (l.foldl (fun d x => reinsertAux d x.1 x.2) target).1.toList,
       bucket.All fun k _ => rank k ≤ i := by
   induction l generalizing target with
   | nil => exact ⟨ht₁, fun _ h₁ _ h₂ => (ht₂ _ h₁ _ h₂).1⟩
   | cons _ _ ih =>
     simp only [List.pairwise_cons, List.mem_cons, forall_eq_or_imp] at hl₁ hl₂ ht₂
     refine ih hl₁.2 hl₂.2
-      (reinsertAux_WF ht₁ fun _ h => (ht₂ _ (Array.getElem_mem_data ..) _ h).2.1)
+      (reinsertAux_WF ht₁ fun _ h => (ht₂ _ (Array.getElem_mem_toList ..) _ h).2.1)
       (fun _ h => ?_)
-    simp only [reinsertAux, Buckets.update, Array.uset, Array.data_length,
-      Array.ugetElem_eq_getElem, Array.data_set] at h
+    simp only [reinsertAux, Buckets.update, Array.uset, Array.toList_length,
+      Array.ugetElem_eq_getElem, Array.toList_set] at h
     match List.mem_or_eq_of_mem_set h with
     | .inl h =>
       intro _ hf
@@ -148,7 +150,7 @@ theorem expand_WF.foldl [BEq α] [Hashable α] (rank : α → Nat) {l : List (α
       | _, .head .. =>
         exact ⟨hl₂.1 ▸ Nat.le_refl _, fun _ h h' => hl₁.1 _ h (PartialEquivBEq.symm h')⟩
       | _, .tail _ h =>
-        have ⟨h₁, h₂⟩ := ht₂ _ (Array.getElem_mem_data ..) _ h
+        have ⟨h₁, h₂⟩ := ht₂ _ (Array.getElem_mem_toList ..) _ h
         exact ⟨h₁, h₂.2⟩
 
 theorem expand_WF [BEq α] [Hashable α] {buckets : Buckets α β} (H : buckets.WF) :
@@ -156,11 +158,11 @@ theorem expand_WF [BEq α] [Hashable α] {buckets : Buckets α β} (H : buckets.
   go _ H.1 H.2 ⟨.mk' _, fun _ _ _ _ => by simp_all [Buckets.mk, List.mem_replicate]⟩
 where
   go (i) {source : Array (AssocList α β)}
-      (hs₁ : ∀ [LawfulHashable α] [PartialEquivBEq α], ∀ bucket ∈ source.data,
+      (hs₁ : ∀ [LawfulHashable α] [PartialEquivBEq α], ∀ bucket ∈ source.toList,
         bucket.toList.Pairwise fun a b => ¬(a.1 == b.1))
       (hs₂ : ∀ (j : Nat) (h : j < source.size),
         source[j].All fun k _ => ((hash k).toUSize % source.size).toNat = j)
-      {target : Buckets α β} (ht : target.WF ∧ ∀ bucket ∈ target.1.data,
+      {target : Buckets α β} (ht : target.WF ∧ ∀ bucket ∈ target.1.toList,
         bucket.All fun k _ => ((hash k).toUSize % source.size).toNat < i) :
       (expand.go i source target).WF := by
     unfold expand.go; split
@@ -169,8 +171,8 @@ where
       · match List.mem_or_eq_of_mem_set hl with
         | .inl hl => exact hs₁ _ hl
         | .inr e => exact e ▸ .nil
-      · simp only [Array.data_length, Array.size_set, Array.getElem_eq_data_getElem, Array.data_set,
-          List.getElem_set]
+      · simp only [Array.toList_length, Array.size_set, Array.getElem_eq_toList_getElem,
+          Array.toList_set, List.getElem_set]
         split
         · nofun
         · exact hs₂ _ (by simp_all)
@@ -178,7 +180,7 @@ where
         have := expand_WF.foldl rank ?_ (hs₂ _ H) ht.1 (fun _ h₁ _ h₂ => ?_)
         · simp only [Array.get_eq_getElem, AssocList.foldl_eq, Array.size_set]
           exact ⟨this.1, fun _ h₁ _ h₂ => Nat.lt_succ_of_le (this.2 _ h₁ _ h₂)⟩
-        · exact hs₁ _ (Array.getElem_mem_data ..)
+        · exact hs₁ _ (Array.getElem_mem_toList ..)
         · have := ht.2 _ h₁ _ h₂
           refine ⟨Nat.le_of_lt this, fun _ h h' => Nat.ne_of_lt this ?_⟩
           exact LawfulHashable.hash_eq h' ▸ hs₂ _ H _ h
@@ -196,7 +198,7 @@ theorem insert_size [BEq α] [Hashable α] {m : Imp α β} {k v}
   · unfold Buckets.size
     refine have ⟨_, _, h₁, _, eq⟩ := Buckets.exists_of_update ..; eq ▸ ?_
     simp [h, h₁, Buckets.size_eq, Nat.succ_add]; rfl
-  · rw [expand_size]; simp only [expand, h, Buckets.size, Array.data_length, Buckets.update_size]
+  · rw [expand_size]; simp only [expand, h, Buckets.size, Array.toList_length, Buckets.update_size]
     refine have ⟨_, _, h₁, _, eq⟩ := Buckets.exists_of_update ..; eq ▸ ?_
     simp [h₁, Buckets.size_eq, Nat.succ_add]; rfl
 
@@ -262,7 +264,7 @@ theorem erase_size [BEq α] [Hashable α] {m : Imp α β} {k}
   · next H =>
     simp only [h, Buckets.size]
     refine have ⟨_, _, h₁, _, eq⟩ := Buckets.exists_of_update ..; eq ▸ ?_
-    simp only [h₁, Array.data_length, Array.ugetElem_eq_getElem, List.map_append, List.map_cons,
+    simp only [h₁, Array.toList_length, Array.ugetElem_eq_getElem, List.map_append, List.map_cons,
       Nat.sum_append, Nat.sum_cons, AssocList.toList_erase]
     rw [(_ : List.length _ = _ + 1), Nat.add_right_comm]; {rfl}
     clear h₁ eq
@@ -315,8 +317,8 @@ theorem WF.mapVal {α β γ} {f : α → β → γ} [BEq α] [Hashable α]
     {m : Imp α β} (H : WF m) : WF (mapVal f m) := by
   have ⟨h₁, h₂⟩ := H.out
   simp only [Imp.mapVal, h₁, Buckets.mapVal, WF_iff]; refine ⟨?_, ?_, fun i h => ?_⟩
-  · simp only [Buckets.size, Array.map_data, List.map_map]; congr; funext l; simp
-  · simp only [Array.map_data, List.forall_mem_map]
+  · simp only [Buckets.size, Array.map_toList, List.map_map]; congr; funext l; simp
+  · simp only [Array.map_toList, List.forall_mem_map]
     simp only [AssocList.toList_mapVal, List.pairwise_map]
     exact fun _ => h₂.1 _
   · simp only [Array.size_map, AssocList.All, Array.getElem_map, AssocList.toList_mapVal,
@@ -359,7 +361,7 @@ theorem WF.filterMap {α β γ} {f : α → β → Option γ} [BEq α] [Hashable
   suffices ∀ bk sz (h : 0 < bk.length),
     m.buckets.val.mapM (m := M) (filterMap.go f .nil) ⟨0⟩ = (⟨bk⟩, ⟨sz⟩) →
     WF ⟨sz, ⟨bk⟩, h⟩ from this _ _ _ rfl
-  simp only [Array.mapM_eq_mapM_data, bind, StateT.bind, H2, List.map_map, Nat.zero_add, g]
+  simp only [Array.mapM_eq_mapM_toList, bind, StateT.bind, H2, List.map_map, Nat.zero_add, g]
   intro bk sz h e'; cases e'
   refine .mk (by simp [Buckets.size]) ⟨?_, fun i h => ?_⟩
   · simp only [List.forall_mem_map, List.toList_toAssocList]
@@ -367,7 +369,7 @@ theorem WF.filterMap {α β γ} {f : α → β → Option γ} [BEq α] [Hashable
     have := H.out.2.1 _ h
     rw [← List.pairwise_map (R := (¬ · == ·))] at this ⊢
     exact this.sublist (H3 l.toList)
-  · simp only [Array.size_mk, List.length_map, Array.data_length, Array.getElem_eq_data_getElem,
+  · simp only [Array.size_mk, List.length_map, Array.toList_length, Array.getElem_eq_toList_getElem,
       List.getElem_map] at h ⊢
     have := H.out.2.2 _ h
     simp only [AssocList.All, List.toList_toAssocList, List.mem_reverse, List.mem_filterMap,
diff --git a/Batteries/Data/Int.lean b/Batteries/Data/Int.lean
deleted file mode 100644
index 29b6c2e4a9..0000000000
--- a/Batteries/Data/Int.lean
+++ /dev/null
@@ -1,3 +0,0 @@
-import Batteries.Data.Int.DivMod
-import Batteries.Data.Int.Lemmas
-import Batteries.Data.Int.Order
diff --git a/Batteries/Data/Int/DivMod.lean b/Batteries/Data/Int/DivMod.lean
deleted file mode 100644
index 7558c98a3d..0000000000
--- a/Batteries/Data/Int/DivMod.lean
+++ /dev/null
@@ -1,84 +0,0 @@
-/-
-Copyright (c) 2016 Jeremy Avigad. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jeremy Avigad, Mario Carneiro
--/
-import Batteries.Data.Int.Order
-
-/-!
-# Lemmas about integer division
--/
-
-
-open Nat
-
-namespace Int
-
-/-!
-### The following lemmas have been commented out here for a while, and need restoration.
--/
-
-/-
-theorem eq_mul_ediv_of_mul_eq_mul_of_dvd_left {a b c d : Int}
-    (hb : b ≠ 0) (hbc : b ∣ c) (h : b * a = c * d) : a = c / b * d := by
-  rcases hbc with ⟨k, hk⟩
-  subst hk
-  rw [Int.mul_ediv_cancel_left _ hb]
-  rw [Int.mul_assoc] at h
-  apply mul_left_cancel₀ hb h
-
-/-- If an integer with larger absolute value divides an integer, it is
-zero. -/
-theorem eq_zero_of_dvd_ofNatAbs_lt_natAbs {a b : Int} (w : a ∣ b) (h : natAbs b < natAbs a) :
-    b = 0 := by
-  rw [← natAbs_dvd, ← dvd_natAbs, ofNat_dvd] at w
-  rw [← natAbs_eq_zero]
-  exact eq_zero_of_dvd_of_lt w h
-
-theorem eq_zero_of_dvd_of_nonneg_of_lt {a b : Int} (w₁ : 0 ≤ a) (w₂ : a < b) (h : b ∣ a) : a = 0 :=
-  eq_zero_of_dvd_ofNatAbs_lt_natAbs h (natAbs_lt_natAbs_of_nonneg_of_lt w₁ w₂)
-
-/-- If two integers are congruent to a sufficiently large modulus,
-they are equal. -/
-theorem eq_of_mod_eq_ofNatAbs_sub_lt_natAbs {a b c : Int}
-    (h1 : a % b = c) (h2 : natAbs (a - c) < natAbs b) : a = c :=
-  Int.eq_of_sub_eq_zero (eq_zero_of_dvd_ofNatAbs_lt_natAbs (dvd_sub_of_emod_eq h1) h2)
-
-theorem ofNat_add_negSucc_of_lt {m n : Nat} (h : m < n.succ) : ofNat m + -[n+1] = -[n+1 - m] := by
-  change subNatNat _ _ = _
-  have h' : n.succ - m = (n - m).succ
-  apply succ_sub
-  apply le_of_lt_succ h
-  simp [*, subNatNat]
-
-theorem ofNat_add_negSucc_of_ge {m n : Nat} (h : n.succ ≤ m) :
-    ofNat m + -[n+1] = ofNat (m - n.succ) := by
-  change subNatNat _ _ = _
-  have h' : n.succ - m = 0
-  apply tsub_eq_zero_iff_le.mpr h
-  simp [*, subNatNat]
-
-@[simp]
-theorem neg_add_neg (m n : Nat) : -[m+1] + -[n+1] = -[Nat+1.succ (m + n)] :=
-  rfl
-
-theorem natAbs_le_of_dvd_ne_zero {s t : Int} (hst : s ∣ t) (ht : t ≠ 0) : natAbs s ≤ natAbs t :=
-  not_lt.mp (mt (eq_zero_of_dvd_ofNatAbs_lt_natAbs hst) ht)
-
-theorem natAbs_eq_of_dvd_dvd {s t : Int} (hst : s ∣ t) (hts : t ∣ s) : natAbs s = natAbs t :=
-  Nat.dvd_antisymm (natAbs_dvd_iff_dvd.mpr hst) (natAbs_dvd_iff_dvd.mpr hts)
-
-theorem div_dvd_of_dvd {s t : Int} (hst : s ∣ t) : t / s ∣ t := by
-  rcases eq_or_ne s 0 with (rfl | hs)
-  · simpa using hst
-  rcases hst with ⟨c, hc⟩
-  simp [hc, Int.mul_div_cancel_left _ hs]
-
-theorem dvd_div_of_mul_dvd {a b c : Int} (h : a * b ∣ c) : b ∣ c / a := by
-  rcases eq_or_ne a 0 with (rfl | ha)
-  · simp only [Int.div_zero, dvd_zero]
-
-  rcases h with ⟨d, rfl⟩
-  refine' ⟨d, _⟩
-  rw [mul_assoc, Int.mul_div_cancel_left _ ha]
--/
diff --git a/Batteries/Data/Int/Lemmas.lean b/Batteries/Data/Int/Lemmas.lean
deleted file mode 100644
index 3ce6c74c04..0000000000
--- a/Batteries/Data/Int/Lemmas.lean
+++ /dev/null
@@ -1,6 +0,0 @@
--- This is a backwards compatibility shim,
--- after `Batteries.Data.Int.Lemmas` was split into smaller files.
--- Hopefully it can later be removed.
-
-import Batteries.Data.Int.Order
-import Batteries.Data.Int.DivMod
diff --git a/Batteries/Data/Int/Order.lean b/Batteries/Data/Int/Order.lean
deleted file mode 100644
index daab75c612..0000000000
--- a/Batteries/Data/Int/Order.lean
+++ /dev/null
@@ -1,10 +0,0 @@
-/-
-Copyright (c) 2016 Jeremy Avigad. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
--/
-import Batteries.Tactic.Alias
-
-namespace Int
-
-@[deprecated (since := "2024-01-24")] alias ofNat_natAbs_eq_of_nonneg := natAbs_of_nonneg
diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean
index a44f430c8d..405f2a4ea9 100644
--- a/Batteries/Data/List/Basic.lean
+++ b/Batteries/Data/List/Basic.lean
@@ -86,7 +86,7 @@ drop_while (· != 1) [0, 1, 2, 3] = [1, 2, 3]
 
 @[csimp] theorem replaceF_eq_replaceFTR : @replaceF = @replaceFTR := by
   funext α p l; simp [replaceFTR]
-  let rec go (acc) : ∀ xs, replaceFTR.go p xs acc = acc.data ++ xs.replaceF p
+  let rec go (acc) : ∀ xs, replaceFTR.go p xs acc = acc.toList ++ xs.replaceF p
   | [] => by simp [replaceFTR.go, replaceF]
   | x::xs => by
     simp [replaceFTR.go, replaceF]; cases p x <;> simp
@@ -149,8 +149,9 @@ def splitOnP (P : α → Bool) (l : List α) : List (List α) := go l [] where
 
 @[csimp] theorem splitOnP_eq_splitOnPTR : @splitOnP = @splitOnPTR := by
   funext α P l; simp [splitOnPTR]
-  suffices ∀ xs acc r, splitOnPTR.go P xs acc r = r.data ++ splitOnP.go P xs acc.data.reverse from
-    (this l #[] #[]).symm
+  suffices ∀ xs acc r,
+    splitOnPTR.go P xs acc r = r.toList ++ splitOnP.go P xs acc.toList.reverse from
+      (this l #[] #[]).symm
   intro xs acc r; induction xs generalizing acc r with simp [splitOnP.go, splitOnPTR.go]
   | cons x xs IH => cases P x <;> simp [*]
 
@@ -196,7 +197,7 @@ def modifyNthTR (f : α → α) (n : Nat) (l : List α) : List α := go l n #[]
   | a :: l, 0, acc => acc.toListAppend (f a :: l)
   | a :: l, n+1, acc => go l n (acc.push a)
 
-theorem modifyNthTR_go_eq : ∀ l n, modifyNthTR.go f l n acc = acc.data ++ modifyNth f n l
+theorem modifyNthTR_go_eq : ∀ l n, modifyNthTR.go f l n acc = acc.toList ++ modifyNth f n l
   | [], n => by cases n <;> simp [modifyNthTR.go, modifyNth]
   | a :: l, 0 => by simp [modifyNthTR.go, modifyNth]
   | a :: l, n+1 => by simp [modifyNthTR.go, modifyNth, modifyNthTR_go_eq l]
@@ -229,7 +230,7 @@ def insertNth (n : Nat) (a : α) : List α → List α :=
   | _, [], acc => acc.toList
   | n+1, a :: l, acc => go n l (acc.push a)
 
-theorem insertNthTR_go_eq : ∀ n l, insertNthTR.go a n l acc = acc.data ++ insertNth n a l
+theorem insertNthTR_go_eq : ∀ n l, insertNthTR.go a n l acc = acc.toList ++ insertNth n a l
   | 0, l | _+1, [] => by simp [insertNthTR.go, insertNth]
   | n+1, a :: l => by simp [insertNthTR.go, insertNth, insertNthTR_go_eq n l]
 
@@ -261,7 +262,7 @@ def takeDTR (n : Nat) (l : List α) (dflt : α) : List α := go n l #[] where
   | 0, _, acc => acc.toList
   | n, [], acc => acc.toListAppend (replicate n dflt)
 
-theorem takeDTR_go_eq : ∀ n l, takeDTR.go dflt n l acc = acc.data ++ takeD n l dflt
+theorem takeDTR_go_eq : ∀ n l, takeDTR.go dflt n l acc = acc.toList ++ takeD n l dflt
   | 0, _ => by simp [takeDTR.go]
   | _+1, [] => by simp [takeDTR.go, replicate_succ]
   | _+1, _::l => by simp [takeDTR.go, takeDTR_go_eq _ l]
@@ -286,7 +287,7 @@ scanl (+) 0 [1, 2, 3] = [0, 1, 3, 6]
   | [], a, acc => acc.toListAppend [a]
   | b :: l, a, acc => go l (f a b) (acc.push a)
 
-theorem scanlTR_go_eq : ∀ l, scanlTR.go f l a acc = acc.data ++ scanl f a l
+theorem scanlTR_go_eq : ∀ l, scanlTR.go f l a acc = acc.toList ++ scanl f a l
   | [] => by simp [scanlTR.go, scanl]
   | a :: l => by simp [scanlTR.go, scanl, scanlTR_go_eq l]
 
@@ -538,8 +539,8 @@ theorem sections_eq_nil_of_isEmpty : ∀ {L}, L.any isEmpty → @sections α L =
   cases e : L.any isEmpty <;> simp [sections_eq_nil_of_isEmpty, *]
   clear e; induction L with | nil => rfl | cons l L IH => ?_
   simp [IH, sectionsTR.go]
-  rw [Array.foldl_eq_foldl_data, Array.foldl_data_eq_bind]; rfl
-  intros; apply Array.foldl_data_eq_map
+  rw [Array.foldl_eq_foldl_toList, Array.foldl_toList_eq_bind]; rfl
+  intros; apply Array.foldl_toList_eq_map
 
 /--
 `extractP p l` returns a pair of an element `a` of `l` satisfying the predicate
@@ -576,8 +577,8 @@ def productTR (l₁ : List α) (l₂ : List β) : List (α × β) :=
 
 @[csimp] theorem product_eq_productTR : @product = @productTR := by
   funext α β l₁ l₂; simp [product, productTR]
-  rw [Array.foldl_data_eq_bind]; rfl
-  intros; apply Array.foldl_data_eq_map
+  rw [Array.foldl_toList_eq_bind]; rfl
+  intros; apply Array.foldl_toList_eq_map
 
 /-- `sigma l₁ l₂` is the list of dependent pairs `(a, b)` where `a ∈ l₁` and `b ∈ l₂ a`.
 ```
@@ -592,8 +593,8 @@ def sigmaTR {σ : α → Type _} (l₁ : List α) (l₂ : ∀ a, List (σ a)) :
 
 @[csimp] theorem sigma_eq_sigmaTR : @List.sigma = @sigmaTR := by
   funext α β l₁ l₂; simp [List.sigma, sigmaTR]
-  rw [Array.foldl_data_eq_bind]; rfl
-  intros; apply Array.foldl_data_eq_map
+  rw [Array.foldl_toList_eq_bind]; rfl
+  intros; apply Array.foldl_toList_eq_map
 
 /--
 `ofFn f` with `f : fin n → α` returns the list whose ith element is `f i`
@@ -706,23 +707,6 @@ Defined as `pwFilter (≠)`.
     eraseDup [1, 0, 2, 2, 1] = [0, 2, 1] -/
 @[inline] def eraseDup [BEq α] : List α → List α := pwFilter (· != ·)
 
-/--
-`ilast' x xs` returns the last element of `xs` if `xs` is non-empty; it returns `x` otherwise.
-Use `List.getLastD` instead.
--/
-@[simp, deprecated getLastD (since := "2024-01-09")] def ilast' {α} : α → List α → α
-  | a, [] => a
-  | _, b :: l => ilast' b l
-
-/--
-`last' xs` returns the last element of `xs` if `xs` is non-empty; it returns `none` otherwise.
-Use `List.getLast?` instead
--/
-@[simp, deprecated getLast? (since := "2024-01-09")] def last' {α} : List α → Option α
-  | [] => none
-  | [a] => some a
-  | _ :: l => last' l
-
 /--
 `rotate l n` rotates the elements of `l` to the left by `n`
 ```
@@ -803,8 +787,8 @@ theorem dropSlice_zero₂ : ∀ n l, @dropSlice α n 0 l = l
   funext α n m l; simp [dropSliceTR]
   split; { rw [dropSlice_zero₂] }
   rename_i m
-  let rec go (acc) : ∀ xs n, l = acc.data ++ xs →
-    dropSliceTR.go l m xs n acc = acc.data ++ xs.dropSlice n (m+1)
+  let rec go (acc) : ∀ xs n, l = acc.toList ++ xs →
+    dropSliceTR.go l m xs n acc = acc.toList ++ xs.dropSlice n (m+1)
   | [],    n
   | _::xs, 0 => fun h => by simp [dropSliceTR.go, dropSlice, h]
   | x::xs, n+1 => by simp [dropSliceTR.go, dropSlice]; intro h; rw [go _ xs]; {simp}; simp [h]
@@ -839,7 +823,7 @@ zipWithLeft' prod.mk [1] ['a', 'b'] = ([(1, some 'a')], ['b'])
   let rec go (acc) : ∀ as bs, zipWithLeft'TR.go f as bs acc =
       let (l, r) := as.zipWithLeft' f bs; (acc.toList ++ l, r)
   | [], bs => by simp [zipWithLeft'TR.go]
-  | _::_, [] => by simp [zipWithLeft'TR.go, Array.foldl_data_eq_map]
+  | _::_, [] => by simp [zipWithLeft'TR.go, Array.foldl_toList_eq_map]
   | a::as, b::bs => by simp [zipWithLeft'TR.go, go _ as bs]
   simp [zipWithLeft'TR, go]
 
@@ -908,7 +892,7 @@ zipWithLeft f as bs = (zipWithLeft' f as bs).fst
   funext α β γ f as bs; simp [zipWithLeftTR]
   let rec go (acc) : ∀ as bs, zipWithLeftTR.go f as bs acc = acc.toList ++ as.zipWithLeft f bs
   | [], bs => by simp [zipWithLeftTR.go]
-  | _::_, [] => by simp [zipWithLeftTR.go, Array.foldl_data_eq_map]
+  | _::_, [] => by simp [zipWithLeftTR.go, Array.foldl_toList_eq_map]
   | a::as, b::bs => by simp [zipWithLeftTR.go, go _ as bs]
   simp [zipWithLeftTR, go]
 
@@ -984,7 +968,7 @@ fillNones [none, some 1, none, none] [2, 3] = [2, 1, 3]
 
 @[csimp] theorem fillNones_eq_fillNonesTR : @fillNones = @fillNonesTR := by
   funext α as as'; simp [fillNonesTR]
-  let rec go (acc) : ∀ as as', @fillNonesTR.go α as as' acc = acc.data ++ as.fillNones as'
+  let rec go (acc) : ∀ as as', @fillNonesTR.go α as as' acc = acc.toList ++ as.fillNones as'
   | [], _ => by simp [fillNonesTR.go]
   | some a :: as, as' => by simp [fillNonesTR.go, go _ as as']
   | none :: as, [] => by simp [fillNonesTR.go, reduceOption, filterMap_eq_filterMapTR.go]
diff --git a/Batteries/Data/List/Count.lean b/Batteries/Data/List/Count.lean
index 036a76b4b8..151169f74b 100644
--- a/Batteries/Data/List/Count.lean
+++ b/Batteries/Data/List/Count.lean
@@ -29,11 +29,3 @@ variable [DecidableEq α]
 theorem count_singleton' (a b : α) : count a [b] = if b = a then 1 else 0 := by simp [count_cons]
 
 theorem count_concat (a : α) (l : List α) : count a (concat l a) = succ (count a l) := by simp
-
-@[deprecated filter_eq (since := "2023-12-14")]
-theorem filter_eq' (l : List α) (a : α) : l.filter (a = ·) = replicate (count a l) a := by
-  simpa only [eq_comm] using filter_eq l a
-
-@[deprecated filter_beq (since := "2023-12-14")]
-theorem filter_beq' (l : List α) (a : α) : l.filter (a == ·) = replicate (count a l) a := by
-  simpa only [eq_comm (b := a)] using filter_eq l a
diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
index 925cdb0e5f..5ce00e2a17 100644
--- a/Batteries/Data/List/Lemmas.lean
+++ b/Batteries/Data/List/Lemmas.lean
@@ -196,8 +196,8 @@ theorem get?_set_of_lt' (a : α) {m n} (l : List α) (h : m < length l) :
 
 @[simp] theorem extractP_eq_find?_eraseP
     (l : List α) : extractP p l = (find? p l, eraseP p l) := by
-  let rec go (acc) : ∀ xs, l = acc.data ++ xs →
-    extractP.go p l xs acc = (xs.find? p, acc.data ++ xs.eraseP p)
+  let rec go (acc) : ∀ xs, l = acc.toList ++ xs →
+    extractP.go p l xs acc = (xs.find? p, acc.toList ++ xs.eraseP p)
   | [] => fun h => by simp [extractP.go, find?, eraseP, h]
   | x::xs => by
     simp [extractP.go, find?, eraseP]; cases p x <;> simp
@@ -593,19 +593,19 @@ theorem insertP_loop (a : α) (l r : List α) :
 /-! ### merge -/
 
 theorem cons_merge_cons (s : α → α → Bool) (a b l r) :
-    merge s (a::l) (b::r) = if s a b then a :: merge s l (b::r) else b :: merge s (a::l) r := by
+    merge (a::l) (b::r) s = if s a b then a :: merge l (b::r) s else b :: merge (a::l) r s := by
   simp only [merge]
 
 @[simp] theorem cons_merge_cons_pos (s : α → α → Bool) (l r) (h : s a b) :
-    merge s (a::l) (b::r) = a :: merge s l (b::r) := by
+    merge (a::l) (b::r) s = a :: merge l (b::r) s := by
   rw [cons_merge_cons, if_pos h]
 
 @[simp] theorem cons_merge_cons_neg (s : α → α → Bool) (l r) (h : ¬ s a b) :
-    merge s (a::l) (b::r) = b :: merge s (a::l) r := by
+    merge (a::l) (b::r) s = b :: merge (a::l) r s := by
   rw [cons_merge_cons, if_neg h]
 
 @[simp] theorem length_merge (s : α → α → Bool) (l r) :
-    (merge s l r).length = l.length + r.length := by
+    (merge l r s).length = l.length + r.length := by
   match l, r with
   | [], r => simp
   | l, [] => simp
@@ -615,10 +615,10 @@ theorem cons_merge_cons (s : α → α → Bool) (a b l r) :
     · simp_arith [length_merge s l (b::r)]
     · simp_arith [length_merge s (a::l) r]
 
-theorem mem_merge_left (s : α → α → Bool) (h : x ∈ l) : x ∈ merge s l r :=
+theorem mem_merge_left (s : α → α → Bool) (h : x ∈ l) : x ∈ merge l r s :=
   mem_merge.2 <| .inl h
 
-theorem mem_merge_right (s : α → α → Bool) (h : x ∈ r) : x ∈ merge s l r :=
+theorem mem_merge_right (s : α → α → Bool) (h : x ∈ r) : x ∈ merge l r s :=
   mem_merge.2 <| .inr h
 
 /-! ### foldlM and foldrM -/
diff --git a/Batteries/Data/List/Pairwise.lean b/Batteries/Data/List/Pairwise.lean
index 9df947bf4c..de13a5e292 100644
--- a/Batteries/Data/List/Pairwise.lean
+++ b/Batteries/Data/List/Pairwise.lean
@@ -29,18 +29,6 @@ namespace List
 
 /-! ### Pairwise -/
 
-@[deprecated pairwise_iff_forall_sublist (since := "2023-09-18")]
-theorem pairwise_of_reflexive_on_dupl_of_forall_ne [DecidableEq α] {l : List α} {r : α → α → Prop}
-    (hr : ∀ a, 1 < count a l → r a a) (h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b) : l.Pairwise r := by
-  apply pairwise_iff_forall_sublist.mpr
-  intro a b hab
-  if heq : a = b then
-    cases heq; apply hr
-    rwa [show [a,a] = replicate 2 a from rfl, ← le_count_iff_replicate_sublist] at hab
-  else
-    apply h <;> try (apply hab.subset; simp)
-    exact heq
-
 theorem pairwise_iff_get : Pairwise R l ↔ ∀ (i j) (_hij : i < j), R (get l i) (get l j) := by
   rw [pairwise_iff_getElem]
   constructor <;> intro h
diff --git a/Batteries/Data/List/Perm.lean b/Batteries/Data/List/Perm.lean
index 42c4bbc9c2..d924ebf4dd 100644
--- a/Batteries/Data/List/Perm.lean
+++ b/Batteries/Data/List/Perm.lean
@@ -235,8 +235,8 @@ theorem subperm_append_diff_self_of_count_le {l₁ l₂ : List α}
   | nil => simp
   | cons hd tl IH =>
     have : hd ∈ l₂ := by
-      rw [← count_pos_iff_mem]
-      exact Nat.lt_of_lt_of_le (count_pos_iff_mem.mpr (.head _)) (h hd (.head _))
+      rw [← count_pos_iff]
+      exact Nat.lt_of_lt_of_le (count_pos_iff.mpr (.head _)) (h hd (.head _))
     have := perm_cons_erase this
     refine Perm.trans ?_ this.symm
     rw [cons_append, diff_cons, perm_cons]
@@ -325,7 +325,7 @@ theorem perm_insertP (p : α → Bool) (a l) : insertP p a l ~ a :: l := by
 theorem Perm.insertP (p : α → Bool) (a) (h : l₁ ~ l₂) : insertP p a l₁ ~ insertP p a l₂ :=
   Perm.trans (perm_insertP ..) <| Perm.trans (Perm.cons _ h) <| Perm.symm (perm_insertP ..)
 
-theorem perm_merge (s : α → α → Bool) (l r) : merge s l r ~ l ++ r := by
+theorem perm_merge (s : α → α → Bool) (l r) : merge l r s ~ l ++ r := by
   match l, r with
   | [], r => simp
   | l, [] => simp
@@ -342,5 +342,5 @@ theorem perm_merge (s : α → α → Bool) (l r) : merge s l r ~ l ++ r := by
       exact Perm.rfl
 
 theorem Perm.merge (s₁ s₂ : α → α → Bool) (hl : l₁ ~ l₂) (hr : r₁ ~ r₂) :
-    merge s₁ l₁ r₁ ~ merge s₂ l₂ r₂ :=
+    merge l₁ r₁ s₁ ~ merge l₂ r₂ s₂ :=
   Perm.trans (perm_merge ..) <| Perm.trans (Perm.append hl hr) <| Perm.symm (perm_merge ..)
diff --git a/Batteries/Data/Nat/Lemmas.lean b/Batteries/Data/Nat/Lemmas.lean
index 3492037135..7fa93705f7 100644
--- a/Batteries/Data/Nat/Lemmas.lean
+++ b/Batteries/Data/Nat/Lemmas.lean
@@ -149,24 +149,6 @@ protected def sum_trichotomy (a b : Nat) : a < b ⊕' a = b ⊕' b < a :=
   | .eq => .inr (.inl (Nat.compare_eq_eq.1 h))
   | .gt => .inr (.inr (Nat.compare_eq_gt.1 h))
 
-/-! ## add -/
-
-@[deprecated (since := "2023-11-25")] alias succ_add_eq_succ_add := Nat.succ_add_eq_add_succ
-
-/-! ## sub -/
-
-@[deprecated (since := "2023-11-25")]
-protected alias le_of_le_of_sub_le_sub_right := Nat.le_of_sub_le_sub_right
-
-@[deprecated (since := "2023-11-25")]
-protected alias le_of_le_of_sub_le_sub_left := Nat.le_of_sub_le_sub_left
-
-/-! ### mul -/
-
-@[deprecated (since := "2024-01-11")] protected alias mul_lt_mul := Nat.mul_lt_mul_of_lt_of_le'
-
-@[deprecated (since := "2024-01-11")] protected alias mul_lt_mul' := Nat.mul_lt_mul_of_le_of_lt
-
 /-! ### div/mod -/
 
 -- TODO mod_core_congr, mod_def
@@ -179,6 +161,3 @@ protected alias le_of_le_of_sub_le_sub_left := Nat.le_of_sub_le_sub_left
 
 @[simp] theorem sum_append : Nat.sum (l₁ ++ l₂) = Nat.sum l₁ + Nat.sum l₂ := by
   induction l₁ <;> simp [*, Nat.add_assoc]
-
-@[deprecated (since := "2024-03-05")] protected alias lt_connex := Nat.lt_or_gt_of_ne
-@[deprecated (since := "2024-02-09")] alias pow_two_pos := Nat.two_pow_pos
diff --git a/Batteries/Data/Option.lean b/Batteries/Data/Option.lean
deleted file mode 100644
index e99c38ee11..0000000000
--- a/Batteries/Data/Option.lean
+++ /dev/null
@@ -1 +0,0 @@
-import Batteries.Data.Option.Lemmas
diff --git a/Batteries/Data/Option/Lemmas.lean b/Batteries/Data/Option/Lemmas.lean
deleted file mode 100644
index 05a38b25a7..0000000000
--- a/Batteries/Data/Option/Lemmas.lean
+++ /dev/null
@@ -1,13 +0,0 @@
-/-
-Copyright (c) 2017 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro
--/
-import Batteries.Tactic.Alias
-
-namespace Option
-
-@[deprecated (since := "2024-03-05")] alias to_list_some := toList_some
-@[deprecated (since := "2024-03-05")] alias to_list_none := toList_none
-
-end Option
diff --git a/Batteries/Data/Rat/Basic.lean b/Batteries/Data/Rat/Basic.lean
index f96651d34c..2032b23ecd 100644
--- a/Batteries/Data/Rat/Basic.lean
+++ b/Batteries/Data/Rat/Basic.lean
@@ -45,23 +45,23 @@ Auxiliary definition for `Rat.normalize`. Constructs `num / den` as a rational n
 dividing both `num` and `den` by `g` (which is the gcd of the two) if it is not 1.
 -/
 @[inline] def Rat.maybeNormalize (num : Int) (den g : Nat)
-    (den_nz : den / g ≠ 0) (reduced : (num.div g).natAbs.Coprime (den / g)) : Rat :=
+    (den_nz : den / g ≠ 0) (reduced : (num.tdiv g).natAbs.Coprime (den / g)) : Rat :=
   if hg : g = 1 then
     { num, den
       den_nz := by simp [hg] at den_nz; exact den_nz
       reduced := by simp [hg, Int.natAbs_ofNat] at reduced; exact reduced }
-  else { num := num.div g, den := den / g, den_nz, reduced }
+  else { num := num.tdiv g, den := den / g, den_nz, reduced }
 
 theorem Rat.normalize.den_nz {num : Int} {den g : Nat} (den_nz : den ≠ 0)
     (e : g = num.natAbs.gcd den) : den / g ≠ 0 :=
   e ▸ Nat.ne_of_gt (Nat.div_gcd_pos_of_pos_right _ (Nat.pos_of_ne_zero den_nz))
 
 theorem Rat.normalize.reduced {num : Int} {den g : Nat} (den_nz : den ≠ 0)
-    (e : g = num.natAbs.gcd den) : (num.div g).natAbs.Coprime (den / g) :=
-  have : Int.natAbs (num.div ↑g) = num.natAbs / g := by
+    (e : g = num.natAbs.gcd den) : (num.tdiv g).natAbs.Coprime (den / g) :=
+  have : Int.natAbs (num.tdiv ↑g) = num.natAbs / g := by
     match num, num.eq_nat_or_neg with
     | _, ⟨_, .inl rfl⟩ => rfl
-    | _, ⟨_, .inr rfl⟩ => rw [Int.neg_div, Int.natAbs_neg, Int.natAbs_neg]; rfl
+    | _, ⟨_, .inr rfl⟩ => rw [Int.neg_tdiv, Int.natAbs_neg, Int.natAbs_neg]; rfl
   this ▸ e ▸ Nat.coprime_div_gcd_div_gcd (Nat.gcd_pos_of_pos_right _ (Nat.pos_of_ne_zero den_nz))
 
 /--
@@ -141,12 +141,12 @@ want to unfold it. Use `Rat.mul_def` instead.) -/
 @[irreducible] protected def mul (a b : Rat) : Rat :=
   let g1 := Nat.gcd a.num.natAbs b.den
   let g2 := Nat.gcd b.num.natAbs a.den
-  { num := (a.num.div g1) * (b.num.div g2)
+  { num := (a.num.tdiv g1) * (b.num.tdiv g2)
     den := (a.den / g2) * (b.den / g1)
     den_nz := Nat.ne_of_gt <| Nat.mul_pos
       (Nat.div_gcd_pos_of_pos_right _ a.den_pos) (Nat.div_gcd_pos_of_pos_right _ b.den_pos)
     reduced := by
-      simp only [Int.natAbs_mul, Int.natAbs_div, Nat.coprime_mul_iff_left]
+      simp only [Int.natAbs_mul, Int.natAbs_tdiv, Nat.coprime_mul_iff_left]
       refine ⟨Nat.coprime_mul_iff_right.2 ⟨?_, ?_⟩, Nat.coprime_mul_iff_right.2 ⟨?_, ?_⟩⟩
       · exact a.reduced.coprime_div_left (Nat.gcd_dvd_left ..)
           |>.coprime_div_right (Nat.gcd_dvd_right ..)
diff --git a/Batteries/Data/Rat/Lemmas.lean b/Batteries/Data/Rat/Lemmas.lean
index 77b911ec94..b3c2d49915 100644
--- a/Batteries/Data/Rat/Lemmas.lean
+++ b/Batteries/Data/Rat/Lemmas.lean
@@ -23,14 +23,14 @@ theorem ext : {p q : Rat} → p.num = q.num → p.den = q.den → p = q
 
 @[simp] theorem maybeNormalize_eq {num den g} (den_nz reduced) :
     maybeNormalize num den g den_nz reduced =
-    { num := num.div g, den := den / g, den_nz, reduced } := by
+    { num := num.tdiv g, den := den / g, den_nz, reduced } := by
   unfold maybeNormalize; split
   · subst g; simp
   · rfl
 
 theorem normalize.reduced' {num : Int} {den g : Nat} (den_nz : den ≠ 0)
     (e : g = num.natAbs.gcd den) : (num / g).natAbs.Coprime (den / g) := by
-  rw [← Int.div_eq_ediv_of_dvd (e ▸ Int.ofNat_dvd_left.2 (Nat.gcd_dvd_left ..))]
+  rw [← Int.tdiv_eq_ediv_of_dvd (e ▸ Int.ofNat_dvd_left.2 (Nat.gcd_dvd_left ..))]
   exact normalize.reduced den_nz e
 
 theorem normalize_eq {num den} (den_nz) : normalize num den den_nz =
@@ -39,10 +39,10 @@ theorem normalize_eq {num den} (den_nz) : normalize num den den_nz =
       den_nz := normalize.den_nz den_nz rfl
       reduced := normalize.reduced' den_nz rfl } := by
   simp only [normalize, maybeNormalize_eq,
-    Int.div_eq_ediv_of_dvd (Int.ofNat_dvd_left.2 (Nat.gcd_dvd_left ..))]
+    Int.tdiv_eq_ediv_of_dvd (Int.ofNat_dvd_left.2 (Nat.gcd_dvd_left ..))]
 
 @[simp] theorem normalize_zero (nz) : normalize 0 d nz = 0 := by
-  simp [normalize, Int.zero_div, Int.natAbs_zero, Nat.div_self (Nat.pos_of_ne_zero nz)]; rfl
+  simp [normalize, Int.zero_tdiv, Int.natAbs_zero, Nat.div_self (Nat.pos_of_ne_zero nz)]; rfl
 
 theorem mk_eq_normalize (num den nz c) : ⟨num, den, nz, c⟩ = normalize num den nz := by
   simp [normalize_eq, c.gcd_eq_one]
@@ -76,7 +76,7 @@ theorem normalize_eq_iff (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :
 theorem maybeNormalize_eq_normalize {num : Int} {den g : Nat} (den_nz reduced)
     (hn : ↑g ∣ num) (hd : g ∣ den) :
     maybeNormalize num den g den_nz reduced = normalize num den (mt (by simp [·]) den_nz) := by
-  simp only [maybeNormalize_eq, mk_eq_normalize, Int.div_eq_ediv_of_dvd hn]
+  simp only [maybeNormalize_eq, mk_eq_normalize, Int.tdiv_eq_ediv_of_dvd hn]
   have : g ≠ 0 := mt (by simp [·]) den_nz
   rw [← normalize_mul_right _ this, Int.ediv_mul_cancel hn]
   congr 1; exact Nat.div_mul_cancel hd
@@ -267,9 +267,9 @@ theorem mul_def (a b : Rat) :
   have H1 : a.num.natAbs.gcd b.den ≠ 0 := Nat.gcd_ne_zero_right b.den_nz
   have H2 : b.num.natAbs.gcd a.den ≠ 0 := Nat.gcd_ne_zero_right a.den_nz
   rw [mk_eq_normalize, ← normalize_mul_right _ (Nat.mul_ne_zero H1 H2)]; congr 1
-  · rw [Int.ofNat_mul, ← Int.mul_assoc, Int.mul_right_comm (Int.div ..),
-      Int.div_mul_cancel (Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left ..), Int.mul_assoc,
-      Int.div_mul_cancel (Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left ..)]
+  · rw [Int.ofNat_mul, ← Int.mul_assoc, Int.mul_right_comm (Int.tdiv ..),
+      Int.tdiv_mul_cancel (Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left ..), Int.mul_assoc,
+      Int.tdiv_mul_cancel (Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left ..)]
   · rw [← Nat.mul_assoc, Nat.mul_right_comm, Nat.mul_right_comm (_/_),
       Nat.div_mul_cancel (Nat.gcd_dvd_right ..), Nat.mul_assoc,
       Nat.div_mul_cancel (Nat.gcd_dvd_right ..)]
diff --git a/Batteries/Data/UnionFind/Basic.lean b/Batteries/Data/UnionFind/Basic.lean
index 549c9e1cde..ca2843db5f 100644
--- a/Batteries/Data/UnionFind/Basic.lean
+++ b/Batteries/Data/UnionFind/Basic.lean
@@ -128,7 +128,7 @@ abbrev parent (self : UnionFind) (i : Nat) : Nat := parentD self.arr i
 
 theorem parent'_lt (self : UnionFind) (i : Fin self.size) :
     (self.arr.get i).parent < self.size := by
-  simp only [← parentD_eq, parentD_lt, Fin.is_lt, Array.data_length]
+  simp only [← parentD_eq, parentD_lt, Fin.is_lt, Array.toList_length]
 
 theorem parent_lt (self : UnionFind) (i : Nat) : self.parent i < self.size ↔ i < self.size := by
   simp only [parentD]; split <;> simp only [*, parent'_lt]
@@ -151,8 +151,8 @@ theorem rank'_lt_rankMax (self : UnionFind) (i : Fin self.size) :
   let rec go : ∀ {l} {x : UFNode}, x ∈ l → x.rank ≤ List.foldr (max ·.rank) 0 l
     | a::l, _, List.Mem.head _ => by dsimp; apply Nat.le_max_left
     | a::l, _, .tail _ h => by dsimp; exact Nat.le_trans (go h) (Nat.le_max_right ..)
-  simp only [Array.get_eq_getElem, rankMax, Array.foldr_eq_foldr_data]
-  exact Nat.lt_succ.2 <| go (self.arr.data.get_mem i.1 i.2)
+  simp only [Array.get_eq_getElem, rankMax, Array.foldr_eq_foldr_toList]
+  exact Nat.lt_succ.2 <| go (self.arr.toList.get_mem i.1 i.2)
 
 theorem rankD_lt_rankMax (self : UnionFind) (i : Nat) :
     rankD self.arr i < self.rankMax := by
@@ -217,7 +217,7 @@ theorem parent_rootD (self : UnionFind) (x : Nat) :
 
 @[nolint unusedHavesSuffices]
 theorem rootD_parent (self : UnionFind) (x : Nat) : self.rootD (self.parent x) = self.rootD x := by
-  simp only [rootD, Array.data_length, parent_lt]
+  simp only [rootD, Array.toList_length, parent_lt]
   split
   · simp only [parentD, ↓reduceDIte, *]
     (conv => rhs; rw [root]); split
@@ -226,7 +226,7 @@ theorem rootD_parent (self : UnionFind) (x : Nat) : self.rootD (self.parent x) =
   · simp only [not_false_eq_true, parentD_of_not_lt, *]
 
 theorem rootD_lt {self : UnionFind} {x : Nat} : self.rootD x < self.size ↔ x < self.size := by
-  simp only [rootD, Array.data_length]; split <;> simp [*]
+  simp only [rootD, Array.toList_length]; split <;> simp [*]
 
 @[nolint unusedHavesSuffices]
 theorem rootD_eq_self {self : UnionFind} {x : Nat} : self.rootD x = x ↔ self.parent x = x := by
@@ -284,7 +284,7 @@ termination_by self.rankMax - self.rank x
 theorem findAux_root {self : UnionFind} {x : Fin self.size} :
     (findAux self x).root = self.root x := by
   rw [findAux, root]
-  simp only [Array.data_length, Array.get_eq_getElem, dite_eq_ite]
+  simp only [Array.toList_length, Array.get_eq_getElem, dite_eq_ite]
   split <;> simp only
   have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
   exact findAux_root
@@ -298,7 +298,7 @@ theorem findAux_s {self : UnionFind} {x : Fin self.size} :
   rw [show self.rootD _ = (self.findAux ⟨_, self.parent'_lt x⟩).root from _]
   · rw [findAux]; split <;> rfl
   · rw [← rootD_parent, parent, parentD_eq]
-    simp only [rootD, Array.get_eq_getElem, Array.data_length, findAux_root]
+    simp only [rootD, Array.get_eq_getElem, Array.toList_length, findAux_root]
     apply dif_pos
     exact parent'_lt ..
 
@@ -364,7 +364,7 @@ theorem parentD_findAux_or (self : UnionFind) (x : Fin self.size) (i) :
     · simp [*]
     · have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
       exact (parentD_findAux_or self ⟨_, self.parent'_lt x⟩ i).imp_left <| .imp_right fun h => by
-        simp only [h, ← parentD_eq, rootD_parent, Array.data_length]
+        simp only [h, ← parentD_eq, rootD_parent, Array.toList_length]
 termination_by self.rankMax - self.rank x
 
 theorem lt_rankD_findAux {self : UnionFind} {x : Fin self.size} :
@@ -386,7 +386,7 @@ def find (self : UnionFind) (x : Fin self.size) :
   { 1.arr := r.s
     2.1.val := r.root
     1.parentD_lt := fun h => by
-      simp only [Array.data_length, FindAux.size_eq] at *
+      simp only [Array.toList_length, FindAux.size_eq] at *
       exact parentD_findAux_lt h
     1.rankD_lt := fun h => by rw [rankD_findAux, rankD_findAux]; exact lt_rankD_findAux h
     2.1.isLt := show _ < r.s.size by rw [r.size_eq]; exact r.root.2
@@ -420,7 +420,7 @@ def findD (self : UnionFind) (x : Nat) : UnionFind × Nat :=
 
 @[simp] theorem find_parent_1 (self : UnionFind) (x : Fin self.size) :
     (self.find x).1.parent x = self.rootD x := by
-  simp only [parent, Array.data_length, find]
+  simp only [parent, Array.toList_length, find]
   rw [parentD_findAux, if_pos rfl]
 
 theorem find_parent_or (self : UnionFind) (x : Fin self.size) (i) :
@@ -500,7 +500,7 @@ theorem setParent_rankD_lt {arr : Array UFNode} {x y : Fin arr.size}
 def link (self : UnionFind) (x y : Fin self.size) (yroot : self.parent y = y) : UnionFind where
   arr := linkAux self.arr x y
   parentD_lt h := by
-    simp only [Array.data_length, linkAux_size] at *
+    simp only [Array.toList_length, linkAux_size] at *
     simp only [linkAux, Array.get_eq_getElem]
     split <;> [skip; split <;> [skip; split]]
     · exact self.parentD_lt h
@@ -522,7 +522,7 @@ def link (self : UnionFind) (x y : Fin self.size) (yroot : self.parent y = y) :
       simp only [rankD_set, Fin.eta, Array.get_eq_getElem]
       split
       · simp_all
-      · simp_all only [Array.get_eq_getElem, Array.data_length, Nat.lt_irrefl, not_false_eq_true,
+      · simp_all only [Array.get_eq_getElem, Array.toList_length, Nat.lt_irrefl, not_false_eq_true,
           and_true, ite_false, ite_eq_right_iff]
         rintro rfl
         simp [rankD_eq, *]
diff --git a/scripts/check_imports.lean b/scripts/check_imports.lean
index 55bf0e8342..bc651dcc12 100644
--- a/scripts/check_imports.lean
+++ b/scripts/check_imports.lean
@@ -34,7 +34,7 @@ def warn (fixable : Bool) (msg : String) : LogIO Unit := do
 -- | Predicate indicates if warnings are present and if they fixable.
 def getWarningInfo : LogIO (Bool × Bool) :=  get
 
-def createModuleHashmap (env : Environment) : HashMap Name ModuleData := Id.run do
+def createModuleHashmap (env : Environment) : Std.HashMap Name ModuleData := Id.run do
   let mut nameMap := {}
   for i in [0:env.header.moduleNames.size] do
     let nm := env.header.moduleNames[i]!
@@ -80,11 +80,11 @@ def checkMissingImports (modName : Name) (modData : ModuleData) (reqImports : Ar
 
 /-- Check directory entry in `Batteries/Data/` -/
 def checkBatteriesDataDir
-    (modMap : HashMap Name ModuleData)
+    (modMap : Std.HashMap Name ModuleData)
     (entry : IO.FS.DirEntry) (autofix : Bool := false) : LogIO Unit := do
   let moduleName := `Batteries.Data ++ .mkSimple entry.fileName
   let requiredImports ← addModulesIn (recurse := true) #[] (root := moduleName) entry.path
-  let .some module := modMap.find? moduleName
+  let .some module := modMap[moduleName]?
     | warn true s!"Could not find {moduleName}; Not imported into Batteries."
       let path := modulePath moduleName
       -- We refuse to generate imported modules whose path doesn't exist.
@@ -134,7 +134,7 @@ def checkBatteriesDataImports : MetaM Unit := do
       if ← entry.path.isDir then
         checkBatteriesDataDir (autofix := autofix) modMap entry
     let batteriesImports ← expectedBatteriesImports
-    let .some batteriesMod := modMap.find? `Batteries
+    let .some batteriesMod := modMap[`Batteries]?
         | warn false "Missing Batteries module!; Run `lake build`."
     let warned ← checkMissingImports `Batteries batteriesMod batteriesImports
     if autofix && warned then