diff --git a/Batteries.lean b/Batteries.lean
index 3bd1f4ef79..f04a7a1f76 100644
--- a/Batteries.lean
+++ b/Batteries.lean
@@ -45,9 +45,7 @@ import Batteries.Lean.HashMap
 import Batteries.Lean.HashSet
 import Batteries.Lean.IO.Process
 import Batteries.Lean.Json
-import Batteries.Lean.Meta.AssertHypotheses
 import Batteries.Lean.Meta.Basic
-import Batteries.Lean.Meta.Clear
 import Batteries.Lean.Meta.DiscrTree
 import Batteries.Lean.Meta.Expr
 import Batteries.Lean.Meta.Inaccessible
diff --git a/Batteries/Classes/SatisfiesM.lean b/Batteries/Classes/SatisfiesM.lean
index 55ded469fc..89f264963a 100644
--- a/Batteries/Classes/SatisfiesM.lean
+++ b/Batteries/Classes/SatisfiesM.lean
@@ -171,7 +171,7 @@ theorem SatisfiesM_StateRefT_eq [Monad m] :
   · refine ⟨fun s => (fun ⟨⟨a, h⟩, s'⟩ => ⟨⟨a, s'⟩, h⟩) <$> f s, fun s => ?_⟩
     rw [← comp_map, map_eq_pure_bind]; rfl
   · refine ⟨fun s => (fun ⟨⟨a, s'⟩, h⟩ => ⟨⟨a, h⟩, s'⟩) <$> f s, funext fun s => ?_⟩
-    show _ >>= _ = _; simp [map_eq_pure_bind, ← h]
+    show _ >>= _ = _; simp [← h]
 
 @[simp] theorem SatisfiesM_ExceptT_eq [Monad m] [LawfulMonad m] :
     SatisfiesM (m := ExceptT ρ m) (α := α) p x ↔ SatisfiesM (m := m) (∀ a, · = .ok a → p a) x := by
@@ -179,4 +179,4 @@ theorem SatisfiesM_StateRefT_eq [Monad m] :
   · exists (fun | .ok ⟨a, h⟩ => ⟨.ok a, fun | _, rfl => h⟩ | .error e => ⟨.error e, nofun⟩) <$> f
     show _ = _ >>= _; rw [← comp_map, map_eq_pure_bind]; congr; funext a; cases a <;> rfl
   · exists ((fun | ⟨.ok a, h⟩ => .ok ⟨a, h _ rfl⟩ | ⟨.error e, _⟩ => .error e) <$> f : m _)
-    show _ >>= _ = _; simp [← comp_map, map_eq_pure_bind]; congr; funext ⟨a, h⟩; cases a <;> rfl
+    show _ >>= _ = _; simp [← comp_map, ← bind_pure_comp]; congr; funext ⟨a, h⟩; cases a <;> rfl
diff --git a/Batteries/Data/Array/Basic.lean b/Batteries/Data/Array/Basic.lean
index f25b5e091b..7fb0cf8cf8 100644
--- a/Batteries/Data/Array/Basic.lean
+++ b/Batteries/Data/Array/Basic.lean
@@ -27,13 +27,6 @@ arrays, remove duplicates and then compare them elementwise.
 def equalSet [BEq α] (xs ys : Array α) : Bool :=
   xs.all (ys.contains ·) && ys.all (xs.contains ·)
 
-set_option linter.unusedVariables.funArgs false in
-/--
-Sort an array using `compare` to compare elements.
--/
-def qsortOrd [ord : Ord α] (xs : Array α) : Array α :=
-  xs.qsort fun x y => compare x y |>.isLT
-
 set_option linter.unusedVariables.funArgs false in
 /--
 Returns the first minimal element among `d` and elements of the array.
@@ -184,22 +177,6 @@ end Array
 
 namespace Subarray
 
-/--
-The empty subarray.
--/
-protected def empty : Subarray α where
-  array := #[]
-  start := 0
-  stop := 0
-  start_le_stop := Nat.le_refl 0
-  stop_le_array_size := Nat.le_refl 0
-
-instance : EmptyCollection (Subarray α) :=
-  ⟨Subarray.empty⟩
-
-instance : Inhabited (Subarray α) :=
-  ⟨{}⟩
-
 /--
 Check whether a subarray is empty.
 -/
diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
index d384a334ab..3f28087212 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_getElem_toList,
+        getElem_eq_getElem_toList]
+      show List.zipWith f (as.toList[i_as] :: List.drop (i_as + 1) as.toList)
+        ((List.get bs.toList i_bs) :: List.drop (i_bs + 1) bs.toList) =
+        List.zipWith f (List.drop i as.toList) (List.drop i bs.toList)
+      simp only [length_toList, Fin.getElem_fin, List.getElem_cons_drop, List.get_eq_getElem]
   simp [zipWith, loop 0 #[] (by simp) (by simp)]
+@[deprecated (since := "2024-09-09")] alias data_zipWith := toList_zipWith
 @[deprecated (since := "2024-08-13")] alias zipWith_eq_zipWith_data := data_zipWith
 
 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,42 +96,43 @@ 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 [← length_toList, toList_filter]
   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₂⟩⟩
 
 /-! ### indexOf? -/
 
-theorem indexOf?_data [BEq α] {a : α} {l : Array α} :
-    l.data.indexOf? a = (l.indexOf? a).map Fin.val := by
+theorem indexOf?_toList [BEq α] {a : α} {l : Array α} :
+    l.toList.indexOf? a = (l.indexOf? a).map Fin.val := by
   simpa using aux l 0
 where
   aux (l : Array α) (i : Nat) :
-       ((l.data.drop i).indexOf? a).map (·+i) = (indexOfAux l a i).map Fin.val := by
+       ((l.toList.drop i).indexOf? a).map (·+i) = (indexOfAux l a i).map Fin.val := by
     rw [indexOfAux]
     if h : i < l.size then
-      rw [List.drop_eq_getElem_cons h, ←getElem_eq_data_getElem, List.indexOf?_cons]
+      rw [List.drop_eq_getElem_cons h, ←getElem_eq_getElem_toList, List.indexOf?_cons]
       if h' : l[i] == a then
         simp [h, h']
       else
@@ -137,42 +144,8 @@ where
 
 /-! ### erase -/
 
-theorem eraseIdx_data_swap {l : Array α} (i : Nat) (lt : i + 1 < size l) :
-    (l.swap ⟨i+1, lt⟩ ⟨i, Nat.lt_of_succ_lt lt⟩).data.eraseIdx (i+1) = l.data.eraseIdx i := by
-  let ⟨xs⟩ := l
-  induction i generalizing xs <;> let x₀::x₁::xs := xs
-  case zero => simp [swap, get]
-  case succ i ih _ =>
-    have lt' := Nat.lt_of_succ_lt_succ lt
-    have : (swap ⟨x₀::x₁::xs⟩ ⟨i.succ + 1, lt⟩ ⟨i.succ, Nat.lt_of_succ_lt lt⟩).data
-        = x₀::(swap ⟨x₁::xs⟩ ⟨i + 1, lt'⟩ ⟨i, Nat.lt_of_succ_lt lt'⟩).data := by
-      simp [swap_def, getElem_eq_data_getElem]
-    simp [this, ih]
-
-@[simp] theorem data_feraseIdx {l : Array α} (i : Fin l.size) :
-    (l.feraseIdx i).data = l.data.eraseIdx i := by
-  induction l, i using feraseIdx.induct with
-  | @case1 a i lt a' i' ih =>
-    rw [feraseIdx]
-    simp [lt, ih, a', eraseIdx_data_swap i lt]
-  | case2 a i lt =>
-    have : i + 1 ≥ a.size := Nat.ge_of_not_lt lt
-    have last : i + 1 = a.size := Nat.le_antisymm i.is_lt this
-    simp [feraseIdx, lt, List.dropLast_eq_eraseIdx last]
-
-@[simp] theorem data_erase [BEq α] (l : Array α) (a : α) : (l.erase a).data = l.data.erase a := by
-  match h : indexOf? l a with
-  | none =>
-    simp only [erase, h]
-    apply Eq.symm
-    rw [List.erase_eq_self_iff_forall_bne, ←List.indexOf?_eq_none_iff, indexOf?_data,
-        h, Option.map_none']
-  | some i =>
-    simp only [erase, h]
-    rw [data_feraseIdx, ←List.eraseIdx_indexOf_eq_erase]
-    congr
-    rw [List.indexOf_eq_indexOf?, indexOf?_data]
-    simp [h]
+@[simp] proof_wanted toList_erase [BEq α] {l : Array α} {a : α} :
+    (l.erase a).toList = l.toList.erase a
 
 /-! ### shrink -/
 
@@ -196,12 +169,10 @@ theorem size_set! (a : Array α) (i v) : (a.set! i v).size = a.size := by
 theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by
   rw [mapM, mapM.map]; rfl
 
-@[simp] theorem map_empty (f : α → β) : map f #[] = #[] := mapM_empty ..
+theorem map_empty (f : α → β) : map f #[] = #[] := mapM_empty f
 
 /-! ### mem -/
 
-alias not_mem_empty := not_mem_nil
-
 theorem mem_singleton : a ∈ #[b] ↔ a = b := by simp
 
 /-! ### append -/
@@ -230,7 +201,7 @@ private theorem get_insertAt_loop_lt (as : Array α) (i : Fin (as.size+1)) (j :
   split
   · have h1 : k ≠ j - 1 := by omega
     have h2 : k ≠ j := by omega
-    rw [get_insertAt_loop_lt, get_swap, if_neg h1, if_neg h2]
+    rw [get_insertAt_loop_lt, getElem_swap, if_neg h1, if_neg h2]
     exact h
   · rfl
 
@@ -241,7 +212,7 @@ private theorem get_insertAt_loop_gt (as : Array α) (i : Fin (as.size+1)) (j :
   split
   · have h1 : k ≠ j - 1 := by omega
     have h2 : k ≠ j := by omega
-    rw [get_insertAt_loop_gt, get_swap, if_neg h1, if_neg h2]
+    rw [get_insertAt_loop_gt, getElem_swap, if_neg h1, if_neg h2]
     exact Nat.lt_of_le_of_lt (Nat.pred_le _) hgt
   · rfl
 
@@ -251,8 +222,7 @@ private theorem get_insertAt_loop_eq (as : Array α) (i : Fin (as.size+1)) (j :
   unfold insertAt.loop
   split
   · next h =>
-    rw [get_insertAt_loop_eq, Fin.getElem_fin, get_swap, if_pos rfl]
-    exact Nat.lt_of_le_of_lt (Nat.pred_le _) j.is_lt
+    rw [get_insertAt_loop_eq, Fin.getElem_fin, getElem_swap, if_pos rfl]
     exact heq
     exact Nat.le_pred_of_lt h
   · congr; omega
@@ -266,18 +236,17 @@ private theorem get_insertAt_loop_gt_le (as : Array α) (i : Fin (as.size+1)) (j
     if h0 : k = j then
       cases h0
       have h1 : j.val ≠ j - 1 := by omega
-      rw [get_insertAt_loop_gt, get_swap, if_neg h1, if_pos rfl]; rfl
-      · exact j.is_lt
-      · exact Nat.pred_lt_of_lt hgt
+      rw [get_insertAt_loop_gt, getElem_swap, if_neg h1, if_pos rfl]; rfl
+      exact Nat.pred_lt_of_lt hgt
     else
       have h1 : k - 1 ≠ j - 1 := by omega
       have h2 : k - 1 ≠ j := by omega
-      rw [get_insertAt_loop_gt_le, get_swap, if_neg h1, if_neg h2]
-      exact hgt
+      rw [get_insertAt_loop_gt_le, getElem_swap, if_neg h1, if_neg h2]
       apply Nat.le_of_lt_add_one
       rw [Nat.sub_one_add_one]
       exact Nat.lt_of_le_of_ne hle h0
       exact Nat.not_eq_zero_of_lt h
+      exact hgt
   · next h =>
     absurd h
     exact Nat.lt_of_lt_of_le hgt hle
diff --git a/Batteries/Data/Array/Merge.lean b/Batteries/Data/Array/Merge.lean
index aa83e0200b..4b806a35d6 100644
--- a/Batteries/Data/Array/Merge.lean
+++ b/Batteries/Data/Array/Merge.lean
@@ -31,6 +31,8 @@ set_option linter.unusedVariables false in
 def mergeSortedPreservingDuplicates [ord : Ord α] (xs ys : Array α) : Array α :=
   merge (compare · · |>.isLT) xs ys
 
+-- We name `ord` so it can be provided as a named argument.
+set_option linter.unusedVariables.funArgs false in
 /--
 `O(|xs| + |ys|)`. Merge arrays `xs` and `ys`, which must be sorted according to `compare` and must
 not contain duplicates. Equal elements are merged using `merge`. If `merge` respects the order
@@ -85,6 +87,8 @@ where
 
 @[deprecated (since := "2024-04-24")] alias mergeUnsortedDeduplicating := mergeUnsortedDedup
 
+-- We name `eq` so it can be provided as a named argument.
+set_option linter.unusedVariables.funArgs false in
 /--
 `O(|xs|)`. Replace each run `[x₁, ⋯, xₙ]` of equal elements in `xs` with
 `f ⋯ (f (f x₁ x₂) x₃) ⋯ xₙ`.
diff --git a/Batteries/Data/Array/OfFn.lean b/Batteries/Data/Array/OfFn.lean
index a5d3bc78bc..e02be7cba1 100644
--- a/Batteries/Data/Array/OfFn.lean
+++ b/Batteries/Data/Array/OfFn.lean
@@ -12,12 +12,7 @@ namespace Array
 /-! ### ofFn -/
 
 @[simp]
-theorem data_ofFn (f : Fin n → α) : (ofFn f).data = List.ofFn f := by
-  ext1
-  simp only [getElem?_eq, data_length, size_ofFn, length_ofFn, getElem_ofFn]
-  split
-  · rw [← getElem_eq_data_getElem]
-    simp
-  · rfl
+theorem toList_ofFn (f : Fin n → α) : (ofFn f).toList = List.ofFn f := by
+  apply ext_getElem <;> simp
 
 end Array
diff --git a/Batteries/Data/Array/Pairwise.lean b/Batteries/Data/Array/Pairwise.lean
index 84dff1f680..9e61e642ed 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]
 
 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, length_toList]
 
 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,16 +46,17 @@ 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, toList_append, ← 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
-  simp only [pairwise_iff_getElem, get_extract, size_extract] at h ⊢
+  simp only [pairwise_iff_getElem, getElem_extract, size_extract] at h ⊢
   intro _ _ _ _ hlt
   apply h
   exact Nat.add_lt_add_left hlt start
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/ByteArray.lean b/Batteries/Data/ByteArray.lean
index ae4544fd21..c10cf6ba65 100644
--- a/Batteries/Data/ByteArray.lean
+++ b/Batteries/Data/ByteArray.lean
@@ -85,12 +85,12 @@ theorem size_append (a b : ByteArray) : (a ++ b).size = a.size + b.size := by
 theorem get_append_left {a b : ByteArray} (hlt : i < a.size)
     (h : i < (a ++ b).size := size_append .. ▸ Nat.lt_of_lt_of_le hlt (Nat.le_add_right ..)) :
     (a ++ b)[i] = a[i] := by
-  simp [getElem_eq_data_getElem]; exact Array.get_append_left hlt
+  simp [getElem_eq_data_getElem]; exact Array.getElem_append_left hlt
 
 theorem get_append_right {a b : ByteArray} (hle : a.size ≤ i) (h : i < (a ++ b).size)
     (h' : i - a.size < b.size := Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) :
     (a ++ b)[i] = b[i - a.size] := by
-  simp [getElem_eq_data_getElem]; exact Array.get_append_right hle
+  simp [getElem_eq_data_getElem]; exact Array.getElem_append_right hle
 
 /-! ### extract -/
 
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 5ddde152de..33534b4549 100644
--- a/Batteries/Data/Fin/Lemmas.lean
+++ b/Batteries/Data/Fin/Lemmas.lean
@@ -26,7 +26,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_getElem_toList, getElem_enum, cast_mk]
 
 @[deprecated getElem_list (since := "2024-06-12")]
 theorem get_list (i : Fin (list n).length) : (list n).get i = i.cast (length_list n) := by
@@ -40,14 +40,14 @@ theorem list_succ (n) : list (n+1) = 0 :: (list n).map Fin.succ := by
 theorem list_succ_last (n) : list (n+1) = (list n).map castSucc ++ [last n] := by
   rw [list_succ]
   induction n with
-  | zero => simp [last]
+  | zero => simp
   | succ n ih =>
     rw [list_succ, List.map_cons castSucc, ih]
     simp [Function.comp_def, succ_castSucc]
 
 theorem list_reverse (n) : (list n).reverse = (list n).map rev := by
   induction n with
-  | zero => simp [last]
+  | zero => simp
   | succ n ih =>
     conv => lhs; rw [list_succ_last]
     conv => rhs; rw [list_succ]
diff --git a/Batteries/Data/HashMap/Basic.lean b/Batteries/Data/HashMap/Basic.lean
index 3419ba35ab..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) :
@@ -237,7 +237,7 @@ inductive WF [BEq α] [Hashable α] : Imp α β → Prop where
   /-- Replacing an element in a well formed hash map yields a well formed hash map. -/
   | modify : WF m → WF (modify m a f)
 
-theorem WF.empty [BEq α] [Hashable α] : WF (empty n : Imp α β) := by unfold empty; apply empty'
+theorem WF.empty [BEq α] [Hashable α] : WF (empty n : Imp α β) := empty'
 
 end Imp
 
diff --git a/Batteries/Data/HashMap/WF.lean b/Batteries/Data/HashMap/WF.lean
index 258723a89b..11b68de28d 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.length_toList, Array.ugetElem_eq_getElem, Array.getElem_eq_getElem_toList]
   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.length_toList]
   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_getElem_toList, 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_getElem_toList, toList_update, List.getElem_set,
+      Array.length_toList, 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.length_toList] 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.length_toList, 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,35 +91,35 @@ 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
       · case a =>
-        simp only [Array.data_length, Array.data_set]
+        simp only [Array.length_toList, Array.toList_set]
         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 =>
-        simp only [Array.data_length, Array.data_set, Array.get_eq_getElem, AssocList.foldl_eq]
+        simp only [Array.length_toList, Array.toList_set, Array.get_eq_getElem, AssocList.foldl_eq]
         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.length_toList]
         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_getElem_toList]
         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.length_toList]
       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
@@ -126,21 +128,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.length_toList,
+      Array.ugetElem_eq_getElem, Array.toList_set] at h
     match List.mem_or_eq_of_mem_set h with
     | .inl h =>
       intro _ hf
@@ -150,7 +152,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) :
@@ -158,11 +160,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
@@ -171,8 +173,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.length_toList, Array.size_set, Array.getElem_eq_getElem_toList,
+          Array.toList_set, List.getElem_set]
         split
         · nofun
         · exact hs₂ _ (by simp_all)
@@ -180,7 +182,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
@@ -198,7 +200,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.length_toList, Buckets.update_size]
     refine have ⟨_, _, h₁, _, eq⟩ := Buckets.exists_of_update ..; eq ▸ ?_
     simp [h₁, Buckets.size_eq, Nat.succ_add]; rfl
 
@@ -264,7 +266,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.length_toList, 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
@@ -317,8 +319,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.toList_map, List.map_map]; congr; funext l; simp
+  · simp only [Array.toList_map, 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,
@@ -361,7 +363,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, Functor.map, StateT.map, 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]
@@ -369,7 +371,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.length_toList, Array.getElem_eq_getElem_toList,
       List.getElem_map] at h ⊢
     have := H.out.2.2 _ h
     simp only [AssocList.All, List.toList_toAssocList, List.mem_reverse, List.mem_filterMap,
@@ -385,13 +387,15 @@ variable {_ : BEq α} {_ : Hashable α}
 @[inline] def mapVal (f : α → β → γ) (self : HashMap α β) : HashMap α γ :=
   ⟨self.1.mapVal f, self.2.mapVal⟩
 
-/--
-Applies `f` to each key-value pair `a, b` in the map. If it returns `some c` then
-`a, c` is pushed into the new map; else the key is removed from the map.
--/
-@[inline] def filterMap (f : α → β → Option γ) (self : HashMap α β) : HashMap α γ :=
-  ⟨self.1.filterMap f, self.2.filterMap⟩
+-- Temporarily removed on lean-pr-testing-5403.
+
+-- /--
+-- Applies `f` to each key-value pair `a, b` in the map. If it returns `some c` then
+-- `a, c` is pushed into the new map; else the key is removed from the map.
+-- -/
+-- @[inline] def filterMap (f : α → β → Option γ) (self : HashMap α β) : HashMap α γ :=
+--   ⟨self.1.filterMap f, self.2.filterMap⟩
 
-/-- Constructs a map with the set of all pairs `a, b` such that `f` returns true. -/
-@[inline] def filter (f : α → β → Bool) (self : HashMap α β) : HashMap α β :=
-  self.filterMap fun a b => bif f a b then some b else none
+-- /-- Constructs a map with the set of all pairs `a, b` such that `f` returns true. -/
+-- @[inline] def filter (f : α → β → Bool) (self : HashMap α β) : HashMap α β :=
+--   self.filterMap fun a b => bif f a b then some b else none
diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean
index 29061c409e..49126faee0 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`
@@ -765,8 +766,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]
@@ -801,7 +802,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]
 
@@ -870,7 +871,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]
 
@@ -946,7 +947,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/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
index f03e693d16..1ac4ae3f57 100644
--- a/Batteries/Data/List/Lemmas.lean
+++ b/Batteries/Data/List/Lemmas.lean
@@ -10,31 +10,11 @@ import Batteries.Tactic.Alias
 
 namespace List
 
-open Nat
-
-/-! ### mem -/
-
-@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
-  simp [Array.mem_def]
-
 /-! ### toArray-/
 
-@[simp] theorem size_toArrayAux (l : List α) (r : Array α) :
-    (l.toArrayAux r).size = r.size + l.length := by
-  induction l generalizing r with
-  | nil => simp [toArrayAux]
-  | cons a l ih =>
-    simp [ih, List.toArrayAux]
-    omega
-
 @[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) :
     (Array.mk xs)[i] = xs[i] := rfl
 
-@[simp] theorem getElem_toArray (l : List α) (i : Nat) (h : i < l.toArray.size) :
-    l.toArray[i] = l[i]'(by simpa using h) := by
-  rw [Array.getElem_eq_data_getElem]
-  simp
-
 /-! ### next? -/
 
 @[simp] theorem next?_nil : @next? α [] = none := rfl
@@ -196,18 +176,18 @@ theorem exists_of_set' {l : List α} (h : n < l.length) :
     ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ l₁.length = n ∧ l.set n a' = l₁ ++ a' :: l₂ := by
   rw [set_eq_modifyNth]; exact exists_of_modifyNth _ h
 
-@[deprecated getElem?_set_eq' (since := "2024-06-12")]
+@[deprecated getElem?_set_self' (since := "2024-06-12")]
 theorem get?_set_eq (a : α) (n) (l : List α) : (set l n a).get? n = (fun _ => a) <$> l.get? n := by
-  simp only [get?_eq_getElem?, getElem?_set_eq', Option.map_eq_map]
+  simp only [get?_eq_getElem?, getElem?_set_self', Option.map_eq_map]
   rfl
 
 theorem getElem?_set_eq_of_lt (a : α) {n} {l : List α} (h : n < length l) :
-    (set l n a)[n]? = some a := by rw [getElem?_set_eq', getElem?_eq_getElem h]; rfl
+    (set l n a)[n]? = some a := by rw [getElem?_set_self', getElem?_eq_getElem h]; rfl
 
 @[deprecated getElem?_set_eq_of_lt (since := "2024-06-12")]
 theorem get?_set_eq_of_lt (a : α) {n} {l : List α} (h : n < length l) :
     (set l n a).get? n = some a := by
-  rw [get?_eq_getElem?, getElem?_set_eq', getElem?_eq_getElem h]; rfl
+  rw [get?_eq_getElem?, getElem?_set_self', getElem?_eq_getElem h]; rfl
 
 @[deprecated getElem?_set_ne (since := "2024-06-12")]
 theorem get?_set_ne (a : α) {m n} (l : List α) (h : m ≠ n) : (set l m a).get? n = l.get? n := by
@@ -216,7 +196,7 @@ theorem get?_set_ne (a : α) {m n} (l : List α) (h : m ≠ n) : (set l m a).get
 @[deprecated getElem?_set (since := "2024-06-12")]
 theorem get?_set (a : α) {m n} (l : List α) :
     (set l m a).get? n = if m = n then (fun _ => a) <$> l.get? n else l.get? n := by
-  simp [getElem?_set']
+  simp [getElem?_set']; rfl
 
 theorem get?_set_of_lt (a : α) {m n} (l : List α) (h : n < length l) :
     (set l m a).get? n = if m = n then some a else l.get? n := by
@@ -233,18 +213,12 @@ theorem get?_set_of_lt' (a : α) {m n} (l : List α) (h : m < length l) :
 theorem length_tail_add_one (l : List α) (h : 0 < length l) : (length (tail l)) + 1 = length l := by
   simp [Nat.sub_add_cancel h]
 
-@[simp] theorem getElem?_tail (l : List α) : l.tail[n]? = l[n + 1]? := by cases l <;> simp
-
-@[simp] theorem getElem_tail (l : List α) (h : n < l.tail.length) :
-    l.tail[n] = l[n + 1]'(by simp at h; omega) := by
-  cases l; contradiction; simp
-
 /-! ### eraseP -/
 
 @[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
@@ -419,7 +393,7 @@ theorem pair_mem_product {xs : List α} {ys : List β} {x : α} {y : β} :
 theorem forIn_eq_bindList [Monad m] [LawfulMonad m]
     (f : α → β → m (ForInStep β)) (l : List α) (init : β) :
     forIn l init f = ForInStep.run <$> (ForInStep.yield init).bindList f l := by
-  induction l generalizing init <;> simp [*, map_eq_pure_bind]
+  induction l generalizing init <;> simp [*]
   congr; ext (b | b) <;> simp
 
 /-! ### diff -/
@@ -675,37 +649,6 @@ theorem insertP_loop (a : α) (l r : List α) :
   induction l with simp [insertP, insertP.loop, cond]
   | cons _ _ ih => split <;> simp [insertP_loop, ih]
 
-/-! ### 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
-  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
-  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
-  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
-  match l, r with
-  | [], r => simp
-  | l, [] => simp
-  | a::l, b::r =>
-    rw [cons_merge_cons]
-    split
-    · 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 :=
-  mem_merge.2 <| .inl h
-
-theorem mem_merge_right (s : α → α → Bool) (h : x ∈ r) : x ∈ merge s l r :=
-  mem_merge.2 <| .inr h
-
 /-! ### foldlM and foldrM -/
 
 theorem foldlM_map [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : List β₁) (init : α) :
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/RBMap/Alter.lean b/Batteries/Data/RBMap/Alter.lean
index 3f6d25c2b3..fd1e8f205a 100644
--- a/Batteries/Data/RBMap/Alter.lean
+++ b/Batteries/Data/RBMap/Alter.lean
@@ -206,14 +206,20 @@ theorem Ordered.ins : ∀ {path : Path α} {t : RBNode α},
     t.Ordered cmp → path.Ordered cmp → t.All (path.RootOrdered cmp) → (path.ins t).Ordered cmp
   | .root, _, ht, _, _ => Ordered.setBlack.2 ht
   | .left red parent x b, a, ha, ⟨hp, xb, xp, bp, hb⟩, H => by
-    unfold ins; have ⟨ax, ap⟩ := All_and.1 H; exact hp.ins ⟨ax, xb, ha, hb⟩ ⟨xp, ap, bp⟩
+    unfold Path.ins
+    have ⟨ax, ap⟩ := All_and.1 H
+    exact hp.ins ⟨ax, xb, ha, hb⟩ ⟨xp, ap, bp⟩
   | .right red a x parent, b, hb, ⟨hp, ax, xp, ap, ha⟩, H => by
-    unfold ins; have ⟨xb, bp⟩ := All_and.1 H; exact hp.ins ⟨ax, xb, ha, hb⟩ ⟨xp, ap, bp⟩
+    unfold Path.ins
+    have ⟨xb, bp⟩ := All_and.1 H
+    exact hp.ins ⟨ax, xb, ha, hb⟩ ⟨xp, ap, bp⟩
   | .left black parent x b, a, ha, ⟨hp, xb, xp, bp, hb⟩, H => by
-    unfold ins; have ⟨ax, ap⟩ := All_and.1 H
+    unfold Path.ins
+    have ⟨ax, ap⟩ := All_and.1 H
     exact hp.ins (ha.balance1 ax xb hb) (balance1_All.2 ⟨xp, ap, bp⟩)
   | .right black a x parent, b, hb, ⟨hp, ax, xp, ap, ha⟩, H => by
-    unfold ins; have ⟨xb, bp⟩ := All_and.1 H
+    unfold Path.ins
+    have ⟨xb, bp⟩ := All_and.1 H
     exact hp.ins (ha.balance2 ax xb hb) (balance2_All.2 ⟨xp, ap, bp⟩)
 
 theorem Ordered.insertNew {path : Path α} (hp : path.Ordered cmp) (vp : path.RootOrdered cmp v) :
@@ -224,14 +230,20 @@ theorem Ordered.del : ∀ {path : Path α} {t : RBNode α} {c},
     t.Ordered cmp → path.Ordered cmp → t.All (path.RootOrdered cmp) → (path.del t c).Ordered cmp
   | .root, _, _, ht, _, _ => Ordered.setBlack.2 ht
   | .left _ parent x b, a, red, ha, ⟨hp, xb, xp, bp, hb⟩, H => by
-    unfold del; have ⟨ax, ap⟩ := All_and.1 H; exact hp.del ⟨ax, xb, ha, hb⟩ ⟨xp, ap, bp⟩
+    unfold Path.del
+    have ⟨ax, ap⟩ := All_and.1 H
+    exact hp.del ⟨ax, xb, ha, hb⟩ ⟨xp, ap, bp⟩
   | .right _ a x parent, b, red, hb, ⟨hp, ax, xp, ap, ha⟩, H => by
-    unfold del; have ⟨xb, bp⟩ := All_and.1 H; exact hp.del ⟨ax, xb, ha, hb⟩ ⟨xp, ap, bp⟩
+    unfold Path.del
+    have ⟨xb, bp⟩ := All_and.1 H
+    exact hp.del ⟨ax, xb, ha, hb⟩ ⟨xp, ap, bp⟩
   | .left _ parent x b, a, black, ha, ⟨hp, xb, xp, bp, hb⟩, H => by
-    unfold del; have ⟨ax, ap⟩ := All_and.1 H
+    unfold Path.del
+    have ⟨ax, ap⟩ := All_and.1 H
     exact hp.del (ha.balLeft ax xb hb) (ap.balLeft xp bp)
   | .right _ a x parent, b, black, hb, ⟨hp, ax, xp, ap, ha⟩, H => by
-    unfold del; have ⟨xb, bp⟩ := All_and.1 H
+    unfold Path.del
+    have ⟨xb, bp⟩ := All_and.1 H
     exact hp.del (ha.balRight ax xb hb) (ap.balRight xp bp)
 
 end Path
diff --git a/Batteries/Data/RBMap/WF.lean b/Batteries/Data/RBMap/WF.lean
index 6fbd669e6e..220852c0ab 100644
--- a/Batteries/Data/RBMap/WF.lean
+++ b/Batteries/Data/RBMap/WF.lean
@@ -261,7 +261,8 @@ so this is only suitable for use on the root of the tree.)
 -/
 theorem Balanced.insert {t : RBNode α} (h : t.Balanced c n) :
     ∃ c' n', (insert cmp t v).Balanced c' n' := by
-  unfold insert; match ins cmp v t, h.ins cmp v with
+  unfold RBNode.insert
+  match ins cmp v t, h.ins cmp v with
   | _, .balanced h => split <;> [exact ⟨_, h.setBlack⟩; exact ⟨_, _, h⟩]
   | _, .redred _ ha hb => have .node red .. := t; exact ⟨_, _, .black ha hb⟩
 
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/String/Lemmas.lean b/Batteries/Data/String/Lemmas.lean
index ddd43d32a4..490c34908b 100644
--- a/Batteries/Data/String/Lemmas.lean
+++ b/Batteries/Data/String/Lemmas.lean
@@ -15,11 +15,11 @@ namespace String
 attribute [ext (iff := false)] ext
 
 theorem lt_trans {s₁ s₂ s₃ : String} : s₁ < s₂ → s₂ < s₃ → s₁ < s₃ :=
-  List.lt_trans' (α := Char) Nat.lt_trans
+  List.lt_trans (α := Char) Nat.lt_trans
     (fun h1 h2 => Nat.not_lt.2 <| Nat.le_trans (Nat.not_lt.1 h2) (Nat.not_lt.1 h1))
 
 theorem lt_antisymm {s₁ s₂ : String} (h₁ : ¬s₁ < s₂) (h₂ : ¬s₂ < s₁) : s₁ = s₂ :=
-  ext <| List.lt_antisymm' (α := Char)
+  ext <| List.lt_antisymm (α := Char)
     (fun h1 h2 => Char.le_antisymm (Nat.not_lt.1 h2) (Nat.not_lt.1 h1)) h₁ h₂
 
 instance : Batteries.TransOrd String := .compareOfLessAndEq
@@ -209,7 +209,7 @@ theorem next_of_valid (cs : List Char) (c : Char) (cs' : List Char) :
     next ⟨cs ++ c :: cs'⟩ ⟨utf8Len cs⟩ = ⟨utf8Len cs + c.utf8Size⟩ := next_of_valid' ..
 
 @[simp] theorem atEnd_iff (s : String) (p : Pos) : atEnd s p ↔ s.endPos ≤ p :=
-  decide_eq_true_iff _
+  decide_eq_true_iff
 
 theorem valid_next {p : Pos} (h : p.Valid s) (h₂ : p < s.endPos) : (next s p).Valid s := by
   match s, p, h with
diff --git a/Batteries/Data/UnionFind/Basic.lean b/Batteries/Data/UnionFind/Basic.lean
index 549c9e1cde..4fff679993 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.length_toList]
 
 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.length_toList, 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.length_toList]; 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.length_toList, Array.get_eq_getElem, dite_eq_ite]
   split <;> simp only
   have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
   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.length_toList, findAux_root]
     apply dif_pos
     exact parent'_lt ..
 
@@ -309,8 +309,7 @@ theorem rankD_findAux {self : UnionFind} {x : Fin self.size} :
     rw [findAux_s]; split <;> [rfl; skip]
     have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
     have := lt_of_parentD (by rwa [parentD_eq])
-    rw [rankD_eq' (by simp [FindAux.size_eq, h])]
-    rw [Array.get_modify (by rwa [FindAux.size_eq])]
+    rw [rankD_eq' (by simp [FindAux.size_eq, h]), Array.get_modify]
     split <;> simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt x⟩), -Array.get_eq_getElem]
   else
     simp only [rankD, Array.data_length, Array.get_eq_getElem, rank]
@@ -364,7 +363,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.length_toList]
 termination_by self.rankMax - self.rank x
 
 theorem lt_rankD_findAux {self : UnionFind} {x : Fin self.size} :
@@ -386,7 +385,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.length_toList, 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 +419,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.length_toList, find]
   rw [parentD_findAux, if_pos rfl]
 
 theorem find_parent_or (self : UnionFind) (x : Fin self.size) (i) :
@@ -500,7 +499,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.length_toList, linkAux_size] at *
     simp only [linkAux, Array.get_eq_getElem]
     split <;> [skip; split <;> [skip; split]]
     · exact self.parentD_lt h
@@ -522,7 +521,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.length_toList, Nat.lt_irrefl, not_false_eq_true,
           and_true, ite_false, ite_eq_right_iff]
         rintro rfl
         simp [rankD_eq, *]
diff --git a/Batteries/Data/Vector/Basic.lean b/Batteries/Data/Vector/Basic.lean
index 7726a5b9e5..534f94030a 100644
--- a/Batteries/Data/Vector/Basic.lean
+++ b/Batteries/Data/Vector/Basic.lean
@@ -263,7 +263,7 @@ alias take := shrink
 if and only if `p a[i] b[i]` holds true for all valid indices `i`.
 -/
 @[inline] def isEqv (a b : Vector α n) (p : α → α → Bool) : Bool :=
-  Array.isEqvAux a.toArray b.toArray (a.size_eq.trans b.size_eq.symm) p 0
+  Array.isEqvAux a.toArray b.toArray (a.size_eq.trans b.size_eq.symm) p 0 (Nat.zero_le _)
 
 instance [BEq α] : BEq (Vector α n) :=
   ⟨fun a b => isEqv a b BEq.beq⟩
diff --git a/Batteries/Lean/HashSet.lean b/Batteries/Lean/HashSet.lean
index 4b6df398b3..2a6ee47909 100644
--- a/Batteries/Lean/HashSet.lean
+++ b/Batteries/Lean/HashSet.lean
@@ -23,13 +23,6 @@ def anyM [Monad m] (s : HashSet α) (f : α → m Bool) : m Bool := do
       return true
   return false
 
-/--
-`O(n)`. Returns `true` if `f` returns `true` for any element of the set.
--/
-@[inline]
-def any (s : HashSet α) (f : α → Bool) : Bool :=
-  Id.run <| s.anyM f
-
 /--
 `O(n)`. Returns `true` if `f` returns `true` for all elements of the set.
 -/
@@ -40,13 +33,6 @@ def allM [Monad m] (s : HashSet α) (f : α → m Bool) : m Bool := do
       return false
   return true
 
-/--
-`O(n)`. Returns `true` if `f` returns `true` for all elements of the set.
--/
-@[inline]
-def all (s : HashSet α) (f : α → Bool) : Bool :=
-  Id.run <| s.allM f
-
 instance : BEq (HashSet α) where
   beq s t := s.all (t.contains ·) && t.all (s.contains ·)
 
@@ -59,10 +45,3 @@ def insert' (s : HashSet α) (a : α) : HashSet α × Bool :=
   let oldSize := s.size
   let s := s.insert a
   (s, s.size == oldSize)
-
-/--
-`O(n)`. Obtain a `HashSet` from an array.
--/
-@[inline]
-protected def ofArray [BEq α] [Hashable α] (as : Array α) : HashSet α :=
-  HashSet.empty.insertMany as
diff --git a/Batteries/Lean/Meta/AssertHypotheses.lean b/Batteries/Lean/Meta/AssertHypotheses.lean
deleted file mode 100644
index 6275032063..0000000000
--- a/Batteries/Lean/Meta/AssertHypotheses.lean
+++ /dev/null
@@ -1,40 +0,0 @@
-/-
-Copyright (c) 2022 Jannis Limperg. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jannis Limperg
--/
-
-import Lean.Meta.Tactic.Assert
-
-open Lean Lean.Meta
-
-namespace Lean.Meta
-
-/--
-Description of a hypothesis for `Lean.MVarId.assertHypotheses'`.
--/
-structure Hypothesis' extends Hypothesis where
-  /-- The hypothesis' `BinderInfo` -/
-  binderInfo : BinderInfo
-  /-- The hypothesis' `LocalDeclKind` -/
-  kind : LocalDeclKind
-
-/--
-Add the given hypotheses to the local context. This is a generalisation of
-`Lean.MVarId.assertHypotheses` which lets you specify
--/
-def _root_.Lean.MVarId.assertHypotheses' (mvarId : MVarId)
-    (hs : Array Hypothesis') : MetaM (Array FVarId × MVarId) := do
-  let (fvarIds, mvarId) ← mvarId.assertHypotheses $ hs.map (·.toHypothesis)
-  mvarId.modifyLCtx fun lctx => Id.run do
-    let mut lctx := lctx
-    for h : i in [:hs.size] do
-      let h := hs[i]
-      if h.kind != .default then
-        lctx := lctx.setKind fvarIds[i]! h.kind
-      if h.binderInfo != .default then
-        lctx := lctx.setBinderInfo fvarIds[i]! h.binderInfo
-    pure lctx
-  return (fvarIds, mvarId)
-
-end Lean.Meta
diff --git a/Batteries/Lean/Meta/Clear.lean b/Batteries/Lean/Meta/Clear.lean
deleted file mode 100644
index 66f38b7798..0000000000
--- a/Batteries/Lean/Meta/Clear.lean
+++ /dev/null
@@ -1,26 +0,0 @@
-/-
-Copyright (c) 2022 Jannis Limperg. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jannis Limperg
--/
-
-import Batteries.Lean.Meta.Basic
-import Lean.Meta.Tactic.Clear
-
-open Lean Lean.Meta
-
-/--
-Try to clear the given fvars from the local context. Returns the new goal and
-the hypotheses that were cleared. Unlike `Lean.MVarId.tryClearMany`, this
-function does not require the `hyps` to be given in the order in which they
-appear in the local context.
--/
-def Lean.MVarId.tryClearMany' (goal : MVarId) (hyps : Array FVarId) :
-    MetaM (MVarId × Array FVarId) :=
-  goal.withContext do
-    let hyps ← sortFVarsByContextOrder hyps
-    hyps.foldrM (init := (goal, Array.mkEmpty hyps.size))
-      fun h (goal, cleared) => do
-        let goal' ← goal.tryClear h
-        let cleared := if goal == goal' then cleared else cleared.push h
-        return (goal', cleared)
diff --git a/lean-toolchain b/lean-toolchain
index 89985206ac..a00797801f 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.12.0
+leanprover/lean4:v4.13.0-rc1
diff --git a/test/lint_lean.lean b/test/lint_lean.lean
index 46eb6591ff..f5657a5b96 100644
--- a/test/lint_lean.lean
+++ b/test/lint_lean.lean
@@ -15,14 +15,13 @@ but it is useful to run locally to see what the linters would catch.
 -- attribute [nolint dupNamespace] Lean.Elab.Tactic.Tactic
 -- attribute [nolint dupNamespace] Lean.Parser.Parser Lean.Parser.Parser.rec Lean.Parser.Parser.mk
 --   Lean.Parser.Parser.info Lean.Parser.Parser.fn
+-- attribute [nolint explicitVarsOfIff] Iff.refl
 
 /-! Failing lints that need work. -/
 
--- #lint only explicitVarsOfIff in all -- Found 156 errors
-
--- Many fixed in https://github.com/leanprover/lean4/pull/4620
+-- Many fixed in https://github.com/leanprover/lean4/pull/4620 and subsequent PRs
 -- and should be checked again.
--- #lint only simpNF in all -- Found 12 errors
+-- #lint only simpNF in all -- Found 22 errors
 
 /-! Lints that fail, but that we're not intending to do anything about. -/
 
@@ -41,6 +40,7 @@ but it is useful to run locally to see what the linters would catch.
 
 /-! Lints that have succeeded in the past, and hopefully still do! -/
 
+-- #lint only explicitVarsOfIff in all -- Found 1 errors, `Iff.refl`, which could be nolinted.
 -- #lint only impossibleInstance  in all -- Found 0 errors
 -- #lint only simpVarHead in all -- Found 0 error
 -- #lint only unusedHavesSuffices in all  -- Found 0 errors