diff --git a/src/Init/Data/Array/Attach.lean b/src/Init/Data/Array/Attach.lean
index 1ad501b248..a1c9b6578d 100644
--- a/src/Init/Data/Array/Attach.lean
+++ b/src/Init/Data/Array/Attach.lean
@@ -70,7 +70,7 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
 @[csimp] private theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
   funext α β p f L h'
   cases L
-  simp only [pmap, pmapImpl, List.attachWith_toArray, List.map_toArray, mk.injEq, List.map_attachWith]
+  simp only [pmap, pmapImpl, List.attachWith_toArray, List.map_toArray, mk.injEq, List.map_attachWith_eq_pmap]
   apply List.pmap_congr_left
   intro a m h₁ h₂
   congr
@@ -318,7 +318,7 @@ See however `foldl_subtype` below.
 theorem foldl_attach (l : Array α) (f : β → α → β) (b : β) :
     l.attach.foldl (fun acc t => f acc t.1) b = l.foldl f b := by
   rcases l with ⟨l⟩
-  simp only [List.attach_toArray, List.attachWith_mem_toArray, List.map_attach, size_toArray,
+  simp only [List.attach_toArray, List.attachWith_mem_toArray, size_toArray,
     List.length_pmap, List.foldl_toArray', mem_toArray, List.foldl_subtype]
   congr
   ext
@@ -337,7 +337,7 @@ See however `foldr_subtype` below.
 theorem foldr_attach (l : Array α) (f : α → β → β) (b : β) :
     l.attach.foldr (fun t acc => f t.1 acc) b = l.foldr f b := by
   rcases l with ⟨l⟩
-  simp only [List.attach_toArray, List.attachWith_mem_toArray, List.map_attach, size_toArray,
+  simp only [List.attach_toArray, List.attachWith_mem_toArray, size_toArray,
     List.length_pmap, List.foldr_toArray', mem_toArray, List.foldr_subtype]
   congr
   ext
@@ -354,7 +354,12 @@ theorem attachWith_map {l : Array α} (f : α → β) {P : β → Prop} {H : ∀
   cases l
   simp [List.attachWith_map]
 
-theorem map_attachWith {l : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
+@[simp] theorem map_attachWith {l : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
+    (f : { x // P x } → β) :
+    (l.attachWith P H).map f = l.attach.map fun ⟨x, h⟩ => f ⟨x, H _ h⟩ := by
+  cases l <;> simp_all
+
+theorem map_attachWith_eq_pmap {l : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
     (f : { x // P x } → β) :
     (l.attachWith P H).map f =
       l.pmap (fun a (h : a ∈ l ∧ P a) => f ⟨a, H _ h.1⟩) (fun a h => ⟨h, H a h⟩) := by
@@ -362,11 +367,14 @@ theorem map_attachWith {l : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈
   ext <;> simp
 
 /-- See also `pmap_eq_map_attach` for writing `pmap` in terms of `map` and `attach`. -/
-theorem map_attach {l : Array α} (f : { x // x ∈ l } → β) :
+theorem map_attach_eq_pmap {l : Array α} (f : { x // x ∈ l } → β) :
     l.attach.map f = l.pmap (fun a h => f ⟨a, h⟩) (fun _ => id) := by
   cases l
   ext <;> simp
 
+@[deprecated map_attach_eq_pmap (since := "2025-02-09")]
+abbrev map_attach := @map_attach_eq_pmap
+
 theorem attach_filterMap {l : Array α} {f : α → Option β} :
     (l.filterMap f).attach = l.attach.filterMap
       fun ⟨x, h⟩ => (f x).pbind (fun b m => some ⟨b, mem_filterMap.mpr ⟨x, h, m⟩⟩) := by
@@ -505,7 +513,7 @@ theorem count_attach [DecidableEq α] (l : Array α) (a : {x // x ∈ l}) :
     l.attach.count a = l.count ↑a := by
   rcases l with ⟨l⟩
   simp only [List.attach_toArray, List.attachWith_mem_toArray, List.count_toArray]
-  rw [List.map_attach, List.count_eq_countP]
+  rw [List.map_attach_eq_pmap, List.count_eq_countP]
   simp only [Subtype.beq_iff]
   rw [List.countP_pmap, List.countP_attach (p := (fun x => x == a.1)), List.count]
 
diff --git a/src/Init/Data/Array/Count.lean b/src/Init/Data/Array/Count.lean
index 7ff5af6394..19405a8626 100644
--- a/src/Init/Data/Array/Count.lean
+++ b/src/Init/Data/Array/Count.lean
@@ -163,7 +163,7 @@ theorem count_le_size (a : α) (l : Array α) : count a l ≤ l.size := countP_l
 theorem count_le_count_push (a b : α) (l : Array α) : count a l ≤ count a (l.push b) := by
   simp [count_push]
 
-@[simp] theorem count_singleton (a b : α) : count a #[b] = if b == a then 1 else 0 := by
+theorem count_singleton (a b : α) : count a #[b] = if b == a then 1 else 0 := by
   simp [count_eq_countP]
 
 @[simp] theorem count_append (a : α) : ∀ l₁ l₂, count a (l₁ ++ l₂) = count a l₁ + count a l₂ :=
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 3e98cf9f34..894e91ccca 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -1350,8 +1350,9 @@ theorem map_filter_eq_foldl (f : α → β) (p : α → Bool) (l : Array α) :
     simp only [List.filter_cons, List.foldr_cons]
     split <;> simp_all
 
-@[simp] theorem filter_append {p : α → Bool} (l₁ l₂ : Array α) :
-    filter p (l₁ ++ l₂) = filter p l₁ ++ filter p l₂ := by
+@[simp] theorem filter_append {p : α → Bool} (l₁ l₂ : Array α) (w : stop = l₁.size + l₂.size) :
+    filter p (l₁ ++ l₂) 0 stop = filter p l₁ ++ filter p l₂ := by
+  subst w
   rcases l₁ with ⟨l₁⟩
   rcases l₂ with ⟨l₂⟩
   simp [List.filter_append]
@@ -1440,12 +1441,18 @@ theorem _root_.List.filterMap_toArray (f : α → Option β) (l : List α) :
   rcases l with ⟨l⟩
   simp [h]
 
-@[simp] theorem filterMap_eq_map (f : α → β) (w : stop = as.size ) :
+@[simp] theorem filterMap_eq_map (f : α → β) (w : stop = as.size) :
     filterMap (some ∘ f) as 0 stop = map f as := by
   subst w
   cases as
   simp
 
+/-- Variant of `filterMap_eq_map` with `some ∘ f` expanded out to a lambda. -/
+@[simp]
+theorem filterMap_eq_map' (f : α → β) (w : stop = as.size) :
+    filterMap (fun x => some (f x)) as 0 stop = map f as :=
+  filterMap_eq_map f w
+
 theorem filterMap_some_fun : filterMap (some : α → Option α) = id := by
   funext l
   cases l
@@ -1514,8 +1521,9 @@ theorem forall_mem_filterMap {f : α → Option β} {l : Array α} {P : β → P
   intro a
   rw [forall_comm]
 
-@[simp] theorem filterMap_append {α β : Type _} (l l' : Array α) (f : α → Option β) :
-    filterMap f (l ++ l') = filterMap f l ++ filterMap f l' := by
+@[simp] theorem filterMap_append {α β : Type _} (l l' : Array α) (f : α → Option β) (w : stop = l.size + l'.size) :
+    filterMap f (l ++ l') 0 stop = filterMap f l ++ filterMap f l' := by
+  subst w
   cases l
   cases l'
   simp
@@ -1557,7 +1565,12 @@ theorem filterMap_eq_push_iff {f : α → Option β} {l : Array α} {l' : Array
 @[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
   simp only [size, toList_append, List.length_append]
 
-@[simp] theorem append_push {as bs : Array α} {a : α} : as ++ bs.push a = (as ++ bs).push a := by
+@[simp] theorem push_append {a : α} {xs ys : Array α} : (xs ++ ys).push a = xs ++ ys.push a := by
+  cases xs
+  cases ys
+  simp
+
+theorem append_push {as bs : Array α} {a : α} : as ++ bs.push a = (as ++ bs).push a := by
   cases as
   cases bs
   simp
@@ -1668,6 +1681,9 @@ theorem getElem_of_append {l l₁ l₂ : Array α} (eq : l = l₁.push a ++ l₂
 
 @[simp] theorem append_singleton {a : α} {as : Array α} : as ++ #[a] = as.push a := rfl
 
+@[simp] theorem append_singleton_assoc {a : α} {as bs : Array α} : as ++ (#[a] ++ bs) = as.push a ++ bs := by
+  rw [← append_assoc, append_singleton]
+
 theorem push_eq_append {a : α} {as : Array α} : as.push a = as ++ #[a] := rfl
 
 theorem append_inj {s₁ s₂ t₁ t₂ : Array α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : s₁.size = s₂.size) :
@@ -1931,15 +1947,17 @@ theorem flatten_eq_flatMap {L : Array (Array α)} : flatten L = L.flatMap id :=
       Function.comp_def]
     rw [← Function.comp_def, ← List.map_map, flatten_toArray_map]
 
-@[simp] theorem filterMap_flatten (f : α → Option β) (L : Array (Array α)) :
-    filterMap f (flatten L) = flatten (map (filterMap f) L) := by
+@[simp] theorem filterMap_flatten (f : α → Option β) (L : Array (Array α)) (w : stop = L.flatten.size) :
+    filterMap f (flatten L) 0 stop = flatten (map (filterMap f) L) := by
+  subst w
   induction L using array₂_induction
   simp only [flatten_toArray_map, size_toArray, List.length_flatten, List.filterMap_toArray',
     List.filterMap_flatten, List.map_toArray, List.map_map, Function.comp_def]
   rw [← Function.comp_def, ← List.map_map, flatten_toArray_map]
 
-@[simp] theorem filter_flatten (p : α → Bool) (L : Array (Array α)) :
-    filter p (flatten L) = flatten (map (filter p) L) := by
+@[simp] theorem filter_flatten (p : α → Bool) (L : Array (Array α)) (w : stop = L.flatten.size) :
+    filter p (flatten L) 0 stop = flatten (map (filter p) L) := by
+  subst w
   induction L using array₂_induction
   simp only [flatten_toArray_map, size_toArray, List.length_flatten, List.filter_toArray',
     List.filter_flatten, List.map_toArray, List.map_map, Function.comp_def]
@@ -2397,11 +2415,25 @@ theorem reverse_eq_iff {as bs : Array α} : as.reverse = bs ↔ as = bs.reverse
 @[simp] theorem map_reverse (f : α → β) (l : Array α) : l.reverse.map f = (l.map f).reverse := by
   cases l <;> simp [*]
 
-@[simp] theorem filter_reverse (p : α → Bool) (l : Array α) : (l.reverse.filter p) = (l.filter p).reverse := by
+/-- Variant of `filter_reverse` with a hypothesis giving the stop condition. -/
+@[simp] theorem filter_reverse' (p : α → Bool) (l : Array α) (w : stop = l.size) :
+     (l.reverse.filter p 0 stop) = (l.filter p).reverse := by
+  subst w
   cases l
   simp
 
-@[simp] theorem filterMap_reverse (f : α → Option β) (l : Array α) : (l.reverse.filterMap f) = (l.filterMap f).reverse := by
+theorem filter_reverse (p : α → Bool) (l : Array α) : (l.reverse.filter p) = (l.filter p).reverse := by
+  cases l
+  simp
+
+/-- Variant of `filterMap_reverse` with a hypothesis giving the stop condition. -/
+@[simp] theorem filterMap_reverse' (f : α → Option β) (l : Array α) (w : stop = l.size) :
+    (l.reverse.filterMap f 0 stop) = (l.filterMap f).reverse := by
+  subst w
+  cases l
+  simp
+
+theorem filterMap_reverse (f : α → Option β) (l : Array α) : (l.reverse.filterMap f) = (l.filterMap f).reverse := by
   cases l
   simp
 
@@ -2877,17 +2909,57 @@ rather than `(arr.push a).size` as the argument.
     (h : start = arr.size + 1) : (arr.push a).foldr f init start = arr.foldr f (f a init) :=
   foldrM_push' _ _ _ _ h
 
-@[simp] theorem foldl_push_eq_append (l l' : Array α) : l.foldl push l' = l' ++ l := by
-  cases l
-  cases l'
+@[simp] theorem foldl_push_eq_append {as : Array α} {bs : Array β} {f : α → β} (w : stop = as.size) :
+    as.foldl (fun b a => Array.push b (f a)) bs 0 stop = bs ++ as.map f := by
+  subst w
+  rcases as with ⟨as⟩
+  rcases bs with ⟨bs⟩
+  simp only [List.foldl_toArray']
+  induction as generalizing bs <;> simp [*]
+
+@[simp] theorem foldl_cons_eq_append {as : Array α} {bs : List β} {f : α → β} (w : stop = as.size) :
+    as.foldl (fun b a => (f a) :: b) bs 0 stop = (as.map f).reverse.toList ++ bs := by
+  subst w
+  rcases as with ⟨as⟩
   simp
 
-@[simp] theorem foldr_flip_push_eq_append (l l' : Array α) :
-    l.foldr (fun x y => push y x) l' = l' ++ l.reverse := by
-  cases l
-  cases l'
+@[simp] theorem foldr_cons_eq_append {as : Array α} {bs : List β} {f : α → β} (w : start = as.size) :
+    as.foldr (fun a b => (f a) :: b) bs start 0 = (as.map f).toList ++ bs := by
+  subst w
+  rcases as with ⟨as⟩
   simp
 
+/-- Variant of `foldr_cons_eq_append` specialized to `f = id`. -/
+@[simp] theorem foldr_cons_eq_append' {as : Array α} {bs : List α} (w : start = as.size) :
+    as.foldr List.cons bs start 0 = as.toList ++ bs := by
+  subst w
+  rcases as with ⟨as⟩
+  simp
+
+@[simp] theorem foldr_append_eq_append (l : Array α) (f : α → Array β) (l' : Array β) :
+    l.foldr (f · ++ ·) l' = (l.map f).flatten ++ l' := by
+  rcases l with ⟨l⟩
+  rcases l' with ⟨l'⟩
+  induction l <;> simp_all [Function.comp_def, flatten_toArray]
+
+@[simp] theorem foldl_append_eq_append (l : Array α) (f : α → Array β) (l' : Array β) :
+    l.foldl (· ++ f ·) l' = l' ++ (l.map f).flatten := by
+  rcases l with ⟨l⟩
+  rcases l' with ⟨l'⟩
+  induction l generalizing l'<;> simp_all [Function.comp_def, flatten_toArray]
+
+@[simp] theorem foldr_flip_append_eq_append (l : Array α) (f : α → Array β) (l' : Array β) :
+    l.foldr (fun x y => y ++ f x) l' = l' ++ (l.map f).reverse.flatten := by
+  rcases l with ⟨l⟩
+  rcases l' with ⟨l'⟩
+  induction l generalizing l' <;> simp_all [Function.comp_def, flatten_toArray]
+
+@[simp] theorem foldl_flip_append_eq_append (l : Array α) (f : α → Array β) (l' : Array β) :
+    l.foldl (fun x y => f y ++ x) l' = (l.map f).reverse.flatten ++ l':= by
+  rcases l with ⟨l⟩
+  rcases l' with ⟨l'⟩
+  induction l generalizing l' <;> simp_all [Function.comp_def, flatten_toArray]
+
 theorem foldl_map' (f : β₁ → β₂) (g : α → β₂ → α) (l : Array β₁) (init : α) (w : stop = l.size) :
     (l.map f).foldl g init 0 stop = l.foldl (fun x y => g x (f y)) init := by
   subst w
@@ -3040,6 +3112,13 @@ theorem foldl_eq_foldr_reverse (l : Array α) (f : β → α → β) (b) :
 theorem foldr_eq_foldl_reverse (l : Array α) (f : α → β → β) (b) :
     l.foldr f b = l.reverse.foldl (fun x y => f y x) b := by simp
 
+@[simp] theorem foldr_push_eq_append {as : Array α} {bs : Array β} {f : α → β} (w : start = as.size) :
+    as.foldr (fun a b => Array.push b (f a)) bs start 0 = bs ++ (as.map f).reverse := by
+  subst w
+  rw [foldr_eq_foldl_reverse, foldl_push_eq_append rfl, map_reverse]
+
+@[deprecated foldr_push_eq_append (since := "2025-02-09")] abbrev foldr_flip_push_eq_append := @foldr_push_eq_append
+
 theorem foldl_assoc {op : α → α → α} [ha : Std.Associative op] {l : Array α} {a₁ a₂} :
      l.foldl op (op a₁ a₂) = op a₁ (l.foldl op a₂) := by
   rcases l with ⟨l⟩
@@ -3445,11 +3524,11 @@ theorem map_induction (as : Array α) (f : α → β) (motive : Nat → Prop) (h
     (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, ?_⟩
+  · refine ⟨m, by simp, ?_⟩
     intro i h
     simp only [eq] at w
     specialize w ⟨i, h⟩ h
-    simpa [map_eq_foldl] using w
+    simpa using w
   · exact ⟨h0, rfl, nofun⟩
   · intro i b ⟨m, ⟨eq, w⟩⟩
     refine ⟨?_, ?_, ?_⟩
diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean
index 09aa2224ca..ee0468d4e3 100644
--- a/src/Init/Data/List/Attach.lean
+++ b/src/Init/Data/List/Attach.lean
@@ -416,7 +416,12 @@ theorem attachWith_map {l : List α} (f : α → β) {P : β → Prop} {H : ∀
       fun ⟨x, h⟩ => ⟨f x, h⟩ := by
   induction l <;> simp [*]
 
-theorem map_attachWith {l : List α} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
+@[simp] theorem map_attachWith {l : List α} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
+    (f : { x // P x } → β) :
+    (l.attachWith P H).map f = l.attach.map fun ⟨x, h⟩ => f ⟨x, H _ h⟩ := by
+  induction l <;> simp_all
+
+theorem map_attachWith_eq_pmap {l : List α} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
     (f : { x // P x } → β) :
     (l.attachWith P H).map f =
       l.pmap (fun a (h : a ∈ l ∧ P a) => f ⟨a, H _ h.1⟩) (fun a h => ⟨h, H a h⟩) := by
@@ -428,7 +433,7 @@ theorem map_attachWith {l : List α} {P : α → Prop} {H : ∀ (a : α), a ∈
     simp
 
 /-- See also `pmap_eq_map_attach` for writing `pmap` in terms of `map` and `attach`. -/
-theorem map_attach {l : List α} (f : { x // x ∈ l } → β) :
+theorem map_attach_eq_pmap {l : List α} (f : { x // x ∈ l } → β) :
     l.attach.map f = l.pmap (fun a h => f ⟨a, h⟩) (fun _ => id) := by
   induction l with
   | nil => rfl
@@ -437,6 +442,9 @@ theorem map_attach {l : List α} (f : { x // x ∈ l } → β) :
     apply pmap_congr_left
     simp
 
+@[deprecated map_attach_eq_pmap (since := "2025-02-09")]
+abbrev map_attach := @map_attach_eq_pmap
+
 theorem attach_filterMap {l : List α} {f : α → Option β} :
     (l.filterMap f).attach = l.attach.filterMap
       fun ⟨x, h⟩ => (f x).pbind (fun b m => some ⟨b, mem_filterMap.mpr ⟨x, h, m⟩⟩) := by
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index c6d72a21ab..5d54b6a265 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -225,10 +225,23 @@ def lex [BEq α] (l₁ l₂ : List α) (lt : α → α → Bool := by exact (·
   | _,      []       => false
   | a :: as, b :: bs => lt a b || (a == b && lex as bs lt)
 
-@[simp] theorem lex_nil_nil [BEq α] : lex ([] : List α) [] lt = false := rfl
-@[simp] theorem lex_nil_cons [BEq α] {b} {bs : List α} : lex [] (b :: bs) lt = true := rfl
-@[simp] theorem lex_cons_nil [BEq α] {a} {as : List α} : lex (a :: as) [] lt = false := rfl
-@[simp] theorem lex_cons_cons [BEq α] {a b} {as bs : List α} :
+theorem nil_lex_nil [BEq α] : lex ([] : List α) [] lt = false := rfl
+@[simp] theorem nil_lex_cons [BEq α] {b} {bs : List α} : lex [] (b :: bs) lt = true := rfl
+theorem cons_lex_nil [BEq α] {a} {as : List α} : lex (a :: as) [] lt = false := rfl
+@[simp] theorem cons_lex_cons [BEq α] {a b} {as bs : List α} :
+    lex (a :: as) (b :: bs) lt = (lt a b || (a == b && lex as bs lt)) := rfl
+
+@[simp] theorem lex_nil [BEq α] {as : List α} : lex as [] lt = false := by
+  cases as <;> simp [nil_lex_nil, cons_lex_nil]
+
+@[deprecated nil_lex_nil (since := "2025-02-10")]
+theorem lex_nil_nil [BEq α] : lex ([] : List α) [] lt = false := rfl
+@[deprecated nil_lex_cons (since := "2025-02-10")]
+theorem lex_nil_cons [BEq α] {b} {bs : List α} : lex [] (b :: bs) lt = true := rfl
+@[deprecated cons_lex_nil (since := "2025-02-10")]
+theorem lex_cons_nil [BEq α] {a} {as : List α} : lex (a :: as) [] lt = false := rfl
+@[deprecated cons_lex_cons (since := "2025-02-10")]
+theorem lex_cons_cons [BEq α] {a b} {as bs : List α} :
     lex (a :: as) (b :: bs) lt = (lt a b || (a == b && lex as bs lt)) := rfl
 
 /-! ## Alternative getters -/
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 77ef29b074..a627bb4bb7 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -1344,6 +1344,11 @@ theorem head_filter_of_pos {p : α → Bool} {l : List α} (w : l ≠ []) (h : p
 theorem filterMap_eq_map (f : α → β) : filterMap (some ∘ f) = map f := by
   funext l; induction l <;> simp [*, filterMap_cons]
 
+/-- Variant of `filterMap_eq_map` with `some ∘ f` expanded out to a lambda. -/
+@[simp]
+theorem filterMap_eq_map' (f : α → β) : filterMap (fun x => some (f x)) = map f :=
+  filterMap_eq_map f
+
 @[simp] theorem filterMap_some_fun : filterMap (some : α → Option α) = id := by
   funext l
   erw [filterMap_eq_map]
@@ -2516,12 +2521,35 @@ theorem foldr_eq_foldrM (f : α → β → β) (b) (l : List α) :
 
 /-! ### foldl and foldr -/
 
-@[simp] theorem foldr_cons_eq_append (l : List α) : l.foldr cons l' = l ++ l' := by
+@[simp] theorem foldr_cons_eq_append (l : List α) (f : α → β) (l' : List β) :
+    l.foldr (fun x y => f x :: y) l' = l.map f ++ l' := by
+  induction l <;> simp [*]
+
+/-- Variant of `foldr_cons_eq_append` specalized to `f = id`. -/
+@[simp] theorem foldr_cons_eq_append' (l l' : List β) :
+    l.foldr cons l' = l ++ l' := by
   induction l <;> simp [*]
 
 @[deprecated foldr_cons_eq_append (since := "2024-08-22")] abbrev foldr_self_append := @foldr_cons_eq_append
 
-@[simp] theorem foldl_flip_cons_eq_append (l : List α) : l.foldl (fun x y => y :: x) l' = l.reverse ++ l' := by
+@[simp] theorem foldl_flip_cons_eq_append (l : List α) (f : α → β) (l' : List β) :
+    l.foldl (fun x y => f y :: x) l' = (l.map f).reverse ++ l' := by
+  induction l generalizing l' <;> simp [*]
+
+@[simp] theorem foldr_append_eq_append (l : List α) (f : α → List β) (l' : List β) :
+    l.foldr (f · ++ ·) l' = (l.map f).flatten ++ l' := by
+  induction l <;> simp [*]
+
+@[simp] theorem foldl_append_eq_append (l : List α) (f : α → List β) (l' : List β) :
+    l.foldl (· ++ f ·) l' = l' ++ (l.map f).flatten := by
+  induction l generalizing l'<;> simp [*]
+
+@[simp] theorem foldr_flip_append_eq_append (l : List α) (f : α → List β) (l' : List β) :
+    l.foldr (fun x y => y ++ f x) l' = l' ++ (l.map f).reverse.flatten := by
+  induction l generalizing l' <;> simp [*]
+
+@[simp] theorem foldl_flip_append_eq_append (l : List α) (f : α → List β) (l' : List β) :
+    l.foldl (fun x y => f y ++ x) l' = (l.map f).reverse.flatten ++ l' := by
   induction l generalizing l' <;> simp [*]
 
 theorem foldr_cons_nil (l : List α) : l.foldr cons [] = l := by simp
diff --git a/src/Init/Data/List/Lex.lean b/src/Init/Data/List/Lex.lean
index b6a72e14c9..82988f2c71 100644
--- a/src/Init/Data/List/Lex.lean
+++ b/src/Init/Data/List/Lex.lean
@@ -48,7 +48,9 @@ instance ltIrrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)] : Std.Irre
 
 @[simp] theorem le_nil [LT α] (l : List α) : l ≤ [] ↔ l = [] := not_nil_lex_iff
 
-@[simp] theorem nil_lex_cons : Lex r [] (a :: l) := Lex.nil
+-- This is named with a prime to avoid conflict with `lex [] (b :: bs) lt = true`.
+-- Better naming for the `Lex` vs `lex` distinction would be welcome.
+@[simp] theorem nil_lex_cons' : Lex r [] (a :: l) := Lex.nil
 
 @[simp] theorem nil_lt_cons [LT α] (a : α) (l : List α) : [] < a :: l := Lex.nil
 
@@ -333,7 +335,7 @@ theorem lex_eq_true_iff_exists [BEq α] (lt : α → α → Bool) :
     cases l₂ with
     | nil => simp [lex]
     | cons b l₂ =>
-      simp [lex_cons_cons, Bool.or_eq_true, Bool.and_eq_true, ih, isEqv, length_cons]
+      simp [cons_lex_cons, Bool.or_eq_true, Bool.and_eq_true, ih, isEqv, length_cons]
       constructor
       · rintro (hab | ⟨hab, ⟨h₁, h₂⟩ | ⟨i, h₁, h₂, w₁, w₂⟩⟩)
         · exact .inr ⟨0, by simp [hab]⟩
@@ -397,7 +399,7 @@ theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : α → α 
     cases l₂ with
     | nil => simp [lex]
     | cons b l₂ =>
-      simp [lex_cons_cons, Bool.or_eq_false_iff, Bool.and_eq_false_imp, ih, isEqv,
+      simp [cons_lex_cons, Bool.or_eq_false_iff, Bool.and_eq_false_imp, ih, isEqv,
         Bool.and_eq_true, length_cons]
       constructor
       · rintro ⟨hab, h⟩
diff --git a/src/Init/Data/Option/Attach.lean b/src/Init/Data/Option/Attach.lean
index f89e467d39..2ff1ff4a2e 100644
--- a/src/Init/Data/Option/Attach.lean
+++ b/src/Init/Data/Option/Attach.lean
@@ -134,16 +134,29 @@ theorem attachWith_map {o : Option α} (f : α → β) {P : β → Prop} {H : 
       fun ⟨x, h⟩ => ⟨f x, h⟩ := by
   cases o <;> simp
 
-theorem map_attach {o : Option α} (f : { x // x ∈ o } → β) :
+theorem map_attach_eq_pmap {o : Option α} (f : { x // x ∈ o } → β) :
     o.attach.map f = o.pmap (fun a (h : a ∈ o) => f ⟨a, h⟩) (fun _ h => h) := by
   cases o <;> simp
 
-theorem map_attachWith {o : Option α} {P : α → Prop} {H : ∀ (a : α), a ∈ o → P a}
+@[deprecated map_attach_eq_pmap (since := "2025-02-09")]
+abbrev map_attach := @map_attach_eq_pmap
+
+@[simp] theorem map_attachWith {l : Option α} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
+    (f : { x // P x } → β) :
+    (l.attachWith P H).map f = l.attach.map fun ⟨x, h⟩ => f ⟨x, H _ h⟩ := by
+  cases l <;> simp_all
+
+theorem map_attachWith_eq_pmap {o : Option α} {P : α → Prop} {H : ∀ (a : α), a ∈ o → P a}
     (f : { x // P x } → β) :
     (o.attachWith P H).map f =
       o.pmap (fun a (h : a ∈ o ∧ P a) => f ⟨a, h.2⟩) (fun a h => ⟨h, H a h⟩) := by
   cases o <;> simp
 
+@[simp]
+theorem map_attach_eq_attachWith {o : Option α} {p : α → Prop} (f : ∀ a, a ∈ o → p a) :
+    o.attach.map (fun x => ⟨x.1, f x.1 x.2⟩) = o.attachWith p f := by
+  cases o <;> simp_all [Function.comp_def]
+
 theorem attach_bind {o : Option α} {f : α → Option β} :
     (o.bind f).attach =
       o.attach.bind fun ⟨x, h⟩ => (f x).attach.map fun ⟨y, h'⟩ => ⟨y, mem_bind_iff.mpr ⟨x, h, h'⟩⟩ := by
diff --git a/src/Init/Data/Vector/Attach.lean b/src/Init/Data/Vector/Attach.lean
index 5385069817..c102619381 100644
--- a/src/Init/Data/Vector/Attach.lean
+++ b/src/Init/Data/Vector/Attach.lean
@@ -81,7 +81,7 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
 @[csimp] private theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
   funext α β n p f L h'
   rcases L with ⟨L, rfl⟩
-  simp only [pmap, pmapImpl, attachWith_mk, map_mk, Array.map_attachWith, eq_mk]
+  simp only [pmap, pmapImpl, attachWith_mk, map_mk, Array.map_attachWith_eq_pmap, eq_mk]
   apply Array.pmap_congr_left
   intro a m h₁ h₂
   congr
@@ -133,7 +133,7 @@ theorem attachWith_congr {l₁ l₂ : Vector α n} (w : l₁ = l₂) {P : α →
     (l.push a).attach =
       (l.attach.map (fun ⟨x, h⟩ => ⟨x, mem_push_of_mem a h⟩)).push ⟨a, by simp⟩ := by
   rcases l with ⟨l, rfl⟩
-  simp [Array.map_attachWith]
+  simp [Array.map_attach_eq_pmap]
 
 @[simp] theorem attachWith_push {a : α} {l : Vector α n} {P : α → Prop} {H : ∀ x ∈ l.push a, P x} :
     (l.push a).attachWith P H =
@@ -145,7 +145,7 @@ theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (l : Vector
     pmap f l H = l.attach.map fun x => f x.1 (H _ x.2) := by
   rcases l with ⟨l, rfl⟩
   simp only [pmap_mk, Array.pmap_eq_map_attach, attach_mk, map_mk, eq_mk]
-  rw [Array.map_attach, Array.map_attachWith]
+  rw [Array.map_attach_eq_pmap, Array.map_attachWith]
   ext i hi₁ hi₂ <;> simp
 
 @[simp]
@@ -299,7 +299,13 @@ theorem attachWith_map {l : Vector α n} (f : α → β) {P : β → Prop} {H :
   rcases l with ⟨l, rfl⟩
   simp [Array.attachWith_map]
 
-theorem map_attachWith {l : Vector α n} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
+@[simp] theorem map_attachWith {l : Vector α n} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
+    (f : { x // P x } → β) :
+    (l.attachWith P H).map f = l.attach.map fun ⟨x, h⟩ => f ⟨x, H _ h⟩ := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.map_attachWith]
+
+theorem map_attachWith_eq_pmap {l : Vector α n} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
     (f : { x // P x } → β) :
     (l.attachWith P H).map f =
       l.pmap (fun a (h : a ∈ l ∧ P a) => f ⟨a, H _ h.1⟩) (fun a h => ⟨h, H a h⟩) := by
@@ -307,11 +313,14 @@ theorem map_attachWith {l : Vector α n} {P : α → Prop} {H : ∀ (a : α), a
   ext <;> simp
 
 /-- See also `pmap_eq_map_attach` for writing `pmap` in terms of `map` and `attach`. -/
-theorem map_attach {l : Vector α n} (f : { x // x ∈ l } → β) :
+theorem map_attach_eq_pmap {l : Vector α n} (f : { x // x ∈ l } → β) :
     l.attach.map f = l.pmap (fun a h => f ⟨a, h⟩) (fun _ => id) := by
   cases l
   ext <;> simp
 
+@[deprecated map_attach_eq_pmap (since := "2025-02-09")]
+abbrev map_attach := @map_attach_eq_pmap
+
 theorem pmap_pmap {p : α → Prop} {q : β → Prop} (g : ∀ a, p a → β) (f : ∀ b, q b → γ) (l : Vector α n) (H₁ H₂) :
     pmap f (pmap g l H₁) H₂ =
       pmap (α := { x // x ∈ l }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) l.attach
@@ -339,7 +348,7 @@ theorem pmap_append' {p : α → Prop} (f : ∀ a : α, p a → β) (l₁ : Vect
       ys.attach.map (fun ⟨y, h⟩ => (⟨y, mem_append_right xs h⟩ : { y // y ∈ xs ++ ys })) := by
   rcases xs with ⟨xs, rfl⟩
   rcases ys with ⟨ys, rfl⟩
-  simp [Array.map_attachWith]
+  simp [Array.map_attach_eq_pmap]
 
 @[simp] theorem attachWith_append {P : α → Prop} {xs : Vector α n} {ys : Vector α m}
     {H : ∀ (a : α), a ∈ xs ++ ys → P a} :
@@ -379,7 +388,7 @@ theorem reverse_attachWith {P : α → Prop} {xs : Vector α n}
 theorem reverse_attach (xs : Vector α n) :
     xs.attach.reverse = xs.reverse.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   cases xs
-  simp [Array.map_attachWith]
+  simp [Array.map_attach_eq_pmap]
 
 @[simp] theorem back?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Vector α n)
     (H : ∀ (a : α), a ∈ xs → P a) :
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index 89058e8a0c..2f505bed00 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -1471,7 +1471,7 @@ theorem vector₂_induction (P : Vector (Vector α n) m → Prop)
       P (mk (xss.attach.map (fun ⟨xs, m⟩ => mk xs (h₂ xs m))) (by simpa using h₁)))
     (ass : Vector (Vector α n) m) : P ass := by
   specialize of (ass.map toArray).toArray (by simp) (by simp)
-  simpa [Array.map_attach, Array.pmap_map] using of
+  simpa [Array.map_attach_eq_pmap, Array.pmap_map] using of
 
 /--
 Use this as `induction ass using vector₃_induction` on a hypothesis of the form `ass : Vector (Vector (Vector α n) m) k`.
@@ -1489,7 +1489,7 @@ theorem vector₃_induction (P : Vector (Vector (Vector α n) m) k → Prop)
           mk x (h₃ xs m x m'))) (by simpa using h₂ xs m))) (by simpa using h₁)))
     (ass : Vector (Vector (Vector α n) m) k) : P ass := by
   specialize of (ass.map (fun as => (as.map toArray).toArray)).toArray (by simp) (by simp) (by simp)
-  simpa [Array.map_attach, Array.pmap_map] using of
+  simpa [Array.map_attach_eq_pmap, Array.pmap_map] using of
 
 /-! ### singleton -/
 
@@ -1800,7 +1800,7 @@ theorem flatten_flatten {L : Vector (Vector (Vector α n) m) k} :
   induction L using vector₃_induction with
   | of xss h₁ h₂ h₃ =>
     -- simp [Array.flatten_flatten] -- FIXME: `simp` produces a bad proof here!
-    simp [Array.map_attach, Array.flatten_flatten, Array.map_pmap]
+    simp [Array.map_attach_eq_pmap, Array.flatten_flatten, Array.map_pmap]
 
 /-- Two vectors of constant length vectors are equal iff their flattens coincide. -/
 theorem eq_iff_flatten_eq {L L' : Vector (Vector α n) m} :
diff --git a/tests/lean/run/treeNode.lean b/tests/lean/run/treeNode.lean
index 7d333da8f6..e78a1e51b1 100644
--- a/tests/lean/run/treeNode.lean
+++ b/tests/lean/run/treeNode.lean
@@ -15,11 +15,6 @@ def treeToList (t : TreeNode) : List String :=
 
 @[simp] theorem treeToList_eq (name : String) (children : List TreeNode) : treeToList (.mkNode name children) = name :: List.flatten (children.map treeToList) := by
   simp [treeToList, Id.run]
-  conv => rhs; rw [← List.singleton_append]
-  generalize [name] = as
-  induction children generalizing as with
-  | nil => simp
-  | cons c cs ih => simp [ih, List.append_assoc]
 
 mutual
   def numNames : TreeNode → Nat