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..c26e25f750e0 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⟩
@@ -227,6 +231,32 @@ 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
+
+/-! ### 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
+  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..81d6da7ee498 100644
--- a/src/Init/Data/List/Control.lean
+++ b/src/Init/Data/List/Control.lean
@@ -227,14 +227,19 @@ def findM? {m : Type → Type u} [Monad m] {α : Type} (p : α → m Bool) : Lis
     | 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 +250,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/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..6e09bae197fd 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 [*]
 
@@ -395,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
@@ -407,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/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⟩
diff --git a/src/Init/Data/Vector/Monadic.lean b/src/Init/Data/Vector/Monadic.lean
index 438745abfbda..18dfdc5b1592 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
@@ -215,4 +221,30 @@ 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
+
+/-! ### 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