From 6c2573fc381e601270feba06eb51021ba1b6fd6d Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Fri, 31 Jan 2025 18:25:24 +1100
Subject: [PATCH] feat: alignment of lemmas about monadic functions on
 `List/Array/Vector` (#6883)

This PR completes the alignment of lemmas about monadic functions on
`List/Array/Vector`. Amongst other changes, we change the simp normal
form from `List.forM` to `ForM.forM`, and correct the definition of
`List.flatMapM`, which previously was returning results in the incorrect
order. There remain many gaps in the verification lemmas for monadic
functions; this PR only makes the lemmas uniform across
`List/Array/Vector`.
---
 src/Init/Control/Lawful.lean        |   1 +
 src/Init/Control/Lawful/Lemmas.lean |  33 +++++
 src/Init/Data/Array/Attach.lean     |  28 +++-
 src/Init/Data/Array/Basic.lean      |  11 +-
 src/Init/Data/Array/Monadic.lean    | 131 ++++++++++++++---
 src/Init/Data/List/Attach.lean      |  28 +++-
 src/Init/Data/List/Control.lean     |   8 +-
 src/Init/Data/List/Monadic.lean     | 146 ++++++++++++++++++-
 src/Init/Data/List/ToArray.lean     |   5 +-
 src/Init/Data/Option/Attach.lean    |   6 +-
 src/Init/Data/Vector.lean           |   1 +
 src/Init/Data/Vector/Attach.lean    |   6 +-
 src/Init/Data/Vector/Basic.lean     |  12 +-
 src/Init/Data/Vector/Lemmas.lean    |  31 +++-
 src/Init/Data/Vector/Monadic.lean   | 217 ++++++++++++++++++++++++++++
 15 files changed, 604 insertions(+), 60 deletions(-)
 create mode 100644 src/Init/Control/Lawful/Lemmas.lean
 create mode 100644 src/Init/Data/Vector/Monadic.lean

diff --git a/src/Init/Control/Lawful.lean b/src/Init/Control/Lawful.lean
index 53641d7229..80bb869e0d 100644
--- a/src/Init/Control/Lawful.lean
+++ b/src/Init/Control/Lawful.lean
@@ -6,3 +6,4 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 prelude
 import Init.Control.Lawful.Basic
 import Init.Control.Lawful.Instances
+import Init.Control.Lawful.Lemmas
diff --git a/src/Init/Control/Lawful/Lemmas.lean b/src/Init/Control/Lawful/Lemmas.lean
new file mode 100644
index 0000000000..aaf8ecc472
--- /dev/null
+++ b/src/Init/Control/Lawful/Lemmas.lean
@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Control.Lawful.Basic
+import Init.RCases
+import Init.ByCases
+
+-- Mapping by a function with a left inverse is injective.
+theorem map_inj_of_left_inverse [Applicative m] [LawfulApplicative m] {f : α → β}
+    (w : ∃ g : β → α, ∀ x, g (f x) = x) {x y : m α}
+    (h : f <$> x = f <$> y) : x = y := by
+  rcases w with ⟨g, w⟩
+  replace h := congrArg (g <$> ·) h
+  simpa [w] using h
+
+-- Mapping by an injective function is injective, as long as the domain is nonempty.
+theorem map_inj_of_inj [Applicative m] [LawfulApplicative m] [Nonempty α] {f : α → β}
+    (w : ∀ x y, f x = f y → x = y) {x y : m α}
+    (h : f <$> x = f <$> y) : x = y := by
+  apply map_inj_of_left_inverse ?_ h
+  let ⟨a⟩ := ‹Nonempty α›
+  refine ⟨?_, ?_⟩
+  · intro b
+    by_cases p : ∃ a, f a = b
+    · exact Exists.choose p
+    · exact a
+  · intro b
+    simp only [exists_apply_eq_apply, ↓reduceDIte]
+    apply w
+    apply Exists.choose_spec (p := fun a => f a = f b)
diff --git a/src/Init/Data/Array/Attach.lean b/src/Init/Data/Array/Attach.lean
index 36ffd5fe7c..297637c8cf 100644
--- a/src/Init/Data/Array/Attach.lean
+++ b/src/Init/Data/Array/Attach.lean
@@ -291,6 +291,20 @@ theorem foldr_pmap (l : Array α) {P : α → Prop} (f : (a : α) → P a → β
     (l.pmap f H).foldr g x = l.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x := by
   rw [pmap_eq_map_attach, foldr_map]
 
+@[simp] theorem foldl_attachWith
+    (l : Array α) {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : β → { x // q x} → β} {b} (w : stop = l.size) :
+    (l.attachWith q H).foldl f b 0 stop = l.attach.foldl (fun b ⟨a, h⟩ => f b ⟨a, H _ h⟩) b := by
+  subst w
+  rcases l with ⟨l⟩
+  simp [List.foldl_attachWith, List.foldl_map]
+
+@[simp] theorem foldr_attachWith
+    (l : Array α) {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : { x // q x} → β → β} {b} (w : start = l.size) :
+    (l.attachWith q H).foldr f b start 0 = l.attach.foldr (fun a acc => f ⟨a.1, H _ a.2⟩ acc) b := by
+  subst w
+  rcases l with ⟨l⟩
+  simp [List.foldr_attachWith, List.foldr_map]
+
 /--
 If we fold over `l.attach` with a function that ignores the membership predicate,
 we get the same results as folding over `l` directly.
@@ -571,7 +585,7 @@ and simplifies these to the function directly taking the value.
 -/
 theorem foldl_subtype {p : α → Prop} {l : Array { x // p x }}
     {f : β → { x // p x } → β} {g : β → α → β} {x : β}
-    {hf : ∀ b x h, f b ⟨x, h⟩ = g b x} :
+    (hf : ∀ b x h, f b ⟨x, h⟩ = g b x) :
     l.foldl f x = l.unattach.foldl g x := by
   cases l
   simp only [List.foldl_toArray', List.unattach_toArray]
@@ -581,7 +595,7 @@ theorem foldl_subtype {p : α → Prop} {l : Array { x // p x }}
 /-- Variant of `foldl_subtype` with side condition to check `stop = l.size`. -/
 @[simp] theorem foldl_subtype' {p : α → Prop} {l : Array { x // p x }}
     {f : β → { x // p x } → β} {g : β → α → β} {x : β}
-    {hf : ∀ b x h, f b ⟨x, h⟩ = g b x} (h : stop = l.size) :
+    (hf : ∀ b x h, f b ⟨x, h⟩ = g b x) (h : stop = l.size) :
     l.foldl f x 0 stop = l.unattach.foldl g x := by
   subst h
   rwa [foldl_subtype]
@@ -592,7 +606,7 @@ and simplifies these to the function directly taking the value.
 -/
 theorem foldr_subtype {p : α → Prop} {l : Array { x // p x }}
     {f : { x // p x } → β → β} {g : α → β → β} {x : β}
-    {hf : ∀ x h b, f ⟨x, h⟩ b = g x b} :
+    (hf : ∀ x h b, f ⟨x, h⟩ b = g x b) :
     l.foldr f x = l.unattach.foldr g x := by
   cases l
   simp only [List.foldr_toArray', List.unattach_toArray]
@@ -602,7 +616,7 @@ theorem foldr_subtype {p : α → Prop} {l : Array { x // p x }}
 /-- Variant of `foldr_subtype` with side condition to check `stop = l.size`. -/
 @[simp] theorem foldr_subtype' {p : α → Prop} {l : Array { x // p x }}
     {f : { x // p x } → β → β} {g : α → β → β} {x : β}
-    {hf : ∀ x h b, f ⟨x, h⟩ b = g x b} (h : start = l.size) :
+    (hf : ∀ x h b, f ⟨x, h⟩ b = g x b) (h : start = l.size) :
     l.foldr f x start 0 = l.unattach.foldr g x := by
   subst h
   rwa [foldr_subtype]
@@ -612,7 +626,7 @@ This lemma identifies maps over arrays of subtypes, where the function only depe
 and simplifies these to the function directly taking the value.
 -/
 @[simp] theorem map_subtype {p : α → Prop} {l : Array { x // p x }}
-    {f : { x // p x } → β} {g : α → β} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
+    {f : { x // p x } → β} {g : α → β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     l.map f = l.unattach.map g := by
   cases l
   simp only [List.map_toArray, List.unattach_toArray]
@@ -620,7 +634,7 @@ and simplifies these to the function directly taking the value.
   simp [hf]
 
 @[simp] theorem filterMap_subtype {p : α → Prop} {l : Array { x // p x }}
-    {f : { x // p x } → Option β} {g : α → Option β} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
+    {f : { x // p x } → Option β} {g : α → Option β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     l.filterMap f = l.unattach.filterMap g := by
   cases l
   simp only [size_toArray, List.filterMap_toArray', List.unattach_toArray, List.length_unattach,
@@ -629,7 +643,7 @@ and simplifies these to the function directly taking the value.
   simp [hf]
 
 @[simp] theorem unattach_filter {p : α → Prop} {l : Array { x // p x }}
-    {f : { x // p x } → Bool} {g : α → Bool} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
+    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     (l.filter f).unattach = l.unattach.filter g := by
   cases l
   simp [hf]
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 473055b35f..71c396578c 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -357,6 +357,9 @@ instance : ForIn' m (Array α) α inferInstance where
 
 -- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
 
+-- We simplify `Array.forIn'` to `forIn'`.
+@[simp] theorem forIn'_eq_forIn' [Monad m] : @Array.forIn' α β m _ = forIn' := rfl
+
 /-- See comment at `forIn'Unsafe` -/
 @[inline]
 unsafe def foldlMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (as : Array α) (start := 0) (stop := as.size) : m β :=
@@ -585,11 +588,15 @@ def findRevM? {α : Type} {m : Type → Type w} [Monad m] (p : α → m Bool) (a
   as.findSomeRevM? fun a => return if (← p a) then some a else none
 
 @[inline]
-def forM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Array α) (start := 0) (stop := as.size) : m PUnit :=
+protected def forM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Array α) (start := 0) (stop := as.size) : m PUnit :=
   as.foldlM (fun _ => f) ⟨⟩ start stop
 
 instance : ForM m (Array α) α where
-  forM xs f := forM f xs
+  forM xs f := Array.forM f xs
+
+-- We simplify `Array.forM` to `forM`.
+@[simp] theorem forM_eq_forM [Monad m] (f : α → m PUnit) :
+    Array.forM f as 0 as.size = forM as f := rfl
 
 @[inline]
 def forRevM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Array α) (start := as.size) (stop := 0) : m PUnit :=
diff --git a/src/Init/Data/Array/Monadic.lean b/src/Init/Data/Array/Monadic.lean
index 0845f48d13..b3428aa201 100644
--- a/src/Init/Data/Array/Monadic.lean
+++ b/src/Init/Data/Array/Monadic.lean
@@ -20,6 +20,12 @@ open Nat
 
 /-! ### mapM -/
 
+@[simp] theorem mapM_append [Monad m] [LawfulMonad m] (f : α → m β) {l₁ l₂ : Array α} :
+    (l₁ ++ l₂).mapM f = (return (← l₁.mapM f) ++ (← l₂.mapM f)) := by
+  rcases l₁ with ⟨l₁⟩
+  rcases l₂ with ⟨l₂⟩
+  simp
+
 theorem mapM_eq_foldlM_push [Monad m] [LawfulMonad m] (f : α → m β) (l : Array α) :
     mapM f l = l.foldlM (fun acc a => return (acc.push (← f a))) #[] := by
   rcases l with ⟨l⟩
@@ -37,58 +43,85 @@ theorem mapM_eq_foldlM_push [Monad m] [LawfulMonad m] (f : α → m β) (l : Arr
 
 /-! ### foldlM and foldrM -/
 
-theorem foldlM_map [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : Array β₁) (init : α) :
-    (l.map f).foldlM g init = l.foldlM (fun x y => g x (f y)) init := by
+theorem foldlM_map [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : Array β₁) (init : α) (w : stop = l.size) :
+    (l.map f).foldlM g init 0 stop = l.foldlM (fun x y => g x (f y)) init 0 stop := by
+  subst w
   cases l
-  rw [List.map_toArray] -- Why doesn't this fire via `simp`?
   simp [List.foldlM_map]
 
 theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂ → α → m α) (l : Array β₁)
-    (init : α) : (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init := by
+    (init : α) (w : start = l.size) :
+    (l.map f).foldrM g init start 0 = l.foldrM (fun x y => g (f x) y) init start 0 := by
+  subst w
   cases l
-  rw [List.map_toArray] -- Why doesn't this fire via `simp`?
   simp [List.foldrM_map]
 
-theorem foldlM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : γ → β → m γ) (l : Array α) (init : γ) :
-    (l.filterMap f).foldlM g init =
+theorem foldlM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : γ → β → m γ)
+    (l : Array α) (init : γ) (w : stop = (l.filterMap f).size) :
+    (l.filterMap f).foldlM g init 0 stop =
       l.foldlM (fun x y => match f y with | some b => g x b | none => pure x) init := by
+  subst w
   cases l
-  rw [List.filterMap_toArray] -- Why doesn't this fire via `simp`?
   simp [List.foldlM_filterMap]
   rfl
 
-theorem foldrM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : β → γ → m γ) (l : Array α) (init : γ) :
-    (l.filterMap f).foldrM g init =
+theorem foldrM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : β → γ → m γ)
+    (l : Array α) (init : γ) (w : start = (l.filterMap f).size) :
+    (l.filterMap f).foldrM g init start 0 =
       l.foldrM (fun x y => match f x with | some b => g b y | none => pure y) init := by
+  subst w
   cases l
-  rw [List.filterMap_toArray] -- Why doesn't this fire via `simp`?
   simp [List.foldrM_filterMap]
   rfl
 
-theorem foldlM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : β → α → m β) (l : Array α) (init : β) :
-    (l.filter p).foldlM g init =
+theorem foldlM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : β → α → m β)
+    (l : Array α) (init : β) (w : stop = (l.filter p).size) :
+    (l.filter p).foldlM g init 0 stop =
       l.foldlM (fun x y => if p y then g x y else pure x) init := by
+  subst w
   cases l
-  rw [List.filter_toArray] -- Why doesn't this fire via `simp`?
   simp [List.foldlM_filter]
 
-theorem foldrM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : α → β → m β) (l : Array α) (init : β) :
-    (l.filter p).foldrM g init =
+theorem foldrM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : α → β → m β)
+    (l : Array α) (init : β) (w : start = (l.filter p).size) :
+    (l.filter p).foldrM g init start 0 =
       l.foldrM (fun x y => if p x then g x y else pure y) init := by
+  subst w
   cases l
-  rw [List.filter_toArray] -- Why doesn't this fire via `simp`?
   simp [List.foldrM_filter]
 
+@[simp] theorem foldlM_attachWith [Monad m]
+    (l : Array α) {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : β → { x // q x} → m β} {b} (w : stop = l.size):
+    (l.attachWith q H).foldlM f b 0 stop =
+      l.attach.foldlM (fun b ⟨a, h⟩ => f b ⟨a, H _ h⟩) b := by
+  subst w
+  rcases l with ⟨l⟩
+  simp [List.foldlM_map]
+
+@[simp] theorem foldrM_attachWith [Monad m] [LawfulMonad m]
+    (l : Array α) {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : { x // q x} → β → m β} {b} (w : start = l.size):
+    (l.attachWith q H).foldrM f b start 0 =
+      l.attach.foldrM (fun a acc => f ⟨a.1, H _ a.2⟩ acc) b := by
+  subst w
+  rcases l with ⟨l⟩
+  simp [List.foldrM_map]
+
 /-! ### forM -/
 
 @[congr] theorem forM_congr [Monad m] {as bs : Array α} (w : as = bs)
     {f : α → m PUnit} :
-    as.forM f = bs.forM f := by
+    forM as f = forM bs f := by
   cases as <;> cases bs
   simp_all
 
+@[simp] theorem forM_append [Monad m] [LawfulMonad m] (l₁ l₂ : Array α) (f : α → m PUnit) :
+    forM (l₁ ++ l₂) f = (do forM l₁ f; forM l₂ f) := by
+  rcases l₁ with ⟨l₁⟩
+  rcases l₂ with ⟨l₂⟩
+  simp
+
 @[simp] theorem forM_map [Monad m] [LawfulMonad m] (l : Array α) (g : α → β) (f : β → m PUnit) :
-    (l.map g).forM f = l.forM (fun a => f (g a)) := by
+    forM (l.map g) f = forM l (fun a => f (g a)) := by
   cases l
   simp
 
@@ -115,9 +148,7 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
         | .yield b => f a m b
         | .done b => pure (.done b)) (ForInStep.yield init) := by
   cases l
-  rw [List.attach_toArray] -- Why doesn't this fire via `simp`?
-  simp only [List.forIn'_toArray, List.forIn'_eq_foldlM, List.attachWith_mem_toArray, size_toArray,
-    List.length_map, List.length_attach, List.foldlM_toArray', List.foldlM_map]
+  simp [List.forIn'_eq_foldlM, List.foldlM_map]
   congr
 
 /-- We can express a for loop over an array which always yields as a fold. -/
@@ -126,7 +157,6 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
     forIn' l init (fun a m b => (fun c => .yield (g a m b c)) <$> f a m b) =
       l.attach.foldlM (fun b ⟨a, m⟩ => g a m b <$> f a m b) init := by
   cases l
-  rw [List.attach_toArray] -- Why doesn't this fire via `simp`?
   simp [List.foldlM_map]
 
 theorem forIn'_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
@@ -191,4 +221,59 @@ theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
   cases l
   simp
 
+/-! ### Recognizing higher order functions using a function that only depends on the value. -/
+
+/--
+This lemma identifies monadic folds over lists of subtypes, where the function only depends on the value, not the proposition,
+and simplifies these to the function directly taking the value.
+-/
+@[simp] theorem foldlM_subtype [Monad m] {p : α → Prop} {l : Array { x // p x }}
+    {f : β → { x // p x } → m β} {g : β → α → m β} {x : β}
+    (hf : ∀ b x h, f b ⟨x, h⟩ = g b x) (w : stop = l.size) :
+    l.foldlM f x 0 stop = l.unattach.foldlM g x 0 stop := by
+  subst w
+  rcases l with ⟨l⟩
+  simp
+  rw [List.foldlM_subtype hf]
+
+/--
+This lemma identifies monadic folds over lists of subtypes, where the function only depends on the value, not the proposition,
+and simplifies these to the function directly taking the value.
+-/
+@[simp] theorem foldrM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : Array { x // p x }}
+    {f : { x // p x } → β → m β} {g : α → β → m β} {x : β}
+    (hf : ∀ x h b, f ⟨x, h⟩ b = g x b) (w : start = l.size) :
+    l.foldrM f x start 0 = l.unattach.foldrM g x start 0:= by
+  subst w
+  rcases l with ⟨l⟩
+  simp
+  rw [List.foldrM_subtype hf]
+
+/--
+This lemma identifies monadic maps over lists of subtypes, where the function only depends on the value, not the proposition,
+and simplifies these to the function directly taking the value.
+-/
+@[simp] theorem mapM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : Array { x // p x }}
+    {f : { x // p x } → m β} {g : α → m β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    l.mapM f = l.unattach.mapM g := by
+  rcases l with ⟨l⟩
+  simp
+  rw [List.mapM_subtype hf]
+
+-- Without `filterMapM_toArray` relating `filterMapM` on `List` and `Array` we can't prove this yet:
+-- @[simp] theorem filterMapM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : Array { x // p x }}
+--     {f : { x // p x } → m (Option β)} {g : α → m (Option β)} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+--     l.filterMapM f = l.unattach.filterMapM g := by
+--   rcases l with ⟨l⟩
+--   simp
+--   rw [List.filterMapM_subtype hf]
+
+-- Without `flatMapM_toArray` relating `flatMapM` on `List` and `Array` we can't prove this yet:
+-- @[simp] theorem flatMapM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : Array { x // p x }}
+--     {f : { x // p x } → m (Array β)} {g : α → m (Array β)} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+--     (l.flatMapM f) = l.unattach.flatMapM g := by
+--   rcases l with ⟨l⟩
+--   simp
+--   rw [List.flatMapM_subtype hf]
+
 end Array
diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean
index e54de34b65..1a52badee3 100644
--- a/src/Init/Data/List/Attach.lean
+++ b/src/Init/Data/List/Attach.lean
@@ -361,6 +361,20 @@ theorem foldr_pmap (l : List α) {P : α → Prop} (f : (a : α) → P a → β)
     (l.pmap f H).foldr g x = l.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x := by
   rw [pmap_eq_map_attach, foldr_map]
 
+@[simp] theorem foldl_attachWith
+    (l : List α) {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : β → { x // q x} → β} {b} :
+    (l.attachWith q H).foldl f b = l.attach.foldl (fun b ⟨a, h⟩ => f b ⟨a, H _ h⟩) b := by
+  induction l generalizing b with
+  | nil => simp
+  | cons a l ih => simp [ih, foldl_map]
+
+@[simp] theorem foldr_attachWith
+    (l : List α) {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : { x // q x} → β → β} {b} :
+    (l.attachWith q H).foldr f b = l.attach.foldr (fun a acc => f ⟨a.1, H _ a.2⟩ acc) b := by
+  induction l generalizing b with
+  | nil => simp
+  | cons a l ih => simp [ih, foldr_map]
+
 /--
 If we fold over `l.attach` with a function that ignores the membership predicate,
 we get the same results as folding over `l` directly.
@@ -676,7 +690,7 @@ and simplifies these to the function directly taking the value.
 -/
 @[simp] theorem foldl_subtype {p : α → Prop} {l : List { x // p x }}
     {f : β → { x // p x } → β} {g : β → α → β} {x : β}
-    {hf : ∀ b x h, f b ⟨x, h⟩ = g b x} :
+    (hf : ∀ b x h, f b ⟨x, h⟩ = g b x) :
     l.foldl f x = l.unattach.foldl g x := by
   unfold unattach
   induction l generalizing x with
@@ -689,7 +703,7 @@ and simplifies these to the function directly taking the value.
 -/
 @[simp] theorem foldr_subtype {p : α → Prop} {l : List { x // p x }}
     {f : { x // p x } → β → β} {g : α → β → β} {x : β}
-    {hf : ∀ x h b, f ⟨x, h⟩ b = g x b} :
+    (hf : ∀ x h b, f ⟨x, h⟩ b = g x b) :
     l.foldr f x = l.unattach.foldr g x := by
   unfold unattach
   induction l generalizing x with
@@ -701,7 +715,7 @@ This lemma identifies maps over lists of subtypes, where the function only depen
 and simplifies these to the function directly taking the value.
 -/
 @[simp] theorem map_subtype {p : α → Prop} {l : List { x // p x }}
-    {f : { x // p x } → β} {g : α → β} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
+    {f : { x // p x } → β} {g : α → β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     l.map f = l.unattach.map g := by
   unfold unattach
   induction l with
@@ -709,7 +723,7 @@ and simplifies these to the function directly taking the value.
   | cons a l ih => simp [ih, hf]
 
 @[simp] theorem filterMap_subtype {p : α → Prop} {l : List { x // p x }}
-    {f : { x // p x } → Option β} {g : α → Option β} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
+    {f : { x // p x } → Option β} {g : α → Option β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     l.filterMap f = l.unattach.filterMap g := by
   unfold unattach
   induction l with
@@ -717,7 +731,7 @@ and simplifies these to the function directly taking the value.
   | cons a l ih => simp [ih, hf, filterMap_cons]
 
 @[simp] theorem flatMap_subtype {p : α → Prop} {l : List { x // p x }}
-    {f : { x // p x } → List β} {g : α → List β} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
+    {f : { x // p x } → List β} {g : α → List β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     (l.flatMap f) = l.unattach.flatMap g := by
   unfold unattach
   induction l with
@@ -726,6 +740,8 @@ and simplifies these to the function directly taking the value.
 
 @[deprecated flatMap_subtype (since := "2024-10-16")] abbrev bind_subtype := @flatMap_subtype
 
+/-! ### Simp lemmas pushing `unattach` inwards. -/
+
 @[simp] theorem unattach_filter {p : α → Prop} {l : List { x // p x }}
     {f : { x // p x } → Bool} {g : α → Bool} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
     (l.filter f).unattach = l.unattach.filter g := by
@@ -735,8 +751,6 @@ and simplifies these to the function directly taking the value.
     simp only [filter_cons, hf, unattach_cons]
     split <;> simp [ih]
 
-/-! ### Simp lemmas pushing `unattach` inwards. -/
-
 @[simp] theorem unattach_reverse {p : α → Prop} {l : List { x // p x }} :
     l.reverse.unattach = l.unattach.reverse := by
   simp [unattach, -map_subtype]
diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean
index 0462b8b8e5..8b7d1a35c5 100644
--- a/src/Init/Data/List/Control.lean
+++ b/src/Init/Data/List/Control.lean
@@ -144,10 +144,10 @@ concatenation of the results.
 @[inline]
 def flatMapM {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (List β)) (as : List α) : m (List β) :=
   let rec @[specialize] loop
-    | [],     bs => pure bs.reverse
+    | [],     bs => pure bs.reverse.flatten
     | a :: as, bs => do
       let bs' ← f a
-      loop as (bs' ++ bs)
+      loop as (bs' :: bs)
   loop as []
 
 /--
@@ -284,6 +284,7 @@ instance : ForIn' m (List α) α inferInstance where
 
 -- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
 
+-- We simplify `List.forIn'` to `forIn'`.
 @[simp] theorem forIn'_eq_forIn' [Monad m] : @List.forIn' α β m _ = forIn' := rfl
 
 @[simp] theorem forIn'_nil [Monad m] (f : (a : α) → a ∈ [] → β → m (ForInStep β)) (b : β) : forIn' [] b f = pure b :=
@@ -295,6 +296,9 @@ instance : ForIn' m (List α) α inferInstance where
 instance : ForM m (List α) α where
   forM := List.forM
 
+-- We simplify `List.forM` to `forM`.
+@[simp] theorem forM_eq_forM [Monad m] : @List.forM m _ α = forM := rfl
+
 @[simp] theorem forM_nil  [Monad m] (f : α → m PUnit) : forM [] f = pure ⟨⟩ :=
   rfl
 @[simp] theorem forM_cons [Monad m] (f : α → m PUnit) (a : α) (as : List α) : forM (a::as) f = f a >>= fun _ => forM as f :=
diff --git a/src/Init/Data/List/Monadic.lean b/src/Init/Data/List/Monadic.lean
index 17bd52f715..92b43444ee 100644
--- a/src/Init/Data/List/Monadic.lean
+++ b/src/Init/Data/List/Monadic.lean
@@ -80,6 +80,63 @@ theorem mapM_eq_reverse_foldlM_cons [Monad m] [LawfulMonad m] (f : α → m β)
       reverse_cons, reverse_nil, nil_append, singleton_append]
     simp [bind_pure_comp]
 
+/-! ### filterMapM -/
+
+@[simp] theorem filterMapM_nil [Monad m] (f : α → m (Option β)) : [].filterMapM f = pure [] := rfl
+
+theorem filterMapM_loop_eq [Monad m] [LawfulMonad m]
+    (f : α → m (Option β)) (l : List α) (acc : List β) :
+    filterMapM.loop f l acc = (acc.reverse ++ ·) <$> filterMapM.loop f l [] := by
+  induction l generalizing acc with
+  | nil => simp [filterMapM.loop]
+  | cons a l ih =>
+    simp only [filterMapM.loop, _root_.map_bind]
+    congr
+    funext b?
+    split <;> rename_i b
+    · apply ih
+    · rw [ih, ih [b]]
+      simp
+
+@[simp] theorem filterMapM_cons [Monad m] [LawfulMonad m] (f : α → m (Option β)) :
+    (a :: l).filterMapM f = do
+      match (← f a) with
+      | none => filterMapM f l
+      | some b => return (b :: (← filterMapM f l)) := by
+  conv => lhs; unfold filterMapM; unfold filterMapM.loop
+  congr
+  funext b?
+  split <;> rename_i b
+  · simp [filterMapM]
+  · simp only [bind_pure_comp]
+    rw [filterMapM_loop_eq, filterMapM]
+    simp
+
+/-! ### flatMapM -/
+
+@[simp] theorem flatMapM_nil [Monad m] (f : α → m (List β)) : [].flatMapM f = pure [] := rfl
+
+theorem flatMapM_loop_eq [Monad m] [LawfulMonad m] (f : α → m (List β)) (l : List α) (acc : List (List β)) :
+    flatMapM.loop f l acc = (acc.reverse.flatten ++ ·) <$> flatMapM.loop f l [] := by
+  induction l generalizing acc with
+  | nil => simp [flatMapM.loop]
+  | cons a l ih =>
+    simp only [flatMapM.loop, append_nil, _root_.map_bind]
+    congr
+    funext bs
+    rw [ih, ih [bs]]
+    simp
+
+@[simp] theorem flatMapM_cons [Monad m] [LawfulMonad m] (f : α → m (List β)) :
+    (a :: l).flatMapM f = do
+      let bs ← f a
+      return (bs ++ (← l.flatMapM f)) := by
+  conv => lhs; unfold flatMapM; unfold flatMapM.loop
+  congr
+  funext bs
+  rw [flatMapM_loop_eq, flatMapM]
+  simp
+
 /-! ### foldlM and foldrM -/
 
 theorem foldlM_map [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : List β₁) (init : α) :
@@ -126,24 +183,36 @@ theorem foldrM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : α → β
     simp only [filter_cons, foldrM_cons]
     split <;> simp [ih]
 
+@[simp] theorem foldlM_attachWith [Monad m]
+    (l : List α) {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : β → { x // q x} → m β} {b} :
+    (l.attachWith q H).foldlM f b = l.attach.foldlM (fun b ⟨a, h⟩ => f b ⟨a, H _ h⟩) b := by
+  induction l generalizing b with
+  | nil => simp
+  | cons a l ih => simp [ih, foldlM_map]
+
+@[simp] theorem foldrM_attachWith [Monad m] [LawfulMonad m]
+    (l : List α) {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : { x // q x} → β → m β} {b} :
+    (l.attachWith q H).foldrM f b = l.attach.foldrM (fun a acc => f ⟨a.1, H _ a.2⟩ acc) b := by
+  induction l generalizing b with
+  | nil => simp
+  | cons a l ih => simp [ih, foldrM_map]
+
 /-! ### forM -/
 
--- We currently use `List.forM` as the simp normal form, rather that `ForM.forM`.
--- (This should probably be revisited.)
--- As such we need to replace `List.forM_nil` and `List.forM_cons`:
+@[deprecated forM_nil (since := "2025-01-31")]
+theorem forM_nil' [Monad m] : ([] : List α).forM f = (pure .unit : m PUnit) := rfl
 
-@[simp] theorem forM_nil' [Monad m] : ([] : List α).forM f = (pure .unit : m PUnit) := rfl
-
-@[simp] theorem forM_cons' [Monad m] :
+@[deprecated forM_cons (since := "2025-01-31")]
+theorem forM_cons' [Monad m] :
     (a::as).forM f = (f a >>= fun _ => as.forM f : m PUnit) :=
   List.forM_cons _ _ _
 
 @[simp] theorem forM_append [Monad m] [LawfulMonad m] (l₁ l₂ : List α) (f : α → m PUnit) :
-    (l₁ ++ l₂).forM f = (do l₁.forM f; l₂.forM f) := by
+    forM (l₁ ++ l₂) f = (do forM l₁ f; forM l₂ f) := by
   induction l₁ <;> simp [*]
 
 @[simp] theorem forM_map [Monad m] [LawfulMonad m] (l : List α) (g : α → β) (f : β → m PUnit) :
-    (l.map g).forM f = l.forM (fun a => f (g a)) := by
+    forM (l.map g) f = forM l (fun a => f (g a)) := by
   induction l <;> simp [*]
 
 /-! ### forIn' -/
@@ -338,4 +407,65 @@ theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as :
     funext b
     split <;> simp_all
 
+/-! ### Recognizing higher order functions using a function that only depends on the value. -/
+
+/--
+This lemma identifies monadic folds over lists of subtypes, where the function only depends on the value, not the proposition,
+and simplifies these to the function directly taking the value.
+-/
+@[simp] theorem foldlM_subtype [Monad m] {p : α → Prop} {l : List { x // p x }}
+    {f : β → { x // p x } → m β} {g : β → α → m β} {x : β}
+    (hf : ∀ b x h, f b ⟨x, h⟩ = g b x) :
+    l.foldlM f x = l.unattach.foldlM g x := by
+  unfold unattach
+  induction l generalizing x with
+  | nil => simp
+  | cons a l ih => simp [ih, hf]
+
+/--
+This lemma identifies monadic folds over lists of subtypes, where the function only depends on the value, not the proposition,
+and simplifies these to the function directly taking the value.
+-/
+@[simp] theorem foldrM_subtype [Monad m] [LawfulMonad m]{p : α → Prop} {l : List { x // p x }}
+    {f : { x // p x } → β → m β} {g : α → β → m β} {x : β}
+    (hf : ∀ x h b, f ⟨x, h⟩ b = g x b) :
+    l.foldrM f x = l.unattach.foldrM g x := by
+  unfold unattach
+  induction l generalizing x with
+  | nil => simp
+  | cons a l ih =>
+    simp [ih, hf, foldrM_cons]
+    congr
+    funext b
+    simp [hf]
+
+/--
+This lemma identifies monadic maps over lists of subtypes, where the function only depends on the value, not the proposition,
+and simplifies these to the function directly taking the value.
+-/
+@[simp] theorem mapM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : List { x // p x }}
+    {f : { x // p x } → m β} {g : α → m β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    l.mapM f = l.unattach.mapM g := by
+  unfold unattach
+  simp [← List.mapM'_eq_mapM]
+  induction l with
+  | nil => simp
+  | cons a l ih => simp [ih, hf]
+
+@[simp] theorem filterMapM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : List { x // p x }}
+    {f : { x // p x } → m (Option β)} {g : α → m (Option β)} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    l.filterMapM f = l.unattach.filterMapM g := by
+  unfold unattach
+  induction l with
+  | nil => simp
+  | cons a l ih => simp [ih, hf, filterMapM_cons]
+
+@[simp] theorem flatMapM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : List { x // p x }}
+    {f : { x // p x } → m (List β)} {g : α → m (List β)} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    (l.flatMapM f) = l.unattach.flatMapM g := by
+  unfold unattach
+  induction l with
+  | nil => simp
+  | cons a l ih => simp [ih, hf]
+
 end List
diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean
index aa689cf6a0..c4a9a52dbb 100644
--- a/src/Init/Data/List/ToArray.lean
+++ b/src/Init/Data/List/ToArray.lean
@@ -140,9 +140,10 @@ theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
   simp only [size_toArray, foldlM_toArray']
   induction l <;> simp_all
 
+@[simp]
 theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) :
-    (l.toArray.forM f) = l.forM f := by
-  simp
+    (forM l.toArray f) = l.forM f :=
+  forM_toArray' l f rfl
 
 /-- Variant of `foldr_toArray` with a side condition for the `start` argument. -/
 @[simp] theorem foldr_toArray' (f : α → β → β) (init : β) (l : List α)
diff --git a/src/Init/Data/Option/Attach.lean b/src/Init/Data/Option/Attach.lean
index 50639ccb9f..f89e467d39 100644
--- a/src/Init/Data/Option/Attach.lean
+++ b/src/Init/Data/Option/Attach.lean
@@ -224,17 +224,17 @@ This lemma identifies maps over lists of subtypes, where the function only depen
 and simplifies these to the function directly taking the value.
 -/
 @[simp] theorem map_subtype {p : α → Prop} {o : Option { x // p x }}
-    {f : { x // p x } → β} {g : α → β} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
+    {f : { x // p x } → β} {g : α → β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     o.map f = o.unattach.map g := by
   cases o <;> simp [hf]
 
 @[simp] theorem bind_subtype {p : α → Prop} {o : Option { x // p x }}
-    {f : { x // p x } → Option β} {g : α → Option β} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
+    {f : { x // p x } → Option β} {g : α → Option β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     (o.bind f) = o.unattach.bind g := by
   cases o <;> simp [hf]
 
 @[simp] theorem unattach_filter {p : α → Prop} {o : Option { x // p x }}
-    {f : { x // p x } → Bool} {g : α → Bool} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
+    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     (o.filter f).unattach = o.unattach.filter g := by
   cases o
   · simp
diff --git a/src/Init/Data/Vector.lean b/src/Init/Data/Vector.lean
index fcbf80477a..dfd52707c5 100644
--- a/src/Init/Data/Vector.lean
+++ b/src/Init/Data/Vector.lean
@@ -14,3 +14,4 @@ import Init.Data.Vector.Zip
 import Init.Data.Vector.OfFn
 import Init.Data.Vector.Range
 import Init.Data.Vector.Erase
+import Init.Data.Vector.Monadic
diff --git a/src/Init/Data/Vector/Attach.lean b/src/Init/Data/Vector/Attach.lean
index ce77d9e164..5c0fbbe5b3 100644
--- a/src/Init/Data/Vector/Attach.lean
+++ b/src/Init/Data/Vector/Attach.lean
@@ -494,7 +494,7 @@ and simplifies these to the function directly taking the value.
 -/
 @[simp] theorem foldl_subtype {p : α → Prop} {l : Vector { x // p x } n}
     {f : β → { x // p x } → β} {g : β → α → β} {x : β}
-    {hf : ∀ b x h, f b ⟨x, h⟩ = g b x} :
+    (hf : ∀ b x h, f b ⟨x, h⟩ = g b x) :
     l.foldl f x = l.unattach.foldl g x := by
   rcases l with ⟨l, rfl⟩
   simp [Array.foldl_subtype (hf := hf)]
@@ -505,7 +505,7 @@ and simplifies these to the function directly taking the value.
 -/
 @[simp] theorem foldr_subtype {p : α → Prop} {l : Vector { x // p x } n}
     {f : { x // p x } → β → β} {g : α → β → β} {x : β}
-    {hf : ∀ x h b, f ⟨x, h⟩ b = g x b} :
+    (hf : ∀ x h b, f ⟨x, h⟩ b = g x b) :
     l.foldr f x = l.unattach.foldr g x := by
   rcases l with ⟨l, rfl⟩
   simp [Array.foldr_subtype (hf := hf)]
@@ -515,7 +515,7 @@ This lemma identifies maps over arrays of subtypes, where the function only depe
 and simplifies these to the function directly taking the value.
 -/
 @[simp] theorem map_subtype {p : α → Prop} {l : Vector { x // p x } n}
-    {f : { x // p x } → β} {g : α → β} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
+    {f : { x // p x } → β} {g : α → β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     l.map f = l.unattach.map g := by
   rcases l with ⟨l, rfl⟩
   simp [Array.map_subtype (hf := hf)]
diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean
index 5c08b02958..de8b96e91d 100644
--- a/src/Init/Data/Vector/Basic.lean
+++ b/src/Init/Data/Vector/Basic.lean
@@ -56,6 +56,9 @@ def elimAsList {motive : Vector α n → Sort u}
 /-- Makes a vector of size `n` with all cells containing `v`. -/
 @[inline] def mkVector (n) (v : α) : Vector α n := ⟨mkArray n v, by simp⟩
 
+instance : Nonempty (Vector α 0) := ⟨#v[]⟩
+instance [Nonempty α] : Nonempty (Vector α n) := ⟨mkVector _ Classical.ofNonempty⟩
+
 /-- Returns a vector of size `1` with element `v`. -/
 @[inline] def singleton (v : α) : Vector α 1 := ⟨#[v], rfl⟩
 
@@ -216,7 +219,7 @@ where
     else
       return r.cast (by omega)
 
-@[inline] def forM [Monad m] (v : Vector α n) (f : α → m PUnit) : m PUnit :=
+@[inline] protected def forM [Monad m] (v : Vector α n) (f : α → m PUnit) : m PUnit :=
   v.toArray.forM f
 
 @[inline] def flatMapM [Monad m] (v : Vector α n) (f : α → m (Vector β k)) : m (Vector β (n * k)) := do
@@ -420,7 +423,12 @@ instance : ForIn' m (Vector α n) α inferInstance where
 /-! ### ForM instance -/
 
 instance : ForM m (Vector α n) α where
-  forM := forM
+  forM := Vector.forM
+
+-- We simplify `Vector.forM` to `forM`.
+@[simp] theorem forM_eq_forM [Monad m] (f : α → m PUnit) :
+    Vector.forM v f = forM v f := rfl
+
 /-! ### ToStream instance -/
 
 instance : ToStream (Vector α n) (Subarray α) where
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index af14d71af3..eaf2dcc012 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -131,7 +131,16 @@ abbrev indexOf?_mk := @finIdxOf?_mk
       Vector.mk (a.mapFinIdx fun i a h' => f i a (by simpa [h] using h')) (by simp [h]) := rfl
 
 @[simp] theorem forM_mk [Monad m] (f : α → m PUnit) (a : Array α) (h : a.size = n) :
-    (Vector.mk a h).forM f = a.forM f := rfl
+    forM (Vector.mk a h) f = forM a f := rfl
+
+@[simp] theorem forIn'_mk [Monad m]
+    (xs : Array α) (h : xs.size = n) (b : β)
+    (f : (a : α) → a ∈ Vector.mk xs h → β → m (ForInStep β)) :
+    forIn' (Vector.mk xs h) b f = forIn' xs b (fun a m b => f a (by simpa using m) b) := rfl
+
+@[simp] theorem forIn_mk [Monad m]
+    (xs : Array α) (h : xs.size = n) (b : β) (f : (a : α) → β → m (ForInStep β)) :
+    forIn (Vector.mk xs h) b f = forIn xs b f := rfl
 
 @[simp] theorem flatMap_mk (f : α → Vector β m) (a : Array α) (h : a.size = n) :
     (Vector.mk a h).flatMap f =
@@ -259,6 +268,26 @@ abbrev zipWithIndex_mk := @zipIdx_mk
       v.toArray.mapFinIdx (fun i a h => f i a (by simpa [v.size_toArray] using h)) :=
   rfl
 
+theorem toArray_mapM_go [Monad m] [LawfulMonad m] (f : α → m β) (v : Vector α n) (i h r) :
+    toArray <$> mapM.go f v i h r = Array.mapM.map f v.toArray i r.toArray := by
+  unfold mapM.go
+  unfold Array.mapM.map
+  simp only [v.size_toArray, getElem_toArray]
+  split
+  · simp only [map_bind]
+    congr
+    funext b
+    rw [toArray_mapM_go]
+    rfl
+  · simp
+
+@[simp] theorem toArray_mapM [Monad m] [LawfulMonad m] (f : α → m β) (a : Vector α n) :
+    toArray <$> a.mapM f = a.toArray.mapM f := by
+  rcases a with ⟨a, rfl⟩
+  unfold mapM
+  rw [toArray_mapM_go]
+  rfl
+
 @[simp] theorem toArray_ofFn (f : Fin n → α) : (Vector.ofFn f).toArray = Array.ofFn f := rfl
 
 @[simp] theorem toArray_pop (a : Vector α n) : a.pop.toArray = a.toArray.pop := rfl
diff --git a/src/Init/Data/Vector/Monadic.lean b/src/Init/Data/Vector/Monadic.lean
new file mode 100644
index 0000000000..6230a721ae
--- /dev/null
+++ b/src/Init/Data/Vector/Monadic.lean
@@ -0,0 +1,217 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.Vector.Lemmas
+import Init.Data.Vector.Attach
+import Init.Data.Array.Monadic
+import Init.Control.Lawful.Lemmas
+
+/-!
+# Lemmas about `Vector.forIn'` and `Vector.forIn`.
+-/
+
+namespace Vector
+
+open Nat
+
+/-! ## Monadic operations -/
+
+theorem map_toArray_inj [Monad m] [LawfulMonad m] [Nonempty α]
+    {v₁ : m (Vector α n)} {v₂ : m (Vector α n)} (w : toArray <$> v₁ = toArray <$> v₂) :
+    v₁ = v₂ := by
+  apply map_inj_of_inj ?_ w
+  simp
+
+/-! ### mapM -/
+
+@[congr] theorem mapM_congr [Monad m] {as bs : Vector α n} (w : as = bs)
+    {f : α → m β} :
+    as.mapM f = bs.mapM f := by
+  subst w
+  simp
+
+@[simp] theorem mapM_mk_empty [Monad m] (f : α → m β)  :
+    (mk #[] rfl).mapM f = pure #v[] := by
+  unfold mapM
+  unfold mapM.go
+  simp
+
+-- The `[Nonempty β]` hypothesis should be avoidable by unfolding `mapM` directly.
+@[simp] theorem mapM_append [Monad m] [LawfulMonad m] [Nonempty β]
+    (f : α → m β) {l₁ : Vector α n} {l₂ : Vector α n'} :
+    (l₁ ++ l₂).mapM f = (return (← l₁.mapM f) ++ (← l₂.mapM f)) := by
+  apply map_toArray_inj
+  suffices toArray <$> (l₁ ++ l₂).mapM f = (return (← toArray <$> l₁.mapM f) ++ (← toArray <$> l₂.mapM f)) by
+    rw [this]
+    simp only [bind_pure_comp, Functor.map_map, bind_map_left, map_bind, toArray_append]
+  simp
+
+/-! ### foldlM and foldrM -/
+
+theorem foldlM_map [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : Vector β₁ n) (init : α) :
+    (l.map f).foldlM g init = l.foldlM (fun x y => g x (f y)) init := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.foldlM_map]
+
+theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂ → α → m α) (l : Vector β₁ n)
+    (init : α) : (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.foldrM_map]
+
+theorem foldlM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : γ → β → m γ) (l : Vector α n) (init : γ) :
+    (l.filterMap f).foldlM g init =
+      l.foldlM (fun x y => match f y with | some b => g x b | none => pure x) init := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.foldlM_filterMap]
+  rfl
+
+theorem foldrM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : β → γ → m γ) (l : Vector α n) (init : γ) :
+    (l.filterMap f).foldrM g init =
+      l.foldrM (fun x y => match f x with | some b => g b y | none => pure y) init := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.foldrM_filterMap]
+  rfl
+
+theorem foldlM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : β → α → m β) (l : Vector α n) (init : β) :
+    (l.filter p).foldlM g init =
+      l.foldlM (fun x y => if p y then g x y else pure x) init := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.foldlM_filter]
+
+theorem foldrM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : α → β → m β) (l : Vector α n) (init : β) :
+    (l.filter p).foldrM g init =
+      l.foldrM (fun x y => if p x then g x y else pure y) init := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.foldrM_filter]
+
+@[simp] theorem foldlM_attachWith [Monad m]
+    (l : Vector α n) {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : β → { x // q x} → m β} {b} :
+    (l.attachWith q H).foldlM f b = l.attach.foldlM (fun b ⟨a, h⟩ => f b ⟨a, H _ h⟩) b := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.foldlM_map]
+
+@[simp] theorem foldrM_attachWith [Monad m] [LawfulMonad m]
+    (l : Vector α n) {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : { x // q x} → β → m β} {b} :
+    (l.attachWith q H).foldrM f b = l.attach.foldrM (fun a acc => f ⟨a.1, H _ a.2⟩ acc) b := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.foldrM_map]
+
+/-! ### forM -/
+
+@[congr] theorem forM_congr [Monad m] {as bs : Vector α n} (w : as = bs)
+    {f : α → m PUnit} :
+    forM as f = forM bs f := by
+  cases as <;> cases bs
+  simp_all
+
+@[simp] theorem forM_append [Monad m] [LawfulMonad m] (l₁ : Vector α n) (l₂ : Vector α n') (f : α → m PUnit) :
+    forM (l₁ ++ l₂) f = (do forM l₁ f; forM l₂ f) := by
+  rcases l₁ with ⟨l₁, rfl⟩
+  rcases l₂ with ⟨l₂, rfl⟩
+  simp
+
+@[simp] theorem forM_map [Monad m] [LawfulMonad m] (l : Vector α n) (g : α → β) (f : β → m PUnit) :
+    forM (l.map g) f = forM l (fun a => f (g a)) := by
+  cases l
+  simp
+
+/-! ### forIn' -/
+
+@[congr] theorem forIn'_congr [Monad m] {as bs : Vector α n} (w : as = bs)
+    {b b' : β} (hb : b = b')
+    {f : (a' : α) → a' ∈ as → β → m (ForInStep β)}
+    {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)}
+    (h : ∀ a m b, f a (by simpa [w] using m) b = g a m b) :
+    forIn' as b f = forIn' bs b' g := by
+  cases as <;> cases bs
+  simp only [eq_mk, mem_mk, forIn'_mk] at w h ⊢
+  exact Array.forIn'_congr w hb h
+
+/--
+We can express a for loop over a vector as a fold,
+in which whenever we reach `.done b` we keep that value through the rest of the fold.
+-/
+theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
+    (l : Vector α n) (f : (a : α) → a ∈ l → β → m (ForInStep β)) (init : β) :
+    forIn' l init f = ForInStep.value <$>
+      l.attach.foldlM (fun b ⟨a, m⟩ => match b with
+        | .yield b => f a m b
+        | .done b => pure (.done b)) (ForInStep.yield init) := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.forIn'_eq_foldlM]
+  rfl
+
+/-- We can express a for loop over a vector which always yields as a fold. -/
+@[simp] theorem forIn'_yield_eq_foldlM [Monad m] [LawfulMonad m]
+    (l : Vector α n) (f : (a : α) → a ∈ l → β → m γ) (g : (a : α) → a ∈ l → β → γ → β) (init : β) :
+    forIn' l init (fun a m b => (fun c => .yield (g a m b c)) <$> f a m b) =
+      l.attach.foldlM (fun b ⟨a, m⟩ => g a m b <$> f a m b) init := by
+  rcases l with ⟨l, rfl⟩
+  simp
+
+theorem forIn'_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
+    (l : Vector α n) (f : (a : α) → a ∈ l → β → β) (init : β) :
+    forIn' l init (fun a m b => pure (.yield (f a m b))) =
+      pure (f := m) (l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init) := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.forIn'_pure_yield_eq_foldl, Array.foldl_map]
+
+@[simp] theorem forIn'_yield_eq_foldl
+    (l : Vector α n) (f : (a : α) → a ∈ l → β → β) (init : β) :
+    forIn' (m := Id) l init (fun a m b => .yield (f a m b)) =
+      l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init := by
+  cases l
+  simp [List.foldl_map]
+
+@[simp] theorem forIn'_map [Monad m] [LawfulMonad m]
+    (l : Vector α n) (g : α → β) (f : (b : β) → b ∈ l.map g → γ → m (ForInStep γ)) :
+    forIn' (l.map g) init f = forIn' l init fun a h y => f (g a) (mem_map_of_mem g h) y := by
+  cases l
+  simp
+
+/--
+We can express a for loop over a vector as a fold,
+in which whenever we reach `.done b` we keep that value through the rest of the fold.
+-/
+theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
+    (f : α → β → m (ForInStep β)) (init : β) (l : Vector α n) :
+    forIn l init f = ForInStep.value <$>
+      l.foldlM (fun b a => match b with
+        | .yield b => f a b
+        | .done b => pure (.done b)) (ForInStep.yield init) := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.forIn_eq_foldlM]
+  rfl
+
+/-- We can express a for loop over a vector which always yields as a fold. -/
+@[simp] theorem forIn_yield_eq_foldlM [Monad m] [LawfulMonad m]
+    (l : Vector α n) (f : α → β → m γ) (g : α → β → γ → β) (init : β) :
+    forIn l init (fun a b => (fun c => .yield (g a b c)) <$> f a b) =
+      l.foldlM (fun b a => g a b <$> f a b) init := by
+  cases l
+  simp
+
+theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
+    (l : Vector α n) (f : α → β → β) (init : β) :
+    forIn l init (fun a b => pure (.yield (f a b))) =
+      pure (f := m) (l.foldl (fun b a => f a b) init) := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.forIn_pure_yield_eq_foldl, Array.foldl_map]
+
+@[simp] theorem forIn_yield_eq_foldl
+    (l : Vector α n) (f : α → β → β) (init : β) :
+    forIn (m := Id) l init (fun a b => .yield (f a b)) =
+      l.foldl (fun b a => f a b) init := by
+  cases l
+  simp
+
+@[simp] theorem forIn_map [Monad m] [LawfulMonad m]
+    (l : Vector α n) (g : α → β) (f : β → γ → m (ForInStep γ)) :
+    forIn (l.map g) init f = forIn l init fun a y => f (g a) y := by
+  cases l
+  simp
+
+end Vector