From 6a63eb6a326181df29d95a84ce1f16c1145e66d8 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Fri, 7 Jun 2024 01:44:22 +0100
Subject: [PATCH] chore: merge bump/v4.9.0 branch (#826)

* chore: adaptations for nightly-2024-05-06 (#783)

* chore: adaptations for nightly-2024-05-11 (#794)

* chore: adaptations for nightly-2024-05-11

* oops

* fix test

* suggestion from review

* chore: adaptations for nightly-2024-06-06 (#825)

* chore: adaptations for nightly-2024-06-06

* move to v4.9.0.-rc1

* suggestions from review
---
 Batteries/CodeAction/Deprecated.lean  |    4 +-
 Batteries/Data/Array/Lemmas.lean      |  754 ---------------
 Batteries/Data/ByteArray.lean         |    3 -
 Batteries/Data/Fin/Basic.lean         |   14 -
 Batteries/Data/Fin/Lemmas.lean        |   32 +-
 Batteries/Data/List/Lemmas.lean       | 1264 +------------------------
 Batteries/Data/String/Lemmas.lean     |  123 +--
 Batteries/Lean/Delaborator.lean       |   18 +-
 Batteries/Tactic/Instances.lean       |    6 +-
 Batteries/Tactic/PrintDependents.lean |    4 +-
 Batteries/Tactic/PrintPrefix.lean     |    8 +-
 Batteries/Tactic/ShowUnused.lean      |    4 +-
 Batteries/WF.lean                     |    4 +
 lakefile.lean                         |    2 +-
 lean-toolchain                        |    2 +-
 test/list_sublists.lean               |    2 +-
 16 files changed, 48 insertions(+), 2196 deletions(-)

diff --git a/Batteries/CodeAction/Deprecated.lean b/Batteries/CodeAction/Deprecated.lean
index 1d74fea98c..f308992885 100644
--- a/Batteries/CodeAction/Deprecated.lean
+++ b/Batteries/CodeAction/Deprecated.lean
@@ -29,10 +29,10 @@ def deprecatedCodeActionProvider : CodeActionProvider := fun params snap => do
   let mut i := 0
   let doc ← readDoc
   let mut msgs := #[]
-  for m in snap.msgLog.msgs do
+  for m in snap.msgLog.toList do
     if m.data.isDeprecationWarning then
       if h : _ then
-        msgs := msgs.push (snap.cmdState.messages.msgs[i])
+        msgs := msgs.push (snap.cmdState.messages.toList[i])
     i := i + 1
   if msgs.isEmpty then return #[]
   let start := doc.meta.text.lspPosToUtf8Pos params.range.start
diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
index 01bd927b18..5a16a355e1 100644
--- a/Batteries/Data/Array/Lemmas.lean
+++ b/Batteries/Data/Array/Lemmas.lean
@@ -9,242 +9,8 @@ import Batteries.Data.Array.Basic
 import Batteries.Tactic.SeqFocus
 import Batteries.Util.ProofWanted
 
-@[simp] theorem getElem_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
-    a[i] = a[i.1] := rfl
-
-@[simp] theorem getElem?_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
-    [Decidable (Dom a i)] : a[i]? = a[i.1]? := rfl
-
-@[simp] theorem getElem!_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
-    [Decidable (Dom a i)] [Inhabited Elem] : a[i]! = a[i.1]! := rfl
-
-@[simp] theorem mkArray_data (n : Nat) (v : α) : (mkArray n v).data = List.replicate n v := rfl
-
-@[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
-    (mkArray n v)[i] = v := by simp [Array.getElem_eq_data_get]
-
 namespace Array
 
-attribute [simp] isEmpty uget
-
-@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
-
-@[simp] theorem toArray_data : (a : Array α) → a.data.toArray = a
-  | ⟨l⟩ => ext' (data_toArray l)
-
-@[simp] theorem data_length {l : Array α} : l.data.length = l.size := rfl
-
-/-- # mem -/
-
-theorem mem_data {a : α} {l : Array α} : a ∈ l.data ↔ a ∈ l := (mem_def _ _).symm
-
-theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun
-
-/-- # get lemmas -/
-
-theorem getElem?_mem {l : Array α} {i : Fin l.size} : l[i] ∈ l := by
-  erw [Array.mem_def, getElem_eq_data_get]
-  apply List.get_mem
-
-theorem getElem_fin_eq_data_get (a : Array α) (i : Fin _) : a[i] = a.data.get i := rfl
-
-@[simp] theorem ugetElem_eq_getElem (a : Array α) {i : USize} (h : i.toNat < a.size) :
-  a[i] = a[i.toNat] := rfl
-
-theorem getElem?_eq_getElem (a : Array α) (i : Nat) (h : i < a.size) : a[i]? = a[i] :=
-  getElem?_pos ..
-
-theorem get?_len_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none := by
-  simp [getElem?_neg, h]
-
-theorem getElem_mem_data (a : Array α) (h : i < a.size) : a[i] ∈ a.data := by
-  simp only [getElem_eq_data_get, List.get_mem]
-
-theorem getElem?_eq_data_get? (a : Array α) (i : Nat) : a[i]? = a.data.get? i := by
-  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]; rfl
-
-theorem get?_eq_data_get? (a : Array α) (i : Nat) : a.get? i = a.data.get? i :=
-  getElem?_eq_data_get? ..
-
-theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
-  simp [get!_eq_getD]
-
-@[simp] theorem back_eq_back? [Inhabited α] (a : Array α) : a.back = a.back?.getD default := by
-  simp [back, back?]
-
-@[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
-  simp [back?, getElem?_eq_data_get?]
-
-theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp
-
-theorem get?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
-    (a.push x)[i]? = some a[i] := by
-  rw [getElem?_pos, get_push_lt]
-
-theorem get?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x := by
-  rw [getElem?_pos, get_push_eq]
-
-theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x else a[i]? := by
-  match Nat.lt_trichotomy i a.size with
-  | Or.inl g =>
-    have h1 : i < a.size + 1 := by omega
-    have h2 : i ≠ a.size := by omega
-    simp [getElem?, size_push, g, h1, h2, get_push_lt]
-  | Or.inr (Or.inl heq) =>
-    simp [heq, getElem?_pos, get_push_eq]
-  | Or.inr (Or.inr g) =>
-    simp only [getElem?, size_push]
-    have h1 : ¬ (i < a.size) := by omega
-    have h2 : ¬ (i < a.size + 1) := by omega
-    have h3 : i ≠ a.size := by omega
-    simp [h1, h2, h3]
-
-@[simp] theorem get?_size {a : Array α} : a[a.size]? = none := by
-  simp only [getElem?, Nat.lt_irrefl, dite_false]
-
-@[simp] theorem data_set (a : Array α) (i v) : (a.set i v).data = a.data.set i.1 v := rfl
-
-theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
-    (a.set i v)[i.1] = v := by
-  simp only [set, getElem_eq_data_get, List.get_set_eq]
-
-theorem get?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
-    (a.set i v)[i.1]? = v := by simp [getElem?_pos, i.2]
-
-@[simp] theorem get?_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α)
-    (h : i.1 ≠ j) : (a.set i v)[j]? = a[j]? := by
-  by_cases j < a.size <;> simp [getElem?_pos, getElem?_neg, *]
-
-theorem get?_set (a : Array α) (i : Fin a.size) (j : Nat) (v : α) :
-    (a.set i v)[j]? = if i.1 = j then some v else a[j]? := by
-  if h : i.1 = j then subst j; simp [*] else simp [*]
-
-theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v : α) :
-    (a.set i v)[j]'(by simp [*]) = if i = j then v else a[j] := by
-  if h : i.1 = j then subst j; simp [*] else simp [*]
-
-@[simp] theorem get_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α) (hj : j < a.size)
-    (h : i.1 ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
-  simp only [set, getElem_eq_data_get, List.get_set_ne _ h]
-
-theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
-  (setD a i v)[i] = v := by
-  simp at h
-  simp only [setD, h, dite_true, get_set, ite_true]
-
-theorem set_set (a : Array α) (i : Fin a.size) (v v' : α) :
-    (a.set i v).set ⟨i, by simp [i.2]⟩ v' = a.set i v' := by simp [set, List.set_set]
-
-private theorem fin_cast_val (e : n = n') (i : Fin n) : e ▸ i = ⟨i.1, e ▸ i.2⟩ := by cases e; rfl
-
-theorem swap_def (a : Array α) (i j : Fin a.size) :
-    a.swap i j = (a.set i (a.get j)).set ⟨j.1, by simp [j.2]⟩ (a.get i) := by
-  simp [swap, fin_cast_val]
-
-theorem data_swap (a : Array α) (i j : Fin a.size) :
-    (a.swap i j).data = (a.data.set i (a.get j)).set j (a.get i) := by simp [swap_def]
-
-theorem get?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]? =
-    if j = k then some a[i.1] else if i = k then some a[j.1] else a[k]? := by
-  simp [swap_def, get?_set, ← getElem_fin_eq_data_get]
-
-@[simp] theorem swapAt_def (a : Array α) (i : Fin a.size) (v : α) :
-    a.swapAt i v = (a[i.1], a.set i v) := rfl
-
--- @[simp] -- FIXME: gives a weird linter error
-theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
-    a.swapAt! i v = (a[i], a.set ⟨i, h⟩ v) := by simp [swapAt!, h]
-
-@[simp] theorem data_pop (a : Array α) : a.pop.data = a.data.dropLast := by simp [pop]
-
-@[simp] theorem pop_empty : (#[] : Array α).pop = #[] := rfl
-
-@[simp] theorem pop_push (a : Array α) : (a.push x).pop = a := by simp [pop]
-
-@[simp] theorem getElem_pop (a : Array α) (i : Nat) (hi : i < a.pop.size) :
-    a.pop[i] = a[i]'(Nat.lt_of_lt_of_le (a.size_pop ▸ hi) (Nat.sub_le _ _)) :=
-  List.get_dropLast ..
-
-theorem eq_empty_of_size_eq_zero {as : Array α} (h : as.size = 0) : as = #[] := by
-  apply ext
-  · simp [h]
-  · intros; contradiction
-
-theorem eq_push_pop_back_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.size ≠ 0) :
-    as = as.pop.push as.back := by
-  apply ext
-  · simp [Nat.sub_add_cancel (Nat.zero_lt_of_ne_zero h)]
-  · intros i h h'
-    if hlt : i < as.pop.size then
-      rw [get_push_lt (h:=hlt), getElem_pop]
-    else
-      have heq : i = as.pop.size :=
-        Nat.le_antisymm (size_pop .. ▸ Nat.le_pred_of_lt h) (Nat.le_of_not_gt hlt)
-      cases heq; rw [get_push_eq, back, ←size_pop, get!_eq_getD, getD, dif_pos h]; rfl
-
-theorem eq_push_of_size_ne_zero {as : Array α} (h : as.size ≠ 0) :
-    ∃ (bs : Array α) (c : α), as = bs.push c :=
-  let _ : Inhabited α := ⟨as[0]⟩
-  ⟨as.pop, as.back, eq_push_pop_back_of_size_ne_zero h⟩
-
-theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl
-
-@[simp] theorem size_swap! (a : Array α) (i j) :
-    (a.swap! i j).size = a.size := by unfold swap!; split <;> (try split) <;> simp [size_swap]
-
-@[simp] theorem size_reverse (a : Array α) : a.reverse.size = a.size := by
-  let rec go (as : Array α) (i j) : (reverse.loop as i j).size = as.size := by
-    rw [reverse.loop]
-    if h : i < j then
-      have := reverse.termination h
-      simp [(go · (i+1) ⟨j-1, ·⟩), h]
-    else simp [h]
-    termination_by j - i
-  simp only [reverse]; split <;> simp [go]
-
-@[simp] theorem size_range {n : Nat} : (range n).size = n := by
-  unfold range
-  induction n with
-  | zero      => simp [Nat.fold]
-  | succ k ih => rw [Nat.fold, flip]; simpa
-
-@[simp] theorem reverse_data (a : Array α) : a.reverse.data = a.data.reverse := by
-  let rec go (as : Array α) (i j hj)
-      (h : i + j + 1 = a.size) (h₂ : as.size = a.size)
-      (H : ∀ k, as.data.get? k = if i ≤ k ∧ k ≤ j then a.data.get? k else a.data.reverse.get? k)
-      (k) : (reverse.loop as i ⟨j, hj⟩).data.get? k = a.data.reverse.get? k := by
-    rw [reverse.loop]; dsimp; split <;> rename_i h₁
-    · have := reverse.termination h₁
-      match j with | j+1 => ?_
-      simp at *
-      rw [(go · (i+1) j)]
-      · rwa [Nat.add_right_comm i]
-      · simp [size_swap, h₂]
-      · intro k
-        rw [← getElem?_eq_data_get?, get?_swap]
-        simp [getElem?_eq_data_get?, getElem_eq_data_get, ← List.get?_eq_get, H, Nat.le_of_lt h₁]
-        split <;> rename_i h₂
-        · simp [← h₂, Nat.not_le.2 (Nat.lt_succ_self _)]
-          exact (List.get?_reverse' _ _ (Eq.trans (by simp_arith) h)).symm
-        split <;> rename_i h₃
-        · simp [← h₃, Nat.not_le.2 (Nat.lt_succ_self _)]
-          exact (List.get?_reverse' _ _ (Eq.trans (by simp_arith) h)).symm
-        simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃),
-          Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))]
-    · rw [H]; split <;> rename_i h₂
-      · cases Nat.le_antisymm (Nat.not_lt.1 h₁) (Nat.le_trans h₂.1 h₂.2)
-        cases Nat.le_antisymm h₂.1 h₂.2
-        exact (List.get?_reverse' _ _ h).symm
-      · rfl
-    termination_by j - i
-  simp only [reverse]; split
-  · match a with | ⟨[]⟩ | ⟨[_]⟩ => rfl
-  · have := Nat.sub_add_cancel (Nat.le_of_not_le ‹_›)
-    refine List.ext <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
-    split; {rfl}; rename_i h
-    simp [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := a.size - 1), this] at h
-    rw [List.get?_eq_none.2 ‹_›, List.get?_eq_none.2 (a.data.length_reverse ▸ ‹_›)]
-
 theorem forIn_eq_data_forIn [Monad m]
     (as : Array α) (b : β) (f : α → β → m (ForInStep β)) :
     forIn as b f = forIn as.data b f := by
@@ -262,41 +28,6 @@ theorem forIn_eq_data_forIn [Monad m]
   conv => lhs; simp only [forIn, Array.forIn]
   rw [loop (Nat.zero_add _)]; rfl
 
-/-! ### foldl / foldr -/
-
--- This proof is the pure version of `Array.SatisfiesM_foldlM`,
--- reproduced to avoid a dependency on `SatisfiesM`.
-theorem foldl_induction
-    {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive 0 init) {f : β → α → β}
-    (hf : ∀ i : Fin as.size, ∀ b, motive i.1 b → motive (i.1 + 1) (f b as[i])) :
-    motive as.size (as.foldl f init) := by
-  let rec go {i j b} (h₁ : j ≤ as.size) (h₂ : as.size ≤ i + j) (H : motive j b) :
-    (motive as.size) (foldlM.loop (m := Id) f as as.size (Nat.le_refl _) i j b) := by
-    unfold foldlM.loop; split
-    · next hj =>
-      split
-      · cases Nat.not_le_of_gt (by simp [hj]) h₂
-      · exact go hj (by rwa [Nat.succ_add] at h₂) (hf ⟨j, hj⟩ b H)
-    · next hj => exact Nat.le_antisymm h₁ (Nat.ge_of_not_lt hj) ▸ H
-  simpa [foldl, foldlM] using go (Nat.zero_le _) (Nat.le_refl _) h0
-
--- This proof is the pure version of `Array.SatisfiesM_foldrM`,
--- reproduced to avoid a dependency on `SatisfiesM`.
-theorem foldr_induction
-    {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive as.size init) {f : α → β → β}
-    (hf : ∀ i : Fin as.size, ∀ b, motive (i.1 + 1) b → motive i.1 (f as[i] b)) :
-    motive 0 (as.foldr f init) := by
-  let rec go {i b} (hi : i ≤ as.size) (H : motive i b) :
-    (motive 0) (foldrM.fold (m := Id) f as 0 i hi b) := by
-    unfold foldrM.fold; simp; split
-    · next hi => exact (hi ▸ H)
-    · next hi =>
-      split; {simp at hi}
-      · next i hi' =>
-        exact go _ (hf ⟨i, hi'⟩ b H)
-  simp [foldr, foldrM]; split; {exact go _ h0}
-  · next h => exact (Nat.eq_zero_of_not_pos h ▸ h0)
-
 /-! ### zipWith / zip -/
 
 theorem zipWith_eq_zipWith_data (f : α → β → γ) (as : Array α) (bs : Array β) :
@@ -353,186 +84,13 @@ theorem size_zip (as : Array α) (bs : Array β) :
     (as.zip bs).size = min as.size bs.size :=
   as.size_zipWith bs Prod.mk
 
-/-! ### map -/
-
-@[simp] theorem mem_map {f : α → β} {l : Array α} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b := by
-  simp only [mem_def, map_data, List.mem_map]
-
-theorem mapM_eq_mapM_data [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
-    arr.mapM f = return mk (← arr.data.mapM f) := by
-  rw [mapM_eq_foldlM, foldlM_eq_foldlM_data, ← List.foldrM_reverse]
-  conv => rhs; rw [← List.reverse_reverse arr.data]
-  induction arr.data.reverse with
-  | nil => simp; rfl
-  | cons a l ih => simp [ih]; simp [map_eq_pure_bind, push]
-
-theorem mapM_map_eq_foldl (as : Array α) (f : α → β) (i) :
-    mapM.map (m := Id) f as i b = as.foldl (start := i) (fun r a => r.push (f a)) b := by
-  unfold mapM.map
-  split <;> rename_i h
-  · simp only [Id.bind_eq]
-    dsimp [foldl, Id.run, foldlM]
-    rw [mapM_map_eq_foldl, dif_pos (by omega), foldlM.loop, dif_pos h]
-    -- Calling `split` here gives a bad goal.
-    have : size as - i = Nat.succ (size as - i - 1) := by omega
-    rw [this]
-    simp [foldl, foldlM, Id.run, Nat.sub_add_eq]
-  · dsimp [foldl, Id.run, foldlM]
-    rw [dif_pos (by omega), foldlM.loop, dif_neg h]
-    rfl
-termination_by as.size - i
-
-theorem map_eq_foldl (as : Array α) (f : α → β) :
-    as.map f = as.foldl (fun r a => r.push (f a)) #[] :=
-  mapM_map_eq_foldl _ _ _
-
-theorem map_induction (as : Array α) (f : α → β) (motive : Nat → Prop) (h0 : motive 0)
-    (p : Fin as.size → β → Prop) (hs : ∀ i, motive i.1 → p i (f as[i]) ∧ motive (i+1)) :
-    motive as.size ∧
-      ∃ eq : (as.map f).size = as.size, ∀ i h, p ⟨i, h⟩ ((as.map f)[i]) := by
-  have t := foldl_induction (as := as) (β := Array β)
-    (motive := fun i arr => motive i ∧ arr.size = i ∧ ∀ i h2, p i arr[i.1])
-    (init := #[]) (f := fun r a => r.push (f a)) ?_ ?_
-  obtain ⟨m, eq, w⟩ := t
-  · refine ⟨m, by simpa [map_eq_foldl] using eq, ?_⟩
-    intro i h
-    simp [eq] at w
-    specialize w ⟨i, h⟩ trivial
-    simpa [map_eq_foldl] using w
-  · exact ⟨h0, rfl, nofun⟩
-  · intro i b ⟨m, ⟨eq, w⟩⟩
-    refine ⟨?_, ?_, ?_⟩
-    · exact (hs _ m).2
-    · simp_all
-    · intro j h
-      simp at h ⊢
-      by_cases h' : j < size b
-      · rw [get_push]
-        simp_all
-      · rw [get_push, dif_neg h']
-        simp only [show j = i by omega]
-        exact (hs _ m).1
-
-theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Prop)
-    (hs : ∀ i, p i (f as[i])) :
-    ∃ eq : (as.map f).size = as.size, ∀ i h, p ⟨i, h⟩ ((as.map f)[i]) := by
-  simpa using map_induction as f (fun _ => True) trivial p (by simp_all)
-
-@[simp] theorem getElem_map (f : α → β) (as : Array α) (i : Nat) (h) :
-    ((as.map f)[i]) = f (as[i]'(size_map .. ▸ h)) := by
-  have := map_spec as f (fun i b => b = f (as[i]))
-  simp only [implies_true, true_implies] at this
-  obtain ⟨eq, w⟩ := this
-  apply w
-  simp_all
-
-/-! ### mapIdx -/
-
--- This could also be prove from `SatisfiesM_mapIdxM`.
-theorem mapIdx_induction (as : Array α) (f : Fin as.size → α → β)
-    (motive : Nat → Prop) (h0 : motive 0)
-    (p : Fin as.size → β → Prop)
-    (hs : ∀ i, motive i.1 → p i (f i as[i]) ∧ motive (i + 1)) :
-    motive as.size ∧ ∃ eq : (Array.mapIdx as f).size = as.size,
-      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) := by
-  let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p ⟨i, h⟩ bs[i]) (hm : motive j) :
-    let arr : Array β := Array.mapIdxM.map (m := Id) as f i j h bs
-    motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i] := by
-    induction i generalizing j bs with simp [mapIdxM.map]
-    | zero =>
-      have := (Nat.zero_add _).symm.trans h
-      exact ⟨this ▸ hm, h₁ ▸ this, fun _ _ => h₂ ..⟩
-    | succ i ih =>
-      apply @ih (bs.push (f ⟨j, by omega⟩ as[j])) (j + 1) (by omega) (by simpa using h₁)
-      · intro i i_lt h'
-        rw [get_push]
-        split
-        · apply h₂
-        · simp only [size_push] at h'
-          obtain rfl : i = j := by omega
-          apply (hs ⟨i, by omega⟩ hm).1
-      · exact (hs ⟨j, by omega⟩ hm).2
-  simp [mapIdx, mapIdxM]; exact go rfl nofun h0
-
-theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β)
-    (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[i])) :
-    ∃ eq : (Array.mapIdx as f).size = as.size,
-      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) :=
-  (mapIdx_induction _ _ (fun _ => True) trivial p fun _ _ => ⟨hs .., trivial⟩).2
-
-@[simp] theorem size_mapIdx (a : Array α) (f : Fin a.size → α → β) : (a.mapIdx f).size = a.size :=
-  (mapIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
-
-@[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size :=
-  Array.size_mapIdx _ _
-
-@[simp] theorem getElem_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat)
-    (h : i < (mapIdx a f).size) :
-    haveI : i < a.size := by simp_all
-    (a.mapIdx f)[i] = f ⟨i, this⟩ a[i] :=
-  (mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
-
-/-! ### modify -/
-
-@[simp] theorem size_modify (a : Array α) (i : Nat) (f : α → α) : (a.modify i f).size = a.size := by
-  unfold modify modifyM Id.run
-  split <;> simp
-
-theorem get_modify {arr : Array α} {x i} (h : i < arr.size) :
-    (arr.modify x f).get ⟨i, by simp [h]⟩ =
-    if x = i then f (arr.get ⟨i, h⟩) else arr.get ⟨i, h⟩ := by
-  simp [modify, modifyM, Id.run]; split
-  · simp [get_set _ _ _ h]; split <;> simp [*]
-  · rw [if_neg (mt (by rintro rfl; exact h) ‹_›)]
-
 /-! ### filter -/
 
-@[simp] theorem filter_data (p : α → Bool) (l : Array α) :
-    (l.filter p).data = l.data.filter p := by
-  dsimp only [filter]
-  rw [foldl_eq_foldl_data]
-  generalize l.data = l
-  suffices ∀ a, (List.foldl (fun r a => if p a = true then push r a else r) a l).data =
-      a.data ++ List.filter p l by
-    simpa using this #[]
-  induction l with simp
-  | cons => split <;> simp [*]
-
-@[simp] theorem filter_filter (q) (l : Array α) :
-    filter p (filter q l) = filter (fun a => p a ∧ q a) l := by
-  apply ext'
-  simp only [filter_data, List.filter_filter]
-
 theorem size_filter_le (p : α → Bool) (l : Array α) :
     (l.filter p).size ≤ l.size := by
   simp only [← data_length, filter_data]
   apply List.length_filter_le
 
-@[simp] theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x := by
-  simp only [mem_def, filter_data, List.mem_filter]
-
-theorem mem_of_mem_filter {a : α} {l} (h : a ∈ filter p l) : a ∈ l :=
-  (mem_filter.mp h).1
-
-/-! ### filterMap -/
-
-@[simp] theorem filterMap_data (f : α → Option β) (l : Array α) :
-    (l.filterMap f).data = l.data.filterMap f := by
-  dsimp only [filterMap, filterMapM]
-  rw [foldlM_eq_foldlM_data]
-  generalize l.data = l
-  have this : ∀ a : Array β, (Id.run (List.foldlM (m := Id) ?_ a l)).data =
-    a.data ++ List.filterMap f l := ?_
-  exact this #[]
-  induction l
-  · simp_all [Id.run]
-  · simp_all [Id.run]
-    split <;> simp_all
-
-@[simp] theorem mem_filterMap (f : α → Option β) (l : Array α) {b : β} :
-    b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b := by
-  simp only [mem_def, filterMap_data, List.mem_filterMap]
-
 /-! ### join -/
 
 @[simp] theorem join_data {l : Array (Array α)} : l.join.data = (l.data.map data).join := by
@@ -554,322 +112,10 @@ theorem mem_join : ∀ {L : Array (Array α)}, a ∈ L.join ↔ ∃ l, l ∈ L 
   · rintro ⟨s, h₁, h₂⟩
     refine ⟨s.data, ⟨⟨s, h₁, rfl⟩, h₂⟩⟩
 
-/-! ### empty -/
-
-theorem size_empty : (#[] : Array α).size = 0 := rfl
-
-theorem empty_data : (#[] : Array α).data = [] := rfl
-
-/-! ### append -/
-
-theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] := rfl
-
-@[simp] theorem mem_append {a : α} {s t : Array α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
-  simp only [mem_def, append_data, List.mem_append]
-
-theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
-  simp only [size, append_data, List.length_append]
-
-theorem get_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
-    (as ++ bs)[i] = as[i] := by
-  simp only [getElem_eq_data_get]
-  have h' : i < (as.data ++ bs.data).length := by rwa [← data_length, append_data] at h
-  conv => rhs; rw [← List.get_append_left (bs:=bs.data) (h':=h')]
-  apply List.get_of_eq; rw [append_data]
-
-theorem get_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i)
-    (hlt : i - as.size < bs.size := Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) :
-    (as ++ bs)[i] = bs[i - as.size] := by
-  simp only [getElem_eq_data_get]
-  have h' : i < (as.data ++ bs.data).length := by rwa [← data_length, append_data] at h
-  conv => rhs; rw [← List.get_append_right (h':=h') (h:=Nat.not_lt_of_ge hle)]
-  apply List.get_of_eq; rw [append_data]
-
-@[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by
-  apply ext'; simp only [append_data, empty_data, List.append_nil]
-
-@[simp] theorem nil_append (as : Array α) : #[] ++ as = as := by
-  apply ext'; simp only [append_data, empty_data, List.nil_append]
-
-theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) := by
-  apply ext'; simp only [append_data, List.append_assoc]
-
-/-! ### extract -/
-
-theorem extract_loop_zero (as bs : Array α) (start : Nat) : extract.loop as 0 start bs = bs := by
-  rw [extract.loop]; split <;> rfl
-
-theorem extract_loop_succ (as bs : Array α) (size start : Nat) (h : start < as.size) :
-    extract.loop as (size+1) start bs = extract.loop as size (start+1) (bs.push as[start]) := by
-  rw [extract.loop, dif_pos h]; rfl
-
-theorem extract_loop_of_ge (as bs : Array α) (size start : Nat) (h : start ≥ as.size) :
-    extract.loop as size start bs = bs := by
-  rw [extract.loop, dif_neg (Nat.not_lt_of_ge h)]
-
-theorem extract_loop_eq_aux (as bs : Array α) (size start : Nat) :
-    extract.loop as size start bs = bs ++ extract.loop as size start #[] := by
-  induction size using Nat.recAux generalizing start bs with
-  | zero => rw [extract_loop_zero, extract_loop_zero, append_nil]
-  | succ size ih =>
-    if h : start < as.size then
-      rw [extract_loop_succ (h:=h), ih (bs.push _), push_eq_append_singleton]
-      rw [extract_loop_succ (h:=h), ih (#[].push _), push_eq_append_singleton, nil_append]
-      rw [append_assoc]
-    else
-      rw [extract_loop_of_ge (h:=Nat.le_of_not_lt h)]
-      rw [extract_loop_of_ge (h:=Nat.le_of_not_lt h)]
-      rw [append_nil]
-
-theorem extract_loop_eq (as bs : Array α) (size start : Nat) (h : start + size ≤ as.size) :
-  extract.loop as size start bs = bs ++ as.extract start (start + size) := by
-  simp [extract]; rw [extract_loop_eq_aux, Nat.min_eq_left h, Nat.add_sub_cancel_left]
-
-theorem size_extract_loop (as bs : Array α) (size start : Nat) :
-    (extract.loop as size start bs).size = bs.size + min size (as.size - start) := by
-  induction size using Nat.recAux generalizing start bs with
-  | zero => rw [extract_loop_zero, Nat.zero_min, Nat.add_zero]
-  | succ size ih =>
-    if h : start < as.size then
-      rw [extract_loop_succ (h:=h), ih, size_push, Nat.add_assoc, ←Nat.add_min_add_left,
-        Nat.sub_succ, Nat.one_add, Nat.one_add, Nat.succ_pred_eq_of_pos (Nat.sub_pos_of_lt h)]
-    else
-      have h := Nat.le_of_not_gt h
-      rw [extract_loop_of_ge (h:=h), Nat.sub_eq_zero_of_le h, Nat.min_zero, Nat.add_zero]
-
-@[simp] theorem size_extract (as : Array α) (start stop : Nat) :
-    (as.extract start stop).size = min stop as.size - start := by
-  simp [extract]; rw [size_extract_loop, size_empty, Nat.zero_add, Nat.sub_min_sub_right,
-    Nat.min_assoc, Nat.min_self]
-
-theorem get_extract_loop_lt_aux (as bs : Array α) (size start : Nat) (hlt : i < bs.size) :
-    i < (extract.loop as size start bs).size := by
-  rw [size_extract_loop]
-  apply Nat.lt_of_lt_of_le hlt
-  exact Nat.le_add_right ..
-
-theorem get_extract_loop_lt (as bs : Array α) (size start : Nat) (hlt : i < bs.size)
-    (h := get_extract_loop_lt_aux as bs size start hlt) :
-    (extract.loop as size start bs)[i] = bs[i] := by
-  apply Eq.trans _ (get_append_left (bs:=extract.loop as size start #[]) hlt)
-  · rw [size_append]; exact Nat.lt_of_lt_of_le hlt (Nat.le_add_right ..)
-  · congr; rw [extract_loop_eq_aux]
-
-theorem get_extract_loop_ge_aux (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
-    (h : i < (extract.loop as size start bs).size) : start + i - bs.size < as.size := by
-  have h : i < bs.size + (as.size - start) := by
-      apply Nat.lt_of_lt_of_le h
-      rw [size_extract_loop]
-      apply Nat.add_le_add_left
-      exact Nat.min_le_right ..
-  rw [Nat.add_sub_assoc hge]
-  apply Nat.add_lt_of_lt_sub'
-  exact Nat.sub_lt_left_of_lt_add hge h
-
-theorem get_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
-    (h : i < (extract.loop as size start bs).size)
-    (h' := get_extract_loop_ge_aux as bs size start hge h) :
-    (extract.loop as size start bs)[i] = as[start + i - bs.size] := by
-  induction size using Nat.recAux generalizing start bs with
-  | zero =>
-    rw [size_extract_loop, Nat.zero_min, Nat.add_zero] at h
-    absurd h; exact Nat.not_lt_of_ge hge
-  | succ size ih =>
-    have : start < as.size := by
-      apply Nat.lt_of_le_of_lt (Nat.le_add_right start (i - bs.size))
-      rwa [← Nat.add_sub_assoc hge]
-    have : i < (extract.loop as size (start+1) (bs.push as[start])).size := by
-      rwa [← extract_loop_succ]
-    have heq : (extract.loop as (size+1) start bs)[i] =
-        (extract.loop as size (start+1) (bs.push as[start]))[i] := by
-      congr 1; rw [extract_loop_succ]
-    rw [heq]
-    if hi : bs.size = i then
-      cases hi
-      have h₁ : bs.size < (bs.push as[start]).size := by rw [size_push]; exact Nat.lt_succ_self ..
-      have h₂ : bs.size < (extract.loop as size (start+1) (bs.push as[start])).size := by
-        rw [size_extract_loop]; apply Nat.lt_of_lt_of_le h₁; exact Nat.le_add_right ..
-      have h : (extract.loop as size (start + 1) (push bs as[start]))[bs.size] = as[start] := by
-        rw [get_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, get_push_eq]
-      rw [h]; congr; rw [Nat.add_sub_cancel]
-    else
-      have hge : bs.size + 1 ≤ i := Nat.lt_of_le_of_ne hge hi
-      rw [ih (bs.push as[start]) (start+1) ((size_push ..).symm ▸ hge)]
-      congr 1; rw [size_push, Nat.add_right_comm, Nat.add_sub_add_right]
-
-theorem get_extract_aux {as : Array α} {start stop : Nat} (h : i < (as.extract start stop).size) :
-    start + i < as.size := by
-  rw [size_extract] at h; apply Nat.add_lt_of_lt_sub'; apply Nat.lt_of_lt_of_le h
-  apply Nat.sub_le_sub_right; apply Nat.min_le_right
-
-@[simp] theorem get_extract {as : Array α} {start stop : Nat}
-    (h : i < (as.extract start stop).size) :
-    (as.extract start stop)[i] = as[start + i]'(get_extract_aux h) :=
-  show (extract.loop as (min stop as.size - start) start #[])[i]
-    = as[start + i]'(get_extract_aux h) by rw [get_extract_loop_ge]; rfl; exact Nat.zero_le _
-
-@[simp] theorem extract_all (as : Array α) : as.extract 0 as.size = as := by
-  apply ext
-  · rw [size_extract, Nat.min_self, Nat.sub_zero]
-  · intros; rw [get_extract]; congr; rw [Nat.zero_add]
-
-theorem extract_empty_of_stop_le_start (as : Array α) {start stop : Nat} (h : stop ≤ start) :
-    as.extract start stop = #[] := by
-  simp [extract]; rw [←Nat.sub_min_sub_right, Nat.sub_eq_zero_of_le h, Nat.zero_min,
-    extract_loop_zero]
-
-theorem extract_empty_of_size_le_start (as : Array α) {start stop : Nat} (h : as.size ≤ start) :
-    as.extract start stop = #[] := by
-  simp [extract]; rw [←Nat.sub_min_sub_right, Nat.sub_eq_zero_of_le h, Nat.min_zero,
-    extract_loop_zero]
-
-@[simp] theorem extract_empty (start stop : Nat) : (#[] : Array α).extract start stop = #[] :=
-  extract_empty_of_size_le_start _ (Nat.zero_le _)
-
-/-! ### any -/
-
--- Auxiliary for `any_iff_exists`.
-theorem anyM_loop_iff_exists (p : α → Bool) (as : Array α) (start stop) (h : stop ≤ as.size) :
-    anyM.loop (m := Id) p as stop h start = true ↔
-      ∃ i : Fin as.size, start ≤ ↑i ∧ ↑i < stop ∧ p as[i] = true := by
-  unfold anyM.loop
-  split <;> rename_i h₁
-  · dsimp
-    split <;> rename_i h₂
-    · simp only [true_iff]
-      refine ⟨⟨start, by omega⟩, by dsimp; omega, by dsimp; omega, h₂⟩
-    · rw [anyM_loop_iff_exists]
-      constructor
-      · rintro ⟨i, ge, lt, h⟩
-        have : start ≠ i := by rintro rfl; omega
-        exact ⟨i, by omega, lt, h⟩
-      · rintro ⟨i, ge, lt, h⟩
-        have : start ≠ i := by rintro rfl; erw [h] at h₂; simp_all
-        exact ⟨i, by omega, lt, h⟩
-  · simp
-    omega
-termination_by stop - start
-
--- This could also be proved from `SatisfiesM_anyM_iff_exists` in
--- `Batteries.Data.Array.Init.Monadic`.
-theorem any_iff_exists (p : α → Bool) (as : Array α) (start stop) :
-    any as p start stop ↔ ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop ∧ p as[i] := by
-  dsimp [any, anyM, Id.run]
-  split
-  · rw [anyM_loop_iff_exists]; rfl
-  · rw [anyM_loop_iff_exists]
-    constructor
-    · rintro ⟨i, ge, _, h⟩
-      exact ⟨i, by omega, by omega, h⟩
-    · rintro ⟨i, ge, _, h⟩
-      exact ⟨i, by omega, by omega, h⟩
-
-theorem any_eq_true (p : α → Bool) (as : Array α) :
-    any as p ↔ ∃ i : Fin as.size, p as[i] := by simp [any_iff_exists, Fin.isLt]
-
-theorem any_def {p : α → Bool} (as : Array α) : as.any p = as.data.any p := by
-  rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]; simp only [List.mem_iff_get]
-  exact ⟨fun ⟨i, h⟩ => ⟨_, ⟨i, rfl⟩, h⟩, fun ⟨_, ⟨i, rfl⟩, h⟩ => ⟨i, h⟩⟩
-
-/-! ### all -/
-
-theorem all_eq_not_any_not (p : α → Bool) (as : Array α) (start stop) :
-    all as p start stop = !(any as (!p ·) start stop) := by
-  dsimp [all, allM]
-  rfl
-
-theorem all_iff_forall (p : α → Bool) (as : Array α) (start stop) :
-    all as p start stop ↔ ∀ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop → p as[i] := by
-  rw [all_eq_not_any_not]
-  suffices ¬(any as (!p ·) start stop = true) ↔
-      ∀ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop → p as[i] by
-    simp_all
-  rw [any_iff_exists]
-  simp
-
-theorem all_eq_true (p : α → Bool) (as : Array α) : all as p ↔ ∀ i : Fin as.size, p as[i] := by
-  simp [all_iff_forall, Fin.isLt]
-
-theorem all_def {p : α → Bool} (as : Array α) : as.all p = as.data.all p := by
-  rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]; simp only [List.mem_iff_get]
-  constructor
-  · rintro w x ⟨r, rfl⟩
-    rw [← getElem_eq_data_get]
-    apply w
-  · intro w i
-    exact w as[i] ⟨i, (getElem_eq_data_get as i.2).symm⟩
-
-theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by
-  simp only [all_def, List.all_eq_true, mem_def]
-
-/-! ### contains -/
-
-theorem contains_def [DecidableEq α] {a : α} {as : Array α} : as.contains a ↔ a ∈ as := by
-  rw [mem_def, contains, any_def, List.any_eq_true]; simp [and_comm]
-
-instance [DecidableEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
-  decidable_of_iff _ contains_def
-
 /-! ### erase -/
 
 @[simp] proof_wanted erase_data [BEq α] {l : Array α} {a : α} : (l.erase a).data = l.data.erase a
 
-/-! ### swap -/
-
-@[simp] theorem get_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.val] = a[i] :=
-  by simp only [swap, fin_cast_val, get_eq_getElem, getElem_set_eq, getElem_fin]
-
-@[simp] theorem get_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.val] = a[j] :=
-  if he : ((Array.size_set _ _ _).symm ▸ j).val = i.val then by
-    simp only [←he, fin_cast_val, get_swap_right, getElem_fin]
-  else by
-    apply Eq.trans
-    · apply Array.get_set_ne
-      · simp only [size_set, Fin.is_lt]
-      · assumption
-    · simp [get_set_ne]
-
-@[simp] theorem get_swap_of_ne (a : Array α) {i j : Fin a.size} (hp : p < a.size)
-    (hi : p ≠ i) (hj : p ≠ j) : (a.swap i j)[p]'(a.size_swap .. |>.symm ▸ hp) = a[p] := by
-  apply Eq.trans
-  · have : ((a.size_set i (a.get j)).symm ▸ j).val = j.val := by simp only [fin_cast_val]
-    apply Array.get_set_ne
-    · simp only [this]
-      apply Ne.symm
-      · assumption
-  · apply Array.get_set_ne
-    · apply Ne.symm
-      · assumption
-
-theorem get_swap (a : Array α) (i j : Fin a.size) (k : Nat) (hk: k < a.size) :
-    (a.swap i j)[k]'(by simp_all) = if k = i then a[j] else if k = j then a[i]  else a[k] := by
-  split
-  · simp_all only [get_swap_left]
-  · split <;> simp_all
-
-theorem get_swap' (a : Array α) (i j : Fin a.size) (k : Nat) (hk' : k < (a.swap i j).size) :
-    (a.swap i j)[k] = if k = i then a[j] else if k = j then a[i] else a[k]'(by simp_all) := by
-  apply get_swap
-
-@[simp] theorem swap_swap (a : Array α) {i j : Fin a.size} :
-    (a.swap i j).swap ⟨i.1, (a.size_swap ..).symm ▸i.2⟩ ⟨j.1, (a.size_swap ..).symm ▸j.2⟩ = a := by
-  apply ext
-  · simp only [size_swap]
-  · intros
-    simp only [get_swap']
-    split
-    · simp_all
-    · split <;> simp_all
-
-theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i := by
-  apply ext
-  · simp only [size_swap]
-  · intros
-    simp only [get_swap']
-    split
-    · split <;> simp_all
-    · split <;> simp_all
-
 /-! ### shrink -/
 
 theorem size_shrink_loop (a : Array α) (n) : (shrink.loop n a).size = a.size - n := by
diff --git a/Batteries/Data/ByteArray.lean b/Batteries/Data/ByteArray.lean
index 4788ecbb36..f147eaf47b 100644
--- a/Batteries/Data/ByteArray.lean
+++ b/Batteries/Data/ByteArray.lean
@@ -14,9 +14,6 @@ theorem getElem_eq_data_getElem (a : ByteArray) (h : i < a.size) : a[i] = a.data
 
 /-! ### uget/uset -/
 
-@[simp] theorem ugetElem_eq_getElem (a : ByteArray) {i : USize} (h : i.toNat < a.size) :
-    a[i] = a[i.toNat] := rfl
-
 @[simp] theorem uset_eq_set (a : ByteArray) {i : USize} (h : i.toNat < a.size) (v : UInt8) :
     a.uset i v h = a.set ⟨i.toNat, h⟩ v := rfl
 
diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean
index 495344f90f..3632d4f254 100644
--- a/Batteries/Data/Fin/Basic.lean
+++ b/Batteries/Data/Fin/Basic.lean
@@ -14,17 +14,3 @@ def enum (n) : Array (Fin n) := Array.ofFn id
 
 /-- `list n` is the list of all elements of `Fin n` in order -/
 def list (n) : List (Fin n) := (enum n).data
-
-/-- Folds over `Fin n` from the left: `foldl 3 f x = f (f (f x 0) 1) 2`. -/
-@[inline] def foldl (n) (f : α → Fin n → α) (init : α) : α := loop init 0 where
-  /-- Inner loop for `Fin.foldl`. `Fin.foldl.loop n f x i = f (f (f x i) ...) (n-1)`  -/
-  loop (x : α) (i : Nat) : α :=
-    if h : i < n then loop (f x ⟨i, h⟩) (i+1) else x
-  termination_by n - i
-
-/-- Folds over `Fin n` from the right: `foldr 3 f x = f 0 (f 1 (f 2 x))`. -/
-@[inline] def foldr (n) (f : Fin n → α → α) (init : α) : α := loop ⟨n, Nat.le_refl n⟩ init where
-  /-- Inner loop for `Fin.foldr`. `Fin.foldr.loop n f i x = f 0 (f ... (f (i-1) x))`  -/
-  loop : {i // i ≤ n} → α → α
-  | ⟨0, _⟩, x => x
-  | ⟨i+1, h⟩, x => loop ⟨i, Nat.le_of_lt h⟩ (f ⟨i, h⟩ x)
diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean
index 7167efa0ed..a310aa6f93 100644
--- a/Batteries/Data/Fin/Lemmas.lean
+++ b/Batteries/Data/Fin/Lemmas.lean
@@ -23,6 +23,8 @@ protected theorem le_antisymm {x y : Fin n} (h1 : x ≤ y) (h2 : y ≤ x) : x =
 
 @[simp] theorem size_enum (n) : (enum n).size = n := Array.size_ofFn ..
 
+@[simp] theorem enum_zero : (enum 0) = #[] := by simp [enum, Array.ofFn, Array.ofFn.go]
+
 @[simp] theorem getElem_enum (i) (h : i < (enum n).size) : (enum n)[i] = ⟨i, size_enum n ▸ h⟩ :=
   Array.getElem_ofFn ..
 
@@ -31,7 +33,7 @@ protected theorem le_antisymm {x y : Fin n} (h1 : x ≤ y) (h2 : y ≤ x) : x =
 @[simp] theorem get_list (i : Fin (list n).length) : (list n).get i = i.cast (length_list n) := by
   cases i; simp only [list]; rw [← Array.getElem_eq_data_get, getElem_enum, cast_mk]
 
-@[simp] theorem list_zero : list 0 = [] := rfl
+@[simp] theorem list_zero : list 0 = [] := by simp [list]
 
 theorem list_succ (n) : list (n+1) = 0 :: (list n).map Fin.succ := by
   apply List.ext_get; simp; intro i; cases i <;> simp
@@ -70,7 +72,7 @@ theorem foldl_loop (f : α → Fin (n+1) → α) (x) (h : m < n+1) :
     rw [foldl_loop_lt, foldl_loop_eq, foldl_loop_eq]
 termination_by n - m
 
-@[simp] theorem foldl_zero (f : α → Fin 0 → α) (x) : foldl 0 f x = x := rfl
+@[simp] theorem foldl_zero (f : α → Fin 0 → α) (x) : foldl 0 f x = x := by simp [foldl, foldl.loop]
 
 theorem foldl_succ (f : α → Fin (n+1) → α) (x) :
     foldl (n+1) f x = foldl n (fun x i => f x i.succ) (f x 0) := foldl_loop ..
@@ -79,43 +81,47 @@ theorem foldl_succ_last (f : α → Fin (n+1) → α) (x) :
     foldl (n+1) f x = f (foldl n (f · ·.castSucc) x) (last n) := by
   rw [foldl_succ]
   induction n generalizing x with
-  | zero => rfl
+  | zero => simp [foldl_succ, Fin.last]
   | succ n ih => rw [foldl_succ, ih (f · ·.succ), foldl_succ]; simp [succ_castSucc]
 
 theorem foldl_eq_foldl_list (f : α → Fin n → α) (x) : foldl n f x = (list n).foldl f x := by
   induction n generalizing x with
-  | zero => rfl
+  | zero => rw [foldl_zero, list_zero, List.foldl_nil]
   | succ n ih => rw [foldl_succ, ih, list_succ, List.foldl_cons, List.foldl_map]
 
 /-! ### foldr -/
 
-theorem foldr_loop_zero (f : Fin n → α → α) (x) : foldr.loop n f ⟨0, Nat.zero_le _⟩ x = x := rfl
+unseal foldr.loop in
+theorem foldr_loop_zero (f : Fin n → α → α) (x) : foldr.loop n f ⟨0, Nat.zero_le _⟩ x = x :=
+  rfl
 
+unseal foldr.loop in
 theorem foldr_loop_succ (f : Fin n → α → α) (x) (h : m < n) :
-    foldr.loop n f ⟨m+1, h⟩ x = foldr.loop n f ⟨m, Nat.le_of_lt h⟩ (f ⟨m, h⟩ x) := rfl
+    foldr.loop n f ⟨m+1, h⟩ x = foldr.loop n f ⟨m, Nat.le_of_lt h⟩ (f ⟨m, h⟩ x) :=
+  rfl
 
 theorem foldr_loop (f : Fin (n+1) → α → α) (x) (h : m+1 ≤ n+1) :
     foldr.loop (n+1) f ⟨m+1, h⟩ x =
       f 0 (foldr.loop n (fun i => f i.succ) ⟨m, Nat.le_of_succ_le_succ h⟩ x) := by
   induction m generalizing x with
   | zero => simp [foldr_loop_zero, foldr_loop_succ]
-  | succ m ih => rw [foldr_loop_succ, ih]; rfl
+  | succ m ih => rw [foldr_loop_succ, ih, foldr_loop_succ, Fin.succ]
 
-@[simp] theorem foldr_zero (f : Fin 0 → α → α) (x) : foldr 0 f x = x := rfl
+@[simp] theorem foldr_zero (f : Fin 0 → α → α) (x) :
+    foldr 0 f x = x := foldr_loop_zero ..
 
 theorem foldr_succ (f : Fin (n+1) → α → α) (x) :
     foldr (n+1) f x = f 0 (foldr n (fun i => f i.succ) x) := foldr_loop ..
 
 theorem foldr_succ_last (f : Fin (n+1) → α → α) (x) :
     foldr (n+1) f x = foldr n (f ·.castSucc) (f (last n) x) := by
-  rw [foldr_succ]
   induction n generalizing x with
-  | zero => rfl
+  | zero => simp [foldr_succ, Fin.last]
   | succ n ih => rw [foldr_succ, ih (f ·.succ), foldr_succ]; simp [succ_castSucc]
 
 theorem foldr_eq_foldr_list (f : Fin n → α → α) (x) : foldr n f x = (list n).foldr f x := by
   induction n with
-  | zero => rfl
+  | zero => rw [foldr_zero, list_zero, List.foldr_nil]
   | succ n ih => rw [foldr_succ, ih, list_succ, List.foldr_cons, List.foldr_map]
 
 /-! ### foldl/foldr -/
@@ -123,11 +129,11 @@ theorem foldr_eq_foldr_list (f : Fin n → α → α) (x) : foldr n f x = (list
 theorem foldl_rev (f : Fin n → α → α) (x) :
     foldl n (fun x i => f i.rev x) x = foldr n f x := by
   induction n generalizing x with
-  | zero => rfl
+  | zero => simp
   | succ n ih => rw [foldl_succ, foldr_succ_last, ← ih]; simp [rev_succ]
 
 theorem foldr_rev (f : α → Fin n → α) (x) :
      foldr n (fun i x => f x i.rev) x = foldl n f x := by
   induction n generalizing x with
-  | zero => rfl
+  | zero => simp
   | succ n ih => rw [foldl_succ_last, foldr_succ, ← ih]; simp [rev_succ]
diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
index d23566b21f..6109b4c9be 100644
--- a/Batteries/Data/List/Lemmas.lean
+++ b/Batteries/Data/List/Lemmas.lean
@@ -12,396 +12,22 @@ namespace List
 
 open Nat
 
-/-! # Basic properties of Lists -/
-
-theorem cons_ne_nil (a : α) (l : List α) : a :: l ≠ [] := nofun
-
-@[simp]
-theorem cons_ne_self (a : α) (l : List α) : a :: l ≠ l := mt (congrArg length) (Nat.succ_ne_self _)
-
-theorem head_eq_of_cons_eq (H : h₁ :: t₁ = h₂ :: t₂) : h₁ = h₂ := (cons.inj H).1
-
-theorem tail_eq_of_cons_eq (H : h₁ :: t₁ = h₂ :: t₂) : t₁ = t₂ := (cons.inj H).2
-
-theorem cons_inj (a : α) {l l' : List α} : a :: l = a :: l' ↔ l = l' :=
-  ⟨tail_eq_of_cons_eq, congrArg _⟩
-
-theorem cons_eq_cons {a b : α} {l l' : List α} : a :: l = b :: l' ↔ a = b ∧ l = l' :=
-  List.cons.injEq .. ▸ .rfl
-
-theorem exists_cons_of_ne_nil : ∀ {l : List α}, l ≠ [] → ∃ b L, l = b :: L
-  | c :: l', _ => ⟨c, l', rfl⟩
-
-/-! ### length -/
-
-@[simp 1100] theorem length_singleton (a : α) : length [a] = 1 := rfl
-
-theorem length_pos_of_mem {a : α} : ∀ {l : List α}, a ∈ l → 0 < length l
-  | _::_, _ => Nat.zero_lt_succ _
-
-theorem exists_mem_of_length_pos : ∀ {l : List α}, 0 < length l → ∃ a, a ∈ l
-  | _::_, _ => ⟨_, .head ..⟩
-
-theorem length_pos_iff_exists_mem {l : List α} : 0 < length l ↔ ∃ a, a ∈ l :=
-  ⟨exists_mem_of_length_pos, fun ⟨_, h⟩ => length_pos_of_mem h⟩
-
-theorem exists_cons_of_length_pos : ∀ {l : List α}, 0 < l.length → ∃ h t, l = h :: t
-  | _::_, _ => ⟨_, _, rfl⟩
-
-theorem length_pos_iff_exists_cons :
-    ∀ {l : List α}, 0 < l.length ↔ ∃ h t, l = h :: t :=
-  ⟨exists_cons_of_length_pos, fun ⟨_, _, eq⟩ => eq ▸ Nat.succ_pos _⟩
-
-theorem exists_cons_of_length_succ :
-    ∀ {l : List α}, l.length = n + 1 → ∃ h t, l = h :: t
-  | _::_, _ => ⟨_, _, rfl⟩
-
-attribute [simp] length_eq_zero -- TODO: suggest to core
-
-@[simp]
-theorem length_pos {l : List α} : 0 < length l ↔ l ≠ [] :=
-  Nat.pos_iff_ne_zero.trans (not_congr length_eq_zero)
-
-theorem exists_mem_of_ne_nil (l : List α) (h : l ≠ []) : ∃ x, x ∈ l :=
-  exists_mem_of_length_pos (length_pos.2 h)
-
-theorem length_eq_one {l : List α} : length l = 1 ↔ ∃ a, l = [a] :=
-  ⟨fun h => match l, h with | [_], _ => ⟨_, rfl⟩, fun ⟨_, h⟩ => by simp [h]⟩
-
 /-! ### mem -/
 
-theorem mem_nil_iff (a : α) : a ∈ ([] : List α) ↔ False := by simp
-
 @[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
   simp [Array.mem_def]
 
-theorem mem_singleton_self (a : α) : a ∈ [a] := mem_cons_self _ _
-
-theorem eq_of_mem_singleton : a ∈ [b] → a = b
-  | .head .. => rfl
-
-@[simp 1100] theorem mem_singleton {a b : α} : a ∈ [b] ↔ a = b :=
-  ⟨eq_of_mem_singleton, (by simp [·])⟩
-
-theorem mem_of_mem_cons_of_mem : ∀ {a b : α} {l : List α}, a ∈ b :: l → b ∈ l → a ∈ l
-  | _, _, _, .head .., h | _, _, _, .tail _ h, _ => h
-
-theorem eq_or_ne_mem_of_mem {a b : α} {l : List α} (h' : a ∈ b :: l) : a = b ∨ (a ≠ b ∧ a ∈ l) :=
-  (Classical.em _).imp_right fun h => ⟨h, (mem_cons.1 h').resolve_left h⟩
-
-theorem ne_nil_of_mem {a : α} {l : List α} (h : a ∈ l) : l ≠ [] := by cases h <;> nofun
-
-theorem append_of_mem {a : α} {l : List α} : a ∈ l → ∃ s t : List α, l = s ++ a :: t
-  | .head l => ⟨[], l, rfl⟩
-  | .tail b h => let ⟨s, t, h'⟩ := append_of_mem h; ⟨b::s, t, by rw [h', cons_append]⟩
-
-theorem elem_iff [BEq α] [LawfulBEq α] {a : α} {as : List α} :
-    elem a as = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
-
-@[simp] theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
-    elem a as = decide (a ∈ as) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
-
-theorem mem_of_ne_of_mem {a y : α} {l : List α} (h₁ : a ≠ y) (h₂ : a ∈ y :: l) : a ∈ l :=
-  Or.elim (mem_cons.mp h₂) (absurd · h₁) (·)
-
-theorem ne_of_not_mem_cons {a b : α} {l : List α} : a ∉ b::l → a ≠ b := mt (· ▸ .head _)
-
-theorem not_mem_of_not_mem_cons {a b : α} {l : List α} : a ∉ b::l → a ∉ l := mt (.tail _)
-
-theorem not_mem_cons_of_ne_of_not_mem {a y : α} {l : List α} : a ≠ y → a ∉ l → a ∉ y::l :=
-  mt ∘ mem_of_ne_of_mem
-
-theorem ne_and_not_mem_of_not_mem_cons {a y : α} {l : List α} : a ∉ y::l → a ≠ y ∧ a ∉ l :=
-  fun p => ⟨ne_of_not_mem_cons p, not_mem_of_not_mem_cons p⟩
-
 /-! ### drop -/
 
 @[simp]
 theorem drop_one : ∀ l : List α, drop 1 l = tail l
   | [] | _ :: _ => rfl
 
-theorem drop_add : ∀ (m n) (l : List α), drop (m + n) l = drop m (drop n l)
-  | _, 0, _ => rfl
-  | _, _ + 1, [] => drop_nil.symm
-  | m, n + 1, _ :: _ => drop_add m n _
-
-@[simp]
-theorem drop_left : ∀ l₁ l₂ : List α, drop (length l₁) (l₁ ++ l₂) = l₂
-  | [], _ => rfl
-  | _ :: l₁, l₂ => drop_left l₁ l₂
-
-theorem drop_left' {l₁ l₂ : List α} {n} (h : length l₁ = n) : drop n (l₁ ++ l₂) = l₂ := by
-  rw [← h]; apply drop_left
-
-/-! ### isEmpty -/
-
-@[simp] theorem isEmpty_nil : ([] : List α).isEmpty = true := rfl
-@[simp] theorem isEmpty_cons : (x :: xs : List α).isEmpty = false := rfl
-
-/-! ### append -/
-
-theorem append_eq_append : List.append l₁ l₂ = l₁ ++ l₂ := rfl
-
-theorem append_ne_nil_of_ne_nil_left (s t : List α) : s ≠ [] → s ++ t ≠ [] := by simp_all
-
-theorem append_ne_nil_of_ne_nil_right (s t : List α) : t ≠ [] → s ++ t ≠ [] := by simp_all
-
-@[simp] theorem nil_eq_append : [] = a ++ b ↔ a = [] ∧ b = [] := by
-  rw [eq_comm, append_eq_nil]
-
-theorem append_ne_nil_of_left_ne_nil (a b : List α) (h0 : a ≠ []) : a ++ b ≠ [] := by simp [*]
-
-theorem append_eq_cons :
-    a ++ b = x :: c ↔ (a = [] ∧ b = x :: c) ∨ (∃ a', a = x :: a' ∧ c = a' ++ b) := by
-  cases a with simp | cons a as => ?_
-  exact ⟨fun h => ⟨as, by simp [h]⟩, fun ⟨a', ⟨aeq, aseq⟩, h⟩ => ⟨aeq, by rw [aseq, h]⟩⟩
-
-theorem cons_eq_append :
-    x :: c = a ++ b ↔ (a = [] ∧ b = x :: c) ∨ (∃ a', a = x :: a' ∧ c = a' ++ b) := by
-  rw [eq_comm, append_eq_cons]
-
-theorem append_eq_append_iff {a b c d : List α} :
-    a ++ b = c ++ d ↔ (∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b := by
-  induction a generalizing c with
-  | nil => simp_all
-  | cons a as ih => cases c <;> simp [eq_comm, and_assoc, ih, and_or_left]
-
-@[simp] theorem mem_append {a : α} {s t : List α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
-  induction s <;> simp_all [or_assoc]
-
-theorem not_mem_append {a : α} {s t : List α} (h₁ : a ∉ s) (h₂ : a ∉ t) : a ∉ s ++ t :=
-  mt mem_append.1 $ not_or.mpr ⟨h₁, h₂⟩
-
-theorem mem_append_eq (a : α) (s t : List α) : (a ∈ s ++ t) = (a ∈ s ∨ a ∈ t) :=
-  propext mem_append
-
-theorem mem_append_left {a : α} {l₁ : List α} (l₂ : List α) (h : a ∈ l₁) : a ∈ l₁ ++ l₂ :=
-  mem_append.2 (Or.inl h)
-
-theorem mem_append_right {a : α} (l₁ : List α) {l₂ : List α} (h : a ∈ l₂) : a ∈ l₁ ++ l₂ :=
-  mem_append.2 (Or.inr h)
-
-theorem mem_iff_append {a : α} {l : List α} : a ∈ l ↔ ∃ s t : List α, l = s ++ a :: t :=
-  ⟨append_of_mem, fun ⟨s, t, e⟩ => e ▸ by simp⟩
-
-/-! ### concat -/
-
-theorem concat_nil (a : α) : concat [] a = [a] :=
-  rfl
-
-theorem concat_cons (a b : α) (l : List α) : concat (a :: l) b = a :: concat l b :=
-  rfl
-
-theorem init_eq_of_concat_eq {a : α} {l₁ l₂ : List α} : concat l₁ a = concat l₂ a → l₁ = l₂ := by
-  simp
-
-theorem last_eq_of_concat_eq {a b : α} {l : List α} : concat l a = concat l b → a = b := by
-  simp
-
-theorem concat_ne_nil (a : α) (l : List α) : concat l a ≠ [] := by simp
-
-theorem concat_append (a : α) (l₁ l₂ : List α) : concat l₁ a ++ l₂ = l₁ ++ a :: l₂ := by simp
-
-theorem append_concat (a : α) (l₁ l₂ : List α) : l₁ ++ concat l₂ a = concat (l₁ ++ l₂) a := by simp
-
-/-! ### map -/
-
-theorem map_singleton (f : α → β) (a : α) : map f [a] = [f a] := rfl
-
-theorem exists_of_mem_map (h : b ∈ map f l) : ∃ a, a ∈ l ∧ f a = b := mem_map.1 h
-
-theorem forall_mem_map_iff {f : α → β} {l : List α} {P : β → Prop} :
-    (∀ i ∈ l.map f, P i) ↔ ∀ j ∈ l, P (f j) := by
-  simp
-
-@[simp] theorem map_eq_nil {f : α → β} {l : List α} : map f l = [] ↔ l = [] := by
-  constructor <;> exact fun _ => match l with | [] => rfl
-
 /-! ### zipWith -/
 
-@[simp] theorem length_zipWith (f : α → β → γ) (l₁ l₂) :
-    length (zipWith f l₁ l₂) = min (length l₁) (length l₂) := by
-  induction l₁ generalizing l₂ <;> cases l₂ <;>
-    simp_all [succ_min_succ, Nat.zero_min, Nat.min_zero]
-
-@[simp]
-theorem zipWith_map {μ} (f : γ → δ → μ) (g : α → γ) (h : β → δ) (l₁ : List α) (l₂ : List β) :
-    zipWith f (l₁.map g) (l₂.map h) = zipWith (fun a b => f (g a) (h b)) l₁ l₂ := by
-  induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
-
-theorem zipWith_map_left (l₁ : List α) (l₂ : List β) (f : α → α') (g : α' → β → γ) :
-    zipWith g (l₁.map f) l₂ = zipWith (fun a b => g (f a) b) l₁ l₂ := by
-  induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
-
-theorem zipWith_map_right (l₁ : List α) (l₂ : List β) (f : β → β') (g : α → β' → γ) :
-    zipWith g l₁ (l₂.map f) = zipWith (fun a b => g a (f b)) l₁ l₂ := by
-  induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
-
-theorem zipWith_foldr_eq_zip_foldr {f : α → β → γ} (i : δ):
-    (zipWith f l₁ l₂).foldr g i = (zip l₁ l₂).foldr (fun p r => g (f p.1 p.2) r) i := by
-  induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
-
-theorem zipWith_foldl_eq_zip_foldl {f : α → β → γ} (i : δ):
-    (zipWith f l₁ l₂).foldl g i = (zip l₁ l₂).foldl (fun r p => g r (f p.1 p.2)) i := by
-  induction l₁ generalizing i l₂ <;> cases l₂ <;> simp_all
-
-@[simp]
-theorem zipWith_eq_nil_iff {f : α → β → γ} {l l'} : zipWith f l l' = [] ↔ l = [] ∨ l' = [] := by
-  cases l <;> cases l' <;> simp
-
-theorem map_zipWith {δ : Type _} (f : α → β) (g : γ → δ → α) (l : List γ) (l' : List δ) :
-    map f (zipWith g l l') = zipWith (fun x y => f (g x y)) l l' := by
-  induction l generalizing l' with
-  | nil => simp
-  | cons hd tl hl =>
-    · cases l'
-      · simp
-      · simp [hl]
-
-theorem zipWith_distrib_take : (zipWith f l l').take n = zipWith f (l.take n) (l'.take n) := by
-  induction l generalizing l' n with
-  | nil => simp
-  | cons hd tl hl =>
-    cases l'
-    · simp
-    · cases n
-      · simp
-      · simp [hl]
-
-theorem zipWith_distrib_drop : (zipWith f l l').drop n = zipWith f (l.drop n) (l'.drop n) := by
-  induction l generalizing l' n with
-  | nil => simp
-  | cons hd tl hl =>
-    · cases l'
-      · simp
-      · cases n
-        · simp
-        · simp [hl]
-
 theorem zipWith_distrib_tail : (zipWith f l l').tail = zipWith f l.tail l'.tail := by
   rw [← drop_one]; simp [zipWith_distrib_drop]
 
-theorem zipWith_append (f : α → β → γ) (l la : List α) (l' lb : List β)
-    (h : l.length = l'.length) :
-    zipWith f (l ++ la) (l' ++ lb) = zipWith f l l' ++ zipWith f la lb := by
-  induction l generalizing l' with
-  | nil =>
-    have : l' = [] := eq_nil_of_length_eq_zero (by simpa using h.symm)
-    simp [this]
-  | cons hl tl ih =>
-    cases l' with
-    | nil => simp at h
-    | cons head tail =>
-      simp only [length_cons, Nat.succ.injEq] at h
-      simp [ih _ h]
-
-/-! ### zip -/
-
-@[simp] theorem length_zip (l₁ : List α) (l₂ : List β) :
-    length (zip l₁ l₂) = min (length l₁) (length l₂) := by
-  simp [zip]
-
-theorem zip_map (f : α → γ) (g : β → δ) :
-    ∀ (l₁ : List α) (l₂ : List β), zip (l₁.map f) (l₂.map g) = (zip l₁ l₂).map (Prod.map f g)
-  | [], l₂ => rfl
-  | l₁, [] => by simp only [map, zip_nil_right]
-  | a :: l₁, b :: l₂ => by
-    simp only [map, zip_cons_cons, zip_map, Prod.map]; constructor
-
-theorem zip_map_left (f : α → γ) (l₁ : List α) (l₂ : List β) :
-    zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id) := by rw [← zip_map, map_id]
-
-theorem zip_map_right (f : β → γ) (l₁ : List α) (l₂ : List β) :
-    zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f) := by rw [← zip_map, map_id]
-
-theorem zip_append :
-    ∀ {l₁ r₁ : List α} {l₂ r₂ : List β} (_h : length l₁ = length l₂),
-      zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂
-  | [], r₁, l₂, r₂, h => by simp only [eq_nil_of_length_eq_zero h.symm]; rfl
-  | l₁, r₁, [], r₂, h => by simp only [eq_nil_of_length_eq_zero h]; rfl
-  | a :: l₁, r₁, b :: l₂, r₂, h => by
-    simp only [cons_append, zip_cons_cons, zip_append (Nat.succ.inj h)]
-
-theorem zip_map' (f : α → β) (g : α → γ) :
-    ∀ l : List α, zip (l.map f) (l.map g) = l.map fun a => (f a, g a)
-  | [] => rfl
-  | a :: l => by simp only [map, zip_cons_cons, zip_map']
-
-theorem of_mem_zip {a b} : ∀ {l₁ : List α} {l₂ : List β}, (a, b) ∈ zip l₁ l₂ → a ∈ l₁ ∧ b ∈ l₂
-  | _ :: l₁, _ :: l₂, h => by
-    cases h
-    case head => simp
-    case tail h =>
-    · have := of_mem_zip h
-      exact ⟨Mem.tail _ this.1, Mem.tail _ this.2⟩
-
-theorem map_fst_zip :
-    ∀ (l₁ : List α) (l₂ : List β), l₁.length ≤ l₂.length → map Prod.fst (zip l₁ l₂) = l₁
-  | [], bs, _ => rfl
-  | _ :: as, _ :: bs, h => by
-    simp [Nat.succ_le_succ_iff] at h
-    show _ :: map Prod.fst (zip as bs) = _ :: as
-    rw [map_fst_zip as bs h]
-  | a :: as, [], h => by simp at h
-
-theorem map_snd_zip :
-    ∀ (l₁ : List α) (l₂ : List β), l₂.length ≤ l₁.length → map Prod.snd (zip l₁ l₂) = l₂
-  | _, [], _ => by
-    rw [zip_nil_right]
-    rfl
-  | [], b :: bs, h => by simp at h
-  | a :: as, b :: bs, h => by
-    simp [Nat.succ_le_succ_iff] at h
-    show _ :: map Prod.snd (zip as bs) = _ :: bs
-    rw [map_snd_zip as bs h]
-
-/-! ### join -/
-
-theorem mem_join : ∀ {L : List (List α)}, a ∈ L.join ↔ ∃ l, l ∈ L ∧ a ∈ l
-  | [] => by simp
-  | b :: l => by simp [mem_join, or_and_right, exists_or]
-
-theorem exists_of_mem_join : a ∈ join L → ∃ l, l ∈ L ∧ a ∈ l := mem_join.1
-
-theorem mem_join_of_mem (lL : l ∈ L) (al : a ∈ l) : a ∈ join L := mem_join.2 ⟨l, lL, al⟩
-
-/-! ### bind -/
-
-theorem mem_bind {f : α → List β} {b} {l : List α} : b ∈ l.bind f ↔ ∃ a, a ∈ l ∧ b ∈ f a := by
-  simp [List.bind, mem_join]
-  exact ⟨fun ⟨_, ⟨a, h₁, rfl⟩, h₂⟩ => ⟨a, h₁, h₂⟩, fun ⟨a, h₁, h₂⟩ => ⟨_, ⟨a, h₁, rfl⟩, h₂⟩⟩
-
-theorem exists_of_mem_bind {b : β} {l : List α} {f : α → List β} :
-    b ∈ List.bind l f → ∃ a, a ∈ l ∧ b ∈ f a := mem_bind.1
-
-theorem mem_bind_of_mem {b : β} {l : List α} {f : α → List β} {a} (al : a ∈ l) (h : b ∈ f a) :
-    b ∈ List.bind l f := mem_bind.2 ⟨a, al, h⟩
-
-theorem bind_map (f : β → γ) (g : α → List β) :
-    ∀ l : List α, map f (l.bind g) = l.bind fun a => (g a).map f
-  | [] => rfl
-  | a::l => by simp only [cons_bind, map_append, bind_map _ _ l]
-
-/-! ### set-theoretic notation of Lists -/
-
-@[simp] theorem empty_eq : (∅ : List α) = [] := rfl
-
-/-! ### bounded quantifiers over Lists -/
-
-theorem exists_mem_nil (p : α → Prop) : ¬∃ x ∈ @nil α, p x := nofun
-
-theorem forall_mem_nil (p : α → Prop) : ∀ x ∈ @nil α, p x := nofun
-
-theorem exists_mem_cons {p : α → Prop} {a : α} {l : List α} :
-    (∃ x ∈ a :: l, p x) ↔ p a ∨ ∃ x ∈ l, p x := by simp
-
-theorem forall_mem_singleton {p : α → Prop} {a : α} : (∀ x ∈ [a], p x) ↔ p a := by
-  simp only [mem_singleton, forall_eq]
-
-theorem forall_mem_append {p : α → Prop} {l₁ l₂ : List α} :
-    (∀ x ∈ l₁ ++ l₂, p x) ↔ (∀ x ∈ l₁, p x) ∧ (∀ x ∈ l₂, p x) := by
-  simp only [mem_append, or_imp, forall_and]
-
 /-! ### List subset -/
 
 theorem subset_def {l₁ l₂ : List α} : l₁ ⊆ l₂ ↔ ∀ {a : α}, a ∈ l₁ → a ∈ l₂ := .rfl
@@ -452,48 +78,6 @@ theorem subset_nil {l : List α} : l ⊆ [] ↔ l = [] :=
 theorem map_subset {l₁ l₂ : List α} (f : α → β) (H : l₁ ⊆ l₂) : map f l₁ ⊆ map f l₂ :=
   fun x => by simp only [mem_map]; exact .imp fun a => .imp_left (@H _)
 
-/-! ### replicate -/
-
-theorem replicate_succ (a : α) (n) : replicate (n+1) a = a :: replicate n a := rfl
-
-theorem mem_replicate {a b : α} : ∀ {n}, b ∈ replicate n a ↔ n ≠ 0 ∧ b = a
-  | 0 => by simp
-  | n+1 => by simp [mem_replicate, Nat.succ_ne_zero]
-
-theorem eq_of_mem_replicate {a b : α} {n} (h : b ∈ replicate n a) : b = a := (mem_replicate.1 h).2
-
-theorem eq_replicate_of_mem {a : α} :
-    ∀ {l : List α}, (∀ b ∈ l, b = a) → l = replicate l.length a
-  | [], _ => rfl
-  | b :: l, H => by
-    let ⟨rfl, H₂⟩ := forall_mem_cons.1 H
-    rw [length_cons, replicate, ← eq_replicate_of_mem H₂]
-
-theorem eq_replicate {a : α} {n} {l : List α} :
-    l = replicate n a ↔ length l = n ∧ ∀ b ∈ l, b = a :=
-  ⟨fun h => h ▸ ⟨length_replicate .., fun _ => eq_of_mem_replicate⟩,
-   fun ⟨e, al⟩ => e ▸ eq_replicate_of_mem al⟩
-
-/-! ### getLast -/
-
-theorem getLast_cons' {a : α} {l : List α} : ∀ (h₁ : a :: l ≠ nil) (h₂ : l ≠ nil),
-  getLast (a :: l) h₁ = getLast l h₂ := by
-  induction l <;> intros; {contradiction}; rfl
-
-@[simp] theorem getLast_append {a : α} : ∀ (l : List α) h, getLast (l ++ [a]) h = a
-  | [], _ => rfl
-  | a::t, h => by
-    simp [getLast_cons' _ fun H => cons_ne_nil _ _ (append_eq_nil.1 H).2, getLast_append t]
-
-theorem getLast_concat : (h : concat l a ≠ []) → getLast (concat l a) h = a :=
-  concat_eq_append .. ▸ getLast_append _
-
-theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ L b, l = L ++ [b]
-  | [] => .inl rfl
-  | a::l => match l, eq_nil_or_concat l with
-    | _, .inl rfl => .inr ⟨[], a, rfl⟩
-    | _, .inr ⟨L, b, rfl⟩ => .inr ⟨a::L, b, rfl⟩
-
 /-! ### sublists -/
 
 @[simp] theorem nil_sublist : ∀ l : List α, [] <+ l
@@ -646,19 +230,8 @@ theorem isSublist_iff_sublist [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
 instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <+ l₂) :=
   decidable_of_iff (l₁.isSublist l₂) isSublist_iff_sublist
 
-/-! ### head -/
-
-theorem head!_of_head? [Inhabited α] : ∀ {l : List α}, head? l = some a → head! l = a
-  | _a::_l, rfl => rfl
-
-theorem head?_eq_head : ∀ l h, @head? α l = some (head l h)
-  | _::_, _ => rfl
-
 /-! ### tail -/
 
-@[simp] theorem tailD_eq_tail? (l l' : List α) : tailD l l' = (tail? l).getD l' := by
-  cases l <;> rfl
-
 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]
@@ -668,110 +241,10 @@ theorem tail_eq_tail? (l) : @tail α l = (tail? l).getD [] := by simp [tail_eq_t
 @[simp] theorem next?_nil : @next? α [] = none := rfl
 @[simp] theorem next?_cons (a l) : @next? α (a :: l) = some (a, l) := rfl
 
-/-! ### getLast -/
-
-@[simp] theorem getLastD_nil (a) : @getLastD α [] a = a := rfl
-@[simp] theorem getLastD_cons (a b l) : @getLastD α (b::l) a = getLastD l b := by cases l <;> rfl
-
-theorem getLast_eq_getLastD (a l h) : @getLast α (a::l) h = getLastD l a := by
-  cases l <;> rfl
-
-theorem getLastD_eq_getLast? (a l) : @getLastD α l a = (getLast? l).getD a := by
-  cases l <;> rfl
-
-@[simp] theorem getLast_singleton (a h) : @getLast α [a] h = a := rfl
-
-theorem getLast!_cons [Inhabited α] : @getLast! α _ (a::l) = getLastD l a := by
-  simp [getLast!, getLast_eq_getLastD]
-
-theorem getLast?_cons : @getLast? α (a::l) = getLastD l a := by
-  simp [getLast?, getLast_eq_getLastD]
-
-@[simp] theorem getLast?_singleton (a : α) : getLast? [a] = a := rfl
-
-theorem getLast_mem : ∀ {l : List α} (h : l ≠ []), getLast l h ∈ l
-  | [], h => absurd rfl h
-  | [_], _ => .head ..
-  | _::a::l, _ => .tail _ <| getLast_mem (cons_ne_nil a l)
-
-theorem getLastD_mem_cons : ∀ (l : List α) (a : α), getLastD l a ∈ a::l
-  | [], _ => .head ..
-  | _::_, _ => .tail _ <| getLast_mem _
-
-@[simp] theorem getLast?_reverse (l : List α) : l.reverse.getLast? = l.head? := by cases l <;> simp
-
-@[simp] theorem head?_reverse (l : List α) : l.reverse.head? = l.getLast? := by
-  rw [← getLast?_reverse, reverse_reverse]
-
-/-! ### dropLast -/
-
-/-! NB: `dropLast` is the specification for `Array.pop`, so theorems about `List.dropLast`
-are often used for theorems about `Array.pop`.  -/
-
-theorem dropLast_cons_of_ne_nil {α : Type u} {x : α}
-    {l : List α} (h : l ≠ []) : (x :: l).dropLast = x :: l.dropLast := by
-  simp [dropLast, h]
-
-@[simp] theorem dropLast_append_of_ne_nil {α : Type u} {l : List α} :
-    ∀ (l' : List α) (_ : l ≠ []), (l' ++ l).dropLast = l' ++ l.dropLast
-  | [], _ => by simp only [nil_append]
-  | a :: l', h => by
-    rw [cons_append, dropLast, dropLast_append_of_ne_nil l' h, cons_append]
-    simp [h]
-
-theorem dropLast_append_cons : dropLast (l₁ ++ b::l₂) = l₁ ++ dropLast (b::l₂) := by
-  simp only [ne_eq, not_false_eq_true, dropLast_append_of_ne_nil]
-
-@[simp 1100] theorem dropLast_concat : dropLast (l₁ ++ [b]) = l₁ := by simp
-
-@[simp] theorem length_dropLast : ∀ (xs : List α), xs.dropLast.length = xs.length - 1
-  | [] => rfl
-  | x::xs => by simp
-
-@[simp] theorem get_dropLast : ∀ (xs : List α) (i : Fin xs.dropLast.length),
-    xs.dropLast.get i = xs.get ⟨i, Nat.lt_of_lt_of_le i.isLt (length_dropLast .. ▸ Nat.pred_le _)⟩
-  | _::_::_, ⟨0, _⟩ => rfl
-  | _::_::_, ⟨i+1, _⟩ => get_dropLast _ ⟨i, _⟩
-
-/-! ### nth element -/
+/-! ### get? -/
 
 theorem get_eq_iff : List.get l n = x ↔ l.get? n.1 = some x := by simp [get?_eq_some]
 
-@[simp] theorem get_cons_cons_one : (a₁ :: a₂ :: as).get (1 : Fin (as.length + 2)) = a₂ := rfl
-
-theorem get!_cons_succ [Inhabited α] (l : List α) (a : α) (n : Nat) :
-    (a::l).get! (n+1) = get! l n := rfl
-
-theorem get!_cons_zero [Inhabited α] (l : List α) (a : α) : (a::l).get! 0 = a := rfl
-
-theorem get!_nil [Inhabited α] (n : Nat) : [].get! n = (default : α) := rfl
-
-theorem get!_len_le [Inhabited α] : ∀ {l : List α} {n}, length l ≤ n → l.get! n = (default : α)
-  | [], _, _ => rfl
-  | _ :: l, _+1, h => get!_len_le (l := l) <| Nat.le_of_succ_le_succ h
-
-theorem get?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, l.get? n = some a :=
-  let ⟨⟨n, _⟩, e⟩ := get_of_mem h; ⟨n, e ▸ get?_eq_get _⟩
-
-theorem get?_mem {l : List α} {n a} (e : l.get? n = some a) : a ∈ l :=
-  let ⟨_, e⟩ := get?_eq_some.1 e; e ▸ get_mem ..
-
--- TODO(Mario): move somewhere else
-theorem Fin.exists_iff (p : Fin n → Prop) : (∃ i, p i) ↔ ∃ i h, p ⟨i, h⟩ :=
-  ⟨fun ⟨i, h⟩ => ⟨i.1, i.2, h⟩, fun ⟨i, hi, h⟩ => ⟨⟨i, hi⟩, h⟩⟩
-
-theorem mem_iff_get? {a} {l : List α} : a ∈ l ↔ ∃ n, l.get? n = some a := by
-  simp [get?_eq_some, Fin.exists_iff, mem_iff_get]
-
-theorem get?_zero (l : List α) : l.get? 0 = l.head? := by cases l <;> rfl
-
-@[simp] theorem getElem_eq_get (l : List α) (i : Nat) (h) : l[i]'h = l.get ⟨i, h⟩ := rfl
-
-@[simp] theorem getElem?_eq_get? (l : List α) (i : Nat) : l[i]? = l.get? i := by
-  simp only [getElem?]; split
-  · exact (get?_eq_get ‹_›).symm
-  · exact (get?_eq_none.2 <| Nat.not_lt.1 ‹_›).symm
-
 theorem get?_inj
     (h₀ : i < xs.length) (h₁ : Nodup xs) (h₂ : xs.get? i = xs.get? j) : i = j := by
   induction xs generalizing i j with
@@ -789,232 +262,8 @@ theorem get?_inj
       rw [mem_iff_get?]
     exact ⟨_, h₂⟩; exact ⟨_ , h₂.symm⟩
 
-/--
-If one has `get l i hi` in a formula and `h : l = l'`, one can not `rw h` in the formula as
-`hi` gives `i < l.length` and not `i < l'.length`. The theorem `get_of_eq` can be used to make
-such a rewrite, with `rw (get_of_eq h)`.
--/
-theorem get_of_eq {l l' : List α} (h : l = l') (i : Fin l.length) :
-    get l i = get l' ⟨i, h ▸ i.2⟩ := by cases h; rfl
-
-@[simp] theorem get_singleton (a : α) : (n : Fin 1) → get [a] n = a
-  | ⟨0, _⟩ => rfl
-
-theorem get_mk_zero : ∀ {l : List α} (h : 0 < l.length), l.get ⟨0, h⟩ = l.head (length_pos.mp h)
-  | _::_, _ => rfl
-
-theorem get_append_right_aux {l₁ l₂ : List α} {n : Nat}
-  (h₁ : l₁.length ≤ n) (h₂ : n < (l₁ ++ l₂).length) : n - l₁.length < l₂.length := by
-  rw [length_append] at h₂
-  exact Nat.sub_lt_left_of_lt_add h₁ h₂
-
-theorem get_append_right' {l₁ l₂ : List α} {n : Nat} (h₁ : l₁.length ≤ n) (h₂) :
-    (l₁ ++ l₂).get ⟨n, h₂⟩ = l₂.get ⟨n - l₁.length, get_append_right_aux h₁ h₂⟩ :=
-Option.some.inj <| by rw [← get?_eq_get, ← get?_eq_get, get?_append_right h₁]
-
-theorem get_of_append_proof {l : List α}
-    (eq : l = l₁ ++ a :: l₂) (h : l₁.length = n) : n < length l := eq ▸ h ▸ by simp_arith
-
-theorem get_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = n) :
-    l.get ⟨n, get_of_append_proof eq h⟩ = a := Option.some.inj <| by
-  rw [← get?_eq_get, eq, get?_append_right (h ▸ Nat.le_refl _), h, Nat.sub_self]; rfl
-
-@[simp] theorem get_replicate (a : α) {n : Nat} (m : Fin _) : (replicate n a).get m = a :=
-  eq_of_mem_replicate (get_mem _ _ _)
-
-@[simp] theorem getLastD_concat (a b l) : @getLastD α (l ++ [b]) a = b := by
-  rw [getLastD_eq_getLast?, getLast?_concat]; rfl
-
-theorem get_cons_length (x : α) (xs : List α) (n : Nat) (h : n = xs.length) :
-    (x :: xs).get ⟨n, by simp [h]⟩ = (x :: xs).getLast (cons_ne_nil x xs) := by
-  rw [getLast_eq_get]; cases h; rfl
-
-theorem get!_of_get? [Inhabited α] : ∀ {l : List α} {n}, get? l n = some a → get! l n = a
-  | _a::_, 0, rfl => rfl
-  | _::l, _+1, e => get!_of_get? (l := l) e
-
-@[simp] theorem get!_eq_getD [Inhabited α] : ∀ (l : List α) n, l.get! n = l.getD n default
-  | [], _      => rfl
-  | _a::_, 0   => rfl
-  | _a::l, n+1 => get!_eq_getD l n
-
-/-! ### take -/
-
-alias take_succ_cons := take_cons_succ
-
-@[simp] theorem length_take : ∀ (i : Nat) (l : List α), length (take i l) = min i (length l)
-  | 0, l => by simp [Nat.zero_min]
-  | succ n, [] => by simp [Nat.min_zero]
-  | succ n, _ :: l => by simp [Nat.succ_min_succ, length_take]
-
-theorem length_take_le (n) (l : List α) : length (take n l) ≤ n := by simp [Nat.min_le_left]
-
-theorem length_take_le' (n) (l : List α) : length (take n l) ≤ l.length :=
-  by simp [Nat.min_le_right]
-
-theorem length_take_of_le (h : n ≤ length l) : length (take n l) = n := by simp [Nat.min_eq_left h]
-
-theorem take_all_of_le {n} {l : List α} (h : length l ≤ n) : take n l = l :=
-  take_length_le h
-
-@[simp]
-theorem take_left : ∀ l₁ l₂ : List α, take (length l₁) (l₁ ++ l₂) = l₁
-  | [], _ => rfl
-  | a :: l₁, l₂ => congrArg (cons a) (take_left l₁ l₂)
-
-theorem take_left' {l₁ l₂ : List α} {n} (h : length l₁ = n) : take n (l₁ ++ l₂) = l₁ := by
-  rw [← h]; apply take_left
-
-theorem take_take : ∀ (n m) (l : List α), take n (take m l) = take (min n m) l
-  | n, 0, l => by rw [Nat.min_zero, take_zero, take_nil]
-  | 0, m, l => by rw [Nat.zero_min, take_zero, take_zero]
-  | succ n, succ m, nil => by simp only [take_nil]
-  | succ n, succ m, a :: l => by
-    simp only [take, succ_min_succ, take_take n m l]
-
-theorem take_replicate (a : α) : ∀ n m : Nat, take n (replicate m a) = replicate (min n m) a
-  | n, 0 => by simp [Nat.min_zero]
-  | 0, m => by simp [Nat.zero_min]
-  | succ n, succ m => by simp [succ_min_succ, take_replicate]
-
-theorem map_take (f : α → β) :
-    ∀ (L : List α) (i : Nat), (L.take i).map f = (L.map f).take i
-  | [], i => by simp
-  | _, 0 => by simp
-  | h :: t, n + 1 => by dsimp; rw [map_take f t n]
-
-/-- Taking the first `n` elements in `l₁ ++ l₂` is the same as appending the first `n` elements
-of `l₁` to the first `n - l₁.length` elements of `l₂`. -/
-theorem take_append_eq_append_take {l₁ l₂ : List α} {n : Nat} :
-    take n (l₁ ++ l₂) = take n l₁ ++ take (n - l₁.length) l₂ := by
-  induction l₁ generalizing n; {simp}
-  cases n <;> simp [*]
-
-theorem take_append_of_le_length {l₁ l₂ : List α} {n : Nat} (h : n ≤ l₁.length) :
-    (l₁ ++ l₂).take n = l₁.take n := by
-  simp [take_append_eq_append_take, Nat.sub_eq_zero_of_le h]
-
-/-- Taking the first `l₁.length + i` elements in `l₁ ++ l₂` is the same as appending the first
-`i` elements of `l₂` to `l₁`. -/
-theorem take_append {l₁ l₂ : List α} (i : Nat) :
-    take (l₁.length + i) (l₁ ++ l₂) = l₁ ++ take i l₂ := by
-  rw [take_append_eq_append_take, take_all_of_le (Nat.le_add_right _ _), Nat.add_sub_cancel_left]
-
-/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
-length `> i`. Version designed to rewrite from the big list to the small list. -/
-theorem get_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) :
-    get L ⟨i, hi⟩ = get (L.take j) ⟨i, length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩⟩ :=
-  get_of_eq (take_append_drop j L).symm _ ▸ get_append ..
-
-/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
-length `> i`. Version designed to rewrite from the small list to the big list. -/
-theorem get_take' (L : List α) {j i} :
-    get (L.take j) i =
-    get L ⟨i.1, Nat.lt_of_lt_of_le i.2 (length_take_le' _ _)⟩ := by
-  let ⟨i, hi⟩ := i; rw [length_take, Nat.lt_min] at hi; rw [get_take L _ hi.1]
-
-theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l.get? m := by
-  induction n generalizing l m with
-  | zero =>
-    exact absurd h (Nat.not_lt_of_le m.zero_le)
-  | succ _ hn =>
-    cases l with
-    | nil => simp only [take_nil]
-    | cons hd tl =>
-      cases m
-      · simp only [get?, take]
-      · simpa only using hn (Nat.lt_of_succ_lt_succ h)
-
-theorem get?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) :
-    (l.take n).get? m = none :=
-  get?_eq_none.mpr <| Nat.le_trans (length_take_le _ _) h
-
-theorem get?_take_eq_if {l : List α} {n m : Nat} :
-    (l.take n).get? m = if m < n then l.get? m else none := by
-  split
-  · next h => exact get?_take h
-  · next h => exact get?_take_eq_none (Nat.le_of_not_lt h)
-
-@[simp]
-theorem nth_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1)).get? n = l.get? n :=
-  get?_take (Nat.lt_succ_self n)
-
-theorem take_succ {l : List α} {n : Nat} : l.take (n + 1) = l.take n ++ (l.get? n).toList := by
-  induction l generalizing n with
-  | nil =>
-    simp only [Option.toList, get?, take_nil, append_nil]
-  | cons hd tl hl =>
-    cases n
-    · simp only [Option.toList, get?, eq_self_iff_true, take, nil_append]
-    · simp only [hl, cons_append, get?, eq_self_iff_true, take]
-
-@[simp]
-theorem take_eq_nil_iff {l : List α} {k : Nat} : l.take k = [] ↔ l = [] ∨ k = 0 := by
-  cases l <;> cases k <;> simp [Nat.succ_ne_zero]
-
-@[simp]
-theorem take_eq_take :
-    ∀ {l : List α} {m n : Nat}, l.take m = l.take n ↔ min m l.length = min n l.length
-  | [], m, n => by simp [Nat.min_zero]
-  | _ :: xs, 0, 0 => by simp
-  | x :: xs, m + 1, 0 => by simp [Nat.zero_min, succ_min_succ]
-  | x :: xs, 0, n + 1 => by simp [Nat.zero_min, succ_min_succ]
-  | x :: xs, m + 1, n + 1 => by simp [succ_min_succ, take_eq_take]
-
-theorem take_add (l : List α) (m n : Nat) : l.take (m + n) = l.take m ++ (l.drop m).take n := by
-  suffices take (m + n) (take m l ++ drop m l) = take m l ++ take n (drop m l) by
-    rw [take_append_drop] at this
-    assumption
-  rw [take_append_eq_append_take, take_all_of_le, append_right_inj]
-  · simp only [take_eq_take, length_take, length_drop]
-    omega
-  apply Nat.le_trans (m := m)
-  · apply length_take_le
-  · apply Nat.le_add_right
-
-theorem take_eq_nil_of_eq_nil : ∀ {as : List α} {i}, as = [] → as.take i = []
-  | _, _, rfl => take_nil
-
-theorem ne_nil_of_take_ne_nil {as : List α} {i : Nat} (h: as.take i ≠ []) : as ≠ [] :=
-  mt take_eq_nil_of_eq_nil h
-
-theorem dropLast_eq_take (l : List α) : l.dropLast = l.take l.length.pred := by
-  cases l with
-  | nil => simp [dropLast]
-  | cons x l =>
-    induction l generalizing x with
-    | nil => simp [dropLast]
-    | cons hd tl hl => simp [dropLast, hl]
-
-theorem dropLast_take {n : Nat} {l : List α} (h : n < l.length) :
-    (l.take n).dropLast = l.take n.pred := by
-  simp only [dropLast_eq_take, length_take, Nat.le_of_lt h, take_take, pred_le, Nat.min_eq_left]
-
-theorem map_eq_append_split {f : α → β} {l : List α} {s₁ s₂ : List β}
-    (h : map f l = s₁ ++ s₂) : ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = s₁ ∧ map f l₂ = s₂ := by
-  have := h
-  rw [← take_append_drop (length s₁) l] at this ⊢
-  rw [map_append] at this
-  refine ⟨_, _, rfl, append_inj this ?_⟩
-  rw [length_map, length_take, Nat.min_eq_left]
-  rw [← length_map l f, h, length_append]
-  apply Nat.le_add_right
-
 /-! ### drop -/
 
-@[simp]
-theorem drop_eq_nil_iff_le {l : List α} {k : Nat} : l.drop k = [] ↔ l.length ≤ k := by
-  refine' ⟨fun h => _, drop_eq_nil_of_le⟩
-  induction k generalizing l with
-  | zero =>
-    simp only [drop] at h
-    simp [h]
-  | succ k hk =>
-    cases l
-    · simp
-    · simp only [drop] at h
-      simpa [Nat.succ_le_succ_iff] using hk h
-
 theorem tail_drop (l : List α) (n : Nat) : (l.drop n).tail = l.drop (n + 1) := by
   induction l generalizing n with
   | nil => simp
@@ -1023,141 +272,6 @@ theorem tail_drop (l : List α) (n : Nat) : (l.drop n).tail = l.drop (n + 1) :=
     · simp
     · simp [hl]
 
-theorem drop_length_cons {l : List α} (h : l ≠ []) (a : α) :
-    (a :: l).drop l.length = [l.getLast h] := by
-  induction l generalizing a with
-  | nil =>
-    cases h rfl
-  | cons y l ih =>
-    simp only [drop, length]
-    by_cases h₁ : l = []
-    · simp [h₁]
-    rw [getLast_cons' _ h₁]
-    exact ih h₁ y
-
-/-- Dropping the elements up to `n` in `l₁ ++ l₂` is the same as dropping the elements up to `n`
-in `l₁`, dropping the elements up to `n - l₁.length` in `l₂`, and appending them. -/
-theorem drop_append_eq_append_drop {l₁ l₂ : List α} {n : Nat} :
-    drop n (l₁ ++ l₂) = drop n l₁ ++ drop (n - l₁.length) l₂ := by
-  induction l₁ generalizing n; · simp
-  cases n <;> simp [*]
-
-theorem drop_append_of_le_length {l₁ l₂ : List α} {n : Nat} (h : n ≤ l₁.length) :
-    (l₁ ++ l₂).drop n = l₁.drop n ++ l₂ := by
-  simp [drop_append_eq_append_drop, Nat.sub_eq_zero_of_le h]
-
-
-/-- Dropping the elements up to `l₁.length + i` in `l₁ + l₂` is the same as dropping the elements
-up to `i` in `l₂`. -/
-@[simp]
-theorem drop_append {l₁ l₂ : List α} (i : Nat) : drop (l₁.length + i) (l₁ ++ l₂) = drop i l₂ := by
-  rw [drop_append_eq_append_drop, drop_eq_nil_of_le] <;>
-    simp [Nat.add_sub_cancel_left, Nat.le_add_right]
-
-theorem drop_sizeOf_le [SizeOf α] (l : List α) (n : Nat) : sizeOf (l.drop n) ≤ sizeOf l := by
-  induction l generalizing n with
-  | nil => rw [drop_nil]; apply Nat.le_refl
-  | cons _ _ lih =>
-    induction n with
-    | zero => apply Nat.le_refl
-    | succ n =>
-      exact Trans.trans (lih _) (Nat.le_add_left _ _)
-
-theorem lt_length_drop (L : List α) {i j : Nat} (h : i + j < L.length) : j < (L.drop i).length := by
-  have A : i < L.length := Nat.lt_of_le_of_lt (Nat.le.intro rfl) h
-  rw [(take_append_drop i L).symm] at h
-  simpa only [Nat.le_of_lt A, Nat.min_eq_left, Nat.add_lt_add_iff_left, length_take,
-    length_append] using h
-
-/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
-dropping the first `i` elements. Version designed to rewrite from the big list to the small list. -/
-theorem get_drop (L : List α) {i j : Nat} (h : i + j < L.length) :
-    get L ⟨i + j, h⟩ = get (L.drop i) ⟨j, lt_length_drop L h⟩ := by
-  have : i ≤ L.length := Nat.le_trans (Nat.le_add_right _ _) (Nat.le_of_lt h)
-  rw [get_of_eq (take_append_drop i L).symm ⟨i + j, h⟩, get_append_right'] <;>
-    simp [Nat.min_eq_left this, Nat.add_sub_cancel_left, Nat.le_add_right]
-
-/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
-dropping the first `i` elements. Version designed to rewrite from the small list to the big list. -/
-theorem get_drop' (L : List α) {i j} :
-    get (L.drop i) j = get L ⟨i + j, by
-      rw [Nat.add_comm]
-      exact Nat.add_lt_of_lt_sub (length_drop i L ▸ j.2)⟩ := by
-  rw [get_drop]
-
-@[simp]
-theorem get?_drop (L : List α) (i j : Nat) : get? (L.drop i) j = get? L (i + j) := by
-  ext
-  simp only [get?_eq_some, get_drop', Option.mem_def]
-  constructor <;> intro ⟨h, ha⟩
-  · exact ⟨_, ha⟩
-  · refine ⟨?_, ha⟩
-    rw [length_drop]
-    rw [Nat.add_comm] at h
-    apply Nat.lt_sub_of_add_lt h
-
-@[simp] theorem drop_drop (n : Nat) : ∀ (m) (l : List α), drop n (drop m l) = drop (n + m) l
-  | m, [] => by simp
-  | 0, l => by simp
-  | m + 1, a :: l =>
-    calc
-      drop n (drop (m + 1) (a :: l)) = drop n (drop m l) := rfl
-      _ = drop (n + m) l := drop_drop n m l
-      _ = drop (n + (m + 1)) (a :: l) := rfl
-
-theorem take_drop : ∀ (m n : Nat) (l : List α), take n (drop m l) = drop m (take (m + n) l)
-  | 0, _, _ => by simp
-  | _, _, [] => by simp
-  | _+1, _, _ :: _ => by simpa [Nat.succ_add, take_succ_cons, drop_succ_cons] using take_drop ..
-
-theorem drop_take : ∀ (m n : Nat) (l : List α), drop n (take m l) = take (m - n) (drop n l)
-  | 0, _, _ => by simp
-  | _, 0, _ => by simp
-  | _, _, [] => by simp
-  | _+1, _+1, _ :: _ => by simpa [take_succ_cons, drop_succ_cons] using drop_take ..
-
-theorem map_drop (f : α → β) :
-    ∀ (L : List α) (i : Nat), (L.drop i).map f = (L.map f).drop i
-  | [], i => by simp
-  | L, 0 => by simp
-  | h :: t, n + 1 => by
-    dsimp
-    rw [map_drop f t]
-
-theorem reverse_take {α} {xs : List α} (n : Nat) (h : n ≤ xs.length) :
-    xs.reverse.take n = (xs.drop (xs.length - n)).reverse := by
-  induction xs generalizing n <;>
-    simp only [reverse_cons, drop, reverse_nil, Nat.zero_sub, length, take_nil]
-  next xs_hd xs_tl xs_ih =>
-  cases Nat.lt_or_eq_of_le h with
-  | inl h' =>
-    have h' := Nat.le_of_succ_le_succ h'
-    rw [take_append_of_le_length, xs_ih _ h']
-    rw [show xs_tl.length + 1 - n = succ (xs_tl.length - n) from _, drop]
-    · rwa [succ_eq_add_one, Nat.sub_add_comm]
-    · rwa [length_reverse]
-  | inr h' =>
-    subst h'
-    rw [length, Nat.sub_self, drop]
-    suffices xs_tl.length + 1 = (xs_tl.reverse ++ [xs_hd]).length by
-      rw [this, take_length, reverse_cons]
-    rw [length_append, length_reverse]
-    rfl
-
-@[simp]
-theorem get_cons_drop : ∀ (l : List α) i, get l i :: drop (i + 1) l = drop i l
-  | _::_, ⟨0, _⟩ => rfl
-  | _::_, ⟨i+1, _⟩ => get_cons_drop _ ⟨i, _⟩
-
-theorem drop_eq_get_cons {n} {l : List α} (h) : drop n l = get l ⟨n, h⟩ :: drop (n + 1) l :=
-  (get_cons_drop _ ⟨n, h⟩).symm
-
-theorem drop_eq_nil_of_eq_nil : ∀ {as : List α} {i}, as = [] → as.drop i = []
-  | _, _, rfl => drop_nil
-
-theorem ne_nil_of_drop_ne_nil {as : List α} {i : Nat} (h: as.drop i ≠ []) : as ≠ [] :=
-  mt drop_eq_nil_of_eq_nil h
-
 /-! ### modifyNth -/
 
 theorem modifyNthTail_id : ∀ n (l : List α), l.modifyNthTail id n = l
@@ -1282,32 +396,6 @@ 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 [get?_set]; split <;> subst_vars <;> simp [*, get?_eq_get h]
 
-@[simp] theorem set_eq_nil (l : List α) (n : Nat) (a : α) : l.set n a = [] ↔ l = [] := by
-  cases l <;> cases n <;> simp only [set]
-
-theorem set_comm (a b : α) : ∀ {n m : Nat} (l : List α), n ≠ m →
-    (l.set n a).set m b = (l.set m b).set n a
-  | _, _, [], _ => by simp
-  | n+1, 0, _ :: _, _ => by simp [set]
-  | 0, m+1, _ :: _, _ => by simp [set]
-  | n+1, m+1, x :: t, h =>
-    congrArg _ <| set_comm a b t fun h' => h <| Nat.succ_inj'.mpr h'
-
-@[simp]
-theorem set_set (a b : α) : ∀ (l : List α) (n : Nat), (l.set n a).set n b = l.set n b
-  | [], _ => by simp
-  | _ :: _, 0 => by simp [set]
-  | _ :: _, _+1 => by simp [set, set_set]
-
-theorem get_set (a : α) {m n} (l : List α) (h) :
-    (set l m a).get ⟨n, h⟩ = if m = n then a else l.get ⟨n, length_set .. ▸ h⟩ := by
-  if h : m = n then subst m; simp else simp [h]
-
-theorem mem_or_eq_of_mem_set : ∀ {l : List α} {n : Nat} {a b : α}, a ∈ l.set n b → a ∈ l ∨ a = b
-  | _ :: _, 0, _, _, h => ((mem_cons ..).1 h).symm.imp_left (.tail _)
-  | _ :: _, _+1, _, _, .head .. => .inl (.head ..)
-  | _ :: _, _+1, _, _, .tail _ h => (mem_or_eq_of_mem_set h).imp_left (.tail _)
-
 theorem drop_set_of_lt (a : α) {n m : Nat} (l : List α) (h : n < m) :
     (l.set n a).drop m = l.drop m :=
   List.ext fun i => by rw [get?_drop, get?_drop, get?_set_ne _ _ (by omega)]
@@ -1336,91 +424,6 @@ theorem length_eraseIdx : ∀ {l i}, i < length l → length (@eraseIdx α l i)
 
 @[simp] theorem length_tail (l : List α) : length (tail l) = length l - 1 := by cases l <;> rfl
 
-/-! ### all / any -/
-
-@[simp] theorem contains_nil [BEq α] : ([] : List α).contains a = false := rfl
-
-@[simp] theorem contains_cons [BEq α] :
-    (a :: as : List α).contains x = (x == a || as.contains x) := by
-  simp only [contains, elem]
-  split <;> simp_all
-
-theorem contains_eq_any_beq [BEq α] (l : List α) (a : α) : l.contains a = l.any (a == ·) := by
-  induction l with simp | cons b l => cases a == b <;> simp [*]
-
-theorem not_all_eq_any_not (l : List α) (p : α → Bool) : (!l.all p) = l.any fun a => !p a := by
-  induction l with simp | cons _ _ ih => rw [ih]
-
-theorem not_any_eq_all_not (l : List α) (p : α → Bool) : (!l.any p) = l.all fun a => !p a := by
-  induction l with simp | cons _ _ ih => rw [ih]
-
-theorem or_all_distrib_left (l : List α) (p : α → Bool) (q : Bool) :
-    (q || l.all p) = l.all fun a => q || p a := by
-  induction l with simp | cons _ _ ih => rw [Bool.or_and_distrib_left, ih]
-
-theorem or_all_distrib_right (l : List α) (p : α → Bool) (q : Bool) :
-    (l.all p || q) = l.all fun a => p a || q := by
-  induction l with simp | cons _ _ ih => rw [Bool.or_and_distrib_right, ih]
-
-theorem and_any_distrib_left (l : List α) (p : α → Bool) (q : Bool) :
-    (q && l.any p) = l.any fun a => q && p a := by
-  induction l with simp | cons _ _ ih => rw [Bool.and_or_distrib_left, ih]
-
-theorem and_any_distrib_right (l : List α) (p : α → Bool) (q : Bool) :
-    (l.any p && q) = l.any fun a => p a && q := by
-  induction l with simp | cons _ _ ih => rw [Bool.and_or_distrib_right, ih]
-
-theorem any_eq_not_all_not (l : List α) (p : α → Bool) : l.any p = !l.all (!p .) := by
-  simp only [not_all_eq_any_not, Bool.not_not]
-
-theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (!p .) := by
-  simp only [not_any_eq_all_not, Bool.not_not]
-
-/-! ### reverse -/
-
-@[simp] theorem mem_reverseAux {x : α} : ∀ {as bs}, x ∈ reverseAux as bs ↔ x ∈ as ∨ x ∈ bs
-  | [], _ => ⟨.inr, fun | .inr h => h⟩
-  | a :: _, _ => by rw [reverseAux, mem_cons, or_assoc, or_left_comm, mem_reverseAux, mem_cons]
-
-@[simp] theorem mem_reverse {x : α} {as : List α} : x ∈ reverse as ↔ x ∈ as := by simp [reverse]
-
-/-! ### insert -/
-
-section insert
-variable [BEq α] [LawfulBEq α]
-
-@[simp] theorem insert_of_mem {l : List α} (h : a ∈ l) : l.insert a = l := by
-  simp [List.insert, h]
-
-@[simp] theorem insert_of_not_mem {l : List α} (h : a ∉ l) : l.insert a = a :: l := by
-  simp [List.insert, h]
-
-@[simp] theorem mem_insert_iff {l : List α} : a ∈ l.insert b ↔ a = b ∨ a ∈ l := by
-  if h : b ∈ l then
-    rw [insert_of_mem h]
-    constructor; {apply Or.inr}
-    intro
-    | Or.inl h' => rw [h']; exact h
-    | Or.inr h' => exact h'
-  else rw [insert_of_not_mem h, mem_cons]
-
-@[simp 1100] theorem mem_insert_self (a : α) (l : List α) : a ∈ l.insert a :=
-  mem_insert_iff.2 (Or.inl rfl)
-
-theorem mem_insert_of_mem {l : List α} (h : a ∈ l) : a ∈ l.insert b :=
-  mem_insert_iff.2 (Or.inr h)
-
-theorem eq_or_mem_of_mem_insert {l : List α} (h : a ∈ l.insert b) : a = b ∨ a ∈ l :=
-  mem_insert_iff.1 h
-
-@[simp] theorem length_insert_of_mem {l : List α} (h : a ∈ l) :
-    length (l.insert a) = length l := by rw [insert_of_mem h]
-
-@[simp] theorem length_insert_of_not_mem {l : List α} (h : a ∉ l) :
-    length (l.insert a) = length l + 1 := by rw [insert_of_not_mem h]; rfl
-
-end insert
-
 /-! ### eraseP -/
 
 @[simp] theorem eraseP_nil : [].eraseP p = [] := rfl
@@ -1525,19 +528,6 @@ theorem eraseP_map (f : β → α) : ∀ (l : List β), (map f l).eraseP p = map
 section erase
 variable [BEq α]
 
-@[simp] theorem erase_nil (a : α) : [].erase a = [] := rfl
-
-theorem erase_cons (a b : α) (l : List α) :
-    (b :: l).erase a = if b == a then l else b :: l.erase a :=
-  if h : b == a then by simp [List.erase, h]
-  else by simp [List.erase, h, (beq_eq_false_iff_ne _ _).2 h]
-
-@[simp] theorem erase_cons_head [LawfulBEq α] (a : α) (l : List α) : (a :: l).erase a = l := by
-  simp [erase_cons]
-
-@[simp] theorem erase_cons_tail {a b : α} (l : List α) (h : ¬(b == a)) :
-    (b :: l).erase a = b :: l.erase a := by simp only [erase_cons, if_neg h]
-
 theorem erase_eq_eraseP' (a : α) (l : List α) : l.erase a = l.eraseP (· == a) := by
   induction l
   · simp
@@ -1550,12 +540,6 @@ theorem erase_eq_eraseP [LawfulBEq α] (a : α) : ∀ l : List α,  l.erase a =
   | b :: l => by
     if h : a = b then simp [h] else simp [h, Ne.symm h, erase_eq_eraseP a l]
 
-theorem erase_of_not_mem [LawfulBEq α] {a : α} : ∀ {l : List α}, a ∉ l → l.erase a = l
-  | [], _ => rfl
-  | b :: l, h => by
-    rw [mem_cons, not_or] at h
-    simp only [erase_cons, if_neg, erase_of_not_mem h.2, beq_iff_eq, Ne.symm h.1, not_false_eq_true]
-
 theorem exists_erase_eq [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) :
     ∃ l₁ l₂, a ∉ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.erase a = l₁ ++ l₂ := by
   let ⟨_, l₁, l₂, h₁, e, h₂, h₃⟩ := exists_of_eraseP h (beq_self_eq_true _)
@@ -1609,105 +593,12 @@ end erase
 
 /-! ### filter and partition -/
 
-@[simp] theorem filter_append {p : α → Bool} :
-    ∀ (l₁ l₂ : List α), filter p (l₁ ++ l₂) = filter p l₁ ++ filter p l₂
-  | [], l₂ => rfl
-  | a :: l₁, l₂ => by simp [filter]; split <;> simp [filter_append l₁]
-
 @[simp] theorem filter_sublist {p : α → Bool} : ∀ (l : List α), filter p l <+ l
   | [] => .slnil
   | a :: l => by rw [filter]; split <;> simp [Sublist.cons, Sublist.cons₂, filter_sublist l]
 
-@[simp] theorem partition_eq_filter_filter (p : α → Bool) (l : List α) :
-    partition p l = (filter p l, filter (not ∘ p) l) := by simp [partition, aux] where
-  aux : ∀ l {as bs}, partition.loop p l (as, bs) =
-    (as.reverse ++ filter p l, bs.reverse ++ filter (not ∘ p) l)
-  | [] => by simp [partition.loop, filter]
-  | a :: l => by cases pa : p a <;> simp [partition.loop, pa, aux, filter, append_assoc]
-
-theorem filter_congr' {p q : α → Bool} :
-    ∀ {l : List α}, (∀ x ∈ l, p x ↔ q x) → filter p l = filter q l
-  | [], _ => rfl
-  | a :: l, h => by
-    rw [forall_mem_cons] at h; by_cases pa : p a
-    · simp [pa, h.1.1 pa, filter_congr' h.2]
-    · simp [pa, mt h.1.2 pa, filter_congr' h.2]
-
 /-! ### filterMap -/
 
-@[simp] theorem filterMap_nil (f : α → Option β) : filterMap f [] = [] := rfl
-
-@[simp] theorem filterMap_cons (f : α → Option β) (a : α) (l : List α) :
-    filterMap f (a :: l) =
-      match f a with
-      | none => filterMap f l
-      | some b => b :: filterMap f l := rfl
-
-theorem filterMap_cons_none {f : α → Option β} (a : α) (l : List α) (h : f a = none) :
-    filterMap f (a :: l) = filterMap f l := by simp only [filterMap, h]
-
-theorem filterMap_cons_some (f : α → Option β) (a : α) (l : List α) {b : β} (h : f a = some b) :
-    filterMap f (a :: l) = b :: filterMap f l := by simp only [filterMap, h]
-
-theorem filterMap_append {α β : Type _} (l l' : List α) (f : α → Option β) :
-    filterMap f (l ++ l') = filterMap f l ++ filterMap f l' := by
-  induction l <;> simp; split <;> simp [*]
-
-@[simp]
-theorem filterMap_eq_map (f : α → β) : filterMap (some ∘ f) = map f := by
-  funext l; induction l <;> simp [*]
-
-@[simp]
-theorem filterMap_eq_filter (p : α → Bool) :
-    filterMap (Option.guard (p ·)) = filter p := by
-  funext l
-  induction l with
-  | nil => rfl
-  | cons a l IH => by_cases pa : p a <;> simp [Option.guard, pa, ← IH]
-
-theorem filterMap_filterMap (f : α → Option β) (g : β → Option γ) (l : List α) :
-    filterMap g (filterMap f l) = filterMap (fun x => (f x).bind g) l := by
-  induction l with
-  | nil => rfl
-  | cons a l IH => cases h : f a <;> simp [*]
-
-theorem map_filterMap (f : α → Option β) (g : β → γ) (l : List α) :
-    map g (filterMap f l) = filterMap (fun x => (f x).map g) l := by
-  simp only [← filterMap_eq_map, filterMap_filterMap, Option.map_eq_bind]
-
-@[simp]
-theorem filterMap_map (f : α → β) (g : β → Option γ) (l : List α) :
-    filterMap g (map f l) = filterMap (g ∘ f) l := by
-  rw [← filterMap_eq_map, filterMap_filterMap]; rfl
-
-theorem filter_filterMap (f : α → Option β) (p : β → Bool) (l : List α) :
-    filter p (filterMap f l) = filterMap (fun x => (f x).filter p) l := by
-  rw [← filterMap_eq_filter, filterMap_filterMap]
-  congr; funext x; cases f x <;> simp [Option.filter, Option.guard]
-
-theorem filterMap_filter (p : α → Bool) (f : α → Option β) (l : List α) :
-    filterMap f (filter p l) = filterMap (fun x => if p x then f x else none) l := by
-  rw [← filterMap_eq_filter, filterMap_filterMap]
-  congr; funext x; by_cases h : p x <;> simp [Option.guard, h]
-
-@[simp] theorem filterMap_some (l : List α) : filterMap some l = l := by
-  erw [filterMap_eq_map, map_id]
-
-theorem map_filterMap_some_eq_filter_map_is_some (f : α → Option β) (l : List α) :
-    (l.filterMap f).map some = (l.map f).filter fun b => b.isSome := by
-  induction l <;> simp; split <;> simp [*]
-
-@[simp] theorem mem_filterMap (f : α → Option β) (l : List α) {b : β} :
-    b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b := by
-  induction l <;> simp; split <;> simp [*, eq_comm]
-
-@[simp] theorem filterMap_join (f : α → Option β) (L : List (List α)) :
-    filterMap f (join L) = join (map (filterMap f) L) := by
-  induction L <;> simp [*, filterMap_append]
-
-theorem map_filterMap_of_inv (f : α → Option β) (g : β → α) (H : ∀ x : α, (f x).map g = some x)
-    (l : List α) : map g (filterMap f l) = l := by simp only [map_filterMap, H, filterMap_some]
-
 theorem length_filter_le (p : α → Bool) (l : List α) :
     (l.filter p).length ≤ l.length := (filter_sublist _).length_le
 
@@ -1723,13 +614,6 @@ protected theorem Sublist.filterMap (f : α → Option β) (s : l₁ <+ l₂) :
 theorem Sublist.filter (p : α → Bool) {l₁ l₂} (s : l₁ <+ l₂) : filter p l₁ <+ filter p l₂ := by
   rw [← filterMap_eq_filter]; apply s.filterMap
 
-theorem map_filter (f : β → α) (l : List β) : filter p (map f l) = map f (filter (p ∘ f) l) := by
-  rw [← filterMap_eq_map, filter_filterMap, filterMap_filter]; rfl
-
-@[simp] theorem filter_filter (q) : ∀ l, filter p (filter q l) = filter (fun a => p a ∧ q a) l
-  | [] => rfl
-  | a :: l => by by_cases hp : p a <;> by_cases hq : q a <;> simp [hp, hq, filter_filter _ l]
-
 @[simp]
 theorem filter_eq_self {l} : filter p l = l ↔ ∀ a ∈ l, p a := by
   induction l with simp
@@ -1741,39 +625,6 @@ theorem filter_eq_self {l} : filter p l = l ↔ ∀ a ∈ l, p a := by
 theorem filter_length_eq_length {l} : (filter p l).length = l.length ↔ ∀ a ∈ l, p a :=
   Iff.trans ⟨l.filter_sublist.eq_of_length, congrArg length⟩ filter_eq_self
 
-/-! ### find? -/
-
-theorem find?_cons_of_pos (l) (h : p a) : find? p (a :: l) = some a :=
-  by simp [find?, h]
-
-theorem find?_cons_of_neg (l) (h : ¬p a) : find? p (a :: l) = find? p l :=
-  by simp [find?, h]
-
-theorem find?_eq_none : find? p l = none ↔ ∀ x ∈ l, ¬ p x := by
-  induction l <;> simp [find?_cons]; split <;> simp [*]
-
-theorem find?_some : ∀ {l}, find? p l = some a → p a
-  | b :: l, H => by
-    by_cases h : p b <;> simp [find?, h] at H
-    · exact H ▸ h
-    · exact find?_some H
-
-@[simp] theorem mem_of_find?_eq_some : ∀ {l}, find? p l = some a → a ∈ l
-  | b :: l, H => by
-    by_cases h : p b <;> simp [find?, h] at H
-    · exact H ▸ .head _
-    · exact .tail _ (mem_of_find?_eq_some H)
-
-/-! ### findSome? -/
-
-theorem exists_of_findSome?_eq_some {l : List α} {f : α → Option β} (w : l.findSome? f = some b) :
-    ∃ a, a ∈ l ∧ f a = b := by
-  induction l with
-  | nil => simp_all
-  | cons h l ih =>
-    simp_all only [findSome?_cons, mem_cons, exists_eq_or_imp]
-    split at w <;> simp_all
-
 /-! ### findIdx -/
 
 @[simp] theorem findIdx_nil {α : Type _} (p : α → Bool) : [].findIdx p = 0 := rfl
@@ -2372,22 +1223,6 @@ theorem disjoint_take_drop : ∀ {l : List α}, l.Nodup → m ≤ n → Disjoint
       refine ⟨fun h => h₀ _ (mem_of_mem_drop h) rfl, ?_⟩
       exact disjoint_take_drop h₁ (Nat.le_of_succ_le_succ h)
 
-/-! ### takeWhile and dropWhile -/
-
-@[simp] theorem takeWhile_append_dropWhile (p : α → Bool) :
-    ∀ (l : List α), takeWhile p l ++ dropWhile p l = l
-  | [] => rfl
-  | x :: xs => by simp [takeWhile, dropWhile]; cases p x <;> simp [takeWhile_append_dropWhile p xs]
-
-theorem dropWhile_append {xs ys : List α} :
-    (xs ++ ys).dropWhile p =
-      if (xs.dropWhile p).isEmpty then ys.dropWhile p else xs.dropWhile p ++ ys := by
-  induction xs with
-  | nil => simp
-  | cons h t ih =>
-    simp only [cons_append, dropWhile_cons]
-    split <;> simp_all
-
 /-! ### Chain -/
 
 attribute [simp] Chain.nil
@@ -2582,60 +1417,8 @@ theorem reverse_range' : ∀ s n : Nat, reverse (range' s n) = map (s + n - 1 -
 @[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']
 
-@[simp] theorem enumFrom_length : ∀ {n} {l : List α}, (enumFrom n l).length = l.length
-  | _, [] => rfl
-  | _, _ :: _ => congrArg Nat.succ enumFrom_length
-
-@[simp] theorem enum_length : (enum l).length = l.length :=
-  enumFrom_length
-
 /-! ### maximum? -/
 
-@[simp] theorem maximum?_nil [Max α] : ([] : List α).maximum? = none := rfl
-
--- We don't put `@[simp]` on `minimum?_cons`,
--- because the definition in terms of `foldl` is not useful for proofs.
-theorem maximum?_cons [Max α] {xs : List α} : (x :: xs).maximum? = foldl max x xs := rfl
-
-@[simp] theorem maximum?_eq_none_iff {xs : List α} [Max α] : xs.maximum? = none ↔ xs = [] := by
-  cases xs <;> simp [maximum?]
-
-theorem maximum?_mem [Max α] (min_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) :
-    {xs : List α} → xs.maximum? = some a → a ∈ xs
-  | nil => by simp
-  | cons x xs => by
-    rw [maximum?]; rintro ⟨⟩
-    induction xs generalizing x with simp at *
-    | cons y xs ih =>
-      rcases ih (max x y) with h | h <;> simp [h]
-      simp [← or_assoc, min_eq_or x y]
-
-theorem maximum?_le_iff [Max α] [LE α]
-    (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) :
-    {xs : List α} → xs.maximum? = some a → ∀ x, a ≤ x ↔ ∀ b ∈ xs, b ≤ x
-  | nil => by simp
-  | cons x xs => by
-    rw [maximum?]; rintro ⟨⟩ y
-    induction xs generalizing x with
-    | nil => simp
-    | cons y xs ih => simp [ih, max_le_iff, and_assoc]
-
--- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `max_eq_or`,
--- and `le_min_iff`.
-theorem maximum?_eq_some_iff [Max α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
-    (le_refl : ∀ a : α, a ≤ a)
-    (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b)
-    (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} :
-    xs.maximum? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, b ≤ a := by
-  refine ⟨fun h => ⟨maximum?_mem max_eq_or h, (maximum?_le_iff max_le_iff h _).1 (le_refl _)⟩, ?_⟩
-  intro ⟨h₁, h₂⟩
-  cases xs with
-  | nil => simp at h₁
-  | cons x xs =>
-    exact congrArg some <| anti.1
-      (h₂ _ (maximum?_mem max_eq_or (xs := x::xs) rfl))
-      ((maximum?_le_iff max_le_iff (xs := x::xs) rfl _).1 (le_refl _) _ h₁)
-
 -- A specialization of `maximum?_eq_some_iff` to Nat.
 theorem maximum?_eq_some_iff' {xs : List Nat} :
     xs.maximum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, b ≤ a) :=
@@ -2719,7 +1502,7 @@ theorem merge_loop (s : α → α → Bool) (l r t) :
   | zero =>
     rw [eq_nil_of_length_eq_zero (Nat.eq_zero_of_add_eq_zero_left hn)]
     rw [eq_nil_of_length_eq_zero (Nat.eq_zero_of_add_eq_zero_right hn)]
-    rfl
+    simp only [merge.loop, reverseAux]
   | succ n ih =>
     match l, r with
     | [], r => simp only [merge_loop_nil_left]; rfl
@@ -2779,46 +1562,3 @@ theorem mem_merge_left (s : α → α → Bool) (h : x ∈ l) : x ∈ merge s l
 
 theorem mem_merge_right (s : α → α → Bool) (h : x ∈ r) : x ∈ merge s l r :=
   mem_merge.2 <| .inr h
-
-/-! ### lt -/
-
-theorem lt_irrefl' [LT α] (lt_irrefl : ∀ x : α, ¬x < x) (l : List α) : ¬l < l := by
-  induction l with
-  | nil => nofun
-  | cons a l ih => intro
-    | .head _ _ h => exact lt_irrefl _ h
-    | .tail _ _ h => exact ih h
-
-theorem lt_trans' [LT α] [DecidableRel (@LT.lt α _)]
-    (lt_trans : ∀ {x y z : α}, x < y → y < z → x < z)
-    (le_trans : ∀ {x y z : α}, ¬x < y → ¬y < z → ¬x < z)
-    {l₁ l₂ l₃ : List α} (h₁ : l₁ < l₂) (h₂ : l₂ < l₃) : l₁ < l₃ := by
-  induction h₁ generalizing l₃ with
-  | nil => let _::_ := l₃; exact List.lt.nil ..
-  | @head a l₁ b l₂ ab =>
-    match h₂ with
-    | .head l₂ l₃ bc => exact List.lt.head _ _ (lt_trans ab bc)
-    | .tail _ cb ih =>
-      exact List.lt.head _ _ <| Decidable.by_contra (le_trans · cb ab)
-  | @tail a l₁ b l₂ ab ba h₁ ih2 =>
-    match h₂ with
-    | .head l₂ l₃ bc =>
-      exact List.lt.head _ _ <| Decidable.by_contra (le_trans ba · bc)
-    | .tail bc cb ih =>
-      exact List.lt.tail (le_trans ab bc) (le_trans cb ba) (ih2 ih)
-
-theorem lt_antisymm' [LT α]
-    (lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y)
-    {l₁ l₂ : List α} (h₁ : ¬l₁ < l₂) (h₂ : ¬l₂ < l₁) : l₁ = l₂ := by
-  induction l₁ generalizing l₂ with
-  | nil =>
-    cases l₂ with
-    | nil => rfl
-    | cons b l₂ => cases h₁ (.nil ..)
-  | cons a l₁ ih =>
-    cases l₂ with
-    | nil => cases h₂ (.nil ..)
-    | cons b l₂ =>
-      have ab : ¬a < b := fun ab => h₁ (.head _ _ ab)
-      cases lt_antisymm ab (fun ba => h₂ (.head _ _ ba))
-      rw [ih (fun ll => h₁ (.tail ab ab ll)) (fun ll => h₂ (.tail ab ab ll))]
diff --git a/Batteries/Data/String/Lemmas.lean b/Batteries/Data/String/Lemmas.lean
index 8deade2f9c..8a9376fe05 100644
--- a/Batteries/Data/String/Lemmas.lean
+++ b/Batteries/Data/String/Lemmas.lean
@@ -9,16 +9,9 @@ import Batteries.Data.String.Basic
 import Batteries.Tactic.Lint.Misc
 import Batteries.Tactic.SeqFocus
 
-@[simp] theorem Char.length_toString (c : Char) : c.toString.length = 1 := rfl
-
 namespace String
 
-@[ext] theorem ext {s₁ s₂ : String} (h : s₁.data = s₂.data) : s₁ = s₂ :=
-  show ⟨s₁.data⟩ = (⟨s₂.data⟩ : String) from h ▸ rfl
-
-theorem ext_iff {s₁ s₂ : String} : s₁ = s₂ ↔ s₁.data = s₂.data := ⟨fun h => h ▸ rfl, ext⟩
-
-theorem lt_irrefl (s : String) : ¬s < s := List.lt_irrefl' (α := Char) (fun _ => Nat.lt_irrefl _) _
+attribute [ext] ext
 
 theorem lt_trans {s₁ s₂ s₃ : String} : s₁ < s₂ → s₂ < s₃ → s₁ < s₃ :=
   List.lt_trans' (α := Char) Nat.lt_trans
@@ -36,34 +29,10 @@ instance : Batteries.LTOrd String := .compareOfLessAndEq
 
 instance : Batteries.BEqOrd String := .compareOfLessAndEq String.lt_irrefl
 
-@[simp] theorem default_eq : default = "" := rfl
-
-@[simp] theorem str_eq : str = push := rfl
-
 @[simp] theorem mk_length (s : List Char) : (String.mk s).length = s.length := rfl
 
-@[simp] theorem length_empty : "".length = 0 := rfl
-
-@[simp] theorem length_singleton (c : Char) : (String.singleton c).length = 1 := rfl
-
-@[simp] theorem length_push (c : Char) : (String.push s c).length = s.length + 1 := by
-  rw [push, mk_length, List.length_append, List.length_singleton, Nat.succ.injEq]
-  rfl
-
-@[simp] theorem length_pushn (c : Char) (n : Nat) : (pushn s c n).length = s.length + n := by
-  unfold pushn; induction n <;> simp [Nat.repeat, Nat.add_assoc, *]
-
-@[simp] theorem length_append (s t : String) : (s ++ t).length = s.length + t.length := by
-  simp only [length, append, List.length_append]
-
-@[simp] theorem data_push (s : String) (c : Char) : (s.push c).1 = s.1 ++ [c] := rfl
-
-@[simp] theorem data_append (s t : String) : (s ++ t).1 = s.1 ++ t.1 := rfl
-
 attribute [simp] toList -- prefer `String.data` over `String.toList` in lemmas
 
-theorem lt_iff (s t : String) : s < t ↔ s.1 < t.1 := .rfl
-
 private theorem add_csize_pos : 0 < i + csize c :=
   Nat.add_pos_right _ (csize_pos c)
 
@@ -117,69 +86,13 @@ end
 
 namespace Pos
 
-@[simp] theorem byteIdx_zero : (0 : Pos).byteIdx = 0 := rfl
-
-theorem byteIdx_mk (n : Nat) : byteIdx ⟨n⟩ = n := rfl
-
-@[simp] theorem mk_zero : ⟨0⟩ = (0 : Pos) := rfl
-
-@[simp] theorem mk_byteIdx (p : Pos) : ⟨p.byteIdx⟩ = p := rfl
-
-@[ext] theorem ext {i₁ i₂ : Pos} (h : i₁.byteIdx = i₂.byteIdx) : i₁ = i₂ :=
-  show ⟨i₁.byteIdx⟩ = (⟨i₂.byteIdx⟩ : Pos) from h ▸ rfl
-
-theorem ext_iff {i₁ i₂ : Pos} : i₁ = i₂ ↔ i₁.byteIdx = i₂.byteIdx := ⟨fun h => h ▸ rfl, ext⟩
-
-@[simp] theorem add_byteIdx (p₁ p₂ : Pos) : (p₁ + p₂).byteIdx = p₁.byteIdx + p₂.byteIdx := rfl
-
-theorem add_eq (p₁ p₂ : Pos) : p₁ + p₂ = ⟨p₁.byteIdx + p₂.byteIdx⟩ := rfl
-
-@[simp] theorem sub_byteIdx (p₁ p₂ : Pos) : (p₁ - p₂).byteIdx = p₁.byteIdx - p₂.byteIdx := rfl
-
-theorem sub_eq (p₁ p₂ : Pos) : p₁ - p₂ = ⟨p₁.byteIdx - p₂.byteIdx⟩ := rfl
-
-@[simp] theorem addChar_byteIdx (p : Pos) (c : Char) : (p + c).byteIdx = p.byteIdx + csize c := rfl
-
-theorem addChar_eq (p : Pos) (c : Char) : p + c = ⟨p.byteIdx + csize c⟩ := rfl
-
-theorem zero_addChar_byteIdx (c : Char) : ((0 : Pos) + c).byteIdx = csize c := by
-  simp only [addChar_byteIdx, byteIdx_zero, Nat.zero_add]
-
-theorem zero_addChar_eq (c : Char) : (0 : Pos) + c = ⟨csize c⟩ := by rw [← zero_addChar_byteIdx]
-
-theorem addChar_right_comm (p : Pos) (c₁ c₂ : Char) : p + c₁ + c₂ = p + c₂ + c₁ := by
-  apply ext
-  repeat rw [pos_add_char]
-  apply Nat.add_right_comm
+attribute [ext] ext
 
 theorem lt_addChar (p : Pos) (c : Char) : p < p + c := Nat.lt_add_of_pos_right (csize_pos _)
 
-theorem ne_of_lt {i₁ i₂ : Pos} (h : i₁ < i₂) : i₁ ≠ i₂ := mt ext_iff.1 (Nat.ne_of_lt h)
-
-theorem ne_of_gt {i₁ i₂ : Pos} (h : i₁ < i₂) : i₂ ≠ i₁ := (ne_of_lt h).symm
-
-@[simp] theorem addString_byteIdx (p : Pos) (s : String) :
-    (p + s).byteIdx = p.byteIdx + s.utf8ByteSize := rfl
-
-theorem addString_eq (p : Pos) (s : String) : p + s = ⟨p.byteIdx + s.utf8ByteSize⟩ := rfl
-
-theorem zero_addString_byteIdx (s : String) : ((0 : Pos) + s).byteIdx = s.utf8ByteSize := by
-  simp only [addString_byteIdx, byteIdx_zero, Nat.zero_add]
-
 private theorem zero_ne_addChar {i : Pos} {c : Char} : 0 ≠ i + c :=
   ne_of_lt add_csize_pos
 
-theorem zero_addString_eq (s : String) : (0 : Pos) + s = ⟨s.utf8ByteSize⟩ := by
-  rw [← zero_addString_byteIdx]
-
-theorem le_iff {i₁ i₂ : Pos} : i₁ ≤ i₂ ↔ i₁.byteIdx ≤ i₂.byteIdx := .rfl
-
-@[simp] theorem mk_le_mk {i₁ i₂ : Nat} : Pos.mk i₁ ≤ Pos.mk i₂ ↔ i₁ ≤ i₂ := .rfl
-
-theorem lt_iff {i₁ i₂ : Pos} : i₁ < i₂ ↔ i₁.byteIdx < i₂.byteIdx := .rfl
-
-@[simp] theorem mk_lt_mk {i₁ i₂ : Nat} : Pos.mk i₁ < Pos.mk i₂ ↔ i₁ < i₂ := .rfl
-
 /-- A string position is valid if it is equal to the UTF-8 length of an initial substring of `s`. -/
 def Valid (s : String) (p : Pos) : Prop :=
   ∃ cs cs', cs ++ cs' = s.1 ∧ p.1 = utf8Len cs
@@ -264,8 +177,6 @@ theorem utf8GetAux?_of_valid (cs cs' : List Char) {i p : Nat} (hp : i + utf8Len
 theorem get?_of_valid (cs cs' : List Char) : get? ⟨cs ++ cs'⟩ ⟨utf8Len cs⟩ = cs'.head? :=
   utf8GetAux?_of_valid _ _ (Nat.zero_add _)
 
-@[simp] theorem get!_eq_get (s : String) (p : Pos) : get! s p = get s p := rfl
-
 theorem utf8SetAux_of_valid (c' : Char) (cs cs' : List Char) {i p : Nat} (hp : i + utf8Len cs = p) :
     utf8SetAux c' (cs ++ cs') ⟨i⟩ ⟨p⟩ = cs ++ cs'.modifyHead fun _ => c' := by
   match cs, cs' with
@@ -292,8 +203,6 @@ theorem next_of_valid' (cs cs' : List Char) :
 theorem next_of_valid (cs : List Char) (c : Char) (cs' : List Char) :
     next ⟨cs ++ c :: cs'⟩ ⟨utf8Len cs⟩ = ⟨utf8Len cs + csize c⟩ := next_of_valid' ..
 
-theorem lt_next' (s : String) (p : Pos) : p < next s p := lt_next ..
-
 @[simp] theorem atEnd_iff (s : String) (p : Pos) : atEnd s p ↔ s.endPos ≤ p :=
   decide_eq_true_iff _
 
@@ -327,8 +236,6 @@ theorem prev_of_valid' (cs cs' : List Char) :
   | _, .inl rfl => rfl
   | _, .inr ⟨cs, c, rfl⟩ => simp [prev_of_valid]
 
-@[simp] theorem prev_zero (s : String) : prev s 0 = 0 := rfl
-
 theorem front_eq (s : String) : front s = s.1.headD default := by
   unfold front; exact get_of_valid [] s.1
 
@@ -342,16 +249,16 @@ theorem atEnd_of_valid (cs : List Char) (cs' : List Char) :
   rw [atEnd_iff]
   cases cs' <;> simp [Nat.lt_add_of_pos_right add_csize_pos]
 
-@[simp] theorem get'_eq (s : String) (p : Pos) (h) : get' s p h = get s p := rfl
-
-@[simp] theorem next'_eq (s : String) (p : Pos) (h) : next' s p h = next s p := rfl
-
+unseal posOfAux findAux in
 theorem posOfAux_eq (s c) : posOfAux s c = findAux s (· == c) := rfl
 
+unseal posOfAux findAux in
 theorem posOf_eq (s c) : posOf s c = find s (· == c) := rfl
 
+unseal revPosOfAux revFindAux in
 theorem revPosOfAux_eq (s c) : revPosOfAux s c = revFindAux s (· == c) := rfl
 
+unseal revPosOfAux revFindAux in
 theorem revPosOf_eq (s c) : revPosOf s c = revFind s (· == c) := rfl
 
 @[nolint unusedHavesSuffices] -- false positive from unfolding String.findAux
@@ -516,16 +423,8 @@ theorem join_eq (ss : List String) : join ss = ⟨(ss.map data).join⟩ := go ss
 @[simp] theorem data_join (ss : List String) : (join ss).data = (ss.map data).join := by
   rw [join_eq]
 
-theorem singleton_eq (c : Char) : singleton c = ⟨[c]⟩ := rfl
-
-@[simp] theorem data_singleton (c : Char) : (singleton c).data = [c] := rfl
-
-@[simp] theorem append_nil (s : String) : s ++ "" = s := ext (List.append_nil _)
-
-@[simp] theorem nil_append (s : String) : "" ++ s = s := rfl
-
-theorem append_assoc (s₁ s₂ s₃ : String) : (s₁ ++ s₂) ++ s₃ = s₁ ++ (s₂ ++ s₃) :=
-  ext (List.append_assoc ..)
+@[deprecated (since := "2024-06-06")] alias append_nil := append_empty
+@[deprecated (since := "2024-06-06")] alias nil_append := empty_append
 
 namespace Iterator
 
@@ -801,12 +700,6 @@ open String
 
 namespace Substring
 
-@[simp] theorem prev_zero (s : Substring) : s.prev 0 = 0 := by simp [prev, Pos.add_eq]
-
-@[simp] theorem prevn_zero (s : Substring) : ∀ n, s.prevn n 0 = 0
-  | 0 => rfl
-  | n+1 => by simp [prevn, prevn_zero s n]
-
 /-- Validity for a substring. -/
 structure Valid (s : Substring) : Prop where
   /-- The start position of a valid substring is valid. -/
diff --git a/Batteries/Lean/Delaborator.lean b/Batteries/Lean/Delaborator.lean
index 98aa890e01..d722eef9d8 100644
--- a/Batteries/Lean/Delaborator.lean
+++ b/Batteries/Lean/Delaborator.lean
@@ -7,19 +7,7 @@ import Lean.PrettyPrinter
 
 open Lean PrettyPrinter Delaborator SubExpr
 
-/-- Pretty print a const expression using `delabConst` and generate terminfo.
-This function avoids inserting `@` if the constant is for a function whose first
-argument is implicit, which is what the default `toMessageData` for `Expr` does.
-Panics if `e` is not a constant. -/
+/-- Abbreviation for `Lean.MessageData.ofConst`. -/
+@[deprecated Lean.MessageData.ofConst]
 def Lean.ppConst (e : Expr) : MessageData :=
-  if e.isConst then
-    .ofPPFormat {
-      pp := fun
-        | some ctx => ctx.runMetaM <| withOptions (pp.tagAppFns.set · true) <|
-          -- The pp.tagAppFns option causes the `delabConst` function to annotate
-          -- the constant with terminfo, which is necessary for seeing the type on mouse hover.
-          PrettyPrinter.ppExprWithInfos (delab := delabConst) e
-        | none => return f!"{e}"
-    }
-  else
-    panic! "not a constant"
+  Lean.MessageData.ofConst e
diff --git a/Batteries/Tactic/Instances.lean b/Batteries/Tactic/Instances.lean
index 703fed87cd..b243c4f153 100644
--- a/Batteries/Tactic/Instances.lean
+++ b/Batteries/Tactic/Instances.lean
@@ -45,11 +45,7 @@ elab (name := instancesCmd) tk:"#instances " stx:term : command => runTermElabM
       let mut msg := m!"\n"
       if e.priority != 1000 then -- evalPrio default := 1000
         msg := msg ++ m!"(prio {e.priority}) "
-      msgs := msgs.push <| msg ++ .ofPPFormat { pp := fun
-        | some ctx => ctx.runMetaM <| withOptions (pp.tagAppFns.set · true) <|
-          PrettyPrinter.ppSignature c
-        | none     => return f!"{c}"
-      }
+      msgs := msgs.push <| msg ++ MessageData.signature c
     for linst in ← getLocalInstances do
       if linst.className == className then
         msgs := msgs.push m!"(local) {linst.fvar} : {← inferType linst.fvar}"
diff --git a/Batteries/Tactic/PrintDependents.lean b/Batteries/Tactic/PrintDependents.lean
index d41c89201b..9c55a04ecd 100644
--- a/Batteries/Tactic/PrintDependents.lean
+++ b/Batteries/Tactic/PrintDependents.lean
@@ -99,7 +99,7 @@ elab tk:"#print" &"dependents" ids:(ppSpace colGt ident)* : command => do
       if let some ranges ← findDeclarationRanges? c then
         out := out.push (c, ranges.range.pos.1)
   let msg ← out.qsort (·.2 < ·.2) |>.mapM fun (c, _) => do
-    let mut msg := m!"{ppConst (← mkConstWithLevelParams c)}: "
+    let mut msg := m!"{MessageData.ofConst (← mkConstWithLevelParams c)}: "
     if init.result.contains c then
       msg := msg ++ m!"<specified>"
     else
@@ -113,6 +113,6 @@ elab tk:"#print" &"dependents" ids:(ppSpace colGt ident)* : command => do
       | _                                => #[]
       for c in RBTree.fromArray consts Name.cmp do
         if state.result.find? c = some true then
-          msg := msg ++ m!"{ppConst (← mkConstWithLevelParams c)} "
+          msg := msg ++ m!"{MessageData.ofConst (← mkConstWithLevelParams c)} "
     return msg
   logInfoAt tk (.joinSep msg.toList "\n")
diff --git a/Batteries/Tactic/PrintPrefix.lean b/Batteries/Tactic/PrintPrefix.lean
index 65314bb486..0046f0a4d7 100644
--- a/Batteries/Tactic/PrintPrefix.lean
+++ b/Batteries/Tactic/PrintPrefix.lean
@@ -79,13 +79,9 @@ private def matchingConstants (opts : PrintPrefixConfig) (pre : Name)
   let cinfos := cinfos.qsort fun p q => lexNameLt (reverseName p.name) (reverseName q.name)
   cinfos.mapM fun cinfo => do
     if opts.showTypes then
-      pure <| .ofPPFormat { pp := fun
-        | some ctx => ctx.runMetaM <|
-          withOptions (pp.tagAppFns.set · true) <| PrettyPrinter.ppSignature cinfo.name
-        | none     => return f!"{cinfo.name}"  -- should never happen
-      } ++ "\n"
+      pure <| MessageData.signature cinfo.name ++ "\n"
     else
-      pure m!"{ppConst (← mkConstWithLevelParams cinfo.name)}\n"
+      pure m!"{MessageData.ofConst (← mkConstWithLevelParams cinfo.name)}\n"
 
 /--
 The command `#print prefix foo` will print all definitions that start with
diff --git a/Batteries/Tactic/ShowUnused.lean b/Batteries/Tactic/ShowUnused.lean
index 8f81c6fa59..25989a3da9 100644
--- a/Batteries/Tactic/ShowUnused.lean
+++ b/Batteries/Tactic/ShowUnused.lean
@@ -61,11 +61,11 @@ elab tk:"#show_unused" ids:(ppSpace colGt ident)* : command => do
   let pos := fileMap.toPosition <| (tk.getPos? <|> (← getRef).getPos?).getD 0
   let pfx := m!"#show_unused (line {pos.line}) says:\n"
   let post := m!" is not used transitively by \
-    {← ns.mapM (Lean.ppConst <$> mkConstWithLevelParams ·)}"
+    {← ns.mapM (MessageData.ofConst <$> mkConstWithLevelParams ·)}"
   for (c, range) in unused do
     logWarningAt (Syntax.ofRange range) <|
       .tagged Linter.linter.unusedVariables.name <|
-        m!"{pfx}{Lean.ppConst (← mkConstWithLevelParams c)}{post}"
+        m!"{pfx}{MessageData.ofConst (← mkConstWithLevelParams c)}{post}"
   if unused.isEmpty then
     logInfoAt tk "No unused definitions"
   else
diff --git a/Batteries/WF.lean b/Batteries/WF.lean
index 7a702665ae..73428fe3bd 100644
--- a/Batteries/WF.lean
+++ b/Batteries/WF.lean
@@ -53,6 +53,8 @@ instance wfRel {r : α → α → Prop} : WellFoundedRelation { val // Acc r val
   intro a (fun x h => t.inv h) (fun y hr => recC intro (t.inv hr))
 termination_by Subtype.mk a t
 
+unseal recC
+
 private theorem recC_intro {motive : (a : α) → Acc r a → Sort v}
     (intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) →
      ((y : α) → (hr : r y x) → motive y (h y hr)) → motive x (intro x h))
@@ -120,6 +122,8 @@ Workaround until Lean has native support for this. -/
   F x (fun y _ => fixC hwf F y)
 termination_by hwf.wrap x
 
+unseal fixC
+
 @[csimp] private theorem fix_eq_fixC : @fix = @fixC := rfl
 
 end WellFounded
diff --git a/lakefile.lean b/lakefile.lean
index 791f3a9c3c..a59342f68c 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -21,6 +21,6 @@ lean_exe runLinter where
 meta if get_config? doc |>.isSome then
 require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
 
-@[test_runner]
+@[test_driver]
 lean_exe test where
   srcDir := "scripts"
diff --git a/lean-toolchain b/lean-toolchain
index ef1f67e9e6..0ba3faf807 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.8.0
+leanprover/lean4:v4.9.0-rc1
diff --git a/test/list_sublists.lean b/test/list_sublists.lean
index 18eee40f2c..871e8a56e5 100644
--- a/test/list_sublists.lean
+++ b/test/list_sublists.lean
@@ -1,7 +1,7 @@
 import Batteries.Data.List.Basic
 
 -- this times out with `sublistsFast`
-set_option maxRecDepth 561 in
+set_option maxRecDepth 562 in
 example : [1, 2, 3].sublists.sublists.length = 256 := rfl
 
 -- TODO(batteries#307): until we have the `csimp` lemma in batteries,