diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean
index fba6f08f39..43915cd733 100644
--- a/Batteries/Data/List/Basic.lean
+++ b/Batteries/Data/List/Basic.lean
@@ -27,15 +27,6 @@ protected def diff {α} [BEq α] : List α → List α → List α
 
 open Option Nat
 
-/-- Get the tail of a nonempty list, or return `[]` for `[]`. -/
-def tail : List α → List α
-  | []    => []
-  | _::as => as
-
--- FIXME: `@[simp]` on the definition simplifies even `tail l`
-@[simp] theorem tail_nil : @tail α [] = [] := rfl
-@[simp] theorem tail_cons : @tail α (a::as) = as := rfl
-
 /-- Get the head and tail of a list, if it is nonempty. -/
 @[inline] def next? : List α → Option (α × List α)
   | [] => none
@@ -73,16 +64,6 @@ drop_while (· != 1) [0, 1, 2, 3] = [1, 2, 3]
   | [] => []
   | x :: xs => bif p x then xs else after p xs
 
-/-- Returns the index of the first element satisfying `p`, or the length of the list otherwise. -/
-@[inline] def findIdx (p : α → Bool) (l : List α) : Nat := go l 0 where
-  /-- Auxiliary for `findIdx`: `findIdx.go p l n = findIdx p l + n` -/
-  @[specialize] go : List α → Nat → Nat
-  | [], n => n
-  | a :: l, n => bif p a then n else go l (n + 1)
-
-/-- Returns the index of the first element equal to `a`, or the length of the list otherwise. -/
-def indexOf [BEq α] (a : α) : List α → Nat := findIdx (· == a)
-
 @[deprecated (since := "2024-05-06")] alias removeNth := eraseIdx
 @[deprecated (since := "2024-05-06")] alias removeNthTR := eraseIdxTR
 @[deprecated (since := "2024-05-06")] alias removeNth_eq_removeNthTR := eraseIdx_eq_eraseIdxTR
@@ -302,19 +283,6 @@ theorem takeDTR_go_eq : ∀ n l, takeDTR.go dflt n l acc = acc.data ++ takeD n l
 @[csimp] theorem takeD_eq_takeDTR : @takeD = @takeDTR := by
   funext α f n l; simp [takeDTR, takeDTR_go_eq]
 
-/--
-Pads `l : List α` with repeated occurrences of `a : α` until it is of length `n`.
-If `l` is initially larger than `n`, just return `l`.
--/
-def leftpad (n : Nat) (a : α) (l : List α) : List α := replicate (n - length l) a ++ l
-
-/-- Optimized version of `leftpad`. -/
-@[inline] def leftpadTR (n : Nat) (a : α) (l : List α) : List α :=
-  replicateTR.loop a (n - length l) l
-
-@[csimp] theorem leftpad_eq_leftpadTR : @leftpad = @leftpadTR := by
-  funext α n a l; simp [leftpad, leftpadTR, replicateTR_loop_eq]
-
 /--
 Fold a function `f` over the list from the left, returning the list of partial results.
 ```
@@ -386,14 +354,6 @@ indexesOf a [a, b, a, a] = [0, 2, 3]
 -/
 @[inline] def indexesOf [BEq α] (a : α) : List α → List Nat := findIdxs (· == a)
 
-/-- Return the index of the first occurrence of an element satisfying `p`. -/
-def findIdx? (p : α → Bool) : List α → (start : Nat := 0) → Option Nat
-| [], _ => none
-| a :: l, i => if p a then some i else findIdx? p l (i + 1)
-
-/-- Return the index of the first occurrence of `a` in the list. -/
-@[inline] def indexOf? [BEq α] (a : α) : List α → Option Nat := findIdx? (· == a)
-
 /--
 `lookmap` is a combination of `lookup` and `filterMap`.
 `lookmap f l` will apply `f : α → Option α` to each element of the list,
@@ -407,16 +367,6 @@ replacing `a → b` at the first value `a` in the list such that `f a = some b`.
     | some b => acc.toListAppend (b :: l)
     | none => go l (acc.push a)
 
-/-- `countP p l` is the number of elements of `l` that satisfy `p`. -/
-@[inline] def countP (p : α → Bool) (l : List α) : Nat := go l 0 where
-  /-- Auxiliary for `countP`: `countP.go p l acc = countP p l + acc`. -/
-  @[specialize] go : List α → Nat → Nat
-  | [], acc => acc
-  | x :: xs, acc => bif p x then go xs (acc + 1) else go xs acc
-
-/-- `count a l` is the number of occurrences of `a` in `l`. -/
-@[inline] def count [BEq α] (a : α) : List α → Nat := countP (· == a)
-
 /--
 `inits l` is the list of initial segments of `l`.
 ```
@@ -770,34 +720,6 @@ Defined as `pwFilter (≠)`.
     eraseDup [1, 0, 2, 2, 1] = [0, 2, 1] -/
 @[inline] def eraseDup [BEq α] : List α → List α := pwFilter (· != ·)
 
-/-- `range' start len step` is the list of numbers `[start, start+step, ..., start+(len-1)*step]`.
-  It is intended mainly for proving properties of `range` and `iota`. -/
-def range' : (start len : Nat) → (step : Nat := 1) → List Nat
-  | _, 0, _ => []
-  | s, n+1, step => s :: range' (s+step) n step
-
-/-- Optimized version of `range'`. -/
-@[inline] def range'TR (s n : Nat) (step : Nat := 1) : List Nat := go n (s + step * n) [] where
-  /-- Auxiliary for `range'TR`: `range'TR.go n e = [e-n, ..., e-1] ++ acc`. -/
-  go : Nat → Nat → List Nat → List Nat
-  | 0, _, acc => acc
-  | n+1, e, acc => go n (e-step) ((e-step) :: acc)
-
-@[csimp] theorem range'_eq_range'TR : @range' = @range'TR := by
-  funext s n step
-  let rec go (s) : ∀ n m,
-    range'TR.go step n (s + step * n) (range' (s + step * n) m step) = range' s (n + m) step
-  | 0, m => by simp [range'TR.go]
-  | n+1, m => by
-    simp [range'TR.go]
-    rw [Nat.mul_succ, ← Nat.add_assoc, Nat.add_sub_cancel, Nat.add_right_comm n]
-    exact go s n (m + 1)
-  exact (go s n 0).symm
-
-/-- Drop `none`s from a list, and replace each remaining `some a` with `a`. -/
-@[inline] def reduceOption {α} : List (Option α) → List α :=
-  List.filterMap id
-
 /--
 `ilast' x xs` returns the last element of `xs` if `xs` is non-empty; it returns `x` otherwise.
 Use `List.getLastD` instead.
diff --git a/Batteries/Data/List/Count.lean b/Batteries/Data/List/Count.lean
index 3aece22185..036a76b4b8 100644
--- a/Batteries/Data/List/Count.lean
+++ b/Batteries/Data/List/Count.lean
@@ -19,111 +19,6 @@ open Nat
 
 namespace List
 
-section countP
-
-variable (p q : α → Bool)
-
-@[simp] theorem countP_nil : countP p [] = 0 := rfl
-
-protected theorem countP_go_eq_add (l) : countP.go p l n = n + countP.go p l 0 := by
-  induction l generalizing n with
-  | nil => rfl
-  | cons head tail ih =>
-    unfold countP.go
-    rw [ih (n := n + 1), ih (n := n), ih (n := 1)]
-    if h : p head then simp [h, Nat.add_assoc] else simp [h]
-
-@[simp] theorem countP_cons_of_pos (l) (pa : p a) : countP p (a :: l) = countP p l + 1 := by
-  have : countP.go p (a :: l) 0 = countP.go p l 1 := show cond .. = _ by rw [pa]; rfl
-  unfold countP
-  rw [this, Nat.add_comm, List.countP_go_eq_add]
-
-@[simp] theorem countP_cons_of_neg (l) (pa : ¬p a) : countP p (a :: l) = countP p l := by
-  simp [countP, countP.go, pa]
-
-theorem countP_cons (a : α) (l) : countP p (a :: l) = countP p l + if p a then 1 else 0 := by
-  by_cases h : p a <;> simp [h]
-
-theorem length_eq_countP_add_countP (l) : length l = countP p l + countP (fun a => ¬p a) l := by
-  induction l with
-  | nil => rfl
-  | cons x h ih =>
-    if h : p x then
-      rw [countP_cons_of_pos _ _ h, countP_cons_of_neg _ _ _, length, ih]
-      · rw [Nat.add_assoc, Nat.add_comm _ 1, Nat.add_assoc]
-      · simp only [h, not_true_eq_false, decide_False, not_false_eq_true]
-    else
-      rw [countP_cons_of_pos (fun a => ¬p a) _ _, countP_cons_of_neg _ _ h, length, ih]
-      · rfl
-      · simp only [h, not_false_eq_true, decide_True]
-
-theorem countP_eq_length_filter (l) : countP p l = length (filter p l) := by
-  induction l with
-  | nil => rfl
-  | cons x l ih =>
-    if h : p x
-    then rw [countP_cons_of_pos p l h, ih, filter_cons_of_pos h, length]
-    else rw [countP_cons_of_neg p l h, ih, filter_cons_of_neg h]
-
-theorem countP_le_length : countP p l ≤ l.length := by
-  simp only [countP_eq_length_filter]
-  apply length_filter_le
-
-@[simp] theorem countP_append (l₁ l₂) : countP p (l₁ ++ l₂) = countP p l₁ + countP p l₂ := by
-  simp only [countP_eq_length_filter, filter_append, length_append]
-
-theorem countP_pos : 0 < countP p l ↔ ∃ a ∈ l, p a := by
-  simp only [countP_eq_length_filter, length_pos_iff_exists_mem, mem_filter, exists_prop]
-
-theorem countP_eq_zero : countP p l = 0 ↔ ∀ a ∈ l, ¬p a := by
-  simp only [countP_eq_length_filter, length_eq_zero, filter_eq_nil]
-
-theorem countP_eq_length : countP p l = l.length ↔ ∀ a ∈ l, p a := by
-  rw [countP_eq_length_filter, filter_length_eq_length]
-
-theorem Sublist.countP_le (s : l₁ <+ l₂) : countP p l₁ ≤ countP p l₂ := by
-  simp only [countP_eq_length_filter]
-  apply s.filter _ |>.length_le
-
-theorem countP_filter (l : List α) :
-    countP p (filter q l) = countP (fun a => p a ∧ q a) l := by
-  simp only [countP_eq_length_filter, filter_filter]
-
-@[simp] theorem countP_true {l : List α} : (l.countP fun _ => true) = l.length := by
-  rw [countP_eq_length]
-  simp
-
-@[simp] theorem countP_false {l : List α} : (l.countP fun _ => false) = 0 := by
-  rw [countP_eq_zero]
-  simp
-
-@[simp] theorem countP_map (p : β → Bool) (f : α → β) :
-    ∀ l, countP p (map f l) = countP (p ∘ f) l
-  | [] => rfl
-  | a :: l => by rw [map_cons, countP_cons, countP_cons, countP_map p f l]; rfl
-
-variable {p q}
-
-theorem countP_mono_left (h : ∀ x ∈ l, p x → q x) : countP p l ≤ countP q l := by
-  induction l with
-  | nil => apply Nat.le_refl
-  | cons a l ihl =>
-    rw [forall_mem_cons] at h
-    have ⟨ha, hl⟩ := h
-    simp [countP_cons]
-    cases h : p a
-    . simp
-      apply Nat.le_trans ?_ (Nat.le_add_right _ _)
-      apply ihl hl
-    . simp [ha h]
-      apply ihl hl
-
-theorem countP_congr (h : ∀ x ∈ l, p x ↔ q x) : countP p l = countP q l :=
-  Nat.le_antisymm
-    (countP_mono_left fun x hx => (h x hx).1)
-    (countP_mono_left fun x hx => (h x hx).2)
-
-end countP
 
 /-! ### count -/
 
@@ -131,71 +26,10 @@ section count
 
 variable [DecidableEq α]
 
-@[simp] theorem count_nil (a : α) : count a [] = 0 := rfl
-
-theorem count_cons (a b : α) (l : List α) :
-    count a (b :: l) = count a l + if a = b then 1 else 0 := by
-  simp [count, countP_cons, eq_comm (a := a)]
-
-@[simp] theorem count_cons_self (a : α) (l : List α) : count a (a :: l) = count a l + 1 := by
-  simp [count_cons]
-
-@[simp] theorem count_cons_of_ne (h : a ≠ b) (l : List α) : count a (b :: l) = count a l := by
-  simp [count_cons, h]
-
-theorem count_tail : ∀ (l : List α) (a : α) (h : l ≠ []),
-      l.tail.count a = l.count a - if a = l.head h then 1 else 0
-  | head :: tail, a, h => by simp [count_cons]
-
-theorem count_le_length (a : α) (l : List α) : count a l ≤ l.length := countP_le_length _
-
-theorem Sublist.count_le (h : l₁ <+ l₂) (a : α) : count a l₁ ≤ count a l₂ := h.countP_le _
-
-theorem count_le_count_cons (a b : α) (l : List α) : count a l ≤ count a (b :: l) :=
-  (sublist_cons_self _ _).count_le _
-
-theorem count_singleton (a : α) : count a [a] = 1 := by simp
-
-theorem count_singleton' (a b : α) : count a [b] = if a = b then 1 else 0 := by simp [count_cons]
-
-@[simp] theorem count_append (a : α) : ∀ l₁ l₂, count a (l₁ ++ l₂) = count a l₁ + count a l₂ :=
-  countP_append _
+theorem count_singleton' (a b : α) : count a [b] = if b = a then 1 else 0 := by simp [count_cons]
 
 theorem count_concat (a : α) (l : List α) : count a (concat l a) = succ (count a l) := by simp
 
-@[simp]
-theorem count_pos_iff_mem {a : α} {l : List α} : 0 < count a l ↔ a ∈ l := by
-  simp only [count, countP_pos, beq_iff_eq, exists_eq_right]
-
-@[simp 900] theorem count_eq_zero_of_not_mem {a : α} {l : List α} (h : a ∉ l) : count a l = 0 :=
-  Decidable.byContradiction fun h' => h <| count_pos_iff_mem.1 (Nat.pos_of_ne_zero h')
-
-theorem not_mem_of_count_eq_zero {a : α} {l : List α} (h : count a l = 0) : a ∉ l :=
-  fun h' => Nat.ne_of_lt (count_pos_iff_mem.2 h') h.symm
-
-theorem count_eq_zero {l : List α} : count a l = 0 ↔ a ∉ l :=
-  ⟨not_mem_of_count_eq_zero, count_eq_zero_of_not_mem⟩
-
-theorem count_eq_length {l : List α} : count a l = l.length ↔ ∀ b ∈ l, a = b := by
-  rw [count, countP_eq_length]
-  refine ⟨fun h b hb => Eq.symm ?_, fun h b hb => ?_⟩
-  · simpa using h b hb
-  · rw [h b hb, beq_self_eq_true]
-
-@[simp] theorem count_replicate_self (a : α) (n : Nat) : count a (replicate n a) = n :=
-  (count_eq_length.2 <| fun _ h => (eq_of_mem_replicate h).symm).trans (length_replicate ..)
-
-theorem count_replicate (a b : α) (n : Nat) : count a (replicate n b) = if a = b then n else 0 := by
-  split
-  exacts [‹a = b› ▸ count_replicate_self .., count_eq_zero.2 <| mt eq_of_mem_replicate ‹a ≠ b›]
-
-theorem filter_beq (l : List α) (a : α) : l.filter (· == a) = replicate (count a l) a := by
-  simp only [count, countP_eq_length_filter, eq_replicate, mem_filter, beq_iff_eq]
-  exact ⟨trivial, fun _ h => h.2⟩
-
-theorem filter_eq (l : List α) (a : α) : l.filter (· = a) = replicate (count a l) a :=
-  filter_beq l a
-
 @[deprecated filter_eq (since := "2023-12-14")]
 theorem filter_eq' (l : List α) (a : α) : l.filter (a = ·) = replicate (count a l) a := by
   simpa only [eq_comm] using filter_eq l a
@@ -203,46 +37,3 @@ theorem filter_eq' (l : List α) (a : α) : l.filter (a = ·) = replicate (count
 @[deprecated filter_beq (since := "2023-12-14")]
 theorem filter_beq' (l : List α) (a : α) : l.filter (a == ·) = replicate (count a l) a := by
   simpa only [eq_comm (b := a)] using filter_eq l a
-
-theorem le_count_iff_replicate_sublist {l : List α} : n ≤ count a l ↔ replicate n a <+ l := by
-  refine ⟨fun h => ?_, fun h => ?_⟩
-  · exact ((replicate_sublist_replicate a).2 h).trans <| filter_eq l a ▸ filter_sublist _
-  · simpa only [count_replicate_self] using h.count_le a
-
-theorem replicate_count_eq_of_count_eq_length {l : List α} (h : count a l = length l) :
-    replicate (count a l) a = l :=
-  (le_count_iff_replicate_sublist.mp (Nat.le_refl _)).eq_of_length <|
-    (length_replicate (count a l) a).trans h
-
-@[simp] theorem count_filter {l : List α} (h : p a) : count a (filter p l) = count a l := by
-  rw [count, countP_filter]; congr; funext b
-  rw [(by rfl : (b == a) = decide (b = a)), decide_eq_decide]
-  simp; rintro rfl; exact h
-
-theorem count_le_count_map [DecidableEq β] (l : List α) (f : α → β) (x : α) :
-    count x l ≤ count (f x) (map f l) := by
-  rw [count, count, countP_map]
-  apply countP_mono_left; simp (config := { contextual := true })
-
-theorem count_erase (a b : α) :
-    ∀ l : List α, count a (l.erase b) = count a l - if a = b then 1 else 0
-  | [] => by simp
-  | c :: l => by
-    rw [erase_cons]
-    if hc : c = b then
-      have hc_beq := (beq_iff_eq _ _).mpr hc
-      rw [if_pos hc_beq, hc, count_cons, Nat.add_sub_cancel]
-    else
-      have hc_beq := beq_false_of_ne hc
-      simp only [hc_beq, if_false, count_cons, count_cons, count_erase a b l]
-      if ha : a = b then
-        rw [← ha, eq_comm] at hc
-        rw [if_pos ha, if_neg hc, Nat.add_zero, Nat.add_zero]
-      else
-        rw [if_neg ha, Nat.sub_zero, Nat.sub_zero]
-
-@[simp] theorem count_erase_self (a : α) (l : List α) :
-    count a (List.erase l a) = count a l - 1 := by rw [count_erase, if_pos rfl]
-
-@[simp] theorem count_erase_of_ne (ab : a ≠ b) (l : List α) : count a (l.erase b) = count a l := by
-  rw [count_erase, if_neg ab, Nat.sub_zero]
diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
index 724b67a56a..add78e3096 100644
--- a/Batteries/Data/List/Lemmas.lean
+++ b/Batteries/Data/List/Lemmas.lean
@@ -17,23 +17,6 @@ open Nat
 @[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
   simp [Array.mem_def]
 
-/-! ### drop -/
-
-@[simp]
-theorem drop_one : ∀ l : List α, drop 1 l = tail l
-  | [] | _ :: _ => rfl
-
-/-! ### zipWith -/
-
-theorem zipWith_distrib_tail : (zipWith f l l').tail = zipWith f l.tail l'.tail := by
-  rw [← drop_one]; simp [drop_zipWith]
-
-/-! ### tail -/
-
-theorem tail_eq_tailD (l) : @tail α l = tailD l [] := by cases l <;> rfl
-
-theorem tail_eq_tail? (l) : @tail α l = (tail? l).getD [] := by simp [tail_eq_tailD]
-
 /-! ### next? -/
 
 @[simp] theorem next?_nil : @next? α [] = none := rfl
@@ -41,10 +24,6 @@ theorem tail_eq_tail? (l) : @tail α l = (tail? l).getD [] := by simp [tail_eq_t
 
 /-! ### get? -/
 
-theorem getElem_eq_iff {l : List α} {n : Nat} {h : n < l.length} : l[n] = x ↔ l[n]? = some x := by
-  simp only [get_eq_getElem, get?_eq_getElem?, getElem?_eq_some]
-  exact ⟨fun w => ⟨h, w⟩, fun h => h.2⟩
-
 @[deprecated getElem_eq_iff (since := "2024-06-12")]
 theorem get_eq_iff : List.get l n = x ↔ l.get? n.1 = some x := by
   simp
@@ -55,16 +34,6 @@ theorem get?_inj
   apply getElem?_inj h₀ h₁
   simp_all
 
-/-! ### drop -/
-
-theorem tail_drop (l : List α) (n : Nat) : (l.drop n).tail = l.drop (n + 1) := by
-  induction l generalizing n with
-  | nil => simp
-  | cons hd tl hl =>
-    cases n
-    · simp
-    · simp [hl]
-
 /-! ### modifyNth -/
 
 @[simp] theorem modifyNth_nil (f : α → α) (n) : [].modifyNth f n = [] := by cases n <;> rfl
@@ -189,10 +158,6 @@ 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
 
-@[simp]
-theorem getElem?_set_eq' (a : α) (n) (l : List α) : (set l n a)[n]? = (fun _ => a) <$> l[n]? := by
-  simp only [set_eq_modifyNth, getElem?_modifyNth_eq]
-
 @[deprecated getElem?_set_eq' (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
@@ -209,10 +174,6 @@ theorem get?_set_eq_of_lt (a : α) {n} {l : List α} (h : n < length l) :
 theorem get?_set_ne (a : α) {m n} (l : List α) (h : m ≠ n) : (set l m a).get? n = l.get? n := by
   simp [h]
 
-theorem getElem?_set' (a : α) {m n} (l : List α) :
-    (set l m a)[n]? = if m = n then (fun _ => a) <$> l[n]? else l[n]? := by
-  by_cases m = n <;> simp [*]
-
 @[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
@@ -226,30 +187,8 @@ theorem get?_set_of_lt' (a : α) {m n} (l : List α) (h : m < length l) :
     (set l m a).get? n = if m = n then some a else l.get? n := by
   simp [getElem?_set]; split <;> subst_vars <;> simp [*, getElem?_eq_getElem h]
 
-theorem take_set_of_lt (a : α) {n m : Nat} (l : List α) (h : m < n) :
-    (l.set n a).take m = l.take m :=
-  List.ext_getElem? fun i => by
-    rw [getElem?_take_eq_if, getElem?_take_eq_if]
-    split
-    · next h' => rw [getElem?_set_ne (by omega)]
-    · rfl
-
-/-! ### removeNth -/
-
-theorem length_eraseIdx : ∀ {l i}, i < length l → length (@eraseIdx α l i) = length l - 1
-  | [], _, _ => rfl
-  | _::_, 0, _ => by simp [eraseIdx]
-  | x::xs, i+1, h => by
-    have : i < length xs := Nat.lt_of_succ_lt_succ h
-    simp [eraseIdx, ← Nat.add_one]
-    rw [length_eraseIdx this, Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) this)]
-
 @[deprecated (since := "2024-05-06")] alias length_removeNth := length_eraseIdx
 
-/-! ### tail -/
-
-@[simp] theorem length_tail (l : List α) : length (tail l) = length l - 1 := by cases l <;> rfl
-
 /-! ### eraseP -/
 
 @[simp] theorem extractP_eq_find?_eraseP
@@ -266,109 +205,6 @@ theorem length_eraseIdx : ∀ {l i}, i < length l → length (@eraseIdx α l i)
 
 @[deprecated (since := "2024-04-22")] alias sublist.erase := Sublist.erase
 
-/-! ### findIdx -/
-
-@[simp] theorem findIdx_nil {α : Type _} (p : α → Bool) : [].findIdx p = 0 := rfl
-
-theorem findIdx_cons (p : α → Bool) (b : α) (l : List α) :
-    (b :: l).findIdx p = bif p b then 0 else (l.findIdx p) + 1 := by
-  cases H : p b with
-  | true => simp [H, findIdx, findIdx.go]
-  | false => simp [H, findIdx, findIdx.go, findIdx_go_succ]
-where
-  findIdx_go_succ (p : α → Bool) (l : List α) (n : Nat) :
-      List.findIdx.go p l (n + 1) = (findIdx.go p l n) + 1 := by
-    cases l with
-    | nil => unfold findIdx.go; exact Nat.succ_eq_add_one n
-    | cons head tail =>
-      unfold findIdx.go
-      cases p head <;> simp only [cond_false, cond_true]
-      exact findIdx_go_succ p tail (n + 1)
-
-theorem findIdx_of_get?_eq_some {xs : List α} (w : xs.get? (xs.findIdx p) = some y) : p y := by
-  induction xs with
-  | nil => simp_all
-  | cons x xs ih => by_cases h : p x <;> simp_all [findIdx_cons]
-
-theorem findIdx_get {xs : List α} {w : xs.findIdx p < xs.length} :
-    p (xs.get ⟨xs.findIdx p, w⟩) :=
-  xs.findIdx_of_get?_eq_some (get?_eq_get w)
-
-theorem findIdx_lt_length_of_exists {xs : List α} (h : ∃ x ∈ xs, p x) :
-    xs.findIdx p < xs.length := by
-  induction xs with
-  | nil => simp_all
-  | cons x xs ih =>
-    by_cases p x
-    · simp_all only [forall_exists_index, and_imp, mem_cons, exists_eq_or_imp, true_or,
-        findIdx_cons, cond_true, length_cons]
-      apply Nat.succ_pos
-    · simp_all [findIdx_cons]
-      refine Nat.succ_lt_succ ?_
-      obtain ⟨x', m', h'⟩ := h
-      exact ih x' m' h'
-
-theorem findIdx_get?_eq_get_of_exists {xs : List α} (h : ∃ x ∈ xs, p x) :
-    xs.get? (xs.findIdx p) = some (xs.get ⟨xs.findIdx p, xs.findIdx_lt_length_of_exists h⟩) :=
-  get?_eq_get (findIdx_lt_length_of_exists h)
-
-  /-! ### findIdx? -/
-
-@[simp] theorem findIdx?_nil : ([] : List α).findIdx? p i = none := rfl
-
-@[simp] theorem findIdx?_cons :
-    (x :: xs).findIdx? p i = if p x then some i else findIdx? p xs (i + 1) := rfl
-
-@[simp] theorem findIdx?_succ :
-    (xs : List α).findIdx? p (i+1) = (xs.findIdx? p i).map fun i => i + 1 := by
-  induction xs generalizing i with simp
-  | cons _ _ _ => split <;> simp_all
-
-theorem findIdx?_eq_some_iff (xs : List α) (p : α → Bool) :
-    xs.findIdx? p = some i ↔ (xs.take (i + 1)).map p = replicate i false ++ [true] := by
-  induction xs generalizing i with
-  | nil => simp
-  | cons x xs ih =>
-    simp only [findIdx?_cons, Nat.zero_add, findIdx?_succ, take_succ_cons, map_cons]
-    split <;> cases i <;> simp_all [replicate_succ]
-
-theorem findIdx?_of_eq_some {xs : List α} {p : α → Bool} (w : xs.findIdx? p = some i) :
-    match xs.get? i with | some a => p a | none => false := by
-  induction xs generalizing i with
-  | nil => simp_all
-  | cons x xs ih =>
-    simp_all only [findIdx?_cons, Nat.zero_add, findIdx?_succ]
-    split at w <;> cases i <;> simp_all
-
-theorem findIdx?_of_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p = none) :
-    ∀ i, match xs.get? i with | some a => ¬ p a | none => true := by
-  intro i
-  induction xs generalizing i with
-  | nil => simp_all
-  | cons x xs ih =>
-    simp_all only [Bool.not_eq_true, findIdx?_cons, Nat.zero_add, findIdx?_succ]
-    cases i with
-    | zero =>
-      split at w <;> simp_all
-    | succ i =>
-      simp only [get?_cons_succ]
-      apply ih
-      split at w <;> simp_all
-
-@[simp] theorem findIdx?_append :
-    (xs ++ ys : List α).findIdx? p =
-      (xs.findIdx? p <|> (ys.findIdx? p).map fun i => i + xs.length) := by
-  induction xs with simp
-  | cons _ _ _ => split <;> simp_all [Option.map_orElse, Option.map_map]; rfl
-
-@[simp] theorem findIdx?_replicate :
-    (replicate n a).findIdx? p = if 0 < n ∧ p a then some 0 else none := by
-  induction n with
-  | zero => simp
-  | succ n ih =>
-    simp only [replicate, findIdx?_cons, Nat.zero_add, findIdx?_succ, Nat.zero_lt_succ, true_and]
-    split <;> simp_all
-
 /-! ### replaceF -/
 
 theorem replaceF_nil : [].replaceF p = [] := rfl
@@ -476,16 +312,6 @@ theorem disjoint_of_disjoint_append_right_left (d : Disjoint l (l₁ ++ l₂)) :
 theorem disjoint_of_disjoint_append_right_right (d : Disjoint l (l₁ ++ l₂)) : Disjoint l l₂ :=
   (disjoint_append_right.1 d).2
 
-/-! ### foldl / foldr -/
-
-theorem foldl_hom (f : α₁ → α₂) (g₁ : α₁ → β → α₁) (g₂ : α₂ → β → α₂) (l : List β) (init : α₁)
-    (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init) := by
-  induction l generalizing init <;> simp [*, H]
-
-theorem foldr_hom (f : β₁ → β₂) (g₁ : α → β₁ → β₁) (g₂ : α → β₂ → β₂) (l : List α) (init : β₁)
-    (H : ∀ x y, g₂ x (f y) = f (g₁ x y)) : l.foldr g₂ (f init) = f (l.foldr g₁ init) := by
-  induction l <;> simp [*, H]
-
 /-! ### union -/
 
 section union
@@ -530,29 +356,14 @@ theorem leftpad_length (n : Nat) (a : α) (l : List α) :
     (leftpad n a l).length = max n l.length := by
   simp only [leftpad, length_append, length_replicate, Nat.sub_add_eq_max]
 
-theorem leftpad_prefix (n : Nat) (a : α) (l : List α) :
-    replicate (n - length l) a <+: leftpad n a l := by
-  simp only [IsPrefix, leftpad]
-  exact Exists.intro l rfl
-
-theorem leftpad_suffix (n : Nat) (a : α) (l : List α) : l <:+ (leftpad n a l) := by
-  simp only [IsSuffix, leftpad]
-  exact Exists.intro (replicate (n - length l) a) rfl
-
 /-! ### monadic operations -/
 
--- we use ForIn.forIn as the simp normal form
-@[simp] theorem forIn_eq_forIn [Monad m] : @List.forIn α β m _ = forIn := rfl
-
 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]
   congr; ext (b | b) <;> simp
 
-@[simp] theorem forM_append [Monad m] [LawfulMonad m] (l₁ l₂ : List α) (f : α → m PUnit) :
-    (l₁ ++ l₂).forM f = (do l₁.forM f; l₂.forM f) := by induction l₁ <;> simp [*]
-
 /-! ### diff -/
 
 section Diff
@@ -631,8 +442,6 @@ end Diff
 
 /-! ### drop -/
 
-theorem mem_of_mem_drop {n} {l : List α} (h : a ∈ l.drop n) : a ∈ l := drop_subset _ _ h
-
 theorem disjoint_take_drop : ∀ {l : List α}, l.Nodup → m ≤ n → Disjoint (l.take m) (l.drop n)
   | [], _, _ => by simp
   | x :: xs, hl, h => by
@@ -681,39 +490,6 @@ protected theorem Pairwise.chain (p : Pairwise R (a :: l)) : Chain R a l := by
 
 /-! ### range', range -/
 
-theorem range'_succ (s n step) : range' s (n + 1) step = s :: range' (s + step) n step := by
-  simp [range', Nat.add_succ, Nat.mul_succ]
-
-@[simp] theorem length_range' (s step) : ∀ n : Nat, length (range' s n step) = n
-  | 0 => rfl
-  | _ + 1 => congrArg succ (length_range' _ _ _)
-
-@[simp] theorem range'_eq_nil : range' s n step = [] ↔ n = 0 := by
-  rw [← length_eq_zero, length_range']
-
-theorem mem_range' : ∀{n}, m ∈ range' s n step ↔ ∃ i < n, m = s + step * i
-  | 0 => by simp [range', Nat.not_lt_zero]
-  | n + 1 => by
-    have h (i) : i ≤ n ↔ i = 0 ∨ ∃ j, i = succ j ∧ j < n := by cases i <;> simp [Nat.succ_le]
-    simp [range', mem_range', Nat.lt_succ, h]; simp only [← exists_and_right, and_assoc]
-    rw [exists_comm]; simp [Nat.mul_succ, Nat.add_assoc, Nat.add_comm]
-
-@[simp] theorem mem_range'_1 : m ∈ range' s n ↔ s ≤ m ∧ m < s + n := by
-  simp [mem_range']; exact ⟨
-    fun ⟨i, h, e⟩ => e ▸ ⟨Nat.le_add_right .., Nat.add_lt_add_left h _⟩,
-    fun ⟨h₁, h₂⟩ => ⟨m - s, Nat.sub_lt_left_of_lt_add h₁ h₂, (Nat.add_sub_cancel' h₁).symm⟩⟩
-
-@[simp]
-theorem map_add_range' (a) : ∀ s n step, map (a + ·) (range' s n step) = range' (a + s) n step
-  | _, 0, _ => rfl
-  | s, n + 1, step => by simp [range', map_add_range' _ (s + step) n step, Nat.add_assoc]
-
-theorem map_sub_range' (a s n : Nat) (h : a ≤ s) :
-    map (· - a) (range' s n step) = range' (s - a) n step := by
-  conv => lhs; rw [← Nat.add_sub_cancel' h]
-  rw [← map_add_range', map_map, (?_ : _∘_ = _), map_id]
-  funext x; apply Nat.add_sub_cancel_left
-
 theorem chain_succ_range' : ∀ s n step : Nat,
     Chain (fun a b => b = a + step) s (range' (s + step) n step)
   | _, 0, _ => Chain.nil
@@ -723,41 +499,6 @@ theorem chain_lt_range' (s n : Nat) {step} (h : 0 < step) :
     Chain (· < ·) s (range' (s + step) n step) :=
   (chain_succ_range' s n step).imp fun _ _ e => e.symm ▸ Nat.lt_add_of_pos_right h
 
-theorem range'_append : ∀ s m n step : Nat,
-    range' s m step ++ range' (s + step * m) n step = range' s (n + m) step
-  | s, 0, n, step => rfl
-  | s, m + 1, n, step => by
-    simpa [range', Nat.mul_succ, Nat.add_assoc, Nat.add_comm]
-      using range'_append (s + step) m n step
-
-@[simp] theorem range'_append_1 (s m n : Nat) :
-    range' s m ++ range' (s + m) n = range' s (n + m) := by simpa using range'_append s m n 1
-
-theorem range'_sublist_right {s m n : Nat} : range' s m step <+ range' s n step ↔ m ≤ n :=
-  ⟨fun h => by simpa only [length_range'] using h.length_le,
-   fun h => by rw [← Nat.sub_add_cancel h, ← range'_append]; apply sublist_append_left⟩
-
-theorem range'_subset_right {s m n : Nat} (step0 : 0 < step) :
-    range' s m step ⊆ range' s n step ↔ m ≤ n := by
-  refine ⟨fun h => Nat.le_of_not_lt fun hn => ?_, fun h => (range'_sublist_right.2 h).subset⟩
-  have ⟨i, h', e⟩ := mem_range'.1 <| h <| mem_range'.2 ⟨_, hn, rfl⟩
-  exact Nat.ne_of_gt h' (Nat.eq_of_mul_eq_mul_left step0 (Nat.add_left_cancel e))
-
-theorem range'_subset_right_1 {s m n : Nat} : range' s m ⊆ range' s n ↔ m ≤ n :=
-  range'_subset_right (by decide)
-
-theorem getElem?_range' (s step) :
-    ∀ {m n : Nat}, m < n → (range' s n step)[m]? = some (s + step * m)
-  | 0, n + 1, _ => by simp [range'_succ]
-  | m + 1, n + 1, h => by
-    simp only [range'_succ, getElem?_cons_succ]
-    exact (getElem?_range' (s + step) step (Nat.lt_of_add_lt_add_right h)).trans <| by
-      simp [Nat.mul_succ, Nat.add_assoc, Nat.add_comm]
-
-@[simp] theorem getElem_range' {n m step} (i) (H : i < (range' n m step).length) :
-    (range' n m step)[i] = n + step * i :=
-  (getElem?_eq_some.1 <| getElem?_range' n step (by simpa using H)).2
-
 @[deprecated getElem?_range' (since := "2024-06-12")]
 theorem get?_range' (s step) {m n : Nat} (h : m < n) :
     get? (range' s n step) m = some (s + step * m) := by
@@ -768,54 +509,6 @@ theorem get_range' {n m step} (i) (H : i < (range' n m step).length) :
     get (range' n m step) ⟨i, H⟩ = n + step * i := by
   simp
 
-theorem range'_concat (s n : Nat) : range' s (n + 1) step = range' s n step ++ [s + step * n] := by
-  rw [Nat.add_comm n 1]; exact (range'_append s n 1 step).symm
-
-theorem range'_1_concat (s n : Nat) : range' s (n + 1) = range' s n ++ [s + n] := by
-  simp [range'_concat]
-
-theorem range_loop_range' : ∀ s n : Nat, range.loop s (range' s n) = range' 0 (n + s)
-  | 0, n => rfl
-  | s + 1, n => by rw [← Nat.add_assoc, Nat.add_right_comm n s 1]; exact range_loop_range' s (n + 1)
-
-theorem range_eq_range' (n : Nat) : range n = range' 0 n :=
-  (range_loop_range' n 0).trans <| by rw [Nat.zero_add]
-
-theorem range_succ_eq_map (n : Nat) : range (n + 1) = 0 :: map succ (range n) := by
-  rw [range_eq_range', range_eq_range', range', Nat.add_comm, ← map_add_range']
-  congr; exact funext one_add
-
-theorem range'_eq_map_range (s n : Nat) : range' s n = map (s + ·) (range n) := by
-  rw [range_eq_range', map_add_range']; rfl
-
-@[simp] theorem length_range (n : Nat) : length (range n) = n := by
-  simp only [range_eq_range', length_range']
-
-@[simp] theorem range_eq_nil {n : Nat} : range n = [] ↔ n = 0 := by
-  rw [← length_eq_zero, length_range]
-
-@[simp]
-theorem range_sublist {m n : Nat} : range m <+ range n ↔ m ≤ n := by
-  simp only [range_eq_range', range'_sublist_right]
-
-@[simp]
-theorem range_subset {m n : Nat} : range m ⊆ range n ↔ m ≤ n := by
-  simp only [range_eq_range', range'_subset_right, lt_succ_self]
-
-@[simp]
-theorem mem_range {m n : Nat} : m ∈ range n ↔ m < n := by
-  simp only [range_eq_range', mem_range'_1, Nat.zero_le, true_and, Nat.zero_add]
-
-theorem not_mem_range_self {n : Nat} : n ∉ range n := by simp
-
-theorem self_mem_range_succ (n : Nat) : n ∈ range (n + 1) := by simp
-
-theorem getElem?_range {m n : Nat} (h : m < n) : (range n)[m]? = some m := by
-  simp [range_eq_range', getElem?_range' _ _ h]
-
-@[simp] theorem getElem_range {n : Nat} (m) (h : m < (range n).length) : (range n)[m] = m := by
-  simp [range_eq_range']
-
 @[deprecated getElem?_range (since := "2024-06-12")]
 theorem get?_range {m n : Nat} (h : m < n) : get? (range n) m = some m := by
   simp [getElem?_range, h]
@@ -824,41 +517,6 @@ theorem get?_range {m n : Nat} (h : m < n) : get? (range n) m = some m := by
 theorem get_range {n} (i) (H : i < (range n).length) : get (range n) ⟨i, H⟩ = i := by
   simp
 
-theorem range_succ (n : Nat) : range (succ n) = range n ++ [n] := by
-  simp only [range_eq_range', range'_1_concat, Nat.zero_add]
-
-theorem range_add (a b : Nat) : range (a + b) = range a ++ (range b).map (a + ·) := by
-  rw [← range'_eq_map_range]
-  simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 a b).symm
-
-theorem iota_eq_reverse_range' : ∀ n : Nat, iota n = reverse (range' 1 n)
-  | 0 => rfl
-  | n + 1 => by simp [iota, range'_concat, iota_eq_reverse_range' n, reverse_append, Nat.add_comm]
-
-@[simp] theorem length_iota (n : Nat) : length (iota n) = n := by simp [iota_eq_reverse_range']
-
-@[simp]
-theorem mem_iota {m n : Nat} : m ∈ iota n ↔ 1 ≤ m ∧ m ≤ n := by
-  simp [iota_eq_reverse_range', Nat.add_comm, Nat.lt_succ]
-
-theorem reverse_range' : ∀ s n : Nat, reverse (range' s n) = map (s + n - 1 - ·) (range n)
-  | s, 0 => rfl
-  | s, n + 1 => by
-    rw [range'_1_concat, reverse_append, range_succ_eq_map,
-      show s + (n + 1) - 1 = s + n from rfl, map, map_map]
-    simp [reverse_range', Nat.sub_right_comm, Nat.sub_sub]
-
-
-/-! ### enum, enumFrom -/
-
-@[simp] theorem enumFrom_map_fst (n) :
-    ∀ (l : List α), map Prod.fst (enumFrom n l) = range' n l.length
-  | [] => rfl
-  | _ :: _ => congrArg (cons _) (enumFrom_map_fst _ _)
-
-@[simp] theorem enum_map_fst (l : List α) : map Prod.fst (enum l) = range l.length := by
-  simp only [enum, enumFrom_map_fst, range_eq_range']
-
 /-! ### indexOf and indexesOf -/
 
 theorem foldrIdx_start :
@@ -898,13 +556,6 @@ theorem indexesOf_cons [BEq α] : (x :: xs : List α).indexesOf y =
     bif x == y then 0 :: (xs.indexesOf y).map (· + 1) else (xs.indexesOf y).map (· + 1) := by
   simp [indexesOf, findIdxs_cons]
 
-@[simp] theorem indexOf_nil [BEq α] : ([] : List α).indexOf x = 0 := rfl
-
-theorem indexOf_cons [BEq α] :
-    (x :: xs : List α).indexOf y = bif x == y then 0 else xs.indexOf y + 1 := by
-  dsimp [indexOf]
-  simp [findIdx_cons]
-
 theorem indexOf_mem_indexesOf [BEq α] [LawfulBEq α] {xs : List α} (m : x ∈ xs) :
     xs.indexOf x ∈ xs.indexesOf x := by
   induction xs with
diff --git a/Batteries/Data/List/Pairwise.lean b/Batteries/Data/List/Pairwise.lean
index 9393d316b9..dbc2a48e0e 100644
--- a/Batteries/Data/List/Pairwise.lean
+++ b/Batteries/Data/List/Pairwise.lean
@@ -30,164 +30,6 @@ namespace List
 
 /-! ### Pairwise -/
 
-theorem rel_of_pairwise_cons (p : (a :: l).Pairwise R) : ∀ {a'}, a' ∈ l → R a a' :=
-  (pairwise_cons.1 p).1 _
-
-theorem Pairwise.of_cons (p : (a :: l).Pairwise R) : Pairwise R l :=
-  (pairwise_cons.1 p).2
-
-theorem Pairwise.tail : ∀ {l : List α} (_p : Pairwise R l), Pairwise R l.tail
-  | [], h => h
-  | _ :: _, h => h.of_cons
-
-theorem Pairwise.drop : ∀ {l : List α} {n : Nat}, List.Pairwise R l → List.Pairwise R (l.drop n)
-  | _, 0, h => h
-  | [], _ + 1, _ => List.Pairwise.nil
-  | _ :: _, n + 1, h => Pairwise.drop (n := n) (pairwise_cons.mp h).right
-
-theorem Pairwise.imp_of_mem {S : α → α → Prop}
-    (H : ∀ {a b}, a ∈ l → b ∈ l → R a b → S a b) (p : Pairwise R l) : Pairwise S l := by
-  induction p with
-  | nil => constructor
-  | @cons a l r _ ih =>
-    constructor
-    · exact fun x h => H (mem_cons_self ..) (mem_cons_of_mem _ h) <| r x h
-    · exact ih fun m m' => H (mem_cons_of_mem _ m) (mem_cons_of_mem _ m')
-
-theorem Pairwise.and (hR : Pairwise R l) (hS : Pairwise S l) :
-    l.Pairwise fun a b => R a b ∧ S a b := by
-  induction hR with
-  | nil => simp only [Pairwise.nil]
-  | cons R1 _ IH =>
-    simp only [Pairwise.nil, pairwise_cons] at hS ⊢
-    exact ⟨fun b bl => ⟨R1 b bl, hS.1 b bl⟩, IH hS.2⟩
-
-theorem pairwise_and_iff : l.Pairwise (fun a b => R a b ∧ S a b) ↔ Pairwise R l ∧ Pairwise S l :=
-  ⟨fun h => ⟨h.imp fun h => h.1, h.imp fun h => h.2⟩, fun ⟨hR, hS⟩ => hR.and hS⟩
-
-theorem Pairwise.imp₂ (H : ∀ a b, R a b → S a b → T a b)
-    (hR : Pairwise R l) (hS : l.Pairwise S) : l.Pairwise T :=
-  (hR.and hS).imp fun ⟨h₁, h₂⟩ => H _ _ h₁ h₂
-
-theorem Pairwise.iff_of_mem {S : α → α → Prop} {l : List α}
-    (H : ∀ {a b}, a ∈ l → b ∈ l → (R a b ↔ S a b)) : Pairwise R l ↔ Pairwise S l :=
-  ⟨Pairwise.imp_of_mem fun m m' => (H m m').1, Pairwise.imp_of_mem fun m m' => (H m m').2⟩
-
-theorem Pairwise.iff {S : α → α → Prop} (H : ∀ a b, R a b ↔ S a b) {l : List α} :
-    Pairwise R l ↔ Pairwise S l :=
-  Pairwise.iff_of_mem fun _ _ => H ..
-
-theorem pairwise_of_forall {l : List α} (H : ∀ x y, R x y) : Pairwise R l := by
-  induction l <;> simp [*]
-
-theorem Pairwise.and_mem {l : List α} :
-    Pairwise R l ↔ Pairwise (fun x y => x ∈ l ∧ y ∈ l ∧ R x y) l :=
-  Pairwise.iff_of_mem <| by simp (config := { contextual := true })
-
-theorem Pairwise.imp_mem {l : List α} :
-    Pairwise R l ↔ Pairwise (fun x y => x ∈ l → y ∈ l → R x y) l :=
-  Pairwise.iff_of_mem <| by simp (config := { contextual := true })
-
-theorem Pairwise.forall_of_forall_of_flip (h₁ : ∀ x ∈ l, R x x) (h₂ : Pairwise R l)
-    (h₃ : l.Pairwise (flip R)) : ∀ ⦃x⦄, x ∈ l → ∀ ⦃y⦄, y ∈ l → R x y := by
-  induction l with
-  | nil => exact forall_mem_nil _
-  | cons a l ih =>
-    rw [pairwise_cons] at h₂ h₃
-    simp only [mem_cons]
-    rintro x (rfl | hx) y (rfl | hy)
-    · exact h₁ _ (l.mem_cons_self _)
-    · exact h₂.1 _ hy
-    · exact h₃.1 _ hx
-    · exact ih (fun x hx => h₁ _ <| mem_cons_of_mem _ hx) h₂.2 h₃.2 hx hy
-
-theorem pairwise_singleton (R) (a : α) : Pairwise R [a] := by simp
-
-theorem pairwise_pair {a b : α} : Pairwise R [a, b] ↔ R a b := by simp
-
-theorem pairwise_append_comm {R : α → α → Prop} (s : ∀ {x y}, R x y → R y x) {l₁ l₂ : List α} :
-    Pairwise R (l₁ ++ l₂) ↔ Pairwise R (l₂ ++ l₁) := by
-  have (l₁ l₂ : List α) (H : ∀ x : α, x ∈ l₁ → ∀ y : α, y ∈ l₂ → R x y)
-    (x : α) (xm : x ∈ l₂) (y : α) (ym : y ∈ l₁) : R x y := s (H y ym x xm)
-  simp only [pairwise_append, and_left_comm]; rw [Iff.intro (this l₁ l₂) (this l₂ l₁)]
-
-theorem pairwise_middle {R : α → α → Prop} (s : ∀ {x y}, R x y → R y x) {a : α} {l₁ l₂ : List α} :
-    Pairwise R (l₁ ++ a :: l₂) ↔ Pairwise R (a :: (l₁ ++ l₂)) := by
-  show Pairwise R (l₁ ++ ([a] ++ l₂)) ↔ Pairwise R ([a] ++ l₁ ++ l₂)
-  rw [← append_assoc, pairwise_append, @pairwise_append _ _ ([a] ++ l₁), pairwise_append_comm s]
-  simp only [mem_append, or_comm]
-
-theorem Pairwise.of_map {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, S (f a) (f b) → R a b)
-    (p : Pairwise S (map f l)) : Pairwise R l :=
-  (pairwise_map.1 p).imp (H _ _)
-
-theorem Pairwise.map {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, R a b → S (f a) (f b))
-    (p : Pairwise R l) : Pairwise S (map f l) :=
-  pairwise_map.2 <| p.imp (H _ _)
-
-theorem pairwise_filterMap (f : β → Option α) {l : List β} :
-    Pairwise R (filterMap f l) ↔ Pairwise (fun a a' : β => ∀ b ∈ f a, ∀ b' ∈ f a', R b b') l := by
-  let _S (a a' : β) := ∀ b ∈ f a, ∀ b' ∈ f a', R b b'
-  simp only [Option.mem_def]
-  induction l with
-  | nil => simp only [filterMap, Pairwise.nil]
-  | cons a l IH => ?_
-  match e : f a with
-  | none =>
-    rw [filterMap_cons_none e, pairwise_cons]
-    simp only [e, false_implies, implies_true, true_and, IH]
-  | some b =>
-    rw [filterMap_cons_some e]
-    simpa [IH, e] using fun _ =>
-      ⟨fun h a ha b hab => h _ _ ha hab, fun h a b ha hab => h _ ha _ hab⟩
-
-theorem Pairwise.filter_map {S : β → β → Prop} (f : α → Option β)
-    (H : ∀ a a' : α, R a a' → ∀ b ∈ f a, ∀ b' ∈ f a', S b b') {l : List α} (p : Pairwise R l) :
-    Pairwise S (filterMap f l) :=
-  (pairwise_filterMap _).2 <| p.imp (H _ _)
-
-theorem pairwise_filter (p : α → Prop) [DecidablePred p] {l : List α} :
-    Pairwise R (filter p l) ↔ Pairwise (fun x y => p x → p y → R x y) l := by
-  rw [← filterMap_eq_filter, pairwise_filterMap]
-  simp
-
-theorem Pairwise.filter (p : α → Bool) : Pairwise R l → Pairwise R (filter p l) :=
-  Pairwise.sublist (filter_sublist _)
-
-theorem pairwise_join {L : List (List α)} :
-    Pairwise R (join L) ↔
-      (∀ l ∈ L, Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ x ∈ l₁, ∀ y ∈ l₂, R x y) L := by
-  induction L with
-  | nil => simp
-  | cons l L IH =>
-    simp only [join, pairwise_append, IH, mem_join, exists_imp, and_imp, forall_mem_cons,
-      pairwise_cons, and_assoc, and_congr_right_iff]
-    rw [and_comm, and_congr_left_iff]
-    intros; exact ⟨fun h a b c d e => h c d e a b, fun h c d e a b => h a b c d e⟩
-
-theorem pairwise_bind {R : β → β → Prop} {l : List α} {f : α → List β} :
-    List.Pairwise R (l.bind f) ↔
-      (∀ a ∈ l, Pairwise R (f a)) ∧ Pairwise (fun a₁ a₂ => ∀ x ∈ f a₁, ∀ y ∈ f a₂, R x y) l := by
-  simp [List.bind, pairwise_join, pairwise_map]
-
-theorem pairwise_iff_forall_sublist : l.Pairwise R ↔ (∀ {a b}, [a,b] <+ l → R a b) := by
-  induction l with
-  | nil => simp
-  | cons hd tl IH =>
-    rw [List.pairwise_cons]
-    constructor <;> intro h
-    · intro
-      | a, b, .cons _ hab => exact IH.mp h.2 hab
-      | _, b, .cons₂ _ hab => refine h.1 _ (hab.subset ?_); simp
-    · constructor
-      · intro x hx
-        apply h
-        rw [List.cons_sublist_cons, List.singleton_sublist]
-        exact hx
-      · apply IH.mpr
-        intro a b hab
-        apply h; exact hab.cons _
-
 @[deprecated pairwise_iff_forall_sublist (since := "2023-09-18")]
 theorem pairwise_of_reflexive_on_dupl_of_forall_ne [DecidableEq α] {l : List α} {r : α → α → Prop}
     (hr : ∀ a, 1 < count a l → r a a) (h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b) : l.Pairwise r := by
diff --git a/Batteries/Data/String/Lemmas.lean b/Batteries/Data/String/Lemmas.lean
index 5420651ba2..2edec48bde 100644
--- a/Batteries/Data/String/Lemmas.lean
+++ b/Batteries/Data/String/Lemmas.lean
@@ -337,7 +337,7 @@ theorem firstDiffPos_loop_eq (l₁ l₂ r₁ r₂ stop p)
   · next h =>
     rw [dif_neg] <;> simp [hstop, ← hl₁, ← hl₂, -Nat.not_lt, Nat.lt_min]
     intro h₁ h₂
-    have : ∀ {cs}, p < p + utf8Len cs → cs ≠ [] := by rintro _ h rfl; simp at h
+    have : ∀ {cs}, 0 < utf8Len cs → cs ≠ [] := by rintro _ h rfl; simp at h
     obtain ⟨a, as, e₁⟩ := List.exists_cons_of_ne_nil (this h₁)
     obtain ⟨b, bs, e₂⟩ := List.exists_cons_of_ne_nil (this h₂)
     exact h _ _ _ _ e₁ e₂
@@ -422,8 +422,9 @@ theorem splitAux_of_valid (p l m r acc) :
     splitAux ⟨l ++ m ++ r⟩ p ⟨utf8Len l⟩ ⟨utf8Len l + utf8Len m⟩ acc =
       acc.reverse ++ (List.splitOnP.go p r m.reverse).map mk := by
   unfold splitAux
-  simp only [List.append_assoc, atEnd_iff, endPos_eq, utf8Len_append, Pos.mk_le_mk, by
-    simpa using atEnd_of_valid (l ++ m) r, List.reverse_cons, dite_eq_ite]
+  simp only [List.append_assoc, atEnd_iff, endPos_eq, utf8Len_append, Pos.mk_le_mk,
+    Nat.add_le_add_iff_left, by simpa using atEnd_of_valid (l ++ m) r, List.reverse_cons,
+    dite_eq_ite]
   split
   · subst r; simpa [List.splitOnP.go] using extract_of_valid l m []
   · obtain ⟨c, r, rfl⟩ := r.exists_cons_of_ne_nil ‹_›
@@ -676,7 +677,7 @@ theorem foldrAux_of_valid (f : Char → α → α) (l m r a) :
   rw [← m.reverse_reverse]
   induction m.reverse generalizing r a with (unfold foldrAux; simp)
   | cons c m IH =>
-    rw [if_pos (by exact Nat.lt_add_of_pos_right add_csize_pos)]
+    rw [if_pos add_csize_pos]
     simp only [← Nat.add_assoc, by simpa using prev_of_valid (l ++ m.reverse) c r]
     simp only [by simpa using get_of_valid (l ++ m.reverse) (c :: r)]
     simpa using IH (c::r) (f c a)