diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean
index cde4aab1c5..771a3dd41b 100644
--- a/src/Init/Data/List/Find.lean
+++ b/src/Init/Data/List/Find.lean
@@ -35,9 +35,11 @@ theorem exists_of_findSome?_eq_some {l : List α} {f : α → Option β} (w : l.
     simp_all only [findSome?_cons, mem_cons, exists_eq_or_imp]
     split at w <;> simp_all
 
-@[simp] theorem findSome?_eq_none : findSome? p l = none ↔ ∀ x ∈ l, p x = none := by
+@[simp] theorem findSome?_eq_none_iff : findSome? p l = none ↔ ∀ x ∈ l, p x = none := by
   induction l <;> simp [findSome?_cons]; split <;> simp [*]
 
+@[deprecated findSome?_eq_none_iff (since := "2024-09-05")] abbrev findSome?_eq_none := @findSome?_eq_none_iff
+
 @[simp] theorem findSome?_isSome_iff {f : α → Option β} {l : List α} :
     (l.findSome? f).isSome ↔ ∃ x, x ∈ l ∧ (f x).isSome := by
   induction l with
@@ -46,6 +48,41 @@ theorem exists_of_findSome?_eq_some {l : List α} {f : α → Option β} (w : l.
     simp only [findSome?_cons]
     split <;> simp_all
 
+theorem findSome?_eq_some_iff {f : α → Option β} {l : List α} {b : β} :
+    l.findSome? f = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ x ∈ l₁, f x = none := by
+  induction l with
+  | nil => simp
+  | cons p l ih =>
+    simp only [findSome?_cons]
+    split <;> rename_i b' h
+    · simp only [Option.some.injEq, exists_and_right]
+      constructor
+      · rintro rfl
+        exact ⟨[], p, ⟨l, rfl⟩, h, by simp⟩
+      · rintro ⟨(⟨⟩ | ⟨p', l₁⟩), a, ⟨l₂, h₁⟩, h₂, h₃⟩
+        · simp only [nil_append, cons.injEq] at h₁
+          apply Option.some.inj
+          simp [← h, ← h₂, h₁.1]
+        · simp only [cons_append, cons.injEq] at h₁
+          obtain ⟨rfl, rfl⟩ := h₁
+          specialize h₃ p
+          simp_all
+    · rw [ih]
+      constructor
+      · rintro ⟨l₁, a, l₂, rfl, h₁, h₂⟩
+        refine ⟨p :: l₁, a, l₂, rfl, h₁, ?_⟩
+        intro a w
+        simp at w
+        rcases w with rfl | w
+        · exact h
+        · exact h₂ _ w
+      · rintro ⟨l₁, a, l₂, h₁, h₂, h₃⟩
+        rcases l₁ with (⟨⟩ | ⟨a', l₁⟩)
+        · simp_all
+        · simp only [cons_append, cons.injEq] at h₁
+          obtain ⟨⟨rfl, rfl⟩, rfl⟩ := h₁
+          exact ⟨l₁, a, l₂, rfl, h₂, fun a' w => h₃ a' (mem_cons_of_mem p w)⟩
+
 @[simp] theorem findSome?_guard (l : List α) : findSome? (Option.guard fun x => p x) l = find? p l := by
   induction l with
   | nil => simp
@@ -95,6 +132,15 @@ theorem findSome?_append {l₁ l₂ : List α} : (l₁ ++ l₂).findSome? f = (l
     simp only [cons_append, findSome?]
     split <;> simp_all
 
+theorem head_join {L : List (List α)} (h : ∃ l, l ∈ L ∧ l ≠ []) :
+    (join L).head (by simpa using h) = (L.findSome? fun l => l.head?).get (by simpa using h) := by
+  simp [head_eq_iff_head?_eq_some, head?_join]
+
+theorem getLast_join {L : List (List α)} (h : ∃ l, l ∈ L ∧ l ≠ []) :
+    (join L).getLast (by simpa using h) =
+      (L.reverse.findSome? fun l => l.getLast?).get (by simpa using h) := by
+  simp [getLast_eq_iff_getLast_eq_some, getLast?_join]
+
 theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none else f a := by
   cases n with
   | zero => simp
@@ -126,7 +172,7 @@ theorem Sublist.findSome?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) :
 
 theorem Sublist.findSome?_eq_none {l₁ l₂ : List α} (h : l₁ <+ l₂) :
     l₂.findSome? f = none → l₁.findSome? f = none := by
-  simp only [List.findSome?_eq_none, Bool.not_eq_true]
+  simp only [List.findSome?_eq_none_iff, Bool.not_eq_true]
   exact fun w x m => w x (Sublist.mem m h)
 
 theorem IsPrefix.findSome?_eq_some {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <+: l₂) :
@@ -776,4 +822,96 @@ theorem indexOf_cons [BEq α] :
   dsimp [indexOf]
   simp [findIdx_cons]
 
+/-! ### lookup -/
+section lookup
+variable [BEq α] [LawfulBEq α]
+
+@[simp] theorem lookup_cons_self  {k : α} : ((k,b) :: es).lookup k = some b := by
+  simp [lookup_cons]
+
+theorem lookup_eq_findSome? (l : List (α × β)) (k : α) :
+    l.lookup k = l.findSome? fun p => if k == p.1 then some p.2 else none := by
+  induction l with
+  | nil => rfl
+  | cons p l ih =>
+    match p with
+    | (k', v) =>
+      simp only [lookup_cons, findSome?_cons]
+      split <;> simp_all
+
+@[simp] theorem lookup_eq_none_iff {l : List (α × β)} {k : α} :
+    l.lookup k = none ↔ ∀ p ∈ l, k != p.1 := by
+  simp [lookup_eq_findSome?]
+
+@[simp] theorem lookup_isSome_iff {l : List (α × β)} {k : α} :
+    (l.lookup k).isSome ↔ ∃ p ∈ l, k == p.1 := by
+  simp [lookup_eq_findSome?]
+
+theorem lookup_eq_some_iff {l : List (α × β)} {k : α} {b : β} :
+    l.lookup k = some b ↔ ∃ l₁ l₂, l = l₁ ++ (k, b) :: l₂ ∧ ∀ p ∈ l₁, k != p.1 := by
+  simp only [lookup_eq_findSome?, findSome?_eq_some_iff]
+  constructor
+  · rintro ⟨l₁, a, l₂, rfl, h₁, h₂⟩
+    simp only [beq_iff_eq, ite_some_none_eq_some] at h₁
+    obtain ⟨rfl, rfl⟩ := h₁
+    simp at h₂
+    exact ⟨l₁, l₂, rfl, by simpa using h₂⟩
+  · rintro ⟨l₁, l₂, rfl, h⟩
+    exact ⟨l₁, (k, b), l₂, rfl, by simp, by simpa using h⟩
+
+theorem lookup_append {l₁ l₂ : List (α × β)} {k : α} :
+    (l₁ ++ l₂).lookup k = (l₁.lookup k).or (l₂.lookup k) := by
+  simp [lookup_eq_findSome?, findSome?_append]
+
+theorem lookup_replicate {k : α} :
+    (replicate n (a,b)).lookup k = if n = 0 then none else if k == a then some b else none := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    simp only [replicate_succ, lookup_cons]
+    split <;> simp_all
+
+theorem lookup_replicate_of_pos {k : α} (h : 0 < n) :
+    (replicate n (a, b)).lookup k = if k == a then some b else none := by
+  simp [lookup_replicate, Nat.ne_of_gt h]
+
+theorem lookup_replicate_self {a : α} :
+    (replicate n (a, b)).lookup a = if n = 0 then none else some b := by
+  simp [lookup_replicate]
+
+@[simp] theorem lookup_replicate_self_of_pos {a : α} (h : 0 < n) :
+    (replicate n (a, b)).lookup a = some b := by
+  simp [lookup_replicate_self, Nat.ne_of_gt h]
+
+@[simp] theorem lookup_replicate_ne {k : α} (h : !k == a) :
+    (replicate n (a, b)).lookup k = none := by
+  simp_all [lookup_replicate]
+
+theorem Sublist.lookup_isSome {l₁ l₂ : List (α × β)} (h : l₁ <+ l₂) :
+    (l₁.lookup k).isSome → (l₂.lookup k).isSome := by
+  simp only [lookup_eq_findSome?]
+  exact h.findSome?_isSome
+
+theorem Sublist.lookup_eq_none {l₁ l₂ : List (α × β)} (h : l₁ <+ l₂) :
+    l₂.lookup k = none → l₁.lookup k = none := by
+  simp only [lookup_eq_findSome?]
+  exact h.findSome?_eq_none
+
+theorem IsPrefix.lookup_eq_some {l₁ l₂ : List (α × β)} (h : l₁ <+: l₂) :
+    List.lookup k l₁ = some b → List.lookup k l₂ = some b := by
+  simp only [lookup_eq_findSome?]
+  exact h.findSome?_eq_some
+
+theorem IsPrefix.lookup_eq_none {l₁ l₂ : List (α × β)} (h : l₁ <+: l₂) :
+    List.lookup k l₂ = none → List.lookup k l₁ = none :=
+  h.sublist.lookup_eq_none
+theorem IsSuffix.lookup_eq_none {l₁ l₂ : List (α × β)} (h : l₁ <:+ l₂) :
+    List.lookup k l₂ = none → List.lookup k l₁ = none :=
+  h.sublist.lookup_eq_none
+theorem IsInfix.lookup_eq_none {l₁ l₂ : List (α × β)} (h : l₁ <:+: l₂) :
+    List.lookup k l₂ = none → List.lookup k l₁ = none :=
+  h.sublist.lookup_eq_none
+
+end lookup
+
 end List
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index d771da16f6..6500c77c64 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -939,8 +939,8 @@ theorem getLast_eq_iff_getLast?_eq_some {xs : List α} (h) :
   rw [getLast?_eq_getLast _ h]
   simp
 
--- `getLast?_eq_none_iff`, `getLast?_eq_some_iff`, and `getLast_mem` are proved later
--- once more `reverse` theorems are available.
+-- `getLast?_eq_none_iff`, `getLast?_eq_some_iff`, `getLast?_isSome`, and `getLast_mem`
+-- are proved later once more `reverse` theorems are available.
 
 theorem getLast?_cons {a : α} : (a::l).getLast? = l.getLast?.getD a := by
   cases l <;> simp [getLast?, getLast]
@@ -986,6 +986,9 @@ theorem head_eq_iff_head?_eq_some {xs : List α} (h) : xs.head h = a ↔ xs.head
 theorem head?_eq_some_iff {xs : List α} {a : α} : xs.head? = some a ↔ ∃ ys, xs = a :: ys := by
   cases xs <;> simp_all
 
+@[simp] theorem head?_isSome : l.head?.isSome ↔ l ≠ [] := by
+  cases l <;> simp
+
 @[simp] theorem head_mem : ∀ {l : List α} (h : l ≠ []), head l h ∈ l
   | [], h => absurd rfl h
   | _::_, _ => .head ..
@@ -1151,6 +1154,10 @@ theorem map_eq_foldr (f : α → β) (l : List α) : map f l = foldr (fun a bs =
 @[simp] theorem tail?_map (f : α → β) (l : List α) : tail? (map f l) = (tail? l).map (map f) := by
   cases l <;> rfl
 
+@[simp] theorem tail_map (f : α → β) (l : List α) :
+    (map f l).tail = map f l.tail := by
+  cases l <;> simp_all
+
 theorem headD_map (f : α → β) (l : List α) (a : α) : headD (map f l) (f a) = f (headD l a) := by
   cases l <;> rfl
 
@@ -1643,9 +1650,27 @@ theorem head_append_right {l₁ l₂ : List α} (w : l₁ ++ l₂ ≠ []) (h : l
 -- `getLast_append_of_ne_nil`, `getLast_append` and `getLast?_append`
 -- are stated and proved later in the `reverse` section.
 
-theorem nil_eq_append : [] = a ++ b ↔ a = [] ∧ b = [] := by
+theorem tail?_append {l l' : List α} : (l ++ l').tail? = (l.tail?.map (· ++ l')).or l'.tail? := by
+  cases l <;> simp
+
+theorem tail?_append_of_ne_nil {l l' : List α} (_ : l ≠ []) : (l ++ l').tail? = some (l.tail ++ l') :=
+  match l with
+  | _ :: _ => by simp
+
+theorem tail_append {l l' : List α} : (l ++ l').tail = if l.isEmpty then l'.tail else l.tail ++ l' := by
+  cases l <;> simp
+
+@[simp] theorem tail_append_of_ne_nil {xs ys : List α} (h : xs ≠ []) :
+    (xs ++ ys).tail = xs.tail ++ ys := by
+  simp_all [tail_append]
+
+@[deprecated tail_append_of_ne_nil (since := "2024-07-24")] abbrev tail_append_left := @tail_append_of_ne_nil
+
+theorem nil_eq_append_iff : [] = a ++ b ↔ a = [] ∧ b = [] := by
   rw [eq_comm, append_eq_nil]
 
+@[deprecated nil_eq_append_iff (since := "2024-07-24")] abbrev nil_eq_append := @nil_eq_append_iff
+
 theorem append_ne_nil_of_left_ne_nil {s : List α} (h : s ≠ []) (t : List α) : s ++ t ≠ [] := by simp_all
 theorem append_ne_nil_of_right_ne_nil (s : List α) : t ≠ [] → s ++ t ≠ [] := by simp_all
 
@@ -1654,22 +1679,6 @@ theorem append_ne_nil_of_ne_nil_left {s : List α} (h : s ≠ []) (t : List α)
 @[deprecated append_ne_nil_of_right_ne_nil (since := "2024-07-24")]
 theorem append_ne_nil_of_ne_nil_right (s : List α) : t ≠ [] → s ++ t ≠ [] := by simp_all
 
-theorem tail_append (xs ys : List α) :
-    (xs ++ ys).tail = if xs.isEmpty then ys.tail else xs.tail ++ ys := by
-  cases xs <;> simp
-
-theorem tail_append_left {xs ys : List α} (h : xs ≠ []) :
-    (xs ++ ys).tail = xs.tail ++ ys := by
-  simp [tail_append, h]
-
-theorem tail_append_right {xs ys : List α} (h : ys = []) :
-    (xs ++ ys).tail = xs.tail := by
-  simp [tail_append, h]
-
-@[simp] theorem tail_append_of_ne_nil (xs ys : List α) (h : xs ≠ []) :
-    (xs ++ ys).tail = xs.tail ++ ys := by
-  simp_all [tail_append]
-
 theorem append_eq_cons_iff :
     a ++ b = x :: c ↔ (a = [] ∧ b = x :: c) ∨ (∃ a', a = x :: a' ∧ c = a' ++ b) := by
   cases a with simp | cons a as => ?_
@@ -1749,7 +1758,7 @@ theorem filterMap_eq_append_iff {f : α → Option β} :
   constructor
   · induction l generalizing L₁ with
     | nil =>
-      simp only [filterMap_nil, nil_eq_append, and_imp]
+      simp only [filterMap_nil, nil_eq_append_iff, and_imp]
       rintro rfl rfl
       exact ⟨[], [], by simp⟩
     | cons x l ih =>
@@ -1895,7 +1904,8 @@ theorem head?_join {L : List (List α)} : (join L).head? = L.findSome? fun l =>
     simp only [findSome?_cons]
     split <;> simp_all
 
--- `getLast?_join` is proved later, after the `reverse` section
+-- `getLast?_join` is proved later, after the `reverse` section.
+-- `head_join` and `getLast_join` are proved in `Init.Data.List.Find`.
 
 theorem foldl_join (f : β → α → β) (b : β) (L : List (List α)) :
     (join L).foldl f b = L.foldl (fun b l => l.foldl f b) b := by
@@ -2465,6 +2475,10 @@ theorem getLast?_eq_some_iff {xs : List α} {a : α} : xs.getLast? = some a ↔
   simp only [reverse_eq_cons_iff]
   exact ⟨fun ⟨ys, h⟩ => ⟨ys.reverse, by simpa using h⟩, fun ⟨ys, h⟩ => ⟨ys.reverse, by simpa using h⟩⟩
 
+@[simp] theorem getLast?_isSome : l.getLast?.isSome ↔ l ≠ [] := by
+  rw [getLast?_eq_head?_reverse, head?_isSome]
+  simp
+
 theorem mem_of_getLast?_eq_some {xs : List α} {a : α} (h : xs.getLast? = some a) : a ∈ xs := by
   obtain ⟨ys, rfl⟩ := getLast?_eq_some_iff.1 h
   exact mem_concat_self ys a
@@ -2790,6 +2804,14 @@ theorem replace_append [LawfulBEq α] {l₁ l₂ : List α} :
     simp only [cons_append, replace_cons]
     split <;> split <;> simp_all
 
+theorem replace_append_left [LawfulBEq α] {l₁ l₂ : List α} (h : a ∈ l₁) :
+    (l₁ ++ l₂).replace a b = l₁.replace a b ++ l₂ := by
+  simp [replace_append, h]
+
+theorem replace_append_right [LawfulBEq α] {l₁ l₂ : List α} (h : ¬ a ∈ l₁) :
+    (l₁ ++ l₂).replace a b = l₁ ++ l₂.replace a b := by
+  simp [replace_append, h]
+
 theorem replace_take {l : List α} {n : Nat} :
     (l.take n).replace a b = (l.replace a b).take n := by
   induction l generalizing n with
@@ -2868,7 +2890,8 @@ theorem length_insert_pos {l : List α} {a : α} : 0 < (l.insert a).length := by
 theorem insert_eq {l : List α} {a : α} : l.insert a = if a ∈ l then l else a :: l := by
   simp [List.insert]
 
-theorem getElem?_insert_zero (l : List α) (a : α) : (l.insert a)[0]? = if a ∈ l then l[0]? else some a := by
+theorem getElem?_insert_zero (l : List α) (a : α) :
+    (l.insert a)[0]? = if a ∈ l then l[0]? else some a := by
   simp only [insert_eq]
   split <;> simp
 
@@ -2912,6 +2935,14 @@ theorem insert_append {l₁ l₂ : List α} {a : α} :
   simp only [insert_eq, mem_append]
   (repeat split) <;> simp_all
 
+theorem insert_append_of_mem_left {l₁ l₂ : List α} (h : a ∈ l₂) :
+    (l₁ ++ l₂).insert a = l₁ ++ l₂ := by
+  simp [insert_append, h]
+
+theorem insert_append_of_not_mem_left {l₁ l₂ : List α} (h : ¬ a ∈ l₂) :
+    (l₁ ++ l₂).insert a = l₁.insert a ++ l₂ := by
+  simp [insert_append, h]
+
 @[simp] theorem insert_replicate_self {a : α} (h : 0 < n) : (replicate n a).insert a = replicate n a := by
   cases n <;> simp_all
 
@@ -2922,39 +2953,6 @@ theorem insert_append {l₁ l₂ : List α} {a : α} :
 
 end insert
 
-/-! ### lookup -/
-section lookup
-variable [BEq α] [LawfulBEq α]
-
-@[simp] theorem lookup_cons_self  {k : α} : ((k,b)::es).lookup k = some b := by
-  simp [lookup_cons]
-
-theorem lookup_replicate {k : α} :
-    (replicate n (a,b)).lookup k = if n = 0 then none else if k == a then some b else none := by
-  induction n with
-  | zero => simp
-  | succ n ih =>
-    simp only [replicate_succ, lookup_cons]
-    split <;> simp_all
-
-theorem lookup_replicate_of_pos {k : α} (h : 0 < n) :
-    (replicate n (a, b)).lookup k = if k == a then some b else none := by
-  simp [lookup_replicate, Nat.ne_of_gt h]
-
-theorem lookup_replicate_self {a : α} :
-    (replicate n (a, b)).lookup a = if n = 0 then none else some b := by
-  simp [lookup_replicate]
-
-@[simp] theorem lookup_replicate_self_of_pos {a : α} (h : 0 < n) :
-    (replicate n (a, b)).lookup a = some b := by
-  simp [lookup_replicate_self, Nat.ne_of_gt h]
-
-@[simp] theorem lookup_replicate_ne {k : α} (h : !k == a) :
-    (replicate n (a, b)).lookup k = none := by
-  simp_all [lookup_replicate]
-
-end lookup
-
 /-! ## Logic -/
 
 /-! ### any / all -/
diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean
index 468b179333..eee93f1d99 100644
--- a/src/Init/Data/List/TakeDrop.lean
+++ b/src/Init/Data/List/TakeDrop.lean
@@ -436,6 +436,18 @@ theorem take_takeWhile {l : List α} (p : α → Bool) n :
   | nil => rfl
   | cons h t ih => by_cases p h <;> simp_all
 
+theorem replace_takeWhile [BEq α] [LawfulBEq α] {l : List α} {p : α → Bool} (h : p a = p b) :
+    (l.takeWhile p).replace a b = (l.replace a b).takeWhile p := by
+  induction l with
+  | nil => rfl
+  | cons x xs ih =>
+    simp only [takeWhile_cons, replace_cons]
+    split <;> rename_i h₁ <;> split <;> rename_i h₂
+    · simp_all
+    · simp [replace_cons, h₂, takeWhile_cons, h₁, ih]
+    · simp_all
+    · simp_all
+
 /-! ### splitAt -/
 
 @[simp] theorem splitAt_eq (n : Nat) (l : List α) : splitAt n l = (l.take n, l.drop n) := by