diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 4f7d576094..403d0e0bae 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -3742,6 +3742,56 @@ theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     xs.contains a ↔ a ∈ xs := by
   simp
 
+@[simp, grind]
+theorem contains_toList [BEq α] {xs : Array α} {x : α} :
+    xs.toList.contains x = xs.contains x := by
+  rcases xs with ⟨xs⟩
+  simp
+
+@[simp, grind]
+theorem contains_map [BEq β] {xs : Array α} {x : β} {f : α → β} :
+    (xs.map f).contains x = xs.any (fun a => x == f a) := by
+  rcases xs with ⟨xs⟩
+  simp
+
+@[simp, grind]
+theorem contains_filter [BEq α] {xs : Array α} {x : α} {p : α → Bool} :
+    (xs.filter p).contains x = xs.any (fun a => x == a && p a) := by
+  rcases xs with ⟨xs⟩
+  simp
+
+@[simp, grind]
+theorem contains_filterMap [BEq β] {xs : Array α} {x : β} {f : α → Option β} :
+    (xs.filterMap f).contains x = xs.any (fun a => (f a).any fun b => x == b) := by
+  rcases xs with ⟨xs⟩
+  simp
+
+@[simp, grind _=_]
+theorem contains_append [BEq α] {xs ys : Array α} {x : α} :
+    (xs ++ ys).contains x = (xs.contains x || ys.contains x) := by
+  rcases xs with ⟨xs⟩
+  rcases ys with ⟨ys⟩
+  simp
+
+@[simp, grind]
+theorem contains_flatten [BEq α] {xs : Array (Array α)} {x : α} :
+    (xs.flatten).contains x = xs.any fun xs => xs.contains x := by
+  rcases xs with ⟨xs⟩
+  simp [Function.comp_def]
+
+@[simp, grind]
+theorem contains_reverse [BEq α] {xs : Array α} {x : α} :
+    (xs.reverse).contains x = xs.contains x := by
+  rcases xs with ⟨xs⟩
+  simp
+
+@[simp, grind]
+theorem contains_flatMap [BEq β] {xs : Array α} {f : α → Array β} {x : β} :
+    (xs.flatMap f).contains x = xs.any fun a => (f a).contains x := by
+  rcases xs with ⟨xs⟩
+  simp
+
+
 /-! ### more lemmas about `pop` -/
 
 theorem pop_append {xs ys : Array α} :
@@ -3754,193 +3804,6 @@ theorem pop_append {xs ys : Array α} :
 @[deprecated pop_replicate (since := "2025-03-18")]
 abbrev pop_mkArray := @pop_replicate
 
-/-! ### modify -/
-
-@[simp] theorem size_modify {xs : Array α} {i : Nat} {f : α → α} : (xs.modify i f).size = xs.size := by
-  unfold modify modifyM Id.run
-  split <;> simp
-
-theorem getElem_modify {xs : Array α} {j i} (h : i < (xs.modify j f).size) :
-    (xs.modify j f)[i] = if j = i then f (xs[i]'(by simpa using h)) else xs[i]'(by simpa using h) := by
-  simp only [modify, modifyM, Id.run, Id.pure_eq]
-  split
-  · simp only [Id.bind_eq, getElem_set]; split <;> simp [*]
-  · rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
-
-@[simp] theorem toList_modify {xs : Array α} {f : α → α} {i : Nat} :
-    (xs.modify i f).toList = xs.toList.modify i f := by
-  apply List.ext_getElem
-  · simp
-  · simp [getElem_modify, List.getElem_modify]
-
-theorem getElem_modify_self {xs : Array α} {i : Nat} (f : α → α) (h : i < (xs.modify i f).size) :
-    (xs.modify i f)[i] = f (xs[i]'(by simpa using h)) := by
-  simp [getElem_modify h]
-
-theorem getElem_modify_of_ne {xs : Array α} {i : Nat} (h : i ≠ j)
-    (f : α → α) (hj : j < (xs.modify i f).size) :
-    (xs.modify i f)[j] = xs[j]'(by simpa using hj) := by
-  simp [getElem_modify hj, h]
-
-theorem getElem?_modify {xs : Array α} {i : Nat} {f : α → α} {j : Nat} :
-    (xs.modify i f)[j]? = if i = j then xs[j]?.map f else xs[j]? := by
-  simp only [getElem?_def, size_modify, getElem_modify, Option.map_dif]
-  split <;> split <;> rfl
-
-/-! ### swap -/
-
-@[simp] theorem getElem_swap_right {xs : Array α} {i j : Nat} {hi hj} :
-    (xs.swap i j hi hj)[j]'(by simpa using hj) = xs[i] := by
-  simp [swap_def, getElem_set]
-
-@[simp] theorem getElem_swap_left {xs : Array α} {i j : Nat} {hi hj} :
-    (xs.swap i j hi hj)[i]'(by simpa using hi) = xs[j] := by
-  simp +contextual [swap_def, getElem_set]
-
-@[simp] theorem getElem_swap_of_ne {xs : Array α} {i j : Nat} {hi hj} (hp : k < xs.size)
-    (hi' : k ≠ i) (hj' : k ≠ j) : (xs.swap i j hi hj)[k]'(xs.size_swap .. |>.symm ▸ hp) = xs[k] := by
-  simp [swap_def, getElem_set, hi'.symm, hj'.symm]
-
-theorem getElem_swap' {xs : Array α} {i j : Nat} {hi hj} {k : Nat} (hk : k < xs.size) :
-    (xs.swap i j hi hj)[k]'(by simp_all) = if k = i then xs[j] else if k = j then xs[i] else xs[k] := by
-  split
-  · simp_all only [getElem_swap_left]
-  · split <;> simp_all
-
-theorem getElem_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} (hk : k < (xs.swap i j hi hj).size) :
-    (xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k]'(by simp_all) := by
-  apply getElem_swap'
-
-@[simp] theorem swap_swap {xs : Array α} {i j : Nat} (hi hj) :
-    (xs.swap i j hi hj).swap i j ((xs.size_swap ..).symm ▸ hi) ((xs.size_swap ..).symm ▸ hj) = xs := by
-  apply ext
-  · simp only [size_swap]
-  · intros
-    simp only [getElem_swap]
-    split
-    · simp_all
-    · split <;> simp_all
-
-theorem swap_comm {xs : Array α} {i j : Nat} (hi hj) : xs.swap i j hi hj = xs.swap j i hj hi := by
-  apply ext
-  · simp only [size_swap]
-  · intros
-    simp only [getElem_swap]
-    split
-    · split <;> simp_all
-    · split <;> simp_all
-
-@[simp] theorem size_swapIfInBounds {xs : Array α} {i j : Nat} :
-    (xs.swapIfInBounds i j).size = xs.size := by unfold swapIfInBounds; split <;> (try split) <;> simp [size_swap]
-
-@[deprecated size_swapIfInBounds (since := "2024-11-24")] abbrev size_swap! := @size_swapIfInBounds
-
-/-! ### swapAt -/
-
-@[simp] theorem swapAt_def {xs : Array α} {i : Nat} {v : α} (hi) :
-    xs.swapAt i v hi = (xs[i], xs.set i v) := rfl
-
-theorem size_swapAt {xs : Array α} {i : Nat} {v : α} (hi) :
-    (xs.swapAt i v hi).2.size = xs.size := by simp
-
-@[simp]
-theorem swapAt!_def {xs : Array α} {i : Nat} {v : α} (h : i < xs.size) :
-    xs.swapAt! i v = (xs[i], xs.set i v) := by simp [swapAt!, h]
-
-@[simp] theorem size_swapAt! {xs : Array α} {i : Nat} {v : α} :
-    (xs.swapAt! i v).2.size = xs.size := by
-  simp only [swapAt!]
-  split
-  · simp
-  · rfl
-
-/-! ### replace -/
-
-section replace
-variable [BEq α]
-
-@[simp, grind] theorem replace_empty : (#[] : Array α).replace a b = #[] := by rfl
-
-@[simp, grind] theorem replace_singleton {a b c : α} : #[a].replace b c = #[if a == b then c else a] := by
-  simp only [replace, List.finIdxOf?_toArray, List.finIdxOf?]
-  by_cases h : a == b <;> simp [h]
-
-@[simp, grind] theorem size_replace {xs : Array α} : (xs.replace a b).size = xs.size := by
-  simp only [replace]
-  split <;> simp
-
--- This hypothesis could probably be dropped from some of the lemmas below,
--- by proving them direct from the definition rather than going via `List`.
-variable [LawfulBEq α]
-
-@[simp] theorem replace_of_not_mem {xs : Array α} (h : ¬ a ∈ xs) : xs.replace a b = xs := by
-  cases xs
-  simp_all
-
-@[grind] theorem getElem?_replace {xs : Array α} {i : Nat} :
-    (xs.replace a b)[i]? = if xs[i]? == some a then if a ∈ xs.take i then some a else some b else xs[i]? := by
-  rcases xs with ⟨xs⟩
-  simp only [List.replace_toArray, List.getElem?_toArray, List.getElem?_replace, take_eq_extract,
-    List.extract_toArray, List.extract_eq_drop_take, Nat.sub_zero, List.drop_zero, mem_toArray]
-
-theorem getElem?_replace_of_ne {xs : Array α} {i : Nat} (h : xs[i]? ≠ some a) :
-    (xs.replace a b)[i]? = xs[i]? := by
-  simp_all [getElem?_replace]
-
-@[grind] theorem getElem_replace {xs : Array α} {i : Nat} (h : i < xs.size) :
-    (xs.replace a b)[i]'(by simpa) = if xs[i] == a then if a ∈ xs.take i then a else b else xs[i] := by
-  apply Option.some.inj
-  rw [← getElem?_eq_getElem, getElem?_replace]
-  split <;> split <;> simp_all
-
-theorem getElem_replace_of_ne {xs : Array α} {i : Nat} {h : i < xs.size} (h' : xs[i] ≠ a) :
-    (xs.replace a b)[i]'(by simpa) = xs[i]'(h) := by
-  rw [getElem_replace h]
-  simp [h']
-
-@[grind] theorem replace_append {xs ys : Array α} :
-    (xs ++ ys).replace a b = if a ∈ xs then xs.replace a b ++ ys else xs ++ ys.replace a b := by
-  rcases xs with ⟨xs⟩
-  rcases ys with ⟨ys⟩
-  simp only [List.append_toArray, List.replace_toArray, List.replace_append, mem_toArray]
-  split <;> simp
-
-@[grind] theorem replace_push {xs : Array α} {a b c : α} :
-    (xs.push a).replace b c = if b ∈ xs then (xs.replace b c).push a else xs.push (if b == a then c else a) := by
-  rcases xs with ⟨xs⟩
-  simp [List.replace_append]
-  split <;> simp
-
-theorem replace_append_left {xs ys : Array α} (h : a ∈ xs) :
-    (xs ++ ys).replace a b = xs.replace a b ++ ys := by
-  simp [replace_append, h]
-
-theorem replace_append_right {xs ys : Array α} (h : ¬ a ∈ xs) :
-    (xs ++ ys).replace a b = xs ++ ys.replace a b := by
-  simp [replace_append, h]
-
-theorem replace_extract {xs : Array α} {i : Nat} :
-    (xs.extract 0 i).replace a b = (xs.replace a b).extract 0 i := by
-  rcases xs with ⟨xs⟩
-  simp [List.replace_take]
-
-@[simp] theorem replace_replicate_self {a : α} (h : 0 < n) :
-    (replicate n a).replace a b = #[b] ++ replicate (n - 1) a := by
-  cases n <;> simp_all [replicate_succ', replace_append]
-
-@[deprecated replace_replicate_self (since := "2025-03-18")]
-abbrev replace_mkArray_self := @replace_replicate_self
-
-@[simp] theorem replace_replicate_ne {a b c : α} (h : !b == a) :
-    (replicate n a).replace b c = replicate n a := by
-  rw [replace_of_not_mem]
-  simp_all
-
-@[deprecated replace_replicate_ne (since := "2025-03-18")]
-abbrev replace_mkArray_ne := @replace_replicate_ne
-
-end replace
-
 /-! ## Logic -/
 
 /-! ### any / all -/
@@ -4180,6 +4043,193 @@ abbrev any_mkArray := @any_replicate
 @[deprecated all_replicate (since := "2025-03-18")]
 abbrev all_mkArray := @all_replicate
 
+/-! ### modify -/
+
+@[simp] theorem size_modify {xs : Array α} {i : Nat} {f : α → α} : (xs.modify i f).size = xs.size := by
+  unfold modify modifyM Id.run
+  split <;> simp
+
+theorem getElem_modify {xs : Array α} {j i} (h : i < (xs.modify j f).size) :
+    (xs.modify j f)[i] = if j = i then f (xs[i]'(by simpa using h)) else xs[i]'(by simpa using h) := by
+  simp only [modify, modifyM, Id.run, Id.pure_eq]
+  split
+  · simp only [Id.bind_eq, getElem_set]; split <;> simp [*]
+  · rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
+
+@[simp] theorem toList_modify {xs : Array α} {f : α → α} {i : Nat} :
+    (xs.modify i f).toList = xs.toList.modify i f := by
+  apply List.ext_getElem
+  · simp
+  · simp [getElem_modify, List.getElem_modify]
+
+theorem getElem_modify_self {xs : Array α} {i : Nat} (f : α → α) (h : i < (xs.modify i f).size) :
+    (xs.modify i f)[i] = f (xs[i]'(by simpa using h)) := by
+  simp [getElem_modify h]
+
+theorem getElem_modify_of_ne {xs : Array α} {i : Nat} (h : i ≠ j)
+    (f : α → α) (hj : j < (xs.modify i f).size) :
+    (xs.modify i f)[j] = xs[j]'(by simpa using hj) := by
+  simp [getElem_modify hj, h]
+
+theorem getElem?_modify {xs : Array α} {i : Nat} {f : α → α} {j : Nat} :
+    (xs.modify i f)[j]? = if i = j then xs[j]?.map f else xs[j]? := by
+  simp only [getElem?_def, size_modify, getElem_modify, Option.map_dif]
+  split <;> split <;> rfl
+
+/-! ### swap -/
+
+@[simp] theorem getElem_swap_right {xs : Array α} {i j : Nat} {hi hj} :
+    (xs.swap i j hi hj)[j]'(by simpa using hj) = xs[i] := by
+  simp [swap_def, getElem_set]
+
+@[simp] theorem getElem_swap_left {xs : Array α} {i j : Nat} {hi hj} :
+    (xs.swap i j hi hj)[i]'(by simpa using hi) = xs[j] := by
+  simp +contextual [swap_def, getElem_set]
+
+@[simp] theorem getElem_swap_of_ne {xs : Array α} {i j : Nat} {hi hj} (hp : k < xs.size)
+    (hi' : k ≠ i) (hj' : k ≠ j) : (xs.swap i j hi hj)[k]'(xs.size_swap .. |>.symm ▸ hp) = xs[k] := by
+  simp [swap_def, getElem_set, hi'.symm, hj'.symm]
+
+theorem getElem_swap' {xs : Array α} {i j : Nat} {hi hj} {k : Nat} (hk : k < xs.size) :
+    (xs.swap i j hi hj)[k]'(by simp_all) = if k = i then xs[j] else if k = j then xs[i] else xs[k] := by
+  split
+  · simp_all only [getElem_swap_left]
+  · split <;> simp_all
+
+theorem getElem_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} (hk : k < (xs.swap i j hi hj).size) :
+    (xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k]'(by simp_all) := by
+  apply getElem_swap'
+
+@[simp] theorem swap_swap {xs : Array α} {i j : Nat} (hi hj) :
+    (xs.swap i j hi hj).swap i j ((xs.size_swap ..).symm ▸ hi) ((xs.size_swap ..).symm ▸ hj) = xs := by
+  apply ext
+  · simp only [size_swap]
+  · intros
+    simp only [getElem_swap]
+    split
+    · simp_all
+    · split <;> simp_all
+
+theorem swap_comm {xs : Array α} {i j : Nat} (hi hj) : xs.swap i j hi hj = xs.swap j i hj hi := by
+  apply ext
+  · simp only [size_swap]
+  · intros
+    simp only [getElem_swap]
+    split
+    · split <;> simp_all
+    · split <;> simp_all
+
+@[simp] theorem size_swapIfInBounds {xs : Array α} {i j : Nat} :
+    (xs.swapIfInBounds i j).size = xs.size := by unfold swapIfInBounds; split <;> (try split) <;> simp [size_swap]
+
+@[deprecated size_swapIfInBounds (since := "2024-11-24")] abbrev size_swap! := @size_swapIfInBounds
+
+/-! ### swapAt -/
+
+@[simp] theorem swapAt_def {xs : Array α} {i : Nat} {v : α} (hi) :
+    xs.swapAt i v hi = (xs[i], xs.set i v) := rfl
+
+theorem size_swapAt {xs : Array α} {i : Nat} {v : α} (hi) :
+    (xs.swapAt i v hi).2.size = xs.size := by simp
+
+@[simp]
+theorem swapAt!_def {xs : Array α} {i : Nat} {v : α} (h : i < xs.size) :
+    xs.swapAt! i v = (xs[i], xs.set i v) := by simp [swapAt!, h]
+
+@[simp] theorem size_swapAt! {xs : Array α} {i : Nat} {v : α} :
+    (xs.swapAt! i v).2.size = xs.size := by
+  simp only [swapAt!]
+  split
+  · simp
+  · rfl
+
+/-! ### replace -/
+
+section replace
+variable [BEq α]
+
+@[simp, grind] theorem replace_empty : (#[] : Array α).replace a b = #[] := by rfl
+
+@[simp, grind] theorem replace_singleton {a b c : α} : #[a].replace b c = #[if a == b then c else a] := by
+  simp only [replace, List.finIdxOf?_toArray, List.finIdxOf?]
+  by_cases h : a == b <;> simp [h]
+
+@[simp, grind] theorem size_replace {xs : Array α} : (xs.replace a b).size = xs.size := by
+  simp only [replace]
+  split <;> simp
+
+-- This hypothesis could probably be dropped from some of the lemmas below,
+-- by proving them direct from the definition rather than going via `List`.
+variable [LawfulBEq α]
+
+@[simp] theorem replace_of_not_mem {xs : Array α} (h : ¬ a ∈ xs) : xs.replace a b = xs := by
+  cases xs
+  simp_all
+
+@[grind] theorem getElem?_replace {xs : Array α} {i : Nat} :
+    (xs.replace a b)[i]? = if xs[i]? == some a then if a ∈ xs.take i then some a else some b else xs[i]? := by
+  rcases xs with ⟨xs⟩
+  simp only [List.replace_toArray, List.getElem?_toArray, List.getElem?_replace, take_eq_extract,
+    List.extract_toArray, List.extract_eq_drop_take, Nat.sub_zero, List.drop_zero, mem_toArray]
+
+theorem getElem?_replace_of_ne {xs : Array α} {i : Nat} (h : xs[i]? ≠ some a) :
+    (xs.replace a b)[i]? = xs[i]? := by
+  simp_all [getElem?_replace]
+
+@[grind] theorem getElem_replace {xs : Array α} {i : Nat} (h : i < xs.size) :
+    (xs.replace a b)[i]'(by simpa) = if xs[i] == a then if a ∈ xs.take i then a else b else xs[i] := by
+  apply Option.some.inj
+  rw [← getElem?_eq_getElem, getElem?_replace]
+  split <;> split <;> simp_all
+
+theorem getElem_replace_of_ne {xs : Array α} {i : Nat} {h : i < xs.size} (h' : xs[i] ≠ a) :
+    (xs.replace a b)[i]'(by simpa) = xs[i]'(h) := by
+  rw [getElem_replace h]
+  simp [h']
+
+@[grind] theorem replace_append {xs ys : Array α} :
+    (xs ++ ys).replace a b = if a ∈ xs then xs.replace a b ++ ys else xs ++ ys.replace a b := by
+  rcases xs with ⟨xs⟩
+  rcases ys with ⟨ys⟩
+  simp only [List.append_toArray, List.replace_toArray, List.replace_append, mem_toArray]
+  split <;> simp
+
+@[grind] theorem replace_push {xs : Array α} {a b c : α} :
+    (xs.push a).replace b c = if b ∈ xs then (xs.replace b c).push a else xs.push (if b == a then c else a) := by
+  rcases xs with ⟨xs⟩
+  simp [List.replace_append]
+  split <;> simp
+
+theorem replace_append_left {xs ys : Array α} (h : a ∈ xs) :
+    (xs ++ ys).replace a b = xs.replace a b ++ ys := by
+  simp [replace_append, h]
+
+theorem replace_append_right {xs ys : Array α} (h : ¬ a ∈ xs) :
+    (xs ++ ys).replace a b = xs ++ ys.replace a b := by
+  simp [replace_append, h]
+
+theorem replace_extract {xs : Array α} {i : Nat} :
+    (xs.extract 0 i).replace a b = (xs.replace a b).extract 0 i := by
+  rcases xs with ⟨xs⟩
+  simp [List.replace_take]
+
+@[simp] theorem replace_replicate_self {a : α} (h : 0 < n) :
+    (replicate n a).replace a b = #[b] ++ replicate (n - 1) a := by
+  cases n <;> simp_all [replicate_succ', replace_append]
+
+@[deprecated replace_replicate_self (since := "2025-03-18")]
+abbrev replace_mkArray_self := @replace_replicate_self
+
+@[simp] theorem replace_replicate_ne {a b c : α} (h : !b == a) :
+    (replicate n a).replace b c = replicate n a := by
+  rw [replace_of_not_mem]
+  simp_all
+
+@[deprecated replace_replicate_ne (since := "2025-03-18")]
+abbrev replace_mkArray_ne := @replace_replicate_ne
+
+end replace
+
 /-! ### toListRev -/
 
 /--
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 8a35704e27..919f6cc628 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -1539,7 +1539,7 @@ Examples:
  * `[1, 2, 3].insert 2 = [1, 2, 3]`
 -/
 @[inline] protected def insert [BEq α] (a : α) (l : List α) : List α :=
-  if l.elem a then l else a :: l
+  if l.contains a then l else a :: l
 
 /--
 Inserts an element into a list at the specified index. If the index is greater than the length of
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 1cbbd047d2..b07ae989d8 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -2972,7 +2972,10 @@ theorem leftpad_suffix {n : Nat} {a : α} {l : List α} : l <:+ (leftpad n a l)
 
 /-! ## List membership -/
 
-/-! ### elem / contains -/
+/-! ### contains / elem
+
+Recall that the preferred simp normal form is `contains` rather than `elem`.
+-/
 
 theorem elem_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).elem a = true := by simp
 
@@ -2987,6 +2990,57 @@ theorem contains_iff_mem [BEq α] [LawfulBEq α] {l : List α} {a : α} :
     l.contains a ↔ a ∈ l := by
   simp
 
+@[simp, grind]
+theorem contains_map [BEq β] {l : List α} {x : β} {f : α → β} :
+    (l.map f).contains x = l.any (fun a => x == f a) := by
+  induction l with simp_all
+
+@[simp, grind]
+theorem contains_filter [BEq α] {l : List α} {x : α} {p : α → Bool} :
+    (l.filter p).contains x = l.any (fun a => x == a && p a) := by
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp only [filter_cons, any_cons]
+    split <;> simp_all
+
+@[simp, grind]
+theorem contains_filterMap [BEq β] {l : List α} {x : β} {f : α → Option β} :
+    (l.filterMap f).contains x = l.any (fun a => (f a).any fun b => x == b) := by
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp only [filterMap_cons, any_cons]
+    split <;> simp_all
+
+@[simp, grind _=_]
+theorem contains_append [BEq α] {l₁ l₂ : List α} {x : α} :
+    (l₁ ++ l₂).contains x = (l₁.contains x || l₂.contains x) := by
+  induction l₁ with
+  | nil => simp
+  | cons a l ih => simp [ih, Bool.or_assoc]
+
+@[simp, grind]
+theorem contains_flatten [BEq α] {l : List (List α)} {x : α} :
+    l.flatten.contains x = l.any fun l => l.contains x := by
+  induction l with
+  | nil => simp
+  | cons _ l ih => simp [ih]
+
+@[simp, grind]
+theorem contains_reverse [BEq α] {l : List α} {x : α} :
+    (l.reverse).contains x = l.contains x := by
+  induction l with
+  | nil => simp
+  | cons a l ih => simp [ih, Bool.or_comm]
+
+@[simp, grind]
+theorem contains_flatMap [BEq β] {l : List α} {f : α → List β} {x : β} :
+    (l.flatMap f).contains x = l.any fun a => (f a).contains x := by
+  induction l with
+  | nil => simp
+  | cons a l ih => simp [ih]
+
 /-! ## Sublists -/
 
 /-! ### partition
@@ -3138,6 +3192,137 @@ theorem splitAt_go {i : Nat} {l acc : List α} :
         singleton_append, length_cons]
       simp only [Nat.succ_lt_succ_iff]
 
+/-! ## Logic -/
+
+/-! ### any / all -/
+
+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 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 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 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 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]
+
+@[simp] theorem any_map {l : List α} {p : β → Bool} : (l.map f).any p = l.any (p ∘ f) := by
+  induction l with simp | cons _ _ ih => rw [ih]
+
+@[simp] theorem all_map {l : List α} {p : β → Bool} : (l.map f).all p = l.all (p ∘ f) := by
+  induction l with simp | cons _ _ ih => rw [ih]
+
+@[simp] theorem any_filter {l : List α} {p q : α → Bool} :
+    (filter p l).any q = l.any fun a => p a && q a := by
+  induction l with
+  | nil => rfl
+  | cons h t ih =>
+    simp only [filter_cons]
+    split <;> simp_all
+
+@[simp] theorem all_filter {l : List α} {p q : α → Bool} :
+    (filter p l).all q = l.all fun a => !(p a) || q a := by
+  induction l with
+  | nil => rfl
+  | cons h t ih =>
+    simp only [filter_cons]
+    split <;> simp_all
+
+@[simp] theorem any_filterMap {l : List α} {f : α → Option β} {p : β → Bool} :
+    (filterMap f l).any p = l.any fun a => match f a with | some b => p b | none => false := by
+  induction l with
+  | nil => rfl
+  | cons h t ih =>
+    simp only [filterMap_cons]
+    split <;> simp_all
+
+@[simp] theorem all_filterMap {l : List α} {f : α → Option β} {p : β → Bool} :
+    (filterMap f l).all p = l.all fun a => match f a with | some b => p b | none => true := by
+  induction l with
+  | nil => rfl
+  | cons h t ih =>
+    simp only [filterMap_cons]
+    split <;> simp_all
+
+@[simp, grind _=_] theorem any_append {xs ys : List α} : (xs ++ ys).any f = (xs.any f || ys.any f) := by
+  induction xs with
+  | nil => rfl
+  | cons h t ih => simp_all [Bool.or_assoc]
+
+@[simp, grind _=_] theorem all_append {xs ys : List α} : (xs ++ ys).all f = (xs.all f && ys.all f) := by
+  induction xs with
+  | nil => rfl
+  | cons h t ih => simp_all [Bool.and_assoc]
+
+@[simp, grind] theorem any_flatten {l : List (List α)} : l.flatten.any f = l.any (any · f) := by
+  induction l <;> simp_all
+
+@[deprecated any_flatten (since := "2024-10-14")] abbrev any_join := @any_flatten
+
+@[simp, grind] theorem all_flatten {l : List (List α)} : l.flatten.all f = l.all (all · f) := by
+  induction l <;> simp_all
+
+@[deprecated all_flatten (since := "2024-10-14")] abbrev all_join := @all_flatten
+
+@[simp, grind] theorem any_flatMap {l : List α} {f : α → List β} :
+    (l.flatMap f).any p = l.any fun a => (f a).any p := by
+  induction l <;> simp_all
+
+@[simp, grind] theorem all_flatMap {l : List α} {f : α → List β} :
+    (l.flatMap f).all p = l.all fun a => (f a).all p := by
+  induction l <;> simp_all
+
+@[simp, grind] theorem any_reverse {l : List α} : l.reverse.any f = l.any f := by
+  induction l <;> simp_all [Bool.or_comm]
+
+@[simp, grind] theorem all_reverse {l : List α} : l.reverse.all f = l.all f := by
+  induction l <;> simp_all [Bool.and_comm]
+
+@[simp] theorem any_replicate {n : Nat} {a : α} :
+    (replicate n a).any f = if n = 0 then false else f a := by
+  cases n <;> simp [replicate_succ]
+
+@[simp] theorem all_replicate {n : Nat} {a : α} :
+    (replicate n a).all f = if n = 0 then true else f a := by
+  cases n <;> simp +contextual [replicate_succ]
+
+theorem any_congr {l₁ l₂ : List α} (w : l₁ = l₂) {p q : α → Bool} (h : ∀ a, p a = q a) :
+    l₁.any p = l₂.any q := by
+  subst w
+  induction l₁ with
+  | nil => rfl
+  | cons a l ih => simp [ih, h]
+
+theorem all_congr {l₁ l₂ : List α} (w : l₁ = l₂) {p q : α → Bool} (h : ∀ a, p a = q a) :
+    l₁.all p = l₂.all q := by
+  subst w
+  induction l₁ with
+  | nil => rfl
+  | cons a l ih => simp [ih, h]
+
+theorem contains_congr [BEq α] [PartialEquivBEq α] {l : List α} {x y : α} (h : x == y) :
+    l.contains x = l.contains y := by
+  simp only [contains_eq_any_beq]
+  exact any_congr rfl fun a => BEq.congr_left h
+
 /-! ## Manipulating elements -/
 
 /-! ### replace -/
@@ -3253,6 +3438,15 @@ variable [BEq α]
 
 @[simp, grind] theorem insert_nil (a : α) : [].insert a = [a] := rfl
 
+@[simp, grind] theorem contains_insert [PartialEquivBEq α] {l : List α} {a : α} {x : α} :
+    (l.insert a).contains x = (x == a || l.contains x) := by
+  simp only [List.insert]
+  split <;> rename_i h
+  · simp only [Bool.eq_or_self]
+    intro h'
+    simpa [contains_congr h']
+  · simp
+
 variable [LawfulBEq α]
 
 @[simp] theorem insert_of_mem {l : List α} (h : a ∈ l) : l.insert a = l := by
@@ -3369,128 +3563,16 @@ theorem insert_append_of_not_mem_left {l₁ l₂ : List α} (h : ¬ a ∈ l₂)
   rw [insert_of_not_mem]
   simp_all
 
-end insert
-
-/-! ## Logic -/
-
-/-! ### any / all -/
-
-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 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 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 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 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]
-
-@[simp] theorem any_map {l : List α} {p : β → Bool} : (l.map f).any p = l.any (p ∘ f) := by
-  induction l with simp | cons _ _ ih => rw [ih]
-
-@[simp] theorem all_map {l : List α} {p : β → Bool} : (l.map f).all p = l.all (p ∘ f) := by
-  induction l with simp | cons _ _ ih => rw [ih]
-
-@[simp] theorem any_filter {l : List α} {p q : α → Bool} :
-    (filter p l).any q = l.any fun a => p a && q a := by
-  induction l with
-  | nil => rfl
-  | cons h t ih =>
-    simp only [filter_cons]
-    split <;> simp_all
-
-@[simp] theorem all_filter {l : List α} {p q : α → Bool} :
-    (filter p l).all q = l.all fun a => !(p a) || q a := by
-  induction l with
-  | nil => rfl
-  | cons h t ih =>
-    simp only [filter_cons]
-    split <;> simp_all
-
-@[simp] theorem any_filterMap {l : List α} {f : α → Option β} {p : β → Bool} :
-    (filterMap f l).any p = l.any fun a => match f a with | some b => p b | none => false := by
-  induction l with
-  | nil => rfl
-  | cons h t ih =>
-    simp only [filterMap_cons]
-    split <;> simp_all
-
-@[simp] theorem all_filterMap {l : List α} {f : α → Option β} {p : β → Bool} :
-    (filterMap f l).all p = l.all fun a => match f a with | some b => p b | none => true := by
-  induction l with
-  | nil => rfl
-  | cons h t ih =>
-    simp only [filterMap_cons]
-    split <;> simp_all
-
-@[simp, grind _=_] theorem any_append {xs ys : List α} : (xs ++ ys).any f = (xs.any f || ys.any f) := by
-  induction xs with
-  | nil => rfl
-  | cons h t ih => simp_all [Bool.or_assoc]
-
-@[simp, grind _=_] theorem all_append {xs ys : List α} : (xs ++ ys).all f = (xs.all f && ys.all f) := by
-  induction xs with
-  | nil => rfl
-  | cons h t ih => simp_all [Bool.and_assoc]
-
-@[simp, grind] theorem any_flatten {l : List (List α)} : l.flatten.any f = l.any (any · f) := by
-  induction l <;> simp_all
-
-@[deprecated any_flatten (since := "2024-10-14")] abbrev any_join := @any_flatten
-
-@[simp, grind] theorem all_flatten {l : List (List α)} : l.flatten.all f = l.all (all · f) := by
-  induction l <;> simp_all
-
-@[deprecated all_flatten (since := "2024-10-14")] abbrev all_join := @all_flatten
-
-@[simp, grind] theorem any_flatMap {l : List α} {f : α → List β} :
-    (l.flatMap f).any p = l.any fun a => (f a).any p := by
-  induction l <;> simp_all
-
-@[simp, grind] theorem all_flatMap {l : List α} {f : α → List β} :
-    (l.flatMap f).all p = l.all fun a => (f a).all p := by
-  induction l <;> simp_all
-
-@[simp, grind] theorem any_reverse {l : List α} : l.reverse.any f = l.any f := by
-  induction l <;> simp_all [Bool.or_comm]
-
-@[simp, grind] theorem all_reverse {l : List α} : l.reverse.all f = l.all f := by
-  induction l <;> simp_all [Bool.and_comm]
-
-@[simp] theorem any_replicate {n : Nat} {a : α} :
-    (replicate n a).any f = if n = 0 then false else f a := by
-  cases n <;> simp [replicate_succ]
-
-@[simp] theorem all_replicate {n : Nat} {a : α} :
-    (replicate n a).all f = if n = 0 then true else f a := by
-  cases n <;> simp +contextual [replicate_succ]
-
-@[simp] theorem any_insert [BEq α] [LawfulBEq α] {l : List α} {a : α} :
+@[simp] theorem any_insert {l : List α} {a : α} :
     (l.insert a).any f = (f a || l.any f) := by
   simp [any_eq]
 
-@[simp] theorem all_insert [BEq α] [LawfulBEq α] {l : List α} {a : α} :
+@[simp] theorem all_insert {l : List α} {a : α} :
     (l.insert a).all f = (f a && l.all f) := by
   simp [all_eq]
 
+end insert
+
 /-! ### `removeAll` -/
 
 @[simp] theorem removeAll_nil [BEq α] {xs : List α} : xs.removeAll [] = xs := by
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index 9d555ee4ca..a2df84a360 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -2679,6 +2679,61 @@ theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Vector α n} {a : α} :
     xs.contains a ↔ a ∈ xs := by
   simp
 
+@[simp, grind]
+theorem contains_toList [BEq α] {xs : Vector α n} {x : α} :
+    xs.toList.contains x = xs.contains x := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
+@[simp, grind]
+theorem contains_toArray [BEq α] {xs : Vector α n} {x : α} :
+    xs.toArray.contains x = xs.contains x := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
+@[simp, grind]
+theorem contains_map [BEq β] {xs : Vector α n} {x : β} {f : α → β} :
+    (xs.map f).contains x = xs.any (fun a => x == f a) := by
+  rcases xs with ⟨xs⟩
+  simp
+
+@[simp, grind]
+theorem contains_filter [BEq α] {xs : Vector α n} {x : α} {p : α → Bool} :
+    (xs.filter p).contains x = xs.any (fun a => x == a && p a) := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
+@[simp, grind]
+theorem contains_filterMap [BEq β] {xs : Vector α n} {x : β} {f : α → Option β} :
+    (xs.filterMap f).contains x = xs.any (fun a => (f a).any fun b => x == b) := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
+@[simp, grind _=_]
+theorem contains_append [BEq α] {xs : Vector α n} {ys : Vector α m} {x : α} :
+    (xs ++ ys).contains x = (xs.contains x || ys.contains x) := by
+  rcases xs with ⟨xs, rfl⟩
+  rcases ys with ⟨ys, rfl⟩
+  simp
+
+@[simp, grind]
+theorem contains_flatten [BEq α] {xs : Vector (Vector α n) m} {x : α} :
+    (xs.flatten).contains x = xs.any fun xs => xs.contains x := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Function.comp_def]
+
+@[simp, grind]
+theorem contains_reverse [BEq α] {xs : Vector α n} {x : α} :
+    (xs.reverse).contains x = xs.contains x := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
+@[simp, grind]
+theorem contains_flatMap [BEq β] {xs : Vector α n} {f : α → Vector β m} {x : β} :
+    (xs.flatMap f).contains x = xs.any fun a => (f a).contains x := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
 /-! ### more lemmas about `pop` -/
 
 @[simp] theorem pop_empty : (#v[] : Vector α 0).pop = #v[] := rfl
@@ -2737,93 +2792,6 @@ theorem pop_append {xs : Vector α n} {ys : Vector α m} :
 @[deprecated pop_replicate (since := "2025-03-18")]
 abbrev pop_mkVector := @pop_replicate
 
-/-! ### replace -/
-
-section replace
-variable [BEq α]
-
-@[simp] theorem replace_cast {xs : Vector α n} {a b : α} :
-    (xs.cast h).replace a b = (xs.replace a b).cast (by simp [h]) := by
-  rcases xs with ⟨xs, rfl⟩
-  simp
-
-@[simp, grind] theorem replace_empty : (#v[] : Vector α 0).replace a b = #v[] := by rfl
-
-@[grind] theorem replace_singleton {a b c : α} : #v[a].replace b c = #v[if a == b then c else a] := by
-  simp
-
--- This hypothesis could probably be dropped from some of the lemmas below,
--- by proving them direct from the definition rather than going via `List`.
-variable [LawfulBEq α]
-
-@[simp] theorem replace_of_not_mem {xs : Vector α n} (h : ¬ a ∈ xs) : xs.replace a b = xs := by
-  rcases xs with ⟨xs, rfl⟩
-  simp_all
-
-@[grind] theorem getElem?_replace {xs : Vector α n} {i : Nat} :
-    (xs.replace a b)[i]? = if xs[i]? == some a then if a ∈ xs.take i then some a else some b else xs[i]? := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.getElem?_replace, -beq_iff_eq]
-
-theorem getElem?_replace_of_ne {xs : Vector α n} {i : Nat} (h : xs[i]? ≠ some a) :
-    (xs.replace a b)[i]? = xs[i]? := by
-  simp_all [getElem?_replace]
-
-@[grind] theorem getElem_replace {xs : Vector α n} {i : Nat} (h : i < n) :
-    (xs.replace a b)[i] = if xs[i] == a then if a ∈ xs.take i then a else b else xs[i] := by
-  apply Option.some.inj
-  rw [← getElem?_eq_getElem, getElem?_replace]
-  split <;> split <;> simp_all
-
-theorem getElem_replace_of_ne {xs : Vector α n} {i : Nat} {h : i < n} (h' : xs[i] ≠ a) :
-    (xs.replace a b)[i]'(by simpa) = xs[i]'(h) := by
-  rw [getElem_replace h]
-  simp [h']
-
-@[grind] theorem replace_append {xs : Vector α n} {ys : Vector α m} :
-    (xs ++ ys).replace a b = if a ∈ xs then xs.replace a b ++ ys else xs ++ ys.replace a b := by
-  rcases xs with ⟨xs, rfl⟩
-  rcases ys with ⟨ys, rfl⟩
-  simp only [mk_append_mk, replace_mk, eq_mk, Array.replace_append]
-  split <;> simp_all
-
-theorem replace_append_left {xs : Vector α n} {ys : Vector α m} (h : a ∈ xs) :
-    (xs ++ ys).replace a b = xs.replace a b ++ ys := by
-  simp [replace_append, h]
-
-theorem replace_append_right {xs : Vector α n} {ys : Vector α m} (h : ¬ a ∈ xs) :
-    (xs ++ ys).replace a b = xs ++ ys.replace a b := by
-  simp [replace_append, h]
-
-@[grind] theorem replace_push {xs : Vector α n} {a b c : α} :
-    (xs.push a).replace b c = if b ∈ xs then (xs.replace b c).push a else xs.push (if b == a then c else a) := by
-  rcases xs with ⟨xs, rfl⟩
-  simp only [push_mk, replace_mk, Array.replace_push, mem_mk]
-  split <;> simp
-
-theorem replace_extract {xs : Vector α n} {i : Nat} :
-    (xs.extract 0 i).replace a b = (xs.replace a b).extract 0 i := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.replace_extract]
-
-@[simp] theorem replace_replicate_self {a : α} (h : 0 < n) :
-    (replicate n a).replace a b = (#v[b] ++ replicate (n - 1) a).cast (by omega) := by
-  match n, h with
-  | n + 1, _ => simp_all [replicate_succ', replace_append]
-
-@[deprecated replace_replicate_self (since := "2025-03-18")]
-abbrev replace_mkArray_self := @replace_replicate_self
-
-@[simp] theorem replace_replicate_ne {a b c : α} (h : !b == a) :
-    (replicate n a).replace b c = replicate n a := by
-  rw [replace_of_not_mem]
-  simp_all
-
-@[deprecated replace_replicate_ne (since := "2025-03-18")]
-abbrev replace_mkArray_ne := @replace_replicate_ne
-
-end replace
-
 /-! ## Logic -/
 
 /-! ### any / all -/
@@ -2985,6 +2953,93 @@ abbrev any_mkVector := @any_replicate
 @[deprecated all_replicate (since := "2025-03-18")]
 abbrev all_mkVector := @all_replicate
 
+/-! ### replace -/
+
+section replace
+variable [BEq α]
+
+@[simp] theorem replace_cast {xs : Vector α n} {a b : α} :
+    (xs.cast h).replace a b = (xs.replace a b).cast (by simp [h]) := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
+@[simp, grind] theorem replace_empty : (#v[] : Vector α 0).replace a b = #v[] := by rfl
+
+@[grind] theorem replace_singleton {a b c : α} : #v[a].replace b c = #v[if a == b then c else a] := by
+  simp
+
+-- This hypothesis could probably be dropped from some of the lemmas below,
+-- by proving them direct from the definition rather than going via `List`.
+variable [LawfulBEq α]
+
+@[simp] theorem replace_of_not_mem {xs : Vector α n} (h : ¬ a ∈ xs) : xs.replace a b = xs := by
+  rcases xs with ⟨xs, rfl⟩
+  simp_all
+
+@[grind] theorem getElem?_replace {xs : Vector α n} {i : Nat} :
+    (xs.replace a b)[i]? = if xs[i]? == some a then if a ∈ xs.take i then some a else some b else xs[i]? := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.getElem?_replace, -beq_iff_eq]
+
+theorem getElem?_replace_of_ne {xs : Vector α n} {i : Nat} (h : xs[i]? ≠ some a) :
+    (xs.replace a b)[i]? = xs[i]? := by
+  simp_all [getElem?_replace]
+
+@[grind] theorem getElem_replace {xs : Vector α n} {i : Nat} (h : i < n) :
+    (xs.replace a b)[i] = if xs[i] == a then if a ∈ xs.take i then a else b else xs[i] := by
+  apply Option.some.inj
+  rw [← getElem?_eq_getElem, getElem?_replace]
+  split <;> split <;> simp_all
+
+theorem getElem_replace_of_ne {xs : Vector α n} {i : Nat} {h : i < n} (h' : xs[i] ≠ a) :
+    (xs.replace a b)[i]'(by simpa) = xs[i]'(h) := by
+  rw [getElem_replace h]
+  simp [h']
+
+@[grind] theorem replace_append {xs : Vector α n} {ys : Vector α m} :
+    (xs ++ ys).replace a b = if a ∈ xs then xs.replace a b ++ ys else xs ++ ys.replace a b := by
+  rcases xs with ⟨xs, rfl⟩
+  rcases ys with ⟨ys, rfl⟩
+  simp only [mk_append_mk, replace_mk, eq_mk, Array.replace_append]
+  split <;> simp_all
+
+theorem replace_append_left {xs : Vector α n} {ys : Vector α m} (h : a ∈ xs) :
+    (xs ++ ys).replace a b = xs.replace a b ++ ys := by
+  simp [replace_append, h]
+
+theorem replace_append_right {xs : Vector α n} {ys : Vector α m} (h : ¬ a ∈ xs) :
+    (xs ++ ys).replace a b = xs ++ ys.replace a b := by
+  simp [replace_append, h]
+
+@[grind] theorem replace_push {xs : Vector α n} {a b c : α} :
+    (xs.push a).replace b c = if b ∈ xs then (xs.replace b c).push a else xs.push (if b == a then c else a) := by
+  rcases xs with ⟨xs, rfl⟩
+  simp only [push_mk, replace_mk, Array.replace_push, mem_mk]
+  split <;> simp
+
+theorem replace_extract {xs : Vector α n} {i : Nat} :
+    (xs.extract 0 i).replace a b = (xs.replace a b).extract 0 i := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.replace_extract]
+
+@[simp] theorem replace_replicate_self {a : α} (h : 0 < n) :
+    (replicate n a).replace a b = (#v[b] ++ replicate (n - 1) a).cast (by omega) := by
+  match n, h with
+  | n + 1, _ => simp_all [replicate_succ', replace_append]
+
+@[deprecated replace_replicate_self (since := "2025-03-18")]
+abbrev replace_mkArray_self := @replace_replicate_self
+
+@[simp] theorem replace_replicate_ne {a b c : α} (h : !b == a) :
+    (replicate n a).replace b c = replicate n a := by
+  rw [replace_of_not_mem]
+  simp_all
+
+@[deprecated replace_replicate_ne (since := "2025-03-18")]
+abbrev replace_mkArray_ne := @replace_replicate_ne
+
+end replace
+
 /-! Content below this point has not yet been aligned with `List` and `Array`. -/
 
 set_option linter.indexVariables false in
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index 8f5bb01023..7bc28c2f7d 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -1795,7 +1795,7 @@ theorem size_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) :
     (∀ (a : α), a ∈ m → (l.map Prod.fst).contains a = false) →
       (insertMany m l).size = m.size + l.length := by
-  simp [← contains_iff_mem]
+  simp only [← contains_iff_mem]
   simp_to_raw using Raw₀.Const.size_insertMany_list
 
 theorem size_le_size_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
index b920d49acd..b9bcb0fb50 100644
--- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
@@ -2380,7 +2380,7 @@ theorem get!_insertMany!_list_of_contains_eq_false [TransOrd α] [BEq α] [Lawfu
     (h' : (l.map Prod.fst).contains k = false) :
     get! (insertMany! t l).1 k = get! t k := by
   simpa only [insertMany_eq_insertMany!] using
-    get!_insertMany_list_of_contains_eq_false h (h' := by simpa [insertMany_eq_insertMany!])
+    get!_insertMany_list_of_contains_eq_false h (h' := by simpa [insertMany_eq_insertMany!] using h')
 
 theorem get!_insertMany_list_of_mem [TransOrd α] [Inhabited β] (h : t.WF)
     {l : List (α × β)} {k k' : α} {v : β} : (k_beq : compare k k' = .eq) →
diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean
index 5d46d35fd6..1b2899ebc5 100644
--- a/src/Std/Data/DTreeMap/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Lemmas.lean
@@ -1769,7 +1769,7 @@ theorem ofList_cons {k : α} {v : β k} {tl : List ((a : α) × (β a))} :
 theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
     {l : List ((a : α) × β a)} {k : α} :
     (ofList l cmp).contains k = (l.map Sigma.fst).contains k := by
-  simp [ofList, contains, Impl.ofList]
+  simp only [contains, ofList, Impl.ofList]
   exact Impl.contains_insertMany_empty_list (instOrd := ⟨cmp⟩) (k := k) (l := l)
 
 @[simp]
diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
index 0e1a2b652e..e710580732 100644
--- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
@@ -1776,7 +1776,7 @@ theorem ofList_cons {k : α} {v : β k} {tl : List ((a : α) × (β a))} :
 theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
     {l : List ((a : α) × β a)} {k : α} :
     (ofList l cmp).contains k = (l.map Sigma.fst).contains k := by
-  simp [ofList, contains, Impl.ofList]
+  simp only [contains, ofList, Impl.ofList]
   exact Impl.contains_insertMany_empty_list (instOrd := ⟨cmp⟩) (k := k) (l := l)
 
 @[simp]
diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean
index 1ecfa1597b..7548c70ca6 100644
--- a/src/Std/Data/Internal/List/Associative.lean
+++ b/src/Std/Data/Internal/List/Associative.lean
@@ -3008,7 +3008,7 @@ theorem containsKey_of_containsKey_insertListConst [BEq α] [PartialEquivBEq α]
     (h₂ : (toInsert.map Prod.fst).contains k = false) : containsKey k l := by
   unfold insertListConst at h₁
   apply containsKey_of_containsKey_insertList h₁
-  simpa
+  simpa using h₂
 
 theorem getKey?_insertListConst_of_contains_eq_false [BEq α] [EquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
@@ -3016,7 +3016,7 @@ theorem getKey?_insertListConst_of_contains_eq_false [BEq α] [EquivBEq α]
     getKey? k (insertListConst l toInsert) = getKey? k l := by
   unfold insertListConst
   apply getKey?_insertList_of_contains_eq_false
-  simpa
+  simpa using not_contains
 
 theorem getKey?_insertListConst_of_mem [BEq α] [EquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)}
@@ -3125,7 +3125,7 @@ theorem getValue?_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq
   unfold insertListConst
   rw [getValue?_eq_getEntry?, getValue?_eq_getEntry?, getEntry?_insertList_of_contains_eq_false]
   rw [containsKey_eq_contains_map_fst]
-  simpa
+  simpa using not_contains
 
 theorem getValue?_insertListConst_of_mem [BEq α] [EquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)}