diff --git a/.github/workflows/test_mathlib.yml b/.github/workflows/test_mathlib.yml
index e3bf84d3ca..3bb9c6dd71 100644
--- a/.github/workflows/test_mathlib.yml
+++ b/.github/workflows/test_mathlib.yml
@@ -15,20 +15,16 @@ jobs:
       - name: Checkout PR
         uses: actions/checkout@v4
         with:
-          repository: ${{ github.event.workflow_run.head_repository.full_name }}
-          ref: ${{github.event.workflow_run.head_branch }}
           fetch-depth: 0
 
       - name: Get PR info
         id: pr-info
         run: |
-          echo "pullRequestNumber=$(gh pr view --json number -q .number || echo '')" >> $GITHUB_OUTPUT
-          echo "targetBranch=$(gh pr view --json baseRefName -q .baseRefName || echo '')" >> $GITHUB_OUTPUT
-          echo "HEAD_BRANCH=$(gh pr view --json headRefName -q .headRefName || echo '')" >> $GITHUB_ENV
-          echo "HEAD_REPO=$(gh pr view --json headRepository -q .headRepository.name || echo '')" >> $GITHUB_ENV
-          echo "HEAD_OWNER=$(gh pr view --json headRepositoryOwner -q .headRepositoryOwner.login || echo '')" >> $GITHUB_ENV
+          echo "pullRequestNumber=$(gh pr list --search $SHA --json number -q '.[0].number' || echo '')" >> $GITHUB_OUTPUT
+          echo "targetBranch=$(gh pr list --search $SHA --json baseRefName -q '.[0].baseRefName' || echo '')" >> $GITHUB_OUTPUT
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          SHA: ${{ github.event.workflow_run.head_sha }}
 
       - name: Checkout mathlib4 repository
         if: steps.pr-info.outputs.pullRequestNumber != '' && steps.pr-info.outputs.targetBranch == 'main'
@@ -52,14 +48,13 @@ jobs:
         id: check_mathlib_tag
         env:
           PR_NUMBER: ${{ steps.pr-info.outputs.pullRequestNumber }}
-          HEAD_OWNER: ${{ env.HEAD_OWNER }}
-          HEAD_REPO: ${{ env.HEAD_REPO }}
-          HEAD_BRANCH: ${{ env.HEAD_BRANCH }}
+          HEAD_REPO: ${{ github.event.workflow_run.head_repository.full_name }}
+          HEAD_BRANCH: ${{ github.event.workflow_run.head_branch }}
         run: |
           git config user.name "leanprover-community-mathlib4-bot"
           git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
 
-          echo "PR info: $HEAD_OWNER $HEAD_REPO $HEAD_BRANCH"
+          echo "PR info: $HEAD_REPO $HEAD_BRANCH"
 
           BASE=master
           echo "Using base tag: $BASE"
diff --git a/Batteries.lean b/Batteries.lean
index ac2a24459a..5746bd7026 100644
--- a/Batteries.lean
+++ b/Batteries.lean
@@ -34,7 +34,6 @@ import Batteries.Data.Range
 import Batteries.Data.Rat
 import Batteries.Data.Stream
 import Batteries.Data.String
-import Batteries.Data.Sum
 import Batteries.Data.UInt
 import Batteries.Data.UnionFind
 import Batteries.Data.Vector
@@ -73,7 +72,6 @@ import Batteries.StdDeprecations
 import Batteries.Tactic.Alias
 import Batteries.Tactic.Basic
 import Batteries.Tactic.Case
-import Batteries.Tactic.Classical
 import Batteries.Tactic.Congr
 import Batteries.Tactic.Exact
 import Batteries.Tactic.HelpCmd
diff --git a/Batteries/Data/Array/Basic.lean b/Batteries/Data/Array/Basic.lean
index c74b8f4750..403c42d9e2 100644
--- a/Batteries/Data/Array/Basic.lean
+++ b/Batteries/Data/Array/Basic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Arthur Paulino, Floris van Doorn, Jannis Limperg
 -/
 import Batteries.Data.Array.Init.Lemmas
+import Batteries.Tactic.Alias
 
 /-!
 ## Definitions on Arrays
@@ -14,10 +15,6 @@ proofs about these definitions, those are contained in other files in `Batteries
 
 namespace Array
 
-/-- Drop `none`s from a Array, and replace each remaining `some a` with `a`. -/
-def reduceOption (l : Array (Option α)) : Array α :=
-  l.filterMap id
-
 /--
 Check whether `xs` and `ys` are equal as sets, i.e. they contain the same
 elements when disregarding order and duplicates. `O(n*m)`! If your element type
@@ -122,11 +119,7 @@ protected def maxI [ord : Ord α] [Inhabited α]
     (xs : Array α) (start := 0) (stop := xs.size) : α :=
   xs.minI (ord := ord.opposite) start stop
 
-/--
-`O(|join L|)`. `join L` concatenates all the arrays in `L` into one array.
-* `join #[#[a], #[], #[b, c], #[d, e, f]] = #[a, b, c, d, e, f]`
--/
-@[inline] def join (l : Array (Array α)) : Array α := l.foldl (· ++ ·) #[]
+@[deprecated (since := "2024-10-15")] alias join := flatten
 
 /-!
 ### Safe Nat Indexed Array functions
diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
index 124f8d412c..8a5544089d 100644
--- a/Batteries/Data/Array/Lemmas.lean
+++ b/Batteries/Data/Array/Lemmas.lean
@@ -14,19 +14,8 @@ namespace Array
 theorem forIn_eq_forIn_toList [Monad m]
     (as : Array α) (b : β) (f : α → β → m (ForInStep β)) :
     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.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.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
+  cases as
+  simp
 
 @[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
@@ -99,28 +88,11 @@ theorem size_filter_le (p : α → Bool) (l : Array α) :
   simp only [← length_toList, toList_filter]
   apply List.length_filter_le
 
-/-! ### join -/
-
-@[simp] theorem toList_join {l : Array (Array α)} : l.join.toList = (l.toList.map toList).join := by
-  dsimp [join]
-  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.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, 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.toList, ⟨⟨s, h₁, rfl⟩, h₂⟩⟩
+/-! ### flatten -/
+
+@[deprecated (since := "2024-09-09")] alias data_join := toList_flatten
+@[deprecated (since := "2024-08-13")] alias join_data := toList_flatten
+@[deprecated (since := "2024-10-15")] alias mem_join := mem_flatten
 
 /-! ### indexOf? -/
 
@@ -154,27 +126,10 @@ where
     (a.eraseIdx i).size = if i < a.size then a.size-1 else a.size := by
   simp only [eraseIdx]; split; simp; rfl
 
-/-! ### shrink -/
-
-theorem size_shrink_loop (a : Array α) (n) : (shrink.loop n a).size = a.size - n := by
-  induction n generalizing a with simp only [shrink.loop, Nat.sub_zero]
-  | succ n ih => simp only [ih, size_pop]; omega
-
-@[simp] theorem size_shrink (a : Array α) (n) : (a.shrink n).size = min a.size n := by
-  simp [shrink, size_shrink_loop]
-  omega
-
 /-! ### set -/
 
 theorem size_set! (a : Array α) (i v) : (a.set! i v).size = a.size := by simp
 
-/-! ### swapAt -/
-
-theorem size_swapAt (a : Array α) (x i) : (a.swapAt i x).snd.size = a.size := by simp
-
-@[simp] theorem size_swapAt! (a : Array α) (x) (h : i < a.size) :
-    (a.swapAt! i x).snd.size = a.size := by simp [h]
-
 /-! ### map -/
 
 theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by
@@ -266,14 +221,14 @@ theorem getElem_insertAt_lt (as : Array α) (i : Fin (as.size+1)) (v : α)
     (k) (hlt : k < i.val) {hk : k < (as.insertAt i v).size} {hk' : k < as.size} :
     (as.insertAt i v)[k] = as[k] := by
   simp only [insertAt]
-  rw [get_insertAt_loop_lt, get_push, dif_pos hk']
+  rw [get_insertAt_loop_lt, getElem_push, dif_pos hk']
   exact hlt
 
 theorem getElem_insertAt_gt (as : Array α) (i : Fin (as.size+1)) (v : α)
     (k) (hgt : k > i.val) {hk : k < (as.insertAt i v).size} {hk' : k - 1 < as.size} :
     (as.insertAt i v)[k] = as[k - 1] := by
   simp only [insertAt]
-  rw [get_insertAt_loop_gt_le, get_push, dif_pos hk']
+  rw [get_insertAt_loop_gt_le, getElem_push, dif_pos hk']
   exact hgt
   rw [size_insertAt] at hk
   exact Nat.le_of_lt_succ hk
@@ -282,6 +237,6 @@ theorem getElem_insertAt_eq (as : Array α) (i : Fin (as.size+1)) (v : α)
     (k) (heq : i.val = k) {hk : k < (as.insertAt i v).size} :
     (as.insertAt i v)[k] = v := by
   simp only [insertAt]
-  rw [get_insertAt_loop_eq, Fin.getElem_fin, get_push_eq]
+  rw [get_insertAt_loop_eq, Fin.getElem_fin, getElem_push_eq]
   exact heq
   exact Nat.le_of_lt_succ i.is_lt
diff --git a/Batteries/Data/Array/Match.lean b/Batteries/Data/Array/Match.lean
index 46b2239f6f..b47ee90adc 100644
--- a/Batteries/Data/Array/Match.lean
+++ b/Batteries/Data/Array/Match.lean
@@ -52,7 +52,7 @@ termination_by k => k.val
 def PrefixTable.extend [BEq α] (t : PrefixTable α) (x : α) : PrefixTable α where
   toArray := t.toArray.push (x, t.step x ⟨t.size, Nat.lt_succ_self _⟩)
   valid _ := by
-    rw [Array.get_push]
+    rw [Array.getElem_push]
     split
     · exact t.valid ..
     · next h => exact Nat.le_trans (Nat.lt_succ.1 <| Fin.isLt ..) (Nat.not_lt.1 h)
diff --git a/Batteries/Data/Array/Monadic.lean b/Batteries/Data/Array/Monadic.lean
index 316813972a..934111e131 100644
--- a/Batteries/Data/Array/Monadic.lean
+++ b/Batteries/Data/Array/Monadic.lean
@@ -44,7 +44,7 @@ theorem SatisfiesM_mapM [Monad m] [LawfulMonad m] (as : Array α) (f : α → m
   · case s =>
     intro ⟨i, hi⟩ arr ⟨ih₁, eq, ih₂⟩
     refine (hs _ ih₁).map fun ⟨h₁, h₂⟩ => ⟨h₂, by simp [eq], fun j hj => ?_⟩
-    simp [get_push] at hj ⊢; split; {apply ih₂}
+    simp [getElem_push] at hj ⊢; split; {apply ih₂}
     cases j; cases (Nat.le_or_eq_of_le_succ hj).resolve_left ‹_›; cases eq; exact h₁
 
 theorem SatisfiesM_mapM' [Monad m] [LawfulMonad m] (as : Array α) (f : α → m β)
@@ -125,27 +125,36 @@ theorem SatisfiesM_foldrM [Monad m] [LawfulMonad m]
   simp [foldrM]; split; {exact go _ h0}
   · next h => exact .pure (Nat.eq_zero_of_not_pos h ▸ h0)
 
-theorem SatisfiesM_mapIdxM [Monad m] [LawfulMonad m] (as : Array α) (f : Fin as.size → α → m β)
+theorem SatisfiesM_mapFinIdxM [Monad m] [LawfulMonad m] (as : Array α) (f : Fin as.size → α → m β)
     (motive : Nat → Prop) (h0 : motive 0)
     (p : Fin as.size → β → Prop)
     (hs : ∀ i, motive i.1 → SatisfiesM (p i · ∧ motive (i + 1)) (f i as[i])) :
     SatisfiesM
       (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i])
-      (Array.mapIdxM as f) := by
+      (Array.mapFinIdxM as f) := by
   let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p ⟨i, h⟩ bs[i]) (hm : motive j) :
     SatisfiesM
       (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i])
-      (Array.mapIdxM.map as f i j h bs) := by
-    induction i generalizing j bs with simp [mapIdxM.map]
+      (Array.mapFinIdxM.map as f i j h bs) := by
+    induction i generalizing j bs with simp [mapFinIdxM.map]
     | zero =>
       have := (Nat.zero_add _).symm.trans h
       exact .pure ⟨this ▸ hm, h₁ ▸ this, fun _ _ => h₂ ..⟩
     | succ i ih =>
       refine (hs _ (by exact hm)).bind fun b hb => ih (by simp [h₁]) (fun i hi hi' => ?_) hb.2
-      simp at hi'; simp [get_push]; split
+      simp at hi'; simp [getElem_push]; split
       · next h => exact h₂ _ _ h
       · next h => cases h₁.symm ▸ (Nat.le_or_eq_of_le_succ hi').resolve_left h; exact hb.1
-  simp [mapIdxM]; exact go rfl nofun h0
+  simp [mapFinIdxM]; exact go rfl nofun h0
+
+theorem SatisfiesM_mapIdxM [Monad m] [LawfulMonad m] (as : Array α) (f : Nat → α → m β)
+    (motive : Nat → Prop) (h0 : motive 0)
+    (p : Fin as.size → β → Prop)
+    (hs : ∀ i, motive i.1 → SatisfiesM (p i · ∧ motive (i + 1)) (f i as[i])) :
+    SatisfiesM
+      (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i])
+      (Array.mapIdxM as f) :=
+  SatisfiesM_mapFinIdxM as (fun i => f i) motive h0 p hs
 
 theorem size_modifyM [Monad m] [LawfulMonad m] (a : Array α) (i : Nat) (f : α → m α) :
     SatisfiesM (·.size = a.size) (a.modifyM i f) := by
diff --git a/Batteries/Data/Array/Pairwise.lean b/Batteries/Data/Array/Pairwise.lean
index 9e61e642ed..82ace9609f 100644
--- a/Batteries/Data/Array/Pairwise.lean
+++ b/Batteries/Data/Array/Pairwise.lean
@@ -21,7 +21,7 @@ def Pairwise (R : α → α → Prop) (as : Array α) : Prop := as.toList.Pairwi
 
 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_toList_get]
+  unfold Pairwise; simp [List.pairwise_iff_get, getElem_fin_eq_getElem_toList]
 
 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
diff --git a/Batteries/Data/AssocList.lean b/Batteries/Data/AssocList.lean
index 1e94b1d2f6..eba8927cef 100644
--- a/Batteries/Data/AssocList.lean
+++ b/Batteries/Data/AssocList.lean
@@ -244,8 +244,8 @@ instance : ForIn m (AssocList α β) (α × β) where
 
 @[simp] theorem forIn_eq [Monad m] (l : AssocList α β) (init : δ)
     (f : (α × β) → δ → m (ForInStep δ)) : forIn l init f = forIn l.toList init f := by
-  simp [forIn, List.forIn]
-  induction l generalizing init <;> simp [AssocList.forIn, List.forIn.loop]
+  simp only [forIn]
+  induction l generalizing init <;> simp [AssocList.forIn]
   congr; funext a; split <;> simp [*]
 
 /-- Split the list into head and tail, if possible. -/
diff --git a/Batteries/Data/ByteArray.lean b/Batteries/Data/ByteArray.lean
index c10cf6ba65..6a95a241aa 100644
--- a/Batteries/Data/ByteArray.lean
+++ b/Batteries/Data/ByteArray.lean
@@ -36,11 +36,11 @@ theorem getElem_eq_data_getElem (a : ByteArray) (h : i < a.size) : a[i] = a.data
   Array.size_push ..
 
 @[simp] theorem get_push_eq (a : ByteArray) (x : UInt8) : (a.push x)[a.size] = x :=
-  Array.get_push_eq ..
+  Array.getElem_push_eq ..
 
 theorem get_push_lt (a : ByteArray) (x : UInt8) (i : Nat) (h : i < a.size) :
     (a.push x)[i]'(size_push .. ▸ Nat.lt_succ_of_lt h) = a[i] :=
-  Array.get_push_lt ..
+  Array.getElem_push_lt ..
 
 /-! ### set -/
 
diff --git a/Batteries/Data/HashMap/Basic.lean b/Batteries/Data/HashMap/Basic.lean
index 98905c3343..3fd1d3350d 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.toList.map (·.toList.length))
+noncomputable def size (data : Buckets α β) : Nat := (data.1.toList.map (·.toList.length)).sum
 
 @[simp] theorem update_size (self : Buckets α β) (i d h) :
     (self.update i d h).1.size = self.1.size := Array.size_uset ..
@@ -56,7 +56,7 @@ structure WF [BEq α] [Hashable α] (buckets : Buckets α β) : Prop where
     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) :
-    buckets.1[i].All fun k _ => ((hash k).toUSize % buckets.1.size).toNat = i
+    buckets.1[i].All fun k _ => ((hash k).toUSize % USize.ofNat buckets.1.size).toNat = i
 
 end Buckets
 end Imp
@@ -93,7 +93,7 @@ def empty (capacity := 0) : Imp α β :=
 
 /-- Calculates the bucket index from a hash value `u`. -/
 def mkIdx {n : Nat} (h : 0 < n) (u : USize) : {u : USize // u.toNat < n} :=
-  ⟨u % n, USize.modn_lt _ h⟩
+  ⟨u % USize.ofNat n, USize.toNat_mod_lt _ h⟩
 
 /--
 Inserts a key-value pair into the bucket array. This function assumes that the data is not
diff --git a/Batteries/Data/HashMap/WF.lean b/Batteries/Data/HashMap/WF.lean
index c95e3ad133..aa33711633 100644
--- a/Batteries/Data/HashMap/WF.lean
+++ b/Batteries/Data/HashMap/WF.lean
@@ -36,7 +36,7 @@ theorem update_update (self : Buckets α β) (i d d' h h') :
   rw [Array.set_set]
 
 theorem size_eq (data : Buckets α β) :
-  size data = .sum (data.1.toList.map (·.toList.length)) := rfl
+  size data = (data.1.toList.map (·.toList.length)).sum := rfl
 
 theorem mk_size (h) : (mk n h : Buckets α β).size = 0 := by
   simp only [mk, mkArray, size_eq]; clear h
@@ -52,8 +52,8 @@ theorem WF.update [BEq α] [Hashable α] {buckets : Buckets α β} {i d h} (H :
     (h₁ : ∀ [PartialEquivBEq α] [LawfulHashable α],
       (buckets.1[i].toList.Pairwise fun a b => ¬(a.1 == b.1)) →
       d.toList.Pairwise fun a b => ¬(a.1 == b.1))
-    (h₂ : (buckets.1[i].All fun k _ => ((hash k).toUSize % buckets.1.size).toNat = i.toNat) →
-      d.All fun k _ => ((hash k).toUSize % buckets.1.size).toNat = i.toNat) :
+    (h₂ : (buckets.1[i].All fun k _ => ((hash k).toUSize % .ofNat buckets.1.size).toNat = i.toNat) →
+      d.All fun k _ => ((hash k).toUSize % USize.ofNat buckets.1.size).toNat = i.toNat) :
     (buckets.update i d h).WF := by
   refine ⟨fun l hl => ?_, fun i hi p hp => ?_⟩
   · exact match List.mem_or_eq_of_mem_set hl with
@@ -93,7 +93,7 @@ theorem expand_size [Hashable α] {buckets : Buckets α β} :
 where
   go (i source) (target : Buckets α β) (hs : ∀ j < i, source.toList[j]?.getD .nil = .nil) :
       (expand.go i source target).size =
-        .sum (source.toList.map (·.toList.length)) + target.size := by
+        (source.toList.map (·.toList.length)).sum + target.size := by
     unfold expand.go; split
     · next H =>
       refine (go (i+1) _ _ fun j hj => ?a).trans ?b
@@ -107,14 +107,14 @@ where
         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.length_toList]
+          List.length_nil, Nat.sum_append, List.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_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 [(_ : List.sum _ = 0), Nat.zero_add]
       rw [← (_ : source.toList.map (fun _ => .nil) = source.toList)]
       · simp only [List.map_map]
         induction source.toList <;> simp [*]
@@ -163,9 +163,9 @@ where
       (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)
+        source[j].All fun k _ => ((hash k).toUSize % USize.ofNat source.size).toNat = j)
       {target : Buckets α β} (ht : target.WF ∧ ∀ bucket ∈ target.1.toList,
-        bucket.All fun k _ => ((hash k).toUSize % source.size).toNat < i) :
+        bucket.All fun k _ => ((hash k).toUSize % USize.ofNat source.size).toNat < i) :
       (expand.go i source target).WF := by
     unfold expand.go; split
     · next H =>
@@ -178,7 +178,7 @@ where
         split
         · nofun
         · exact hs₂ _ (by simp_all)
-      · let rank (k : α) := ((hash k).toUSize % source.size).toNat
+      · let rank (k : α) := ((hash k).toUSize % USize.ofNat source.size).toNat
         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₂)⟩
@@ -267,7 +267,7 @@ theorem erase_size [BEq α] [Hashable α] {m : Imp α β} {k}
     simp only [h, Buckets.size]
     refine have ⟨_, _, h₁, _, eq⟩ := Buckets.exists_of_update ..; eq ▸ ?_
     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]
+      Nat.sum_append, List.sum_cons, AssocList.toList_erase]
     rw [(_ : List.length _ = _ + 1), Nat.add_right_comm]; {rfl}
     clear h₁ eq
     simp only [AssocList.contains_eq, List.any_eq_true] at H
@@ -347,7 +347,7 @@ theorem WF.filterMap {α β γ} {f : α → β → Option γ} [BEq α] [Hashable
   let M := StateT (ULift Nat) Id
   have H2 (l : List (AssocList α β)) n :
       l.mapM (m := M) (filterMap.go f .nil) n =
-      (l.map g, ⟨n.1 + .sum ((l.map g).map (·.toList.length))⟩) := by
+      (l.map g, ⟨n.1 + ((l.map g).map (·.toList.length)).sum⟩) := by
     induction l generalizing n with
     | nil => rfl
     | cons l L IH => simp [bind, StateT.bind, IH, H1, Nat.add_assoc, g]; rfl
diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean
index c4c262a016..3e2460f18c 100644
--- a/Batteries/Data/List/Basic.lean
+++ b/Batteries/Data/List/Basic.lean
@@ -32,17 +32,6 @@ open Option Nat
   | [] => none
   | a :: l => some (a, l)
 
-/--
-Given a function `f : Nat → α → β` and `as : list α`, `as = [a₀, a₁, ...]`, returns the list
-`[f 0 a₀, f 1 a₁, ...]`.
--/
-@[inline] def mapIdx (f : Nat → α → β) (as : List α) : List β := go as #[] where
-  /-- Auxiliary for `mapIdx`:
-  `mapIdx.go [a₀, a₁, ...] acc = acc.toList ++ [f acc.size a₀, f (acc.size + 1) a₁, ...]` -/
-  @[specialize] go : List α → Array β → List β
-  | [], acc => acc.toList
-  | a :: as, acc => go as (acc.push (f acc.size a))
-
 /-- Monadic variant of `mapIdx`. -/
 @[inline] def mapIdxM {m : Type v → Type w} [Monad m]
     (as : List α) (f : Nat → α → m β) : m (List β) := go as #[] where
@@ -163,54 +152,9 @@ Split a list at every occurrence of a separator element. The separators are not
 -/
 @[inline] def splitOn [BEq α] (a : α) (as : List α) : List (List α) := as.splitOnP (· == a)
 
-/--
-Apply a function to the nth tail of `l`. Returns the input without
-using `f` if the index is larger than the length of the List.
-```
-modifyTailIdx f 2 [a, b, c] = [a, b] ++ f [c]
-```
--/
-@[simp] def modifyTailIdx (f : List α → List α) : Nat → List α → List α
-  | 0, l => f l
-  | _+1, [] => []
-  | n+1, a :: l => a :: modifyTailIdx f n l
-
 @[deprecated (since := "2024-10-21")] alias modifyNthTail := modifyTailIdx
-
-/-- Apply `f` to the head of the list, if it exists. -/
-@[inline] def modifyHead (f : α → α) : List α → List α
-  | [] => []
-  | a :: l => f a :: l
-
-@[simp] theorem modifyHead_nil (f : α → α) : [].modifyHead f = [] := by rw [modifyHead]
-
-@[simp] theorem modifyHead_cons (a : α) (l : List α) (f : α → α) :
-    (a :: l).modifyHead f = f a :: l := by rw [modifyHead]
-
-/--
-Apply `f` to the nth element of the list, if it exists, replacing that element with the result.
--/
-def modify (f : α → α) : Nat → List α → List α :=
-  modifyTailIdx (modifyHead f)
-
 @[deprecated (since := "2024-10-21")] alias modifyNth := modify
 
-/-- Tail-recursive version of `modify`. -/
-def modifyTR (f : α → α) (n : Nat) (l : List α) : List α := go l n #[] where
-  /-- Auxiliary for `modifyTR`: `modifyTR.go f l n acc = acc.toList ++ modify f n l`. -/
-  go : List α → Nat → Array α → List α
-  | [], _, acc => acc.toList
-  | a :: l, 0, acc => acc.toListAppend (f a :: l)
-  | a :: l, n+1, acc => go l n (acc.push a)
-
-theorem modifyTR_go_eq : ∀ l n, modifyTR.go f l n acc = acc.toList ++ modify f n l
-  | [], n => by cases n <;> simp [modifyTR.go, modify]
-  | a :: l, 0 => by simp [modifyTR.go, modify]
-  | a :: l, n+1 => by simp [modifyTR.go, modify, modifyTR_go_eq l]
-
-@[csimp] theorem modify_eq_modifyTR : @modify = @modifyTR := by
-  funext α f n l; simp [modifyTR, modifyTR_go_eq]
-
 /-- Apply `f` to the last element of `l`, if it exists. -/
 @[inline] def modifyLast (f : α → α) (l : List α) : List α := go l #[] where
   /-- Auxiliary for `modifyLast`: `modifyLast.go f l acc = acc.toList ++ modifyLast f l`. -/
@@ -424,7 +368,7 @@ sublists [1, 2, 3] = [[], [1], [2], [1, 2], [3], [1, 3], [2, 3], [1, 2, 3]]
 ```
 -/
 def sublists (l : List α) : List (List α) :=
-  l.foldr (fun a acc => acc.bind fun x => [x, a :: x]) [[]]
+  l.foldr (fun a acc => acc.flatMap fun x => [x, a :: x]) [[]]
 
 /-- A version of `List.sublists` that has faster runtime performance but worse kernel performance -/
 def sublistsFast (l : List α) : List (List α) :=
@@ -522,7 +466,7 @@ of `[L₁, L₂, ..., Lₙ]` is a list whose first element comes from
 -/
 @[simp] def sections : List (List α) → List (List α)
   | [] => [[]]
-  | l :: L => (sections L).bind fun s => l.map fun a => a :: s
+  | l :: L => (sections L).flatMap fun s => l.map fun a => a :: s
 
 /-- Optimized version of `sections`. -/
 def sectionsTR (L : List (List α)) : List (List α) :=
@@ -547,7 +491,7 @@ 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_toList, Array.foldl_toList_eq_bind]; rfl
+  rw [Array.foldl_eq_foldl_toList, Array.foldl_toList_eq_flatMap]; rfl
   intros; apply Array.foldl_toList_eq_map
 
 /--
@@ -577,7 +521,7 @@ def revzip (l : List α) : List (α × α) := zip l l.reverse
 product [1, 2] [5, 6] = [(1, 5), (1, 6), (2, 5), (2, 6)]
 ```
 -/
-def product (l₁ : List α) (l₂ : List β) : List (α × β) := l₁.bind fun a => l₂.map (Prod.mk a)
+def product (l₁ : List α) (l₂ : List β) : List (α × β) := l₁.flatMap fun a => l₂.map (Prod.mk a)
 
 /-- Optimized version of `product`. -/
 def productTR (l₁ : List α) (l₂ : List β) : List (α × β) :=
@@ -585,7 +529,7 @@ def productTR (l₁ : List α) (l₂ : List β) : List (α × β) :=
 
 @[csimp] theorem product_eq_productTR : @product = @productTR := by
   funext α β l₁ l₂; simp [product, productTR]
-  rw [Array.foldl_toList_eq_bind]; rfl
+  rw [Array.foldl_toList_eq_flatMap]; 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`.
@@ -593,7 +537,7 @@ def productTR (l₁ : List α) (l₂ : List β) : List (α × β) :=
 sigma [1, 2] (λ_, [(5 : Nat), 6]) = [(1, 5), (1, 6), (2, 5), (2, 6)]
 ``` -/
 protected def sigma {σ : α → Type _} (l₁ : List α) (l₂ : ∀ a, List (σ a)) : List (Σ a, σ a) :=
-  l₁.bind fun a => (l₂ a).map (Sigma.mk a)
+  l₁.flatMap fun a => (l₂ a).map (Sigma.mk a)
 
 /-- Optimized version of `sigma`. -/
 def sigmaTR {σ : α → Type _} (l₁ : List α) (l₂ : ∀ a, List (σ a)) : List (Σ a, σ a) :=
@@ -601,7 +545,7 @@ 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_toList_eq_bind]; rfl
+  rw [Array.foldl_toList_eq_flatMap]; rfl
   intros; apply Array.foldl_toList_eq_map
 
 /--
diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
index 5179c81ba0..89f1de368d 100644
--- a/Batteries/Data/List/Lemmas.lean
+++ b/Batteries/Data/List/Lemmas.lean
@@ -36,89 +36,6 @@ theorem dropLast_eq_eraseIdx {xs : List α} {i : Nat} (last_idx : i + 1 = xs.len
     exact ih last_idx
     exact fun _ => nomatch xs
 
-/-! ### modifyHead -/
-
-@[simp] theorem modifyHead_modifyHead (l : List α) (f g : α → α) :
-    (l.modifyHead f).modifyHead g = l.modifyHead (g ∘ f) := by cases l <;> simp [modifyHead]
-
-/-! ### modify -/
-
-@[simp] theorem modify_nil (f : α → α) (n) : [].modify f n = [] := by cases n <;> rfl
-
-@[simp] theorem modify_zero_cons (f : α → α) (a : α) (l : List α) :
-    (a :: l).modify f 0 = f a :: l := rfl
-
-@[simp] theorem modify_succ_cons (f : α → α) (a : α) (l : List α) (n) :
-    (a :: l).modify f (n + 1) = a :: l.modify f n := by rfl
-
-theorem modifyTailIdx_id : ∀ n (l : List α), l.modifyTailIdx id n = l
-  | 0, _ => rfl
-  | _+1, [] => rfl
-  | n+1, a :: l => congrArg (cons a) (modifyTailIdx_id n l)
-
-theorem eraseIdx_eq_modifyTailIdx : ∀ n (l : List α), eraseIdx l n = modifyTailIdx tail n l
-  | 0, l => by cases l <;> rfl
-  | _+1, [] => rfl
-  | _+1, _ :: _ => congrArg (cons _) (eraseIdx_eq_modifyTailIdx _ _)
-
-theorem getElem?_modify (f : α → α) :
-    ∀ n (l : List α) m, (modify f n l)[m]? = (fun a => if n = m then f a else a) <$> l[m]?
-  | n, l, 0 => by cases l <;> cases n <;> simp
-  | n, [], _+1 => by cases n <;> rfl
-  | 0, _ :: l, m+1 => by cases h : l[m]? <;> simp [h, modify, m.succ_ne_zero.symm]
-  | n+1, a :: l, m+1 => by
-    simp only [modify_succ_cons, getElem?_cons_succ, Nat.reduceEqDiff, Option.map_eq_map]
-    refine (getElem?_modify f n l m).trans ?_
-    cases h' : l[m]? <;> by_cases h : n = m <;>
-      simp [h, if_pos, if_neg, Option.map, mt Nat.succ.inj, not_false_iff, h']
-
-theorem length_modifyTailIdx (f : List α → List α) (H : ∀ l, length (f l) = length l) :
-    ∀ n l, length (modifyTailIdx f n l) = length l
-  | 0, _ => H _
-  | _+1, [] => rfl
-  | _+1, _ :: _ => congrArg (·+1) (length_modifyTailIdx _ H _ _)
-
-theorem modifyTailIdx_add (f : List α → List α) (n) (l₁ l₂ : List α) :
-    modifyTailIdx f (l₁.length + n) (l₁ ++ l₂) = l₁ ++ modifyTailIdx f n l₂ := by
-  induction l₁ <;> simp [*, Nat.succ_add]
-
-theorem exists_of_modifyTailIdx (f : List α → List α) {n} {l : List α} (h : n ≤ l.length) :
-    ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.length = n ∧ modifyTailIdx f n l = l₁ ++ f l₂ :=
-  have ⟨_, _, eq, hl⟩ : ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.length = n :=
-    ⟨_, _, (take_append_drop n l).symm, length_take_of_le h⟩
-  ⟨_, _, eq, hl, hl ▸ eq ▸ modifyTailIdx_add (n := 0) ..⟩
-
-@[simp] theorem length_modify (f : α → α) : ∀ n l, length (modify f n l) = length l :=
-  length_modifyTailIdx _ fun l => by cases l <;> rfl
-
-@[simp] theorem getElem?_modify_eq (f : α → α) (n) (l : List α) :
-    (modify f n l)[n]? = f <$> l[n]? := by
-  simp only [getElem?_modify, if_pos]
-
-@[simp] theorem getElem?_modify_ne (f : α → α) {m n} (l : List α) (h : m ≠ n) :
-    (modify f m l)[n]? = l[n]? := by
-  simp only [getElem?_modify, if_neg h, id_map']
-
-theorem exists_of_modify (f : α → α) {n} {l : List α} (h : n < l.length) :
-    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ l₁.length = n ∧ modify f n l = l₁ ++ f a :: l₂ :=
-  match exists_of_modifyTailIdx _ (Nat.le_of_lt h) with
-  | ⟨_, _::_, eq, hl, H⟩ => ⟨_, _, _, eq, hl, H⟩
-  | ⟨_, [], eq, hl, _⟩ => nomatch Nat.ne_of_gt h (eq ▸ append_nil _ ▸ hl)
-
-theorem modifyTailIdx_eq_take_drop (f : List α → List α) (H : f [] = []) :
-    ∀ n l, modifyTailIdx f n l = take n l ++ f (drop n l)
-  | 0, _ => rfl
-  | _ + 1, [] => H.symm
-  | n + 1, b :: l => congrArg (cons b) (modifyTailIdx_eq_take_drop f H n l)
-
-theorem modify_eq_take_drop (f : α → α) :
-    ∀ n l, modify f n l = take n l ++ modifyHead f (drop n l) :=
-  modifyTailIdx_eq_take_drop _ rfl
-
-theorem modify_eq_take_cons_drop (f : α → α) {n l} (h : n < length l) :
-    modify f n l = take n l ++ f l[n] :: drop (n + 1) l := by
-  rw [modify_eq_take_drop, drop_eq_getElem_cons h]; rfl
-
 /-! ### set -/
 
 theorem set_eq_modify (a : α) : ∀ n (l : List α), set l n a = modify (fun _ => a) n l
@@ -128,7 +45,7 @@ theorem set_eq_modify (a : α) : ∀ n (l : List α), set l n a = modify (fun _
 
 theorem set_eq_take_cons_drop (a : α) {n l} (h : n < length l) :
     set l n a = take n l ++ a :: drop (n + 1) l := by
-  rw [set_eq_modify, modify_eq_take_cons_drop _ h]
+  rw [set_eq_modify, modify_eq_take_cons_drop h]
 
 theorem modify_eq_set_get? (f : α → α) :
     ∀ n (l : List α), l.modify f n = ((fun a => l.set n (f a)) <$> l.get? n).getD l
@@ -328,7 +245,7 @@ theorem inter_def [BEq α] (l₁ l₂ : List α)  : l₁ ∩ l₂ = filter (elem
 theorem pair_mem_product {xs : List α} {ys : List β} {x : α} {y : β} :
     (x, y) ∈ product xs ys ↔ x ∈ xs ∧ y ∈ ys := by
   simp only [product, and_imp, mem_map, Prod.mk.injEq,
-    exists_eq_right_right, mem_bind, iff_self]
+    exists_eq_right_right, mem_flatMap, iff_self]
 
 /-! ### monadic operations -/
 
@@ -591,16 +508,6 @@ theorem insertP_loop (a : α) (l r : List α) :
   induction l with simp [insertP, insertP.loop, cond]
   | cons _ _ ih => split <;> simp [insertP_loop, ih]
 
-/-! ### foldlM and foldrM -/
-
-theorem foldlM_map [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : List β₁) (init : α) :
-    (l.map f).foldlM g init = l.foldlM (fun x y => g x (f y)) init := by
-  induction l generalizing g init <;> simp [*]
-
-theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂ → α → m α) (l : List β₁)
-    (init : α) : (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init := by
-  induction l generalizing g init <;> simp [*]
-
 /-! ### deprecations -/
 
 @[deprecated (since := "2024-08-15")] alias isEmpty_iff_eq_nil := isEmpty_iff
diff --git a/Batteries/Data/List/Perm.lean b/Batteries/Data/List/Perm.lean
index 2196d88367..6eb06d1d9e 100644
--- a/Batteries/Data/List/Perm.lean
+++ b/Batteries/Data/List/Perm.lean
@@ -316,10 +316,12 @@ theorem Perm.inter {l₁ l₂ t₁ t₂ : List α} (p₁ : l₁ ~ l₂) (p₂ :
 
 end DecidableEq
 
-theorem Perm.join_congr :
-    ∀ {l₁ l₂ : List (List α)} (_ : List.Forall₂ (· ~ ·) l₁ l₂), l₁.join ~ l₂.join
+theorem Perm.flatten_congr :
+    ∀ {l₁ l₂ : List (List α)} (_ : List.Forall₂ (· ~ ·) l₁ l₂), l₁.flatten ~ l₂.flatten
   | _, _, .nil => .rfl
-  | _ :: _, _ :: _, .cons h₁ h₂ => h₁.append (Perm.join_congr h₂)
+  | _ :: _, _ :: _, .cons h₁ h₂ => h₁.append (Perm.flatten_congr h₂)
+
+@[deprecated (since := "2024-10-15")] alias Perm.join_congr := Perm.flatten_congr
 
 theorem perm_insertP (p : α → Bool) (a l) : insertP p a l ~ a :: l := by
   induction l with simp [insertP, insertP.loop, cond]
diff --git a/Batteries/Data/Nat/Lemmas.lean b/Batteries/Data/Nat/Lemmas.lean
index 7fa93705f7..a97c558c44 100644
--- a/Batteries/Data/Nat/Lemmas.lean
+++ b/Batteries/Data/Nat/Lemmas.lean
@@ -159,5 +159,6 @@ protected def sum_trichotomy (a b : Nat) : a < b ⊕' a = b ⊕' b < a :=
 
 /-! ### sum -/
 
-@[simp] theorem sum_append : Nat.sum (l₁ ++ l₂) = Nat.sum l₁ + Nat.sum l₂ := by
+
+@[simp] theorem sum_append {l₁ l₂ : List Nat}: (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by
   induction l₁ <;> simp [*, Nat.add_assoc]
diff --git a/Batteries/Data/Range/Lemmas.lean b/Batteries/Data/Range/Lemmas.lean
index d71082848f..a075e0b6b4 100644
--- a/Batteries/Data/Range/Lemmas.lean
+++ b/Batteries/Data/Range/Lemmas.lean
@@ -69,7 +69,7 @@ theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range)
       suffices ∀ fuel l i hle H, l ≤ fuel →
           (∀ j, stop ≤ i + step * j ↔ l ≤ j) → ∀ init,
           forIn'.loop start stop step f fuel i hle init =
-          List.forIn ((List.range' i l step).pmap Subtype.mk H) init f' by
+          forIn ((List.range' i l step).pmap Subtype.mk H) init f' by
         refine this _ _ _ _ _
           ((numElems_le_iff hstep).2 (Nat.le_trans ?_ (Nat.le_add_left ..)))
           (fun _ => (numElems_le_iff hstep).symm) _
@@ -85,7 +85,7 @@ theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range)
             (List.forall_mem_cons.1 H).2 (Nat.le_of_succ_le_succ h1) fun i => by
               rw [Nat.add_right_comm, Nat.add_assoc, ← Nat.mul_succ, h2, Nat.succ_le_succ_iff]
           have := h2 0; simp at this
-          rw [forIn'.loop]; simp [List.forIn, this, ih]; rfl
+          rw [forIn'.loop]; simp [this, ih]; rfl
   else
     simp [List.range', h, numElems_stop_le_start ⟨start, stop, step⟩ (Nat.not_lt.1 h), L]
     cases stop <;> unfold forIn'.loop <;> simp [List.forIn', h]
@@ -94,13 +94,6 @@ theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
     (init : β) (f : Nat → β → m (ForInStep β)) :
     forIn r init f = forIn (List.range' r.start r.numElems r.step) init f := by
   refine Eq.trans ?_ <| (forIn'_eq_forIn_range' r init (fun x _ => f x)).trans ?_
-  · simp [forIn, forIn', Range.forIn, Range.forIn']
-    suffices ∀ fuel i hl b, forIn'.loop r.start r.stop r.step (fun x _ => f x) fuel i hl b =
-        forIn.loop f fuel i r.stop r.step b from (this _ ..).symm
-    intro fuel; induction fuel <;> intro i hl b <;>
-      unfold forIn.loop forIn'.loop <;> simp [*]
-    split
-    · simp [if_neg (Nat.not_le.2 ‹_›)]
-    · simp [if_pos (Nat.not_lt.1 ‹_›)]
+  · simp [forIn, forIn']
   · suffices ∀ L H, forIn (List.pmap Subtype.mk L H) init (f ·.1) = forIn L init f from this _ ..
     intro L; induction L generalizing init <;> intro H <;> simp [*]
diff --git a/Batteries/Data/Stream.lean b/Batteries/Data/Stream.lean
index 3b0197a810..fb9df787be 100644
--- a/Batteries/Data/Stream.lean
+++ b/Batteries/Data/Stream.lean
@@ -4,20 +4,90 @@ Released under Apache 2. license as described in the file LICENSE.
 Authors: François G. Dorais
 -/
 
+namespace Stream
+
 /-- Drop up to `n` values from the stream `s`. -/
-def Stream.drop [Stream σ α] (s : σ) : Nat → σ
+def drop [Stream σ α] (s : σ) : Nat → σ
   | 0 => s
-  | n+1 => match Stream.next? s with
+  | n+1 =>
+    match next? s with
     | none => s
     | some (_, s) => drop s n
 
-/-- Read up to `n` values from the stream `s`. -/
-def Stream.take [Stream σ α] (s : σ) (n : Nat) : Array α × σ :=
-  loop s (.mkEmpty n) n
+/-- Read up to `n` values from the stream `s` as a list from first to last. -/
+def take [Stream σ α] (s : σ) : Nat → List α × σ
+  | 0 => ([], s)
+  | n+1 =>
+    match next? s with
+    | none => ([], s)
+    | some (a, s) =>
+      match take s n with
+      | (as, s) => (a :: as, s)
+
+@[simp] theorem fst_take_zero [Stream σ α] (s : σ) :
+    (take s 0).fst = [] := rfl
+
+theorem fst_take_succ [Stream σ α] (s : σ) :
+    (take s (n+1)).fst = match next? s with
+      | none => []
+      | some (a, s) => a :: (take s n).fst := by
+  simp only [take]; split <;> rfl
+
+@[simp] theorem snd_take_eq_drop [Stream σ α] (s : σ) (n : Nat) :
+    (take s n).snd = drop s n := by
+  induction n generalizing s with
+  | zero => rfl
+  | succ n ih =>
+    simp only [take, drop]
+    split <;> simp [ih]
+
+/-- Tail recursive version of `Stream.take`. -/
+def takeTR [Stream σ α] (s : σ) (n : Nat) : List α × σ :=
+  loop s [] n
 where
-  /-- Inner loop for `Stream.take`. -/
-  loop (s : σ) (acc : Array α)
-    | 0 => (acc, s)
-    | n+1 => match Stream.next? s with
-      | none => (acc, s)
-      | some (v, s) => loop s (acc.push v) n
+  /-- Inner loop for `Stream.takeTR`. -/
+  loop (s : σ) (acc : List α)
+    | 0 => (acc.reverse, s)
+    | n+1 => match next? s with
+      | none => (acc.reverse, s)
+      | some (a, s) => loop s (a :: acc) n
+
+theorem fst_takeTR_loop [Stream σ α] (s : σ) (acc : List α) (n : Nat) :
+    (takeTR.loop s acc n).fst = acc.reverseAux (take s n).fst := by
+  induction n generalizing acc s with
+  | zero => rfl
+  | succ n ih => simp only [take, takeTR.loop]; split; rfl; simp [ih]
+
+theorem fst_takeTR [Stream σ α] (s : σ) (n : Nat) : (takeTR s n).fst = (take s n).fst :=
+  fst_takeTR_loop ..
+
+theorem snd_takeTR_loop [Stream σ α] (s : σ) (acc : List α) (n : Nat) :
+    (takeTR.loop s acc n).snd = drop s n := by
+  induction n generalizing acc s with
+  | zero => rfl
+  | succ n ih => simp only [takeTR.loop, drop]; split; rfl; simp [ih]
+
+theorem snd_takeTR [Stream σ α] (s : σ) (n : Nat) :
+    (takeTR s n).snd = drop s n := snd_takeTR_loop ..
+
+@[csimp] theorem take_eq_takeTR : @take = @takeTR := by
+  funext; ext : 1; rw [fst_takeTR]; rw [snd_takeTR, snd_take_eq_drop]
+
+end Stream
+
+@[simp] theorem List.stream_drop_eq_drop (l : List α) : Stream.drop l n = l.drop n := by
+  induction n generalizing l with
+  | zero => rfl
+  | succ n ih =>
+    match l with
+    | [] => rfl
+    | _::_ => simp [Stream.drop, List.drop_succ_cons, ih]
+
+@[simp] theorem List.stream_take_eq_take_drop (l : List α) :
+    Stream.take l n = (l.take n, l.drop n) := by
+  induction n generalizing l with
+  | zero => rfl
+  | succ n ih =>
+    match l with
+    | [] => rfl
+    | _::_ => simp [Stream.take, ih]
diff --git a/Batteries/Data/String/Basic.lean b/Batteries/Data/String/Basic.lean
index 6ff6ac98bf..aad3484c05 100644
--- a/Batteries/Data/String/Basic.lean
+++ b/Batteries/Data/String/Basic.lean
@@ -8,99 +8,6 @@ instance : Coe String Substring := ⟨String.toSubstring⟩
 
 namespace String
 
-protected theorem Pos.ne_zero_of_lt : {a b : Pos} → a < b → b ≠ 0
-  | _, _, hlt, rfl => Nat.not_lt_zero _ hlt
-
-end String
-
-namespace Substring
-
-/--
-Returns the longest common prefix of two substrings.
-The returned substring will use the same underlying string as `s`.
--/
-def commonPrefix (s t : Substring) : Substring :=
-  { s with stopPos := loop s.startPos t.startPos }
-where
-  /-- Returns the ending position of the common prefix, working up from `spos, tpos`. -/
-  loop spos tpos :=
-    if h : spos < s.stopPos ∧ tpos < t.stopPos then
-      if s.str.get spos == t.str.get tpos then
-        have := Nat.sub_lt_sub_left h.1 (s.str.lt_next spos)
-        loop (s.str.next spos) (t.str.next tpos)
-      else
-        spos
-    else
-      spos
-  termination_by s.stopPos.byteIdx - spos.byteIdx
-
-/--
-Returns the longest common suffix of two substrings.
-The returned substring will use the same underlying string as `s`.
--/
-def commonSuffix (s t : Substring) : Substring :=
-  { s with startPos := loop s.stopPos t.stopPos }
-where
-  /-- Returns the starting position of the common prefix, working down from `spos, tpos`. -/
-  loop spos tpos :=
-    if h : s.startPos < spos ∧ t.startPos < tpos then
-      let spos' := s.str.prev spos
-      let tpos' := t.str.prev tpos
-      if s.str.get spos' == t.str.get tpos' then
-        have : spos' < spos := s.str.prev_lt_of_pos spos (String.Pos.ne_zero_of_lt h.1)
-        loop spos' tpos'
-      else
-        spos
-    else
-      spos
-  termination_by spos.byteIdx
-
-/--
-If `pre` is a prefix of `s`, i.e. `s = pre ++ t`, returns the remainder `t`.
--/
-def dropPrefix? (s : Substring) (pre : Substring) : Option Substring :=
-  let t := s.commonPrefix pre
-  if t.bsize = pre.bsize then
-    some { s with startPos := t.stopPos }
-  else
-    none
-
-/--
-If `suff` is a suffix of `s`, i.e. `s = t ++ suff`, returns the remainder `t`.
--/
-def dropSuffix? (s : Substring) (suff : Substring) : Option Substring :=
-  let t := s.commonSuffix suff
-  if t.bsize = suff.bsize then
-    some { s with stopPos := t.startPos }
-  else
-    none
-
-end Substring
-
-namespace String
-
-/--
-If `pre` is a prefix of `s`, i.e. `s = pre ++ t`, returns the remainder `t`.
--/
-def dropPrefix? (s : String) (pre : Substring) : Option Substring :=
-  Substring.dropPrefix? s pre
-
-/--
-If `suff` is a suffix of `s`, i.e. `s = t ++ suff`, returns the remainder `t`.
--/
-def dropSuffix? (s : String) (suff : Substring) : Option Substring :=
-  Substring.dropSuffix? s suff
-
-/-- `s.stripPrefix pre` will remove `pre` from the beginning of `s` if it occurs there,
-or otherwise return `s`. -/
-def stripPrefix (s : String) (pre : Substring) : String :=
-  s.dropPrefix? pre |>.map Substring.toString |>.getD s
-
-/-- `s.stripSuffix suff` will remove `suff` from the end of `s` if it occurs there,
-or otherwise return `s`. -/
-def stripSuffix (s : String) (suff : Substring) : String :=
-  s.dropSuffix? suff |>.map Substring.toString |>.getD s
-
 /-- Count the occurrences of a character in a string. -/
 def count (s : String) (c : Char) : Nat :=
   s.foldl (fun n d => if d = c then n + 1 else n) 0
diff --git a/Batteries/Data/String/Lemmas.lean b/Batteries/Data/String/Lemmas.lean
index 490c34908b..5854890f25 100644
--- a/Batteries/Data/String/Lemmas.lean
+++ b/Batteries/Data/String/Lemmas.lean
@@ -447,12 +447,12 @@ theorem split_of_valid (s p) : split s p = (List.splitOnP p s.1).map mk := by
 
 attribute [simp] toSubstring'
 
-theorem join_eq (ss : List String) : join ss = ⟨(ss.map data).join⟩ := go ss [] where
-  go : ∀ (ss : List String) cs, ss.foldl (· ++ ·) (mk cs) = ⟨cs ++ (ss.map data).join⟩
+theorem join_eq (ss : List String) : join ss = ⟨(ss.map data).flatten⟩ := go ss [] where
+  go : ∀ (ss : List String) cs, ss.foldl (· ++ ·) (mk cs) = ⟨cs ++ (ss.map data).flatten⟩
     | [], _ => by simp
     | ⟨s⟩::ss, _ => (go ss _).trans (by simp)
 
-@[simp] theorem data_join (ss : List String) : (join ss).data = (ss.map data).join := by
+@[simp] theorem data_join (ss : List String) : (join ss).data = (ss.map data).flatten := by
   rw [join_eq]
 
 @[deprecated (since := "2024-06-06")] alias append_nil := append_empty
diff --git a/Batteries/Data/Sum.lean b/Batteries/Data/Sum.lean
deleted file mode 100644
index 51d4518942..0000000000
--- a/Batteries/Data/Sum.lean
+++ /dev/null
@@ -1,2 +0,0 @@
-import Batteries.Data.Sum.Basic
-import Batteries.Data.Sum.Lemmas
diff --git a/Batteries/Data/Sum/Basic.lean b/Batteries/Data/Sum/Basic.lean
deleted file mode 100644
index 6740f19228..0000000000
--- a/Batteries/Data/Sum/Basic.lean
+++ /dev/null
@@ -1,164 +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, Yury G. Kudryashov
--/
-
-/-!
-# Disjoint union of types
-
-This file defines basic operations on the the sum type `α ⊕ β`.
-
-`α ⊕ β` is the type made of a copy of `α` and a copy of `β`. It is also called *disjoint union*.
-
-## Main declarations
-
-* `Sum.isLeft`: Returns whether `x : α ⊕ β` comes from the left component or not.
-* `Sum.isRight`: Returns whether `x : α ⊕ β` comes from the right component or not.
-* `Sum.getLeft`: Retrieves the left content of a `x : α ⊕ β` that is known to come from the left.
-* `Sum.getRight`: Retrieves the right content of `x : α ⊕ β` that is known to come from the right.
-* `Sum.getLeft?`: Retrieves the left content of `x : α ⊕ β` as an option type or returns `none`
-  if it's coming from the right.
-* `Sum.getRight?`: Retrieves the right content of `x : α ⊕ β` as an option type or returns `none`
-  if it's coming from the left.
-* `Sum.map`: Maps `α ⊕ β` to `γ ⊕ δ` component-wise.
-* `Sum.elim`: Nondependent eliminator/induction principle for `α ⊕ β`.
-* `Sum.swap`: Maps `α ⊕ β` to `β ⊕ α` by swapping components.
-* `Sum.LiftRel`: The disjoint union of two relations.
-* `Sum.Lex`: Lexicographic order on `α ⊕ β` induced by a relation on `α` and a relation on `β`.
-
-## Further material
-
-See `Batteries.Data.Sum.Lemmas` for theorems about these definitions.
-
-## Notes
-
-The definition of `Sum` takes values in `Type _`. This effectively forbids `Prop`- valued sum types.
-To this effect, we have `PSum`, which takes value in `Sort _` and carries a more complicated
-universe signature in consequence. The `Prop` version is `Or`.
--/
-
-namespace Sum
-
-deriving instance DecidableEq for Sum
-deriving instance BEq for Sum
-
-section get
-
-/-- Check if a sum is `inl`. -/
-def isLeft : α ⊕ β → Bool
-  | inl _ => true
-  | inr _ => false
-
-/-- Check if a sum is `inr`. -/
-def isRight : α ⊕ β → Bool
-  | inl _ => false
-  | inr _ => true
-
-/-- Retrieve the contents from a sum known to be `inl`.-/
-def getLeft : (ab : α ⊕ β) → ab.isLeft → α
-  | inl a, _ => a
-
-/-- Retrieve the contents from a sum known to be `inr`.-/
-def getRight : (ab : α ⊕ β) → ab.isRight → β
-  | inr b, _ => b
-
-@[simp] theorem isLeft_inl : (inl x : α ⊕ β).isLeft = true := rfl
-@[simp] theorem isLeft_inr : (inr x : α ⊕ β).isLeft = false := rfl
-@[simp] theorem isRight_inl : (inl x : α ⊕ β).isRight = false := rfl
-@[simp] theorem isRight_inr : (inr x : α ⊕ β).isRight = true := rfl
-
-@[simp] theorem getLeft_inl (h : (inl x : α ⊕ β).isLeft) : (inl x).getLeft h = x := rfl
-@[simp] theorem getRight_inr (h : (inr x : α ⊕ β).isRight) : (inr x).getRight h = x := rfl
-
-@[simp] theorem getLeft?_inl : (inl x : α ⊕ β).getLeft? = some x := rfl
-@[simp] theorem getLeft?_inr : (inr x : α ⊕ β).getLeft? = none := rfl
-@[simp] theorem getRight?_inl : (inl x : α ⊕ β).getRight? = none := rfl
-@[simp] theorem getRight?_inr : (inr x : α ⊕ β).getRight? = some x := rfl
-
-end get
-
-/-- Define a function on `α ⊕ β` by giving separate definitions on `α` and `β`. -/
-protected def elim {α β γ} (f : α → γ) (g : β → γ) : α ⊕ β → γ :=
-  fun x => Sum.casesOn x f g
-
-@[simp] theorem elim_inl (f : α → γ) (g : β → γ) (x : α) :
-    Sum.elim f g (inl x) = f x := rfl
-
-@[simp] theorem elim_inr (f : α → γ) (g : β → γ) (x : β) :
-    Sum.elim f g (inr x) = g x := rfl
-
-/-- Map `α ⊕ β` to `α' ⊕ β'` sending `α` to `α'` and `β` to `β'`. -/
-protected def map (f : α → α') (g : β → β') : α ⊕ β → α' ⊕ β' :=
-  Sum.elim (inl ∘ f) (inr ∘ g)
-
-@[simp] theorem map_inl (f : α → α') (g : β → β') (x : α) : (inl x).map f g = inl (f x) := rfl
-
-@[simp] theorem map_inr (f : α → α') (g : β → β') (x : β) : (inr x).map f g = inr (g x) := rfl
-
-/-- Swap the factors of a sum type -/
-def swap : α ⊕ β → β ⊕ α := Sum.elim inr inl
-
-@[simp] theorem swap_inl : swap (inl x : α ⊕ β) = inr x := rfl
-
-@[simp] theorem swap_inr : swap (inr x : α ⊕ β) = inl x := rfl
-
-section LiftRel
-
-/-- Lifts pointwise two relations between `α` and `γ` and between `β` and `δ` to a relation between
-`α ⊕ β` and `γ ⊕ δ`. -/
-inductive LiftRel (r : α → γ → Prop) (s : β → δ → Prop) : α ⊕ β → γ ⊕ δ → Prop
-  /-- `inl a` and `inl c` are related via `LiftRel r s` if `a` and `c` are related via `r`. -/
-  | protected inl {a c} : r a c → LiftRel r s (inl a) (inl c)
-  /-- `inr b` and `inr d` are related via `LiftRel r s` if `b` and `d` are related via `s`. -/
-  | protected inr {b d} : s b d → LiftRel r s (inr b) (inr d)
-
-@[simp] theorem liftRel_inl_inl : LiftRel r s (inl a) (inl c) ↔ r a c :=
-  ⟨fun h => by cases h; assumption, LiftRel.inl⟩
-
-@[simp] theorem not_liftRel_inl_inr : ¬LiftRel r s (inl a) (inr d) := nofun
-
-@[simp] theorem not_liftRel_inr_inl : ¬LiftRel r s (inr b) (inl c) := nofun
-
-@[simp] theorem liftRel_inr_inr : LiftRel r s (inr b) (inr d) ↔ s b d :=
-  ⟨fun h => by cases h; assumption, LiftRel.inr⟩
-
-instance {r : α → γ → Prop} {s : β → δ → Prop}
-    [∀ a c, Decidable (r a c)] [∀ b d, Decidable (s b d)] :
-    ∀ (ab : α ⊕ β) (cd : γ ⊕ δ), Decidable (LiftRel r s ab cd)
-  | inl _, inl _ => decidable_of_iff' _ liftRel_inl_inl
-  | inl _, inr _ => Decidable.isFalse not_liftRel_inl_inr
-  | inr _, inl _ => Decidable.isFalse not_liftRel_inr_inl
-  | inr _, inr _ => decidable_of_iff' _ liftRel_inr_inr
-
-end LiftRel
-
-section Lex
-
-/-- Lexicographic order for sum. Sort all the `inl a` before the `inr b`, otherwise use the
-respective order on `α` or `β`. -/
-inductive Lex (r : α → α → Prop) (s : β → β → Prop) : α ⊕ β → α ⊕ β → Prop
-  /-- `inl a₁` and `inl a₂` are related via `Lex r s` if `a₁` and `a₂` are related via `r`. -/
-  | protected inl {a₁ a₂} (h : r a₁ a₂) : Lex r s (inl a₁) (inl a₂)
-  /-- `inr b₁` and `inr b₂` are related via `Lex r s` if `b₁` and `b₂` are related via `s`. -/
-  | protected inr {b₁ b₂} (h : s b₁ b₂) : Lex r s (inr b₁) (inr b₂)
-  /-- `inl a` and `inr b` are always related via `Lex r s`. -/
-  | sep (a b) : Lex r s (inl a) (inr b)
-
-attribute [simp] Lex.sep
-
-@[simp] theorem lex_inl_inl : Lex r s (inl a₁) (inl a₂) ↔ r a₁ a₂ :=
-  ⟨fun h => by cases h; assumption, Lex.inl⟩
-
-@[simp] theorem lex_inr_inr : Lex r s (inr b₁) (inr b₂) ↔ s b₁ b₂ :=
-  ⟨fun h => by cases h; assumption, Lex.inr⟩
-
-@[simp] theorem lex_inr_inl : ¬Lex r s (inr b) (inl a) := nofun
-
-instance instDecidableRelSumLex [DecidableRel r] [DecidableRel s] : DecidableRel (Lex r s)
-  | inl _, inl _ => decidable_of_iff' _ lex_inl_inl
-  | inl _, inr _ => Decidable.isTrue (Lex.sep _ _)
-  | inr _, inl _ => Decidable.isFalse lex_inr_inl
-  | inr _, inr _ => decidable_of_iff' _ lex_inr_inr
-
-end Lex
diff --git a/Batteries/Data/Sum/Lemmas.lean b/Batteries/Data/Sum/Lemmas.lean
deleted file mode 100644
index ffc24dcd76..0000000000
--- a/Batteries/Data/Sum/Lemmas.lean
+++ /dev/null
@@ -1,250 +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, Yury G. Kudryashov
--/
-
-import Batteries.Data.Sum.Basic
-import Batteries.Logic
-
-/-!
-# Disjoint union of types
-
-Theorems about the definitions introduced in `Batteries.Data.Sum.Basic`.
--/
-
-open Function
-
-namespace Sum
-
-@[simp] protected theorem «forall» {p : α ⊕ β → Prop} :
-    (∀ x, p x) ↔ (∀ a, p (inl a)) ∧ ∀ b, p (inr b) :=
-  ⟨fun h => ⟨fun _ => h _, fun _ => h _⟩, fun ⟨h₁, h₂⟩ => Sum.rec h₁ h₂⟩
-
-@[simp] protected theorem «exists» {p : α ⊕ β → Prop} :
-    (∃ x, p x) ↔ (∃ a, p (inl a)) ∨ ∃ b, p (inr b) :=
-  ⟨ fun
-    | ⟨inl a, h⟩ => Or.inl ⟨a, h⟩
-    | ⟨inr b, h⟩ => Or.inr ⟨b, h⟩,
-    fun
-    | Or.inl ⟨a, h⟩ => ⟨inl a, h⟩
-    | Or.inr ⟨b, h⟩ => ⟨inr b, h⟩⟩
-
-theorem forall_sum {γ : α ⊕ β → Sort _} (p : (∀ ab, γ ab) → Prop) :
-    (∀ fab, p fab) ↔ (∀ fa fb, p (Sum.rec fa fb)) := by
-  refine ⟨fun h fa fb => h _, fun h fab => ?_⟩
-  have h1 : fab = Sum.rec (fun a => fab (Sum.inl a)) (fun b => fab (Sum.inr b)) := by
-    ext ab; cases ab <;> rfl
-  rw [h1]; exact h _ _
-
-section get
-
-@[simp] theorem inl_getLeft : ∀ (x : α ⊕ β) (h : x.isLeft), inl (x.getLeft h) = x
-  | inl _, _ => rfl
-@[simp] theorem inr_getRight : ∀ (x : α ⊕ β) (h : x.isRight), inr (x.getRight h) = x
-  | inr _, _ => rfl
-
-@[simp] theorem getLeft?_eq_none_iff {x : α ⊕ β} : x.getLeft? = none ↔ x.isRight := by
-  cases x <;> simp only [getLeft?, isRight, eq_self_iff_true, reduceCtorEq]
-
-@[simp] theorem getRight?_eq_none_iff {x : α ⊕ β} : x.getRight? = none ↔ x.isLeft := by
-  cases x <;> simp only [getRight?, isLeft, eq_self_iff_true, reduceCtorEq]
-
-theorem eq_left_getLeft_of_isLeft : ∀ {x : α ⊕ β} (h : x.isLeft), x = inl (x.getLeft h)
-  | inl _, _ => rfl
-
-@[simp] theorem getLeft_eq_iff (h : x.isLeft) : x.getLeft h = a ↔ x = inl a := by
-  cases x <;> simp at h ⊢
-
-theorem eq_right_getRight_of_isRight : ∀ {x : α ⊕ β} (h : x.isRight), x = inr (x.getRight h)
-  | inr _, _ => rfl
-
-@[simp] theorem getRight_eq_iff (h : x.isRight) : x.getRight h = b ↔ x = inr b := by
-  cases x <;> simp at h ⊢
-
-@[simp] theorem getLeft?_eq_some_iff : x.getLeft? = some a ↔ x = inl a := by
-  cases x <;> simp only [getLeft?, Option.some.injEq, inl.injEq, reduceCtorEq]
-
-@[simp] theorem getRight?_eq_some_iff : x.getRight? = some b ↔ x = inr b := by
-  cases x <;> simp only [getRight?, Option.some.injEq, inr.injEq, reduceCtorEq]
-
-@[simp] theorem bnot_isLeft (x : α ⊕ β) : !x.isLeft = x.isRight := by cases x <;> rfl
-
-@[simp] theorem isLeft_eq_false {x : α ⊕ β} : x.isLeft = false ↔ x.isRight := by cases x <;> simp
-
-theorem not_isLeft {x : α ⊕ β} : ¬x.isLeft ↔ x.isRight := by simp
-
-@[simp] theorem bnot_isRight (x : α ⊕ β) : !x.isRight = x.isLeft := by cases x <;> rfl
-
-@[simp] theorem isRight_eq_false {x : α ⊕ β} : x.isRight = false ↔ x.isLeft := by cases x <;> simp
-
-theorem not_isRight {x : α ⊕ β} : ¬x.isRight ↔ x.isLeft := by simp
-
-theorem isLeft_iff : x.isLeft ↔ ∃ y, x = Sum.inl y := by cases x <;> simp
-
-theorem isRight_iff : x.isRight ↔ ∃ y, x = Sum.inr y := by cases x <;> simp
-
-end get
-
-theorem inl.inj_iff : (inl a : α ⊕ β) = inl b ↔ a = b := ⟨inl.inj, congrArg _⟩
-
-theorem inr.inj_iff : (inr a : α ⊕ β) = inr b ↔ a = b := ⟨inr.inj, congrArg _⟩
-
-theorem inl_ne_inr : inl a ≠ inr b := nofun
-
-theorem inr_ne_inl : inr b ≠ inl a := nofun
-
-/-! ### `Sum.elim` -/
-
-@[simp] theorem elim_comp_inl (f : α → γ) (g : β → γ) : Sum.elim f g ∘ inl = f :=
-  rfl
-
-@[simp] theorem elim_comp_inr (f : α → γ) (g : β → γ) : Sum.elim f g ∘ inr = g :=
-  rfl
-
-@[simp] theorem elim_inl_inr : @Sum.elim α β _ inl inr = id :=
-  funext fun x => Sum.casesOn x (fun _ => rfl) fun _ => rfl
-
-theorem comp_elim (f : γ → δ) (g : α → γ) (h : β → γ) :
-    f ∘ Sum.elim g h = Sum.elim (f ∘ g) (f ∘ h) :=
-  funext fun x => Sum.casesOn x (fun _ => rfl) fun _ => rfl
-
-@[simp] theorem elim_comp_inl_inr (f : α ⊕ β → γ) :
-    Sum.elim (f ∘ inl) (f ∘ inr) = f :=
-  funext fun x => Sum.casesOn x (fun _ => rfl) fun _ => rfl
-
-theorem elim_eq_iff {u u' : α → γ} {v v' : β → γ} :
-    Sum.elim u v = Sum.elim u' v' ↔ u = u' ∧ v = v' := by
-  simp [funext_iff]
-
-/-! ### `Sum.map` -/
-
-@[simp] theorem map_map (f' : α' → α'') (g' : β' → β'') (f : α → α') (g : β → β') :
-    ∀ x : Sum α β, (x.map f g).map f' g' = x.map (f' ∘ f) (g' ∘ g)
-  | inl _ => rfl
-  | inr _ => rfl
-
-@[simp] theorem map_comp_map (f' : α' → α'') (g' : β' → β'') (f : α → α') (g : β → β') :
-    Sum.map f' g' ∘ Sum.map f g = Sum.map (f' ∘ f) (g' ∘ g) :=
-  funext <| map_map f' g' f g
-
-@[simp] theorem map_id_id : Sum.map (@id α) (@id β) = id :=
-  funext fun x => Sum.recOn x (fun _ => rfl) fun _ => rfl
-
-theorem elim_map {f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ} {g₂ : δ → ε} {x} :
-    Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) x := by
-  cases x <;> rfl
-
-theorem elim_comp_map {f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ} {g₂ : δ → ε} :
-    Sum.elim f₂ g₂ ∘ Sum.map f₁ g₁ = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) :=
-  funext fun _ => elim_map
-
-@[simp] theorem isLeft_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
-    isLeft (x.map f g) = isLeft x := by
-  cases x <;> rfl
-
-@[simp] theorem isRight_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
-    isRight (x.map f g) = isRight x := by
-  cases x <;> rfl
-
-@[simp] theorem getLeft?_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
-    (x.map f g).getLeft? = x.getLeft?.map f := by
-  cases x <;> rfl
-
-@[simp] theorem getRight?_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
-    (x.map f g).getRight? = x.getRight?.map g := by cases x <;> rfl
-
-/-! ### `Sum.swap` -/
-
-@[simp] theorem swap_swap (x : α ⊕ β) : swap (swap x) = x := by cases x <;> rfl
-
-@[simp] theorem swap_swap_eq : swap ∘ swap = @id (α ⊕ β) := funext <| swap_swap
-
-@[simp] theorem isLeft_swap (x : α ⊕ β) : x.swap.isLeft = x.isRight := by cases x <;> rfl
-
-@[simp] theorem isRight_swap (x : α ⊕ β) : x.swap.isRight = x.isLeft := by cases x <;> rfl
-
-@[simp] theorem getLeft?_swap (x : α ⊕ β) : x.swap.getLeft? = x.getRight? := by cases x <;> rfl
-
-@[simp] theorem getRight?_swap (x : α ⊕ β) : x.swap.getRight? = x.getLeft? := by cases x <;> rfl
-
-section LiftRel
-
-theorem LiftRel.mono (hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ a b, s₁ a b → s₂ a b)
-  (h : LiftRel r₁ s₁ x y) : LiftRel r₂ s₂ x y := by
-  cases h
-  · exact LiftRel.inl (hr _ _ ‹_›)
-  · exact LiftRel.inr (hs _ _ ‹_›)
-
-theorem LiftRel.mono_left (hr : ∀ a b, r₁ a b → r₂ a b) (h : LiftRel r₁ s x y) :
-    LiftRel r₂ s x y :=
-  (h.mono hr) fun _ _ => id
-
-theorem LiftRel.mono_right (hs : ∀ a b, s₁ a b → s₂ a b) (h : LiftRel r s₁ x y) :
-    LiftRel r s₂ x y :=
-  h.mono (fun _ _ => id) hs
-
-protected theorem LiftRel.swap (h : LiftRel r s x y) : LiftRel s r x.swap y.swap := by
-  cases h
-  · exact LiftRel.inr ‹_›
-  · exact LiftRel.inl ‹_›
-
-@[simp] theorem liftRel_swap_iff : LiftRel s r x.swap y.swap ↔ LiftRel r s x y :=
-  ⟨fun h => by rw [← swap_swap x, ← swap_swap y]; exact h.swap, LiftRel.swap⟩
-
-end LiftRel
-
-section Lex
-
-protected theorem LiftRel.lex {a b : α ⊕ β} (h : LiftRel r s a b) : Lex r s a b := by
-  cases h
-  · exact Lex.inl ‹_›
-  · exact Lex.inr ‹_›
-
-theorem liftRel_subrelation_lex : Subrelation (LiftRel r s) (Lex r s) := LiftRel.lex
-
-theorem Lex.mono (hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ a b, s₁ a b → s₂ a b) (h : Lex r₁ s₁ x y) :
-    Lex r₂ s₂ x y := by
-  cases h
-  · exact Lex.inl (hr _ _ ‹_›)
-  · exact Lex.inr (hs _ _ ‹_›)
-  · exact Lex.sep _ _
-
-theorem Lex.mono_left (hr : ∀ a b, r₁ a b → r₂ a b) (h : Lex r₁ s x y) : Lex r₂ s x y :=
-  (h.mono hr) fun _ _ => id
-
-theorem Lex.mono_right (hs : ∀ a b, s₁ a b → s₂ a b) (h : Lex r s₁ x y) : Lex r s₂ x y :=
-  h.mono (fun _ _ => id) hs
-
-theorem lex_acc_inl (aca : Acc r a) : Acc (Lex r s) (inl a) := by
-  induction aca with
-  | intro _ _ IH =>
-    constructor
-    intro y h
-    cases h with
-    | inl h' => exact IH _ h'
-
-theorem lex_acc_inr (aca : ∀ a, Acc (Lex r s) (inl a)) {b} (acb : Acc s b) :
-    Acc (Lex r s) (inr b) := by
-  induction acb with
-  | intro _ _ IH =>
-    constructor
-    intro y h
-    cases h with
-    | inr h' => exact IH _ h'
-    | sep => exact aca _
-
-theorem lex_wf (ha : WellFounded r) (hb : WellFounded s) : WellFounded (Lex r s) :=
-  have aca : ∀ a, Acc (Lex r s) (inl a) := fun a => lex_acc_inl (ha.apply a)
-  ⟨fun x => Sum.recOn x aca fun b => lex_acc_inr aca (hb.apply b)⟩
-
-end Lex
-
-theorem elim_const_const (c : γ) :
-    Sum.elim (const _ c : α → γ) (const _ c : β → γ) = const _ c := by
-  ext x
-  cases x <;> rfl
-
-@[simp] theorem elim_lam_const_lam_const (c : γ) :
-    Sum.elim (fun _ : α => c) (fun _ : β => c) = fun _ => c :=
-  Sum.elim_const_const c
diff --git a/Batteries/Data/UInt.lean b/Batteries/Data/UInt.lean
index a7c2a4cbaa..3f9b495629 100644
--- a/Batteries/Data/UInt.lean
+++ b/Batteries/Data/UInt.lean
@@ -12,9 +12,6 @@ import Batteries.Classes.Order
 
 @[simp] theorem UInt8.val_val_eq_toNat (x : UInt8) : x.val.val = x.toNat := rfl
 
-@[simp] theorem UInt8.val_ofNat (n) :
-    (no_index (OfNat.ofNat n) : UInt8).val = OfNat.ofNat n := rfl
-
 @[simp] theorem UInt8.toNat_ofNat (n) :
     (no_index (OfNat.ofNat n) : UInt8).toNat = n % UInt8.size := rfl
 
@@ -49,9 +46,6 @@ instance : Batteries.LawfulOrd UInt8 := .compareOfLessAndEq
 
 @[simp] theorem UInt16.val_val_eq_toNat (x : UInt16) : x.val.val = x.toNat := rfl
 
-@[simp] theorem UInt16.val_ofNat (n) :
-    (no_index (OfNat.ofNat n) : UInt16).val = OfNat.ofNat n := rfl
-
 @[simp] theorem UInt16.toNat_ofNat (n) :
     (no_index (OfNat.ofNat n) : UInt16).toNat = n % UInt16.size := rfl
 
@@ -86,9 +80,6 @@ instance : Batteries.LawfulOrd UInt16 := .compareOfLessAndEq
 
 @[simp] theorem UInt32.val_val_eq_toNat (x : UInt32) : x.val.val = x.toNat := rfl
 
-@[simp] theorem UInt32.val_ofNat (n) :
-    (no_index (OfNat.ofNat n) : UInt32).val = OfNat.ofNat n := rfl
-
 @[simp] theorem UInt32.toNat_ofNat (n) :
     (no_index (OfNat.ofNat n) : UInt32).toNat = n % UInt32.size := rfl
 
@@ -123,9 +114,6 @@ instance : Batteries.LawfulOrd UInt32 := .compareOfLessAndEq
 
 @[simp] theorem UInt64.val_val_eq_toNat (x : UInt64) : x.val.val = x.toNat := rfl
 
-@[simp] theorem UInt64.val_ofNat (n) :
-    (no_index (OfNat.ofNat n) : UInt64).val = OfNat.ofNat n := rfl
-
 @[simp] theorem UInt64.toNat_ofNat (n) :
     (no_index (OfNat.ofNat n) : UInt64).toNat = n % UInt64.size := rfl
 
@@ -160,15 +148,11 @@ instance : Batteries.LawfulOrd UInt64 := .compareOfLessAndEq
 
 @[simp] theorem USize.val_val_eq_toNat (x : USize) : x.val.val = x.toNat := rfl
 
-@[simp] theorem USize.val_ofNat (n) :
-    (no_index (OfNat.ofNat n) : USize).val = OfNat.ofNat n := rfl
-
 @[simp] theorem USize.toNat_ofNat (n) :
     (no_index (OfNat.ofNat n) : USize).toNat = n % USize.size := rfl
 
 theorem USize.size_eq : USize.size = 2 ^ System.Platform.numBits := by
-  have : 1 ≤ 2 ^ System.Platform.numBits := Nat.succ_le_of_lt (Nat.two_pow_pos _)
-  rw [USize.size, Nat.sub_add_cancel this]
+  rw [USize.size]
 
 theorem USize.le_size : 2 ^ 32 ≤ USize.size := by
   rw [size_eq]
diff --git a/Batteries/Data/UnionFind/Basic.lean b/Batteries/Data/UnionFind/Basic.lean
index ce9c99a77e..c48bb5bda1 100644
--- a/Batteries/Data/UnionFind/Basic.lean
+++ b/Batteries/Data/UnionFind/Basic.lean
@@ -161,11 +161,11 @@ theorem rankD_lt_rankMax (self : UnionFind) (i : Nat) :
 theorem lt_rankMax (self : UnionFind) (i : Nat) : self.rank i < self.rankMax := rankD_lt_rankMax ..
 
 theorem push_rankD (arr : Array UFNode) : rankD (arr.push ⟨arr.size, 0⟩) i = rankD arr i := by
-  simp only [rankD, Array.size_push, Array.get_eq_getElem, Array.get_push, dite_eq_ite]
+  simp only [rankD, Array.size_push, Array.get_eq_getElem, Array.getElem_push, dite_eq_ite]
   split <;> split <;> first | simp | cases ‹¬_› (Nat.lt_succ_of_lt ‹_›)
 
 theorem push_parentD (arr : Array UFNode) : parentD (arr.push ⟨arr.size, 0⟩) i = parentD arr i := by
-  simp only [parentD, Array.size_push, Array.get_eq_getElem, Array.get_push, dite_eq_ite]
+  simp only [parentD, Array.size_push, Array.get_eq_getElem, Array.getElem_push, dite_eq_ite]
   split <;> split <;> try simp
   · exact Nat.le_antisymm (Nat.ge_of_not_lt ‹_›) (Nat.le_of_lt_succ ‹_›)
   · cases ‹¬_› (Nat.lt_succ_of_lt ‹_›)
diff --git a/Batteries/Data/UnionFind/Lemmas.lean b/Batteries/Data/UnionFind/Lemmas.lean
index a42ece4508..9a7b0dac58 100644
--- a/Batteries/Data/UnionFind/Lemmas.lean
+++ b/Batteries/Data/UnionFind/Lemmas.lean
@@ -16,7 +16,7 @@ namespace Batteries.UnionFind
 
 @[simp] theorem parentD_push {arr : Array UFNode} :
     parentD (arr.push ⟨arr.size, 0⟩) a = parentD arr a := by
-  simp [parentD]; split <;> split <;> try simp [Array.get_push, *]
+  simp [parentD]; split <;> split <;> try simp [Array.getElem_push, *]
   · next h1 h2 =>
     simp [Nat.lt_succ] at h1 h2
     exact Nat.le_antisymm h2 h1
@@ -26,7 +26,7 @@ namespace Batteries.UnionFind
 
 @[simp] theorem rankD_push {arr : Array UFNode} :
     rankD (arr.push ⟨arr.size, 0⟩) a = rankD arr a := by
-  simp [rankD]; split <;> split <;> try simp [Array.get_push, *]
+  simp [rankD]; split <;> split <;> try simp [Array.getElem_push, *]
   next h1 h2 => cases h1 (Nat.lt_succ_of_lt h2)
 
 @[simp] theorem rank_push {m : UnionFind} : m.push.rank a = m.rank a := by simp [rank]
diff --git a/Batteries/Data/Vector/Basic.lean b/Batteries/Data/Vector/Basic.lean
index 534f94030a..2d4708d5b2 100644
--- a/Batteries/Data/Vector/Basic.lean
+++ b/Batteries/Data/Vector/Basic.lean
@@ -238,11 +238,13 @@ Otherwise it panics The old entry is returned with the modified vector.
 def range (n : Nat) : Vector Nat n := ⟨Array.range n, Array.size_range ..⟩
 
 /--
-`shrink v m` shrinks the vector to the first `m` elements if `m < n`.
+`take v m` shrinks the vector to the first `m` elements if `m < n`.
 Returns `v` unchanged if `m ≥ n`.
 -/
-def shrink (v : Vector α n) (m : Nat) : Vector α (min n m) :=
-  ⟨v.toArray.shrink m, by simp [Array.size_shrink, v.size_eq]⟩
+def take (v : Vector α n) (m : Nat) : Vector α (min n m) :=
+  ⟨v.toArray.take m, by simp [Array.size_take, v.size_eq, Nat.min_comm]⟩
+
+@[deprecated (since := "2024-10-22")] alias shrink := take
 
 /--
 Drops the first (up to) `i` elements from a vector of length `n`.
@@ -252,12 +254,6 @@ def drop (i : Nat) (v : Vector α n) : Vector α (n - i) :=
   have : min n n - i = n - i := by rw [Nat.min_self]
   Vector.cast this (extract v i n)
 
-/--
-Takes the first (up to) `i` elements from a vector of length `n`.
-
--/
-alias take := shrink
-
 /--
 `isEqv` takes a given boolean property `p`. It returns `true`
 if and only if `p a[i] b[i]` holds true for all valid indices `i`.
diff --git a/Batteries/Data/Vector/Lemmas.lean b/Batteries/Data/Vector/Lemmas.lean
index 0f8caa5c45..d40c7b79cb 100644
--- a/Batteries/Data/Vector/Lemmas.lean
+++ b/Batteries/Data/Vector/Lemmas.lean
@@ -19,6 +19,26 @@ namespace Batteries
 
 namespace Vector
 
+attribute [simp] Vector.size_eq
+
+@[simp] theorem length_toList {α n} (xs : Vector α n) : xs.toList.length = n :=
+  xs.size_eq
+
+@[simp] theorem getElem_mk {data : Array α} {size : data.size = n} {i : Nat} (h : i < n) :
+    (Vector.mk data size)[i] = data[i] := rfl
+
+@[simp] theorem getElem_toArray {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toArray.size) :
+    xs.toArray[i] = xs[i]'(by simpa using h) := by
+  cases xs
+  simp
+
+@[simp] theorem getElem_toList {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toList.length) :
+    xs.toList[i] = xs[i]'(by simpa using h) := by
+  simp [toList]
+
+@[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) :
+    (Vector.ofFn f)[i] = f ⟨i, by simpa using h⟩ := by
+  simp [ofFn]
 
 /-- An `empty` vector maps to a `empty` vector. -/
 @[simp]
@@ -47,9 +67,6 @@ protected theorem ext {a b : Vector α n} (h : (i : Nat) → (_ : i < n) → a[i
     rw [a.size_eq] at hi
     exact h i hi
 
-@[simp] theorem getElem_mk {data : Array α} {size : data.size = n} {i : Nat} (h : i < n) :
-    (Vector.mk data size)[i] = data[i] := rfl
-
 @[simp] theorem push_mk {data : Array α} {size : data.size = n} {x : α} :
     (Vector.mk data size).push x =
       Vector.mk (data.push x) (by simp [size, Nat.succ_eq_add_one]) := rfl
@@ -65,7 +82,7 @@ protected theorem ext {a b : Vector α n} (h : (i : Nat) → (_ : i < n) → a[i
 @[simp, nolint simpNF] theorem getElem_push_lt {v : Vector α n} {x : α} {i : Nat} (h : i < n) :
     (v.push x)[i] = v[i] := by
   rcases v with ⟨data, rfl⟩
-  simp [Array.get_push_lt, h]
+  simp [Array.getElem_push_lt, h]
 
 @[simp] theorem getElem_pop {v : Vector α n} {i : Nat} (h : i < n - 1) : (v.pop)[i] = v[i] := by
   rcases v with ⟨data, rfl⟩
diff --git a/Batteries/Lean/Expr.lean b/Batteries/Lean/Expr.lean
index d1c568f3e4..9ac9a09238 100644
--- a/Batteries/Lean/Expr.lean
+++ b/Batteries/Lean/Expr.lean
@@ -39,16 +39,6 @@ def forallArity : Expr → Nat
 -- @[deprecated (since := "2024-10-16"), inherit_doc getNumHeadForalls]
 -- abbrev forallArity := @getNumHeadForalls
 
-/-- Like `getAppNumArgs` but ignores metadata. -/
-def getAppNumArgs' (e : Expr) : Nat :=
-  go e 0
-where
-  /-- Auxiliary definition for `getAppNumArgs'`. -/
-  go : Expr → Nat → Nat
-    | mdata _ b, n => go b n
-    | app f _  , n => go f (n + 1)
-    | _        , n => n
-
 /-- Like `withApp` but ignores metadata. -/
 @[inline]
 def withApp' (e : Expr) (k : Expr → Array Expr → α) : α :=
diff --git a/Batteries/Logic.lean b/Batteries/Logic.lean
index 70091ae973..4bc5f9f102 100644
--- a/Batteries/Logic.lean
+++ b/Batteries/Logic.lean
@@ -57,9 +57,6 @@ theorem funext₃ {β : α → Sort _} {γ : ∀ a, β a → Sort _} {δ : ∀ a
 @[deprecated (since := "2024-10-17")]
 protected alias Function.funext_iff := funext_iff
 
-theorem ne_of_apply_ne {α β : Sort _} (f : α → β) {x y : α} : f x ≠ f y → x ≠ y :=
-  mt <| congrArg _
-
 protected theorem Eq.congr (h₁ : x₁ = y₁) (h₂ : x₂ = y₂) : x₁ = x₂ ↔ y₁ = y₂ := by
   subst h₁; subst h₂; rfl
 
@@ -102,17 +99,6 @@ theorem heq_eqRec_iff_heq {α : Sort _} {a : α} {motive : (a' : α) → a = a'
     HEq y (@Eq.rec α a motive x a' e) ↔ HEq y x := by
   subst e; rfl
 
-/-! ## membership -/
-
-section Mem
-variable [Membership α β] {s t : β} {a b : α}
-
-theorem ne_of_mem_of_not_mem (h : a ∈ s) : b ∉ s → a ≠ b := mt fun e => e ▸ h
-
-theorem ne_of_mem_of_not_mem' (h : a ∈ s) : a ∉ t → s ≠ t := mt fun e => e ▸ h
-
-end Mem
-
 /-! ## miscellaneous -/
 
 @[simp] theorem not_nonempty_empty  : ¬Nonempty Empty := fun ⟨h⟩ => h.elim
diff --git a/Batteries/Tactic/Alias.lean b/Batteries/Tactic/Alias.lean
index 471dfd883a..1f22940b0a 100644
--- a/Batteries/Tactic/Alias.lean
+++ b/Batteries/Tactic/Alias.lean
@@ -109,10 +109,7 @@ elab (name := alias) mods:declModifiers "alias " alias:ident " := " name:ident :
       addDecl decl
     else
       addAndCompile decl
-    Lean.addDeclarationRanges declName {
-      range := ← getDeclarationRange (← getRef)
-      selectionRange := ← getDeclarationRange alias
-    }
+    addDeclarationRangesFromSyntax declName (← getRef) alias
     Term.addTermInfo' alias (← mkConstWithLevelParams declName) (isBinder := true)
     addDocString' declName declMods.docString?
     Term.applyAttributes declName declMods.attrs
@@ -174,16 +171,10 @@ elab (name := aliasLR) mods:declModifiers "alias "
     if let `(binderIdent| $idFwd:ident) := aliasFwd then
       let (declName, _) ← mkDeclName (← getCurrNamespace) declMods idFwd.getId
       addSide true declName declMods thm
-      Lean.addDeclarationRanges declName {
-        range := ← getDeclarationRange (← getRef)
-        selectionRange := ← getDeclarationRange idFwd
-      }
+      addDeclarationRangesFromSyntax declName (← getRef) idFwd
       Term.addTermInfo' idFwd (← mkConstWithLevelParams declName) (isBinder := true)
     if let `(binderIdent| $idRev:ident) := aliasRev then
       let (declName, _) ← mkDeclName (← getCurrNamespace) declMods idRev.getId
       addSide false declName declMods thm
-      Lean.addDeclarationRanges declName {
-        range := ← getDeclarationRange (← getRef)
-        selectionRange := ← getDeclarationRange idRev
-      }
+      addDeclarationRangesFromSyntax declName (← getRef) idRev
       Term.addTermInfo' idRev (← mkConstWithLevelParams declName) (isBinder := true)
diff --git a/Batteries/Tactic/Classical.lean b/Batteries/Tactic/Classical.lean
deleted file mode 100644
index a3bc78b0a4..0000000000
--- a/Batteries/Tactic/Classical.lean
+++ /dev/null
@@ -1,41 +0,0 @@
-/-
-Copyright (c) 2021 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro
--/
-import Lean.Elab.Tactic.Basic
-
-/-! # `classical` tactic -/
-
-namespace Batteries.Tactic
-open Lean Meta Elab.Tactic
-
-/--
-`classical t` runs `t` in a scope where `Classical.propDecidable` is a low priority
-local instance.
--/
-def classical [Monad m] [MonadEnv m] [MonadFinally m] [MonadLiftT MetaM m] (t : m α) :
-    m α := do
-  modifyEnv Meta.instanceExtension.pushScope
-  Meta.addInstance ``Classical.propDecidable .local 10
-  try
-    t
-  finally
-    modifyEnv Meta.instanceExtension.popScope
-
-/-- `classical!` has been removed; use `classical` instead -/
--- Deprecated 2024-04-19
-elab "classical!" : tactic => do
-  throwError "`classical!` has been removed; use `classical` instead"
-
-/--
-`classical tacs` runs `tacs` in a scope where `Classical.propDecidable` is a low priority
-local instance.
-
-Note that (unlike lean 3) `classical` is a scoping tactic - it adds the instance only within the
-scope of the tactic.
--/
--- FIXME: using ppDedent looks good in the common case, but produces the incorrect result when
--- the `classical` does not scope over the rest of the block.
-elab "classical" tacs:ppDedent(tacticSeq) : tactic => do
-  classical <| Elab.Tactic.evalTactic tacs
diff --git a/Batteries/Tactic/HelpCmd.lean b/Batteries/Tactic/HelpCmd.lean
index 7fbe67bf3a..1d955310a0 100644
--- a/Batteries/Tactic/HelpCmd.lean
+++ b/Batteries/Tactic/HelpCmd.lean
@@ -306,7 +306,7 @@ elab "#help " colGt &"note" colGt ppSpace name:strLit : command => do
   let valid_entries := imported_entries_filtered ++ local_entries.filterMap
     fun x => if label_prefix.isPrefixOf x.fst then some x else none
   let grouped_valid_entries := valid_entries.mergeSort (·.fst ≤ ·.fst)
-    |>.groupBy (·.fst == ·.fst)
+    |>.splitBy (·.fst == ·.fst)
 
   -- display results in a readable style
   if grouped_valid_entries.isEmpty then
diff --git a/Batteries/Tactic/PrintPrefix.lean b/Batteries/Tactic/PrintPrefix.lean
index dbedad072f..42b879b9b7 100644
--- a/Batteries/Tactic/PrintPrefix.lean
+++ b/Batteries/Tactic/PrintPrefix.lean
@@ -27,7 +27,7 @@ structure PrintPrefixConfig where
   internals : Bool := false
 
 /-- Function elaborating `Config`. -/
-declare_config_elab elabPrintPrefixConfig PrintPrefixConfig
+declare_command_config_elab elabPrintPrefixConfig PrintPrefixConfig
 
 /--
 `reverseName name` reverses the components of a name.
@@ -109,11 +109,12 @@ The complete set of flags can be seen in the documentation
 for `Lean.Elab.Command.PrintPrefixConfig`.
 -/
 elab (name := printPrefix) tk:"#print " colGt "prefix"
-    cfg:(Lean.Parser.Tactic.config)? name:(ident)? : command => liftTermElabM do
+    cfg:Lean.Parser.Tactic.optConfig name:(ident)? : command => do
   if let some name := name then
-    let opts ← elabPrintPrefixConfig (mkOptionalNode cfg)
-    let mut msgs ← matchingConstants opts name.getId
-    if msgs.isEmpty then
-      if let [name] ← resolveGlobalConst name then
-        msgs ← matchingConstants opts name
-    logInfoAt tk (.joinSep msgs.toList "")
+    let opts ← elabPrintPrefixConfig cfg
+    liftTermElabM do
+      let mut msgs ← matchingConstants opts name.getId
+      if msgs.isEmpty then
+        if let [name] ← resolveGlobalConst name then
+          msgs ← matchingConstants opts name
+      logInfoAt tk (.joinSep msgs.toList "")
diff --git a/Batteries/Util/LibraryNote.lean b/Batteries/Util/LibraryNote.lean
index 3d578c342b..8268c757ca 100644
--- a/Batteries/Util/LibraryNote.lean
+++ b/Batteries/Util/LibraryNote.lean
@@ -21,7 +21,7 @@ deriving Inhabited
 initialize libraryNoteExt : SimplePersistentEnvExtension LibraryNoteEntry (Array LibraryNoteEntry) ←
   registerSimplePersistentEnvExtension {
     addEntryFn := Array.push
-    addImportedFn := Array.concatMap id
+    addImportedFn := Array.flatMap id
   }
 
 open Lean Parser Command in
diff --git a/lean-toolchain b/lean-toolchain
index eff86fd63d..0bef727630 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.13.0-rc3
+leanprover/lean4:v4.14.0-rc1
diff --git a/test/array.lean b/test/array.lean
index 2ba3a29577..89f784293e 100644
--- a/test/array.lean
+++ b/test/array.lean
@@ -10,7 +10,7 @@ variable (g : i < (a.set! i v).size)
 variable (j_lt : j < (a.set! i v).size)
 
 #check_simp (a.set! i v).get ⟨i, g⟩ ~> v
-#check_simp (a.set! i v).get! i ~> if i < a.size then v else default
+#check_simp (a.set! i v).get! i ~> (a.setD i v)[i]!
 #check_simp (a.set! i v).getD i d ~> if i < a.size then v else d
 #check_simp (a.set! i v)[i] ~> v
 
diff --git a/test/case.lean b/test/case.lean
index 4e7892d964..b8e3444d1d 100644
--- a/test/case.lean
+++ b/test/case.lean
@@ -182,16 +182,6 @@ example : True ∧ ∀ x : Nat, x = x := by
   rfl
 
 -- Test focusing by full match, suffix match, and prefix match
-/--
-warning: unused variable `x`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
----
-warning: unused variable `y`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
----
-warning: unused variable `z`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
--/
 #guard_msgs in
 example : True := by
   have x : Bool := ?a
diff --git a/test/classical.lean b/test/classical.lean
deleted file mode 100644
index d2d460253c..0000000000
--- a/test/classical.lean
+++ /dev/null
@@ -1,23 +0,0 @@
-import Batteries.Tactic.Classical
-import Batteries.Tactic.PermuteGoals
-
-example : Bool := by
-  fail_if_success have := ∀ p, decide p -- no classical in scope
-  classical
-  have := ∀ p, decide p -- uses the classical instance
-  guard_expr decide (0 < 1) = @decide (0 < 1) (Nat.decLt 0 1)
-  exact decide (0 < 1) -- will use the decidable instance
-
--- double check no leakage
-example : Bool := by
-  fail_if_success have := ∀ p, decide p -- no classical in scope
-  exact decide (0 < 1) -- uses the decidable instance
-
--- check that classical respects tactic blocks
-example : Bool := by
-  fail_if_success have := ∀ p, decide p -- no classical in scope
-  on_goal 1 =>
-    classical
-    have := ∀ p, decide p -- uses the classical instance
-  fail_if_success have := ∀ p, decide p -- no classical in scope again
-  exact decide (0 < 1) -- will use the decidable instance
diff --git a/test/congr.lean b/test/congr.lean
index 065a899f99..eee4c6dbac 100644
--- a/test/congr.lean
+++ b/test/congr.lean
@@ -38,11 +38,9 @@ section
 -- In order to preserve the test behaviour we locally remove the `ext` attribute.
 attribute [-ext] List.ext_getElem?
 
-private opaque List.sum : List Nat → Nat
-
 example {ls : List Nat} :
-    (ls.map fun x => (ls.map fun y => 1 + y).sum + 1) =
-    (ls.map fun x => (ls.map fun y => Nat.succ y).sum + 1) := by
+    (ls.map fun _ => (ls.map fun y => 1 + y).sum + 1) =
+    (ls.map fun _ => (ls.map fun y => Nat.succ y).sum + 1) := by
   rcongr (_x y)
   guard_target =ₐ 1 + y = y.succ
   rw [Nat.add_comm]
diff --git a/test/help_cmd.lean b/test/help_cmd.lean
index 57e214cafd..23e3698b6d 100644
--- a/test/help_cmd.lean
+++ b/test/help_cmd.lean
@@ -184,22 +184,106 @@ error: no command declarations start with foobarbaz
 #help command foobarbaz
 
 /--
-info:
-syntax "#eval"... [Lean.Parser.Command.eval]
+info: syntax "#eval"... [Lean.Parser.Command.eval]
+  `#eval e` evaluates the expression `e` by compiling and evaluating it.
+  ⏎
+  * The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
+  * If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
+    to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
+    Users can define `MonadEval` instances to extend the list of supported monads.
+  ⏎
+  The `#eval` command gracefully degrades in capability depending on what is imported.
+  Importing the `Lean.Elab.Command` module provides full capabilities.
+  ⏎
+  Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
+  since the presence of `sorry` can lead to runtime instability and crashes.
+  This check can be overridden with the `#eval! e` command.
+  ⏎
+  Options:
+  * If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
+    usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
+  * If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
+  * If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
+    when there is no other way to print the result.
+  ⏎
+  See also: `#reduce e` for evaluation by term reduction.
 
 syntax "#eval!"... [Lean.Parser.Command.evalBang]
-
-syntax "#exit"... [Lean.Parser.Command.exit]
+  `#eval e` evaluates the expression `e` by compiling and evaluating it.
+  ⏎
+  * The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
+  * If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
+    to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
+    Users can define `MonadEval` instances to extend the list of supported monads.
+  ⏎
+  The `#eval` command gracefully degrades in capability depending on what is imported.
+  Importing the `Lean.Elab.Command` module provides full capabilities.
+  ⏎
+  Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
+  since the presence of `sorry` can lead to runtime instability and crashes.
+  This check can be overridden with the `#eval! e` command.
+  ⏎
+  Options:
+  * If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
+    usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
+  * If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
+  * If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
+    when there is no other way to print the result.
+  ⏎
+  See also: `#reduce e` for evaluation by term reduction.  syntax "#exit"... [Lean.Parser.Command.exit]
 -/
 #guard_msgs in
 #help command "#e"
 
 /--
-info:
-syntax "#eval"... [Lean.Parser.Command.eval]
+info: syntax "#eval"... [Lean.Parser.Command.eval]
+  `#eval e` evaluates the expression `e` by compiling and evaluating it.
+  ⏎
+  * The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
+  * If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
+    to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
+    Users can define `MonadEval` instances to extend the list of supported monads.
+  ⏎
+  The `#eval` command gracefully degrades in capability depending on what is imported.
+  Importing the `Lean.Elab.Command` module provides full capabilities.
+  ⏎
+  Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
+  since the presence of `sorry` can lead to runtime instability and crashes.
+  This check can be overridden with the `#eval! e` command.
+  ⏎
+  Options:
+  * If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
+    usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
+  * If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
+  * If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
+    when there is no other way to print the result.
+  ⏎
+  See also: `#reduce e` for evaluation by term reduction.
 + command elab Lean.Elab.Command.elabEval
 
 syntax "#eval!"... [Lean.Parser.Command.evalBang]
+  `#eval e` evaluates the expression `e` by compiling and evaluating it.
+  ⏎
+  * The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
+  * If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
+    to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
+    Users can define `MonadEval` instances to extend the list of supported monads.
+  ⏎
+  The `#eval` command gracefully degrades in capability depending on what is imported.
+  Importing the `Lean.Elab.Command` module provides full capabilities.
+  ⏎
+  Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
+  since the presence of `sorry` can lead to runtime instability and crashes.
+  This check can be overridden with the `#eval! e` command.
+  ⏎
+  Options:
+  * If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
+    usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
+  * If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
+  * If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
+    when there is no other way to print the result.
+  ⏎
+  See also: `#reduce e` for evaluation by term reduction.
 + command elab Lean.Elab.Command.elabEvalBang
 
 syntax "#exit"... [Lean.Parser.Command.exit]
diff --git a/test/lint_simpNF.lean b/test/lint_simpNF.lean
index e06e067d18..c9c8f9d307 100644
--- a/test/lint_simpNF.lean
+++ b/test/lint_simpNF.lean
@@ -2,9 +2,6 @@ import Batteries.Tactic.Lint
 
 set_option linter.missingDocs false
 
-protected def Sum.elim {α β γ : Sort _} (f : α → γ) (g : β → γ) : Sum α β → γ :=
-  fun x => Sum.casesOn x f g
-
 structure Equiv (α : Sort _) (β : Sort _) where
   toFun : α → β
   invFun : β → α
diff --git a/test/print_prefix.lean b/test/print_prefix.lean
index 0d14e95aa3..32467e4b37 100644
--- a/test/print_prefix.lean
+++ b/test/print_prefix.lean
@@ -14,7 +14,7 @@ TEmpty.recOn.{u} (motive : TEmpty → Sort u) (t : TEmpty) : motive t
 
 /-- info: -/
 #guard_msgs in
-#print prefix (config := {imported := false}) Empty
+#print prefix -imported Empty
 
 namespace EmptyPrefixTest
 
@@ -52,10 +52,10 @@ TestStruct.casesOn.{u} {motive : TestStruct → Sort u} (t : TestStruct)
   (mk : (foo bar : Int) → motive { foo := foo, bar := bar }) : motive t
 TestStruct.foo (self : TestStruct) : Int
 TestStruct.mk (foo bar : Int) : TestStruct
-TestStruct.mk.inj {foo bar : Int} :
-  ∀ {foo_1 bar_1 : Int}, { foo := foo, bar := bar } = { foo := foo_1, bar := bar_1 } → foo = foo_1 ∧ bar = bar_1
-TestStruct.mk.injEq (foo bar : Int) :
-  ∀ (foo_1 bar_1 : Int), ({ foo := foo, bar := bar } = { foo := foo_1, bar := bar_1 }) = (foo = foo_1 ∧ bar = bar_1)
+TestStruct.mk.inj {foo bar foo✝ bar✝ : Int} :
+  { foo := foo, bar := bar } = { foo := foo✝, bar := bar✝ } → foo = foo✝ ∧ bar = bar✝
+TestStruct.mk.injEq (foo bar foo✝ bar✝ : Int) :
+  ({ foo := foo, bar := bar } = { foo := foo✝, bar := bar✝ }) = (foo = foo✝ ∧ bar = bar✝)
 TestStruct.mk.sizeOf_spec (foo bar : Int) : sizeOf { foo := foo, bar := bar } = 1 + sizeOf foo + sizeOf bar
 TestStruct.noConfusion.{u} {P : Sort u} {v1 v2 : TestStruct} (h12 : v1 = v2) : TestStruct.noConfusionType P v1 v2
 TestStruct.noConfusionType.{u} (P : Sort u) (v1 v2 : TestStruct) : Sort u
@@ -82,17 +82,17 @@ TestStruct.recOn.{u} {motive : TestStruct → Sort u} (t : TestStruct)
   (mk : (foo bar : Int) → motive { foo := foo, bar := bar }) : motive t
 -/
 #guard_msgs in
-#print prefix (config := {propositions := false}) TestStruct
+#print prefix -propositions TestStruct
 
 /--
-info: TestStruct.mk.inj {foo bar : Int} :
-  ∀ {foo_1 bar_1 : Int}, { foo := foo, bar := bar } = { foo := foo_1, bar := bar_1 } → foo = foo_1 ∧ bar = bar_1
-TestStruct.mk.injEq (foo bar : Int) :
-  ∀ (foo_1 bar_1 : Int), ({ foo := foo, bar := bar } = { foo := foo_1, bar := bar_1 }) = (foo = foo_1 ∧ bar = bar_1)
+info: TestStruct.mk.inj {foo bar foo✝ bar✝ : Int} :
+  { foo := foo, bar := bar } = { foo := foo✝, bar := bar✝ } → foo = foo✝ ∧ bar = bar✝
+TestStruct.mk.injEq (foo bar foo✝ bar✝ : Int) :
+  ({ foo := foo, bar := bar } = { foo := foo✝, bar := bar✝ }) = (foo = foo✝ ∧ bar = bar✝)
 TestStruct.mk.sizeOf_spec (foo bar : Int) : sizeOf { foo := foo, bar := bar } = 1 + sizeOf foo + sizeOf bar
 -/
 #guard_msgs in
-#print prefix (config := {propositionsOnly := true}) TestStruct
+#print prefix +propositionsOnly TestStruct
 
 /--
 info: TestStruct
@@ -109,7 +109,7 @@ TestStruct.rec
 TestStruct.recOn
 -/
 #guard_msgs in
-#print prefix (config := {showTypes := false}) TestStruct
+#print prefix -showTypes TestStruct
 
 /--
 Artificial test function to show #print prefix filters out internals
@@ -133,21 +133,17 @@ testMatchProof._cstage1 (n : Nat) : Fin n → Unit
 testMatchProof._cstage2 : _obj → _obj → _obj
 testMatchProof._sunfold (n : Nat) : Fin n → Unit
 testMatchProof._unsafe_rec (n : Nat) : Fin n → Unit
-testMatchProof.match_1.{u_1} (motive : (x : Nat) → Fin x → Sort u_1) :
-  (x : Nat) →
-    (x_1 : Fin x) →
-      ((n : Nat) → (isLt : 0 < n) → motive n ⟨0, isLt⟩) →
-        ((as i : Nat) → (h : i.succ < as.succ) → motive as.succ ⟨i.succ, h⟩) → motive x x_1
-testMatchProof.match_1._cstage1.{u_1} (motive : (x : Nat) → Fin x → Sort u_1) :
-  (x : Nat) →
-    (x_1 : Fin x) →
-      ((n : Nat) → (isLt : 0 < n) → motive n ⟨0, isLt⟩) →
-        ((as i : Nat) → (h : i.succ < as.succ) → motive as.succ ⟨i.succ, h⟩) → motive x x_1
+testMatchProof.match_1.{u_1} (motive : (x : Nat) → Fin x → Sort u_1) (x✝ : Nat) (x✝¹ : Fin x✝)
+  (h_1 : (n : Nat) → (isLt : 0 < n) → motive n ⟨0, isLt⟩)
+  (h_2 : (as i : Nat) → (h : i.succ < as.succ) → motive as.succ ⟨i.succ, h⟩) : motive x✝ x✝¹
+testMatchProof.match_1._cstage1.{u_1} (motive : (x : Nat) → Fin x → Sort u_1) (x✝ : Nat) (x✝¹ : Fin x✝)
+  (h_1 : (n : Nat) → (isLt : 0 < n) → motive n ⟨0, isLt⟩)
+  (h_2 : (as i : Nat) → (h : i.succ < as.succ) → motive as.succ ⟨i.succ, h⟩) : motive x✝ x✝¹
 testMatchProof.proof_1 (as i : Nat) (h : i.succ < as.succ) : i.succ ≤ as
 testMatchProof.proof_2 (as i : Nat) (h : i.succ < as.succ) : i.succ ≤ as
 -/
 #guard_msgs in
-#print prefix (config := {internals := true}) testMatchProof
+#print prefix +internals testMatchProof
 
 private inductive TestInd where
 | foo : TestInd
diff --git a/test/simpa.lean b/test/simpa.lean
index 9528b26382..edbd58c161 100644
--- a/test/simpa.lean
+++ b/test/simpa.lean
@@ -70,7 +70,7 @@ end Prod
 theorem implicit_lambda (h : ∀ {x : Nat}, a = x) : a = 2 := by
   simpa using h
 
-theorem implicit_lambda2 (h : a = 2) : ∀ {x : Nat}, a = 2 := by
+theorem implicit_lambda2 (h : a = 2) : ∀ {_ : Nat}, a = 2 := by
   simpa using h
 
 theorem no_implicit_lambda (h : ∀ {x : Nat}, a = x) : ∀ {x : Nat}, a = x := by
diff --git a/test/vector.lean b/test/vector.lean
index 5a8b9e8587..7c93888528 100644
--- a/test/vector.lean
+++ b/test/vector.lean
@@ -17,7 +17,7 @@ def and : Gate 2 := .if (.if (.const true) (.const false)) (.if (.const false) (
 def eval (g : Gate n) (v : Vector Bool n) : Bool :=
   match g, v with
   | .const b, _ => b
-  | .if g₁ g₂, v => if v.1.back then eval g₁ v.pop else eval g₂ v.pop
+  | .if g₁ g₂, v => if v.1.back! then eval g₁ v.pop else eval g₂ v.pop
 
 example : ∀ v, and.eval v = (v[0] && v[1]) := by decide
 example : ∃ v, and.eval v = false := by decide