fix

src/Init/Data/List/Attach.lean

@@ -86,7 +86,7 @@ theorem attach_map_val (l : List α) (f : α → β) : (l.attach.map fun i => f
 
 @[simp]
 theorem attach_map_subtype_val (l : List α) : l.attach.map Subtype.val = l :=
-  (attach_map_coe _ _).trans l.map_id
+  (attach_map_coe _ _).trans (List.map_id _)
 
 theorem countP_attach (l : List α) (p : α → Bool) : l.attach.countP (fun a : {x // x ∈ l} => p a) = l.countP p := by
   simp only [← Function.comp_apply (g := Subtype.val), ← countP_map, attach_map_subtype_val]

src/Init/Data/List/Find.lean

@@ -42,7 +42,7 @@ theorem exists_of_findSome?_eq_some {l : List α} {f : α → Option β} (w : l.
     (l.findSome? f).map g = l.findSome? (Option.map g ∘ f) := by
   induction l <;> simp [findSome?_cons]; split <;> simp [*]
 
-@[simp] theorem findSome?_map (f : β → γ) (l : List β) : findSome? p (l.map f) = l.findSome? (p ∘ f) := by
+theorem findSome?_map (f : β → γ) (l : List β) : findSome? p (l.map f) = l.findSome? (p ∘ f) := by
   induction l with
   | nil => simp
   | cons x xs ih =>
@@ -217,7 +217,7 @@ theorem mem_of_find?_eq_some : ∀ {l}, find? p l = some a → a ∈ l
     simp only [map_cons, find?]
     by_cases h : p (f x) <;> simp [h, ih]
 
-theorem find?_append {l₁ l₂ : List α} : (l₁ ++ l₂).find? p = (l₁.find? p).or (l₂.find? p) := by
+@[simp] theorem find?_append {l₁ l₂ : List α} : (l₁ ++ l₂).find? p = (l₁.find? p).or (l₂.find? p) := by
   induction l₁ with
   | nil => simp
   | cons x xs ih =>
@@ -238,7 +238,7 @@ theorem find?_join_eq_none (xs : List (List α)) (p : α → Bool) :
 
 @[simp] theorem find?_bind (xs : List α) (f : α → List β) (p : β → Bool) :
     (xs.bind f).find? p = xs.findSome? (fun x => (f x).find? p) := by
-  simp [bind_def]; rfl
+  simp [bind_def, findSome?_map]; rfl
 
 theorem find?_replicate : find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by
   cases n
@@ -633,7 +633,7 @@ theorem findIdx?_eq_enum_findSome? {xs : List α} {p : α → Bool} :
     split
     · simp_all
     · simp_all only [enumFrom_cons, ite_false, Option.isNone_none, findSome?_cons_of_isNone]
-      simp [Function.comp_def, ← map_fst_add_enum_eq_enumFrom]
+      simp [Function.comp_def, ← map_fst_add_enum_eq_enumFrom, findSome?_map]
 
 theorem Sublist.findIdx?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) :
     (l₁.findIdx? p).isSome → (l₂.findIdx? p).isSome := by

src/Init/Data/List/Lemmas.lean

@@ -717,9 +717,14 @@ theorem foldr_eq_foldrM (f : α → β → β) (b) (l : List α) :
 
 /-! ### foldl and foldr -/
 
-@[simp] theorem foldr_self_append (l : List α) : l.foldr cons l' = l ++ l' := by
+@[simp] theorem foldr_cons_eq_append (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
+  induction l generalizing l' <;> simp [*]
+
 theorem foldr_self (l : List α) : l.foldr cons [] = l := by simp
 
 theorem foldl_map (f : β₁ → β₂) (g : α → β₂ → α) (l : List β₁) (init : α) :
@@ -930,9 +935,16 @@ theorem tail_eq_tail? (l) : @tail α l = (tail? l).getD [] := by simp [tail_eq_t
 
 /-! ### map -/
 
-@[simp] theorem map_id (l : List α) : map id l = l := by induction l <;> simp_all
+@[simp] theorem map_id_fun : map (id : α → α) = id := by
+  funext l
+  induction l <;> simp_all
 
-@[simp] theorem map_id' (l : List α) : map (fun a => a) l = l := by induction l <;> simp_all
+@[simp] theorem map_id_fun' : map (fun (a : α) => a) = id := map_id_fun
+
+theorem map_id (l : List α) : map (id : α → α) l = l := by
+  induction l <;> simp_all
+
+theorem map_id' (l : List α) : map (fun (a : α) => a) l = l := map_id l
 
 theorem map_id'' {f : α → α} (h : ∀ x, f x = x) (l : List α) : map f l = l := by
   simp [show f = id from funext h]
@@ -1207,8 +1219,13 @@ 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]
 
-@[simp] theorem filterMap_some (l : List α) : filterMap some l = l := by
-  erw [filterMap_eq_map, map_id]
+@[simp] theorem filterMap_some_fun : filterMap (some : α → Option α) = id := by
+  funext l
+  erw [filterMap_eq_map]
+  simp
+
+theorem filterMap_some (l : List α) : filterMap some l = l := by
+  rw [filterMap_some_fun, id]
 
 theorem map_filterMap_some_eq_filter_map_isSome (f : α → Option β) (l : List α) :
     (l.filterMap f).map some = (l.map f).filter fun b => b.isSome := by
@@ -1283,7 +1300,7 @@ theorem forall_mem_filterMap {f : α → Option β} {l : List α} {P : β → Pr
   induction l <;> simp [filterMap_cons]; split <;> simp [*]
 
 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]
+    (l : List α) : map g (filterMap f l) = l := by simp only [map_filterMap, H, filterMap_some, id]
 
 theorem head_filterMap_of_eq_some {f : α → Option β} {l : List α} (w : l ≠ []) {b : β} (h : f (l.head w) = some b) :
     (filterMap f l).head ((ne_nil_of_mem (mem_filterMap.2 ⟨_, head_mem w, h⟩))) =
@@ -1762,6 +1779,12 @@ theorem join_filter_ne_nil [DecidablePred fun l : List α => l ≠ []] {L : List
   simp only [ne_eq, ← isEmpty_iff, Bool.not_eq_true, Bool.decide_eq_false,
     join_filter_not_isEmpty]
 
+@[simp] theorem join_map_filter (p : α → Bool) (l : List (List α)) : (l.map (filter p)).join = (l.join).filter p := by
+  induction l with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [ih, map_cons, join_cons, filter_append]
+
 @[simp] theorem join_append (L₁ L₂ : List (List α)) : join (L₁ ++ L₂) = join L₁ ++ join L₂ := by
   induction L₁ <;> simp_all
 

src/Init/Data/List/Zip.lean

@@ -78,13 +78,13 @@ theorem map_prod_left_eq_zip {l : List α} (f : α → β) :
     (l.map fun x => (x, f x)) = l.zip (l.map f) := by
   rw [← zip_map']
   congr
-  exact map_id _
+  simp
 
 theorem map_prod_right_eq_zip {l : List α} (f : α → β) :
     (l.map fun x => (f x, x)) = (l.map f).zip l := by
   rw [← zip_map']
   congr
-  exact map_id _
+  simp
 
 /-- See also `List.zip_replicate` in `Init.Data.List.TakeDrop` for a generalization with different lengths. -/
 @[simp] theorem zip_replicate' {a : α} {b : β} {n : Nat} :

tests/lean/run/list_simp.lean

@@ -113,8 +113,6 @@ variable (L : List (List α)) in
 
 variable (p : β → Bool) in
 #check_simp (l.map f).find? p ~> (l.find? (p ∘ f)).map f
-variable (p : β → Option γ) in
-#check_simp (l.map f).findSome? p ~> l.findSome? (p ∘ f)
 
 /-! ### filter -/