From b49953b904a639c63773ab1d5e25fe89fcc9eff8 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 6 Mar 2025 01:58:48 +0000
Subject: [PATCH 1/8] feat: lemmas about pure for `mapM`, `foldlM`, and
 `foldrM`

These are more general cases of the existing lemmas about `Id`.
---
 src/Init/Data/Array/Lemmas.lean  |  8 ++++++++
 src/Init/Data/Array/Monadic.lean |  6 +++++-
 src/Init/Data/List/Lemmas.lean   |  8 ++++++++
 src/Init/Data/List/Monadic.lean  |  6 +++++-
 src/Init/Data/Vector/Lemmas.lean | 10 ++++++++++
 5 files changed, 36 insertions(+), 2 deletions(-)

diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index fc9fc9e6d87f..fbcc5ed5faf4 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -2984,6 +2984,14 @@ theorem foldlM_push [Monad m] [LawfulMonad m] (xs : Array α) (a : α) (f : β 
     (xs.push a).foldlM f b = xs.foldlM f b >>= fun b => f b a := by
   simp
 
+@[simp] theorem foldlM_pure [Monad m] [LawfulMonad m] (f : β → α → β) (b) (xs : Array α) :
+    xs.foldlM (m := m) (pure <| f · ·) b start stop = pure (xs.foldl f b start stop) := by
+  rw [foldl, foldlM_start_stop, ← foldlM_toList, List.foldlM_pure, foldl_toList, foldl, ← foldlM_start_stop]
+
+@[simp] theorem foldrM_pure [Monad m] [LawfulMonad m] (f : α → β → β) (b) (xs : Array α) :
+    xs.foldrM (m := m) (pure <| f · ·) b start stop = pure (xs.foldr f b start stop) := by
+  rw [foldr, foldrM_start_stop, ← foldrM_toList, List.foldrM_pure, foldr_toList, foldr, ← foldrM_start_stop]
+
 theorem foldl_eq_foldlM (f : β → α → β) (b) (xs : Array α) :
     xs.foldl f b start stop = xs.foldlM (m := Id) f b start stop := by
   simp [foldl, Id.run]
diff --git a/src/Init/Data/Array/Monadic.lean b/src/Init/Data/Array/Monadic.lean
index 8004bc6350b9..3059b2c7d698 100644
--- a/src/Init/Data/Array/Monadic.lean
+++ b/src/Init/Data/Array/Monadic.lean
@@ -23,9 +23,13 @@ open Nat
 
 /-! ### mapM -/
 
-@[simp] theorem mapM_id {xs : Array α} {f : α → Id β} : xs.mapM f = xs.map f := by
+@[simp] theorem mapM_pure [Monad m] [LawfulMonad m] (xs : Array α) (f : α → β) :
+    xs.mapM (m := m) (pure <| f ·) = pure (xs.map f) := by
   induction xs; simp_all
 
+@[simp] theorem mapM_id {xs : Array α} {f : α → Id β} : xs.mapM f = xs.map f :=
+  mapM_pure _ _
+
 @[simp] theorem mapM_append [Monad m] [LawfulMonad m] (f : α → m β) {xs ys : Array α} :
     (xs ++ ys).mapM f = (return (← xs.mapM f) ++ (← ys.mapM f)) := by
   rcases xs with ⟨xs⟩
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 1b86f91e395f..2d0edfff253a 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -2535,6 +2535,14 @@ theorem flatMap_reverse {β} (l : List α) (f : α → List β) : (l.reverse.fla
   simp only [foldrM]
   induction l <;> simp_all
 
+@[simp] theorem foldlM_pure [Monad m] [LawfulMonad m] (f : β → α → β) (b) (l : List α) :
+    l.foldlM (m := m) (pure <| f · ·) b = pure (l.foldl f b) := by
+  induction l generalizing b <;> simp [*]
+
+@[simp] theorem foldrM_pure [Monad m] [LawfulMonad m] (f : α → β → β) (b) (l : List α) :
+    l.foldrM (m := m) (pure <| f · ·) b = pure (l.foldr f b) := by
+  induction l generalizing b <;> simp [*]
+
 theorem foldl_eq_foldlM (f : β → α → β) (b) (l : List α) :
     l.foldl f b = l.foldlM (m := Id) f b := by
   induction l generalizing b <;> simp [*, foldl]
diff --git a/src/Init/Data/List/Monadic.lean b/src/Init/Data/List/Monadic.lean
index e0e49acbc6e7..d0d6b4046671 100644
--- a/src/Init/Data/List/Monadic.lean
+++ b/src/Init/Data/List/Monadic.lean
@@ -56,9 +56,13 @@ theorem mapM'_eq_mapM [Monad m] [LawfulMonad m] (f : α → m β) (l : List α)
 @[simp] theorem mapM_cons [Monad m] [LawfulMonad m] (f : α → m β) :
     (a :: l).mapM f = (return (← f a) :: (← l.mapM f)) := by simp [← mapM'_eq_mapM, mapM']
 
-@[simp] theorem mapM_id {l : List α} {f : α → Id β} : l.mapM f = l.map f := by
+@[simp] theorem mapM_pure [Monad m] [LawfulMonad m] (l : List α) (f : α → β) :
+    l.mapM (m := m) (pure <| f ·) = pure (l.map f) := by
   induction l <;> simp_all
 
+@[simp] theorem mapM_id {l : List α} {f : α → Id β} : l.mapM f = l.map f :=
+  mapM_pure _ _
+
 @[simp] theorem mapM_append [Monad m] [LawfulMonad m] (f : α → m β) {l₁ l₂ : List α} :
     (l₁ ++ l₂).mapM f = (return (← l₁.mapM f) ++ (← l₂.mapM f)) := by induction l₁ <;> simp [*]
 
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index 1e8b97652ecc..ecb3b4b1f93c 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -2189,6 +2189,16 @@ theorem extract_empty (start stop : Nat) :
   rcases xs with ⟨xs, rfl⟩
   simp
 
+@[simp]
+theorem foldlM_pure [Monad m] [LawfulMonad m] (f : β → α → β) (b) (xs : Vector α n) :
+    xs.foldlM (m := m) (pure <| f · ·) b = pure (xs.foldl f b) :=
+  Array.foldlM_pure _ _ _
+
+@[simp]
+theorem foldrM_pure [Monad m] [LawfulMonad m] (f : α → β → β) (b) (xs : Vector α n) :
+    xs.foldrM (m := m) (pure <| f · ·) b = pure (xs.foldr f b) :=
+  Array.foldrM_pure _ _ _
+
 theorem foldl_eq_foldlM (f : β → α → β) (b) (xs : Vector α n) :
     xs.foldl f b = xs.foldlM (m := Id) f b := by
   rcases xs with ⟨xs, rfl⟩

From 7a7e6e294dd5282e46441ab58259c938b083b413 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 6 Mar 2025 02:06:13 +0000
Subject: [PATCH 2/8] one more

---
 src/Init/Data/Vector/Monadic.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/Init/Data/Vector/Monadic.lean b/src/Init/Data/Vector/Monadic.lean
index 438745abfbda..13028f5c32e7 100644
--- a/src/Init/Data/Vector/Monadic.lean
+++ b/src/Init/Data/Vector/Monadic.lean
@@ -29,6 +29,12 @@ open Nat
 
 /-! ### mapM -/
 
+@[simp]
+theorem mapM_pure [Monad m] [LawfulMonad m] {xs : Vector α n} (f : α → β) :
+    xs.mapM (m := m) (pure <| f ·) = pure (xs.map f) := by
+  apply map_toArray_inj.mp
+  simp
+
 @[congr] theorem mapM_congr [Monad m] {xs ys : Vector α n} (w : xs = ys)
     {f : α → m β} :
     xs.mapM f = ys.mapM f := by

From bd83099d99f1e930de61b4faa2b4bc0ed3ba19cd Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 6 Mar 2025 11:09:40 +0000
Subject: [PATCH 3/8] allM_pure

---
 src/Init/Data/Array/Monadic.lean  | 12 ++++++++++++
 src/Init/Data/List/Monadic.lean   | 14 +++++++++++++-
 src/Init/Data/Vector/Monadic.lean | 14 ++++++++++++++
 3 files changed, 39 insertions(+), 1 deletion(-)

diff --git a/src/Init/Data/Array/Monadic.lean b/src/Init/Data/Array/Monadic.lean
index 3059b2c7d698..091289baddf6 100644
--- a/src/Init/Data/Array/Monadic.lean
+++ b/src/Init/Data/Array/Monadic.lean
@@ -231,6 +231,18 @@ theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
   rcases xs with ⟨xs⟩
   simp
 
+/-! ### allM and anyM -/
+
+@[simp] theorem anyM_pure [Monad m] [LawfulMonad m] (p : α → Bool) (xs : Array α) :
+    xs.anyM (m := m) (pure <| p ·) = pure (xs.any p) := by
+  cases xs
+  simp
+
+@[simp] theorem allM_pure [Monad m] [LawfulMonad m] (p : α → Bool) (xs : Array α) :
+    xs.allM (m := m) (pure <| p ·) = pure (xs.all p) := by
+  cases xs
+  simp
+
 end Array
 
 namespace List
diff --git a/src/Init/Data/List/Monadic.lean b/src/Init/Data/List/Monadic.lean
index d0d6b4046671..6e09bae197fd 100644
--- a/src/Init/Data/List/Monadic.lean
+++ b/src/Init/Data/List/Monadic.lean
@@ -399,7 +399,7 @@ theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
     forIn (l.map g) init f = forIn l init fun a y => f (g a) y := by
   induction l generalizing init <;> simp_all
 
-/-! ### allM -/
+/-! ### allM and anyM -/
 
 theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as : List α) :
     allM p as = (! ·) <$> anyM ((! ·) <$> p ·) as := by
@@ -411,6 +411,18 @@ theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as :
     funext b
     split <;> simp_all
 
+@[simp] theorem anyM_pure [Monad m] [LawfulMonad m] (p : α → Bool) (as : List α) :
+    as.anyM (m := m) (pure <| p ·) = pure (as.any p) := by
+  induction as with
+  | nil => simp
+  | cons a as ih =>
+    simp only [anyM, ih, pure_bind, all_cons]
+    split <;> simp_all
+
+@[simp] theorem allM_pure [Monad m] [LawfulMonad m] (p : α → Bool) (as : List α) :
+    as.allM (m := m) (pure <| p ·) = pure (as.all p) := by
+  simp [allM_eq_not_anyM_not, all_eq_not_any_not]
+
 /-! ### Recognizing higher order functions using a function that only depends on the value. -/
 
 /--
diff --git a/src/Init/Data/Vector/Monadic.lean b/src/Init/Data/Vector/Monadic.lean
index 13028f5c32e7..944b1026f4a3 100644
--- a/src/Init/Data/Vector/Monadic.lean
+++ b/src/Init/Data/Vector/Monadic.lean
@@ -221,4 +221,18 @@ theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
   rcases xs with ⟨xs, rfl⟩
   simp
 
+
+/-! ### allM and anyM -/
+
+@[simp] theorem anyM_pure [Monad m] [LawfulMonad m] (p : α → Bool) (xs : Vector α n) :
+    xs.anyM (m := m) (pure <| p ·) = pure (xs.any p) := by
+  cases xs
+  simp
+
+@[simp] theorem allM_pure [Monad m] [LawfulMonad m] (p : α → Bool) (xs : Vector α n) :
+    xs.allM (m := m) (pure <| p ·) = pure (xs.all p) := by
+  cases xs
+  simp
+
+
 end Vector

From 310a9289574d3c3e5e739f83a1045c88964dfb75 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 6 Mar 2025 11:36:33 +0000
Subject: [PATCH 4/8] findM and findSomeM

---
 src/Init/Data/Array/Monadic.lean  | 13 +++++++++++++
 src/Init/Data/List/Control.lean   | 23 ++++++++++++++++-------
 src/Init/Data/Vector/Monadic.lean | 12 ++++++++++++
 3 files changed, 41 insertions(+), 7 deletions(-)

diff --git a/src/Init/Data/Array/Monadic.lean b/src/Init/Data/Array/Monadic.lean
index 091289baddf6..1ff51a917bcb 100644
--- a/src/Init/Data/Array/Monadic.lean
+++ b/src/Init/Data/Array/Monadic.lean
@@ -243,6 +243,19 @@ theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
   cases xs
   simp
 
+/-! ### findM? and findSomeM? -/
+
+theorem findM?_pure {m} [Monad m] [LawfulMonad m] (p : α → Bool) (xs : Array α) :
+    findM? (m := m) (pure <| p ·) xs = pure (xs.find? p) := by
+  cases xs
+  simp
+
+@[simp]
+theorem findSomeM?_pure [Monad m] [LawfulMonad m] (f : α → Option β) (xs : Array α) :
+    findSomeM? (m := m) (pure <| f ·) xs = pure (xs.findSome? f) := by
+  cases xs
+  simp
+
 end Array
 
 namespace List
diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean
index 018ed2b5174b..af17215ee54e 100644
--- a/src/Init/Data/List/Control.lean
+++ b/src/Init/Data/List/Control.lean
@@ -226,15 +226,19 @@ def findM? {m : Type → Type u} [Monad m] {α : Type} (p : α → m Bool) : Lis
     | true  => pure (some a)
     | false => findM? p as
 
-@[simp]
-theorem findM?_id (p : α → Bool) (as : List α) : findM? (m := Id) p as = as.find? p := by
+theorem findM?_pure {m} [Monad m] [LawfulMonad m] (p : α → Bool) (as : List α) :
+    findM? (m := m) (pure <| p ·) as = pure (as.find? p) := by
   induction as with
   | nil => rfl
   | cons a as ih =>
     simp only [findM?, find?]
     cases p a with
-    | true  => rfl
-    | false => rw [ih]; rfl
+    | true  => simp
+    | false => simp [ih]
+
+@[simp]
+theorem findM?_id (p : α → Bool) (as : List α) : findM? (m := Id) p as = as.find? p :=
+  findM?_pure _ _
 
 @[specialize]
 def findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) : List α → m (Option β)
@@ -245,14 +249,19 @@ def findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f
     | none   => findSomeM? f as
 
 @[simp]
-theorem findSomeM?_id (f : α → Option β) (as : List α) : findSomeM? (m := Id) f as = as.findSome? f := by
+theorem findSomeM?_pure [Monad m] [LawfulMonad m] (f : α → Option β) (as : List α) :
+    findSomeM? (m := m) (pure <| f ·) as = pure (as.findSome? f) := by
   induction as with
   | nil => rfl
   | cons a as ih =>
     simp only [findSomeM?, findSome?]
     cases f a with
-    | some b => rfl
-    | none   => rw [ih]; rfl
+    | some b => simp
+    | none   => simp [ih]
+
+@[simp]
+theorem findSomeM?_id (f : α → Option β) (as : List α) : findSomeM? (m := Id) f as = as.findSome? f :=
+  findSomeM?_pure _ _
 
 theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] (p : α → m Bool) (as : List α) :
     as.findM? p = as.findSomeM? fun a => return if (← p a) then some a else none := by
diff --git a/src/Init/Data/Vector/Monadic.lean b/src/Init/Data/Vector/Monadic.lean
index 944b1026f4a3..18dfdc5b1592 100644
--- a/src/Init/Data/Vector/Monadic.lean
+++ b/src/Init/Data/Vector/Monadic.lean
@@ -234,5 +234,17 @@ theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
   cases xs
   simp
 
+/-! ### findM? and findSomeM? -/
+
+theorem findM?_pure {m} [Monad m] [LawfulMonad m] (p : α → Bool) (xs : Vector α n) :
+    findM? (m := m) (pure <| p ·) xs = pure (xs.find? p) := by
+  cases xs
+  simp
+
+@[simp]
+theorem findSomeM?_pure [Monad m] [LawfulMonad m] (f : α → Option β) (xs : Vector α n) :
+    findSomeM? (m := m) (pure <| f ·) xs = pure (xs.findSome? f) := by
+  cases xs
+  simp
 
 end Vector

From da9b2b57a71bd8ac672897afd42d2efd10e9d42a Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 6 Mar 2025 14:26:07 +0000
Subject: [PATCH 5/8] simp

---
 src/Init/Data/Array/Monadic.lean | 1 +
 src/Init/Data/List/Control.lean  | 1 +
 2 files changed, 2 insertions(+)

diff --git a/src/Init/Data/Array/Monadic.lean b/src/Init/Data/Array/Monadic.lean
index 1ff51a917bcb..c26e25f750e0 100644
--- a/src/Init/Data/Array/Monadic.lean
+++ b/src/Init/Data/Array/Monadic.lean
@@ -245,6 +245,7 @@ theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
 
 /-! ### findM? and findSomeM? -/
 
+@[simp]
 theorem findM?_pure {m} [Monad m] [LawfulMonad m] (p : α → Bool) (xs : Array α) :
     findM? (m := m) (pure <| p ·) xs = pure (xs.find? p) := by
   cases xs
diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean
index af17215ee54e..81d6da7ee498 100644
--- a/src/Init/Data/List/Control.lean
+++ b/src/Init/Data/List/Control.lean
@@ -226,6 +226,7 @@ def findM? {m : Type → Type u} [Monad m] {α : Type} (p : α → m Bool) : Lis
     | true  => pure (some a)
     | false => findM? p as
 
+@[simp]
 theorem findM?_pure {m} [Monad m] [LawfulMonad m] (p : α → Bool) (as : List α) :
     findM? (m := m) (pure <| p ·) as = pure (as.find? p) := by
   induction as with

From 2b3d1489e4995806e887b670c36bf97b7591132c Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 10 Mar 2025 10:10:38 +0000
Subject: [PATCH 6/8] filterM

---
 src/Init/Data/List/Control.lean | 10 ++++++++++
 src/Init/Data/List/Lemmas.lean  | 34 +++++++++++++++++++++++++++++++++
 2 files changed, 44 insertions(+)

diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean
index 81d6da7ee498..9bdfd788e1a6 100644
--- a/src/Init/Data/List/Control.lean
+++ b/src/Init/Data/List/Control.lean
@@ -118,6 +118,11 @@ def filterM {m : Type → Type v} [Monad m] {α : Type} (p : α → m Bool) (as
   let as ← filterAuxM p as []
   pure as.reverse
 
+@[simp]
+theorem filterM_nil {m} [Monad m] [LawfulMonad m] {α : Type} (p : α → m Bool) :
+    filterM p [] = pure [] := by
+  simp [filterM, filterAuxM]
+
 /--
 Applies the monadic predicate `p` on every element in the list, right-to-left, and returns those
 elements `x` for which `p x` returns `true`.
@@ -126,6 +131,11 @@ elements `x` for which `p x` returns `true`.
 def filterRevM {m : Type → Type v} [Monad m] {α : Type} (p : α → m Bool) (as : List α) : m (List α) :=
   filterAuxM p as.reverse []
 
+@[simp]
+theorem filterRevM_nil {m} [Monad m] {α : Type} (p : α → m Bool) :
+    filterRevM p [] = pure [] := by
+  simp [filterRevM, filterAuxM]
+
 /--
 Applies the monadic function `f` on every element `x` in the list, left-to-right, and returns those
 results `y` for which `f x` returns `some y`.
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 2d0edfff253a..50690ba6810d 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -2523,6 +2523,40 @@ theorem flatMap_reverse {β} (l : List α) (f : α → List β) : (l.reverse.fla
     ⟨by rw [length_reverse, length_replicate],
      fun _ h => eq_of_mem_replicate (mem_reverse.1 h)⟩
 
+/--! ### filterM -/
+
+theorem filterAuxM_append_right [Monad m] [LawfulMonad m] {as acc₁ acc₂ : List α} {p : α → m Bool} :
+    filterAuxM p as (acc₁ ++ acc₂) = (· ++ acc₂) <$> filterAuxM p as acc₁ := by
+  induction as generalizing acc₁ with
+  | nil => simp [filterAuxM]
+  | cons a as ih =>
+    simp only [filterAuxM, map_bind]
+    congr 1
+    ext pa
+    cases pa <;> simp only [← cons_append, cond_true, cond_false, ih]
+
+theorem filterAuxM_eq_map [Monad m] [LawfulMonad m] {as acc : List α} {p : α → m Bool} :
+    filterAuxM p as acc = (· ++ acc) <$> filterAuxM p as [] := by
+  simpa using filterAuxM_append_right (acc₁ := [])
+
+theorem filterM_cons {m} [Monad m] [LawfulMonad m] {a : α} {as : List α} {p : α → m Bool} :
+    filterM p (a :: as) =
+      (do let pa ← p a; if pa then .cons a <$> filterM p as else filterM p as) := by
+  simp only [filterM, filterAuxM, bind_pure_comp, map_bind, Functor.map_map]
+  congr 1
+  ext pa
+  cases pa
+  · simp
+  rw [filterAuxM_eq_map]
+  simp
+
+@[simp]
+theorem filterM_pure {m} [Monad m] [LawfulMonad m] {α : Type} (p : α → Bool) (as : List α) :
+    filterM (m := m) (pure <| p ·) as = pure (as.filter p) := by
+  induction as with
+  | nil => simp [filterM_nil]
+  | cons a as ih =>
+    by_cases h : p a <;> simp [filterM_cons, filter, ih, h]
 
 /-! ### foldlM and foldrM -/
 

From da43908b2c07db066f7f7a2ec7db628a0bcb8826 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 10 Mar 2025 16:34:04 +0000
Subject: [PATCH 7/8] more

---
 src/Init/Data/List/Basic.lean   | 15 ++++++++
 src/Init/Data/List/Control.lean | 68 ++++++++++++++++++++++++++++++++-
 src/Init/Data/List/Lemmas.lean  | 38 ------------------
 3 files changed, 81 insertions(+), 40 deletions(-)

diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 3c320ac98405..1e5beee0d94e 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -474,6 +474,15 @@ theorem reverseAux_reverseAux (as bs cs : List α) : reverseAux (reverseAux as b
   | nil => rfl
   | cons a as ih => simp [reverseAux, ih (a::bs), ih [a]]
 
+
+theorem reverseAux_reverseAux_nil (as bs : List α) : reverseAux (reverseAux as bs) [] = reverseAux bs as := by
+  induction as generalizing bs with
+  | nil => rfl
+  | cons a as ih => simp [reverseAux, ih]
+
+@[simp] theorem reverse_reverse (as : List α) : as.reverse.reverse = as := by
+  simp only [reverse]; rw [reverseAux_reverseAux_nil]; rfl
+
 /-! ### append -/
 
 /--
@@ -549,6 +558,12 @@ theorem reverseAux_eq_append (as bs : List α) : reverseAux as bs = reverseAux a
   simp [reverse, reverseAux]
   rw [← reverseAux_eq_append]
 
+@[simp] theorem reverse_append (as bs : List α) : (as ++ bs).reverse = bs.reverse ++ as.reverse := by
+  induction as <;> simp_all
+
+theorem reverse_concat (l : List α) (a : α) : (l ++ [a]).reverse = a :: l.reverse := by
+  rw [reverse_append]; rfl
+
 /-! ### flatten -/
 
 /--
diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean
index 9bdfd788e1a6..383a2b3814b2 100644
--- a/src/Init/Data/List/Control.lean
+++ b/src/Init/Data/List/Control.lean
@@ -109,6 +109,20 @@ def filterAuxM {m : Type → Type v} [Monad m] {α : Type} (f : α → m Bool) :
     let b ← f h
     filterAuxM f t (cond b (h :: acc) acc)
 
+theorem filterAuxM_append_right [Monad m] [LawfulMonad m] {as acc₁ acc₂ : List α} {p : α → m Bool} :
+    filterAuxM p as (acc₁ ++ acc₂) = (· ++ acc₂) <$> filterAuxM p as acc₁ := by
+  induction as generalizing acc₁ with
+  | nil => simp [filterAuxM]
+  | cons a as ih =>
+    simp only [filterAuxM, map_bind]
+    congr 1
+    ext pa
+    cases pa <;> simp only [← cons_append, cond_true, cond_false, ih]
+
+theorem filterAuxM_eq_map [Monad m] [LawfulMonad m] {as acc : List α} {p : α → m Bool} :
+    filterAuxM p as acc = (· ++ acc) <$> filterAuxM p as [] := by
+  simpa using filterAuxM_append_right (acc₁ := [])
+
 /--
 Applies the monadic predicate `p` on every element in the list, left-to-right, and returns those
 elements `x` for which `p x` returns `true`.
@@ -119,10 +133,40 @@ def filterM {m : Type → Type v} [Monad m] {α : Type} (p : α → m Bool) (as
   pure as.reverse
 
 @[simp]
-theorem filterM_nil {m} [Monad m] [LawfulMonad m] {α : Type} (p : α → m Bool) :
+theorem filterM_nil {m : Type → Type v} [Monad m] [LawfulMonad m] {α : Type} (p : α → m Bool) :
     filterM p [] = pure [] := by
   simp [filterM, filterAuxM]
 
+theorem filterM_cons {m : Type → Type v} [Monad m] [LawfulMonad m] {a : α} {as : List α} {p : α → m Bool} :
+    filterM p (a :: as) =
+      (do let pa ← p a; let as ← filterM p as; return if pa then a :: as else as) := by
+  simp only [filterM, filterAuxM, bind_pure_comp, map_bind, Functor.map_map]
+  congr 1; ext pa
+  cases pa
+  · simp
+  rw [filterAuxM_eq_map]
+  simp
+
+theorem filterM_append {m : Type → Type v} [Monad m] [LawfulMonad m] {as bs : List α} {p : α → m Bool} :
+    filterM p (as ++ bs) = HAppend.hAppend <$> filterM p as <*> filterM p bs := by
+  induction as with
+  | nil =>
+    have : HAppend.hAppend ([] : List α) = id := funext List.nil_append
+    simp [filterM_cons, pure_seq, this]
+  | cons a' as ih =>
+    simp only [cons_append, filterM_cons, ih, bind_pure_comp, map_bind, Functor.map_map, bind_assoc,
+      bind_map_left, seq_eq_bind_map]
+    congr; ext pa; congr; ext as'; congr; ext bs'
+    split <;> simp
+
+theorem filterM_concat {m : Type → Type v} [Monad m] [LawfulMonad m] {as : List α} {a : α} {p : α → m Bool} :
+    filterM p (as ++ [a]) =
+      (do let as ← filterM p as; let pa ← p a; return if pa then as ++ [a] else as) := by
+  rw [filterM_append, filterM_cons, filterM_nil, seq_eq_bind_map]
+  simp only [bind_pure_comp, map_pure, Functor.map_map, bind_map_left]
+  congr; ext as'; congr; ext pa
+  split <;> simp
+
 /--
 Applies the monadic predicate `p` on every element in the list, right-to-left, and returns those
 elements `x` for which `p x` returns `true`.
@@ -131,11 +175,31 @@ elements `x` for which `p x` returns `true`.
 def filterRevM {m : Type → Type v} [Monad m] {α : Type} (p : α → m Bool) (as : List α) : m (List α) :=
   filterAuxM p as.reverse []
 
+theorem filterRevM_eq_reverse_map_filterM_reverse {m : Type → Type v} [Monad m] [LawfulMonad m] {α : Type} (p : α → m Bool) (as : List α):
+    filterRevM p as = reverse <$> filterM p as.reverse := by
+  simp [filterRevM, filterM]
+
 @[simp]
-theorem filterRevM_nil {m} [Monad m] {α : Type} (p : α → m Bool) :
+theorem filterRevM_nil {m : Type → Type v} [Monad m] {α : Type} (p : α → m Bool) :
     filterRevM p [] = pure [] := by
   simp [filterRevM, filterAuxM]
 
+@[simp]
+theorem filterRevM_concat {m : Type → Type v} [Monad m] [LawfulMonad m] {as : List α} {a : α} {p : α → m Bool} :
+    filterRevM p (as ++ [a]) =
+      (do let pa ← p a; let as ← filterRevM p as; return if pa then as ++ [a] else as) := by
+  simp only [filterRevM_eq_reverse_map_filterM_reverse, reverse_append, reverse_cons, reverse_nil,
+    nil_append, cons_append, filterM_cons, bind_pure_comp, map_bind, Functor.map_map]
+  congr; ext pa; congr; ext as'
+  split <;> simp
+
+theorem filterRevM_cons {m : Type → Type v} [Monad m] [LawfulMonad m] {as : List α} {a : α} {p : α → m Bool} :
+    filterRevM p (a :: as) =
+      (do let as ← filterRevM p as; let pa ← p a; return if pa then a :: as else as) := by
+  simp [filterRevM_eq_reverse_map_filterM_reverse, filterM_concat]
+  congr; ext as'; congr; ext pa
+  split <;> simp
+
 /--
 Applies the monadic function `f` on every element `x` in the list, left-to-right, and returns those
 results `y` for which `f x` returns `some y`.
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 50690ba6810d..17c89c92a4b5 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -2492,9 +2492,6 @@ theorem mem_of_mem_getLast? {l : List α} {a : α} (h : a ∈ getLast? l) : a 
 
 @[deprecated reverse_eq_append_iff (since := "2024-09-05")] abbrev reverse_eq_append := @reverse_eq_append_iff
 
-theorem reverse_concat (l : List α) (a : α) : (l ++ [a]).reverse = a :: l.reverse := by
-  rw [reverse_append]; rfl
-
 theorem reverse_eq_concat {xs ys : List α} {a : α} :
     xs.reverse = ys ++ [a] ↔ xs = a :: ys.reverse := by
   rw [reverse_eq_iff, reverse_concat]
@@ -2523,41 +2520,6 @@ theorem flatMap_reverse {β} (l : List α) (f : α → List β) : (l.reverse.fla
     ⟨by rw [length_reverse, length_replicate],
      fun _ h => eq_of_mem_replicate (mem_reverse.1 h)⟩
 
-/--! ### filterM -/
-
-theorem filterAuxM_append_right [Monad m] [LawfulMonad m] {as acc₁ acc₂ : List α} {p : α → m Bool} :
-    filterAuxM p as (acc₁ ++ acc₂) = (· ++ acc₂) <$> filterAuxM p as acc₁ := by
-  induction as generalizing acc₁ with
-  | nil => simp [filterAuxM]
-  | cons a as ih =>
-    simp only [filterAuxM, map_bind]
-    congr 1
-    ext pa
-    cases pa <;> simp only [← cons_append, cond_true, cond_false, ih]
-
-theorem filterAuxM_eq_map [Monad m] [LawfulMonad m] {as acc : List α} {p : α → m Bool} :
-    filterAuxM p as acc = (· ++ acc) <$> filterAuxM p as [] := by
-  simpa using filterAuxM_append_right (acc₁ := [])
-
-theorem filterM_cons {m} [Monad m] [LawfulMonad m] {a : α} {as : List α} {p : α → m Bool} :
-    filterM p (a :: as) =
-      (do let pa ← p a; if pa then .cons a <$> filterM p as else filterM p as) := by
-  simp only [filterM, filterAuxM, bind_pure_comp, map_bind, Functor.map_map]
-  congr 1
-  ext pa
-  cases pa
-  · simp
-  rw [filterAuxM_eq_map]
-  simp
-
-@[simp]
-theorem filterM_pure {m} [Monad m] [LawfulMonad m] {α : Type} (p : α → Bool) (as : List α) :
-    filterM (m := m) (pure <| p ·) as = pure (as.filter p) := by
-  induction as with
-  | nil => simp [filterM_nil]
-  | cons a as ih =>
-    by_cases h : p a <;> simp [filterM_cons, filter, ih, h]
-
 /-! ### foldlM and foldrM -/
 
 @[simp] theorem foldlM_append [Monad m] [LawfulMonad m] (f : β → α → m β) (b) (l l' : List α) :

From 440555e6a9ac68ffbca035ac134c848cdfafbdac Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Wed, 3 Dec 2025 03:46:18 +0000
Subject: [PATCH 8/8] fix

---
 src/Init/Data/List/Basic.lean   | 17 ++++++++++++++---
 src/Init/Data/List/Control.lean |  2 +-
 src/Init/Data/List/Lemmas.lean  | 27 ---------------------------
 3 files changed, 15 insertions(+), 31 deletions(-)

diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 380154894b36..5b5a1583fa1a 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -572,7 +572,6 @@ theorem reverseAux_reverseAux {as bs cs : List α} :
   | nil => rfl
   | cons a as ih => simp [reverseAux, ih (bs := a::bs), ih (bs := [a])]
 
-
 theorem reverseAux_reverseAux_nil (as bs : List α) : reverseAux (reverseAux as bs) [] = reverseAux bs as := by
   induction as generalizing bs with
   | nil => rfl
@@ -663,12 +662,24 @@ theorem reverseAux_eq_append {as bs : List α} : reverseAux as bs = reverseAux a
   simp [reverse, reverseAux]
   rw [← reverseAux_eq_append]
 
-@[simp] theorem reverse_append (as bs : List α) : (as ++ bs).reverse = bs.reverse ++ as.reverse := by
+@[simp] theorem reverse_append {as bs : List α} : (as ++ bs).reverse = bs.reverse ++ as.reverse := by
   induction as <;> simp_all
 
-theorem reverse_concat (l : List α) (a : α) : (l ++ [a]).reverse = a :: l.reverse := by
+grind_pattern reverse_append => (as ++ bs).reverse where
+  as =/= []
+  bs =/= []
+grind_pattern reverse_append => bs.reverse ++ as.reverse where
+  as =/= []
+  bs =/= []
+
+theorem reverse_concat {l : List α} {a : α} : (l ++ [a]).reverse = a :: l.reverse := by
   rw [reverse_append]; rfl
 
+grind_pattern reverse_concat => (l ++ [a]).reverse where
+  l =/= []
+grind_pattern reverse_concat => a :: l.reverse where
+  l =/= []
+
 /-! ### flatten -/
 
 
diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean
index c5192e17109e..b363d9fc7ec6 100644
--- a/src/Init/Data/List/Control.lean
+++ b/src/Init/Data/List/Control.lean
@@ -187,7 +187,7 @@ theorem filterM_append {m : Type → Type v} [Monad m] [LawfulMonad m] {as bs :
   induction as with
   | nil =>
     have : HAppend.hAppend ([] : List α) = id := funext List.nil_append
-    simp [filterM_cons, pure_seq, this]
+    simp [pure_seq, this]
   | cons a' as ih =>
     simp only [cons_append, filterM_cons, ih, bind_pure_comp, map_bind, Functor.map_map, bind_assoc,
       bind_map_left, seq_eq_bind_map]
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 7735f1c12591..32c7dbe9c78e 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -2414,15 +2414,6 @@ theorem getElem_reverse {l : List α} {i} (h : i < l.reverse.length) :
   rw [← getElem?_eq_getElem, ← getElem?_eq_getElem]
   rw [getElem?_reverse (by simpa using h)]
 
-theorem reverseAux_reverseAux_nil {as bs : List α} : reverseAux (reverseAux as bs) [] = reverseAux bs as := by
-  induction as generalizing bs with
-  | nil => rfl
-  | cons a as ih => simp [reverseAux, ih]
-
--- The argument `as : List α` is explicit to allow rewriting from right to left.
-@[simp, grind =] theorem reverse_reverse (as : List α) : as.reverse.reverse = as := by
-  simp only [reverse]; rw [reverseAux_reverseAux_nil]; rfl
-
 theorem reverse_eq_iff {as bs : List α} : as.reverse = bs ↔ as = bs.reverse := by
   constructor <;> (rintro rfl; simp)
 
@@ -2476,28 +2467,10 @@ theorem getLast_of_mem_getLast? {l : List α} (hx : x ∈ l.getLast?) :
     simp only [reverse_cons, filterMap_append, filterMap_cons, ih]
     split <;> simp_all
 
-@[simp] theorem reverse_append {as bs : List α} : (as ++ bs).reverse = bs.reverse ++ as.reverse := by
-  induction as <;> simp_all
-
-grind_pattern reverse_append => (as ++ bs).reverse where
-  as =/= []
-  bs =/= []
-grind_pattern reverse_append => bs.reverse ++ as.reverse where
-  as =/= []
-  bs =/= []
-
 @[simp] theorem reverse_eq_append_iff {xs ys zs : List α} :
     xs.reverse = ys ++ zs ↔ xs = zs.reverse ++ ys.reverse := by
   rw [reverse_eq_iff, reverse_append]
 
-theorem reverse_concat {l : List α} {a : α} : (l ++ [a]).reverse = a :: l.reverse := by
-  rw [reverse_append]; rfl
-
-grind_pattern reverse_concat => (l ++ [a]).reverse where
-  l =/= []
-grind_pattern reverse_concat => a :: l.reverse where
-  l =/= []
-
 theorem reverse_eq_concat {xs ys : List α} {a : α} :
     xs.reverse = ys ++ [a] ↔ xs = a :: ys.reverse := by
   rw [reverse_eq_iff, reverse_concat]