diff --git a/src/Init/Data/Array.lean b/src/Init/Data/Array.lean
index ab2e05a270..c0f92afdbb 100644
--- a/src/Init/Data/Array.lean
+++ b/src/Init/Data/Array.lean
@@ -18,3 +18,4 @@ import Init.Data.Array.Bootstrap
 import Init.Data.Array.GetLit
 import Init.Data.Array.MapIdx
 import Init.Data.Array.Set
+import Init.Data.Array.Monadic
diff --git a/src/Init/Data/Array/Attach.lean b/src/Init/Data/Array/Attach.lean
index d34780a93c..bfac53ff1c 100644
--- a/src/Init/Data/Array/Attach.lean
+++ b/src/Init/Data/Array/Attach.lean
@@ -43,6 +43,13 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
     l.attach.toList = l.toList.attachWith (· ∈ l) (by simp [mem_toList]) := by
   simp [attach]
 
+@[simp] theorem _root_.List.attachWith_mem_toArray {l : List α} :
+    l.attachWith (fun x => x ∈ l.toArray) (fun x h => by simpa using h) =
+      l.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
+  simp only [List.attachWith, List.attach, List.map_pmap]
+  apply List.pmap_congr_left
+  simp
+
 /-! ## unattach
 
 `Array.unattach` is the (one-sided) inverse of `Array.attach`. It is a synonym for `Array.map Subtype.val`.
@@ -83,7 +90,7 @@ def unattach {α : Type _} {p : α → Prop} (l : Array { x // p x }) := l.map (
 
 @[simp] theorem unattach_attach {l : Array α} : l.attach.unattach = l := by
   cases l
-  simp
+  simp only [List.attach_toArray, List.unattach_toArray, List.unattach_attachWith]
 
 @[simp] theorem unattach_attachWith {p : α → Prop} {l : Array α}
     {H : ∀ a ∈ l, p a} :
diff --git a/src/Init/Data/Array/Bootstrap.lean b/src/Init/Data/Array/Bootstrap.lean
index 09686e2b09..2cefb7db4d 100644
--- a/src/Init/Data/Array/Bootstrap.lean
+++ b/src/Init/Data/Array/Bootstrap.lean
@@ -15,26 +15,26 @@ This file contains some theorems about `Array` and `List` needed for `Init.Data.
 
 namespace Array
 
-theorem foldlM_eq_foldlM_toList.aux [Monad m]
+theorem foldlM_toList.aux [Monad m]
     (f : β → α → m β) (arr : Array α) (i j) (H : arr.size ≤ i + j) (b) :
     foldlM.loop f arr arr.size (Nat.le_refl _) i j b = (arr.toList.drop j).foldlM f b := by
   unfold foldlM.loop
   split; split
   · cases Nat.not_le_of_gt ‹_› (Nat.zero_add _ ▸ H)
   · rename_i i; rw [Nat.succ_add] at H
-    simp [foldlM_eq_foldlM_toList.aux f arr i (j+1) H]
+    simp [foldlM_toList.aux f arr i (j+1) H]
     rw (occs := .pos [2]) [← List.getElem_cons_drop_succ_eq_drop ‹_›]
     rfl
   · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
 
-theorem foldlM_eq_foldlM_toList [Monad m]
+@[simp] theorem foldlM_toList [Monad m]
     (f : β → α → m β) (init : β) (arr : Array α) :
-    arr.foldlM f init = arr.toList.foldlM f init := by
-  simp [foldlM, foldlM_eq_foldlM_toList.aux]
+    arr.toList.foldlM f init = arr.foldlM f init := by
+  simp [foldlM, foldlM_toList.aux]
 
-theorem foldl_eq_foldl_toList (f : β → α → β) (init : β) (arr : Array α) :
-    arr.foldl f init = arr.toList.foldl f init :=
-  List.foldl_eq_foldlM .. ▸ foldlM_eq_foldlM_toList ..
+@[simp] theorem foldl_toList (f : β → α → β) (init : β) (arr : Array α) :
+    arr.toList.foldl f init = arr.foldl f init :=
+  List.foldl_eq_foldlM .. ▸ foldlM_toList ..
 
 theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
     (f : α → β → m β) (arr : Array α) (init : β) (i h) :
@@ -51,23 +51,23 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init
   match arr, this with | _, .inl rfl => rfl | arr, .inr h => ?_
   simp [foldrM, h, ← foldrM_eq_reverse_foldlM_toList.aux, List.take_length]
 
-theorem foldrM_eq_foldrM_toList [Monad m]
+@[simp] theorem foldrM_toList [Monad m]
     (f : α → β → m β) (init : β) (arr : Array α) :
-    arr.foldrM f init = arr.toList.foldrM f init := by
+    arr.toList.foldrM f init = arr.foldrM f init := by
   rw [foldrM_eq_reverse_foldlM_toList, List.foldlM_reverse]
 
-theorem foldr_eq_foldr_toList (f : α → β → β) (init : β) (arr : Array α) :
-    arr.foldr f init = arr.toList.foldr f init :=
-  List.foldr_eq_foldrM .. ▸ foldrM_eq_foldrM_toList ..
+@[simp] theorem foldr_toList (f : α → β → β) (init : β) (arr : Array α) :
+    arr.toList.foldr f init = arr.foldr f init :=
+  List.foldr_eq_foldrM .. ▸ foldrM_toList ..
 
 @[simp] theorem push_toList (arr : Array α) (a : α) : (arr.push a).toList = arr.toList ++ [a] := by
   simp [push, List.concat_eq_append]
 
 @[simp] theorem toListAppend_eq (arr : Array α) (l) : arr.toListAppend l = arr.toList ++ l := by
-  simp [toListAppend, foldr_eq_foldr_toList]
+  simp [toListAppend, ← foldr_toList]
 
 @[simp] theorem toListImpl_eq (arr : Array α) : arr.toListImpl = arr.toList := by
-  simp [toListImpl, foldr_eq_foldr_toList]
+  simp [toListImpl, ← foldr_toList]
 
 @[simp] theorem pop_toList (arr : Array α) : arr.pop.toList = arr.toList.dropLast := rfl
 
@@ -76,7 +76,7 @@ theorem foldr_eq_foldr_toList (f : α → β → β) (init : β) (arr : Array α
 @[simp] theorem toList_append (arr arr' : Array α) :
     (arr ++ arr').toList = arr.toList ++ arr'.toList := by
   rw [← append_eq_append]; unfold Array.append
-  rw [foldl_eq_foldl_toList]
+  rw [← foldl_toList]
   induction arr'.toList generalizing arr <;> simp [*]
 
 @[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl
@@ -98,20 +98,44 @@ theorem foldr_eq_foldr_toList (f : α → β → β) (init : β) (arr : Array α
   rw [← appendList_eq_append]; unfold Array.appendList
   induction l generalizing arr <;> simp [*]
 
-@[deprecated foldlM_eq_foldlM_toList (since := "2024-09-09")]
-abbrev foldlM_eq_foldlM_data := @foldlM_eq_foldlM_toList
+@[deprecated "Use the reverse direction of `foldrM_toList`." (since := "2024-11-13")]
+theorem foldrM_eq_foldrM_toList [Monad m]
+    (f : α → β → m β) (init : β) (arr : Array α) :
+    arr.foldrM f init = arr.toList.foldrM f init := by
+  simp
 
-@[deprecated foldl_eq_foldl_toList (since := "2024-09-09")]
-abbrev foldl_eq_foldl_data := @foldl_eq_foldl_toList
+@[deprecated "Use the reverse direction of `foldlM_toList`." (since := "2024-11-13")]
+theorem foldlM_eq_foldlM_toList [Monad m]
+    (f : β → α → m β) (init : β) (arr : Array α) :
+    arr.foldlM f init = arr.toList.foldlM f init:= by
+  simp
+
+@[deprecated "Use the reverse direction of `foldr_toList`." (since := "2024-11-13")]
+theorem foldr_eq_foldr_toList
+    (f : α → β → β) (init : β) (arr : Array α) :
+    arr.foldr f init = arr.toList.foldr f init := by
+  simp
+
+@[deprecated "Use the reverse direction of `foldl_toList`." (since := "2024-11-13")]
+theorem foldl_eq_foldl_toList
+    (f : β → α → β) (init : β) (arr : Array α) :
+    arr.foldl f init = arr.toList.foldl f init:= by
+  simp
+
+@[deprecated foldlM_toList (since := "2024-09-09")]
+abbrev foldlM_eq_foldlM_data := @foldlM_toList
+
+@[deprecated foldl_toList (since := "2024-09-09")]
+abbrev foldl_eq_foldl_data := @foldl_toList
 
 @[deprecated foldrM_eq_reverse_foldlM_toList (since := "2024-09-09")]
 abbrev foldrM_eq_reverse_foldlM_data := @foldrM_eq_reverse_foldlM_toList
 
-@[deprecated foldrM_eq_foldrM_toList (since := "2024-09-09")]
-abbrev foldrM_eq_foldrM_data := @foldrM_eq_foldrM_toList
+@[deprecated foldrM_toList (since := "2024-09-09")]
+abbrev foldrM_eq_foldrM_data := @foldrM_toList
 
-@[deprecated foldr_eq_foldr_toList (since := "2024-09-09")]
-abbrev foldr_eq_foldr_data := @foldr_eq_foldr_toList
+@[deprecated foldr_toList (since := "2024-09-09")]
+abbrev foldr_eq_foldr_data := @foldr_toList
 
 @[deprecated push_toList (since := "2024-09-09")]
 abbrev push_data := @push_toList
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index edd111714e..955bc8d1aa 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -151,15 +151,15 @@ theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List
 
 theorem foldlM_toArray [Monad m] (f : β → α → m β) (init : β) (l : List α) :
     l.toArray.foldlM f init = l.foldlM f init := by
-  rw [foldlM_eq_foldlM_toList]
+  rw [foldlM_toList]
 
 theorem foldr_toArray (f : α → β → β) (init : β) (l : List α) :
     l.toArray.foldr f init = l.foldr f init := by
-  rw [foldr_eq_foldr_toList]
+  rw [foldr_toList]
 
 theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
     l.toArray.foldl f init = l.foldl f init := by
-  rw [foldl_eq_foldl_toList]
+  rw [foldl_toList]
 
 /-- Variant of `foldrM_toArray` with a side condition for the `start` argument. -/
 @[simp] theorem foldrM_toArray' [Monad m] (f : α → β → m β) (init : β) (l : List α)
@@ -174,21 +174,21 @@ theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
     (h : stop = l.toArray.size) :
     l.toArray.foldlM f init 0 stop = l.foldlM f init := by
   subst h
-  rw [foldlM_eq_foldlM_toList]
+  rw [foldlM_toList]
 
 /-- Variant of `foldr_toArray` with a side condition for the `start` argument. -/
 @[simp] theorem foldr_toArray' (f : α → β → β) (init : β) (l : List α)
     (h : start = l.toArray.size) :
     l.toArray.foldr f init start 0 = l.foldr f init := by
   subst h
-  rw [foldr_eq_foldr_toList]
+  rw [foldr_toList]
 
 /-- Variant of `foldl_toArray` with a side condition for the `stop` argument. -/
 @[simp] theorem foldl_toArray' (f : β → α → β) (init : β) (l : List α)
     (h : stop = l.toArray.size) :
     l.toArray.foldl f init 0 stop = l.foldl f init := by
   subst h
-  rw [foldl_eq_foldl_toList]
+  rw [foldl_toList]
 
 @[simp] theorem append_toArray (l₁ l₂ : List α) :
     l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
@@ -202,6 +202,9 @@ theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
 @[simp] theorem foldl_push {l : List α} {as : Array α} : l.foldl Array.push as = as ++ l.toArray := by
   induction l generalizing as <;> simp [*]
 
+@[simp] theorem foldr_push {l : List α} {as : Array α} : l.foldr (fun a b => push b a) as = as ++ l.reverse.toArray := by
+  rw [foldr_eq_foldl_reverse, foldl_push]
+
 @[simp] theorem findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :
     l.toArray.findSomeM? f = l.findSomeM? f := by
   rw [Array.findSomeM?]
@@ -362,7 +365,8 @@ namespace Array
 
 theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
     (arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
-  simp [foldrM_eq_reverse_foldlM_toList, -size_push]
+  simp only [foldrM_eq_reverse_foldlM_toList, push_toList, List.reverse_append, List.reverse_cons,
+    List.reverse_nil, List.nil_append, List.singleton_append, List.foldlM_cons, List.foldlM_reverse]
 
 /--
 Variant of `foldrM_push` with `h : start = arr.size + 1`
@@ -388,11 +392,11 @@ rather than `(arr.push a).size` as the argument.
 @[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) []
 
 @[simp] theorem toListRev_eq (arr : Array α) : arr.toListRev = arr.toList.reverse := by
-  rw [toListRev, foldl_eq_foldl_toList, ← List.foldr_reverse, List.foldr_cons_nil]
+  rw [toListRev, ← foldl_toList, ← List.foldr_reverse, List.foldr_cons_nil]
 
 theorem mapM_eq_foldlM [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
     arr.mapM f = arr.foldlM (fun bs a => bs.push <$> f a) #[] := by
-  rw [mapM, aux, foldlM_eq_foldlM_toList]; rfl
+  rw [mapM, aux, ← foldlM_toList]; rfl
 where
   aux (i r) :
       mapM.map f arr i r = (arr.toList.drop i).foldlM (fun bs a => bs.push <$> f a) r := by
@@ -407,7 +411,7 @@ where
 
 @[simp] theorem toList_map (f : α → β) (arr : Array α) : (arr.map f).toList = arr.toList.map f := by
   rw [map, mapM_eq_foldlM]
-  apply congrArg toList (foldl_eq_foldl_toList (fun bs a => push bs (f a)) #[] arr) |>.trans
+  apply congrArg toList (foldl_toList (fun bs a => push bs (f a)) #[] arr).symm |>.trans
   have H (l arr) : List.foldl (fun bs a => push bs (f a)) arr l = ⟨arr.toList ++ l.map f⟩ := by
     induction l generalizing arr <;> simp [*]
   simp [H]
@@ -1023,7 +1027,7 @@ theorem foldr_congr {as bs : Array α} (h₀ : as = bs) {f g : α → β → β}
 
 theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
     arr.mapM f = List.toArray <$> (arr.toList.mapM f) := by
-  rw [mapM_eq_foldlM, foldlM_eq_foldlM_toList, ← List.foldrM_reverse]
+  rw [mapM_eq_foldlM, ← foldlM_toList, ← List.foldrM_reverse]
   conv => rhs; rw [← List.reverse_reverse arr.toList]
   induction arr.toList.reverse with
   | nil => simp
@@ -1148,7 +1152,7 @@ theorem getElem?_modify {as : Array α} {i : Nat} {f : α → α} {j : Nat} :
 @[simp] theorem toList_filter (p : α → Bool) (l : Array α) :
     (l.filter p).toList = l.toList.filter p := by
   dsimp only [filter]
-  rw [foldl_eq_foldl_toList]
+  rw [← foldl_toList]
   generalize l.toList = l
   suffices ∀ a, (List.foldl (fun r a => if p a = true then push r a else r) a l).toList =
       a.toList ++ List.filter p l by
@@ -1179,7 +1183,7 @@ theorem filter_congr {as bs : Array α} (h : as = bs)
 @[simp] theorem toList_filterMap (f : α → Option β) (l : Array α) :
     (l.filterMap f).toList = l.toList.filterMap f := by
   dsimp only [filterMap, filterMapM]
-  rw [foldlM_eq_foldlM_toList]
+  rw [← foldlM_toList]
   generalize l.toList = l
   have this : ∀ a : Array β, (Id.run (List.foldlM (m := Id) ?_ a l)).toList =
     a.toList ++ List.filterMap f l := ?_
@@ -1258,7 +1262,7 @@ theorem getElem?_append {as bs : Array α} {n : Nat} :
 @[simp] theorem toList_flatten {l : Array (Array α)} :
     l.flatten.toList = (l.toList.map toList).flatten := by
   dsimp [flatten]
-  simp only [foldl_eq_foldl_toList]
+  simp only [← foldl_toList]
   generalize l.toList = l
   have : ∀ a : Array α, (List.foldl ?_ a l).toList = a.toList ++ ?_ := ?_
   exact this #[]
diff --git a/src/Init/Data/Array/Monadic.lean b/src/Init/Data/Array/Monadic.lean
new file mode 100644
index 0000000000..8056b54b71
--- /dev/null
+++ b/src/Init/Data/Array/Monadic.lean
@@ -0,0 +1,159 @@
+/-
+Copyright (c) 2024 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.Array.Lemmas
+import Init.Data.Array.Attach
+import Init.Data.List.Monadic
+
+/-!
+# Lemmas about `Array.forIn'` and `Array.forIn`.
+-/
+
+namespace Array
+
+open Nat
+
+/-! ## Monadic operations -/
+
+/-! ### mapM -/
+
+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⟩
+  simp only [List.mapM_toArray, bind_pure_comp, size_toArray, List.foldlM_toArray']
+  rw [List.mapM_eq_reverse_foldlM_cons]
+  simp only [bind_pure_comp, Functor.map_map]
+  suffices ∀ (k), (fun a => a.reverse.toArray) <$> List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) k l =
+      List.foldlM (fun acc a => acc.push <$> f a) k.reverse.toArray l by
+    exact this []
+  intro k
+  induction l generalizing k with
+  | nil => simp
+  | cons a as ih =>
+    simp [ih, List.foldlM_cons]
+
+/-! ### 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
+  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
+  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 =
+      l.foldlM (fun x y => match f y with | some b => g x b | none => pure x) init := by
+  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 =
+      l.foldrM (fun x y => match f x with | some b => g b y | none => pure y) init := by
+  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 =
+      l.foldlM (fun x y => if p y then g x y else pure x) init := by
+  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 =
+      l.foldrM (fun x y => if p x then g x y else pure y) init := by
+  cases l
+  rw [List.filter_toArray] -- Why doesn't this fire via `simp`?
+  simp [List.foldrM_filter]
+
+/-! ### forIn' -/
+
+/--
+We can express a for loop over an array 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 : Array α) (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
+  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]
+  congr
+
+/-- We can express a for loop over an array which always yields as a fold. -/
+@[simp] theorem forIn'_yield_eq_foldlM [Monad m] [LawfulMonad m]
+    (l : Array α) (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
+  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]
+    (l : Array α) (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
+  cases l
+  simp [List.forIn'_pure_yield_eq_foldl, List.foldl_map]
+
+@[simp] theorem forIn'_yield_eq_foldl
+    (l : Array α) (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]
+
+/--
+We can express a for loop over an array 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 : Array α) :
+    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
+  cases l
+  simp only [List.forIn_toArray, List.forIn_eq_foldlM, size_toArray, List.foldlM_toArray']
+  congr
+
+/-- We can express a for loop over an array which always yields as a fold. -/
+@[simp] theorem forIn_yield_eq_foldlM [Monad m] [LawfulMonad m]
+    (l : Array α) (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 [List.foldlM_map]
+
+theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
+    (l : Array α) (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
+  cases l
+  simp [List.forIn_pure_yield_eq_foldl, List.foldl_map]
+
+@[simp] theorem forIn_yield_eq_foldl
+    (l : Array α) (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 [List.foldl_map]
+
+end Array
diff --git a/src/Init/Data/List/Impl.lean b/src/Init/Data/List/Impl.lean
index 430321ab12..e01f043353 100644
--- a/src/Init/Data/List/Impl.lean
+++ b/src/Init/Data/List/Impl.lean
@@ -91,7 +91,7 @@ The following operations are given `@[csimp]` replacements below:
 @[specialize] def foldrTR (f : α → β → β) (init : β) (l : List α) : β := l.toArray.foldr f init
 
 @[csimp] theorem foldr_eq_foldrTR : @foldr = @foldrTR := by
-  funext α β f init l; simp [foldrTR, Array.foldr_eq_foldr_toList, -Array.size_toArray]
+  funext α β f init l; simp [foldrTR, ← Array.foldr_toList, -Array.size_toArray]
 
 /-! ### flatMap  -/
 
@@ -331,7 +331,7 @@ def enumFromTR (n : Nat) (l : List α) : List (Nat × α) :=
     | a::as, n => by
       rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as]
       simp [enumFrom, f]
-  rw [Array.foldr_eq_foldr_toList]
+  rw [← Array.foldr_toList]
   simp [go]
 
 /-! ## Other list operations -/
diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean
index 715433eefb..d10b37a527 100644
--- a/src/Std/Data/DHashMap/Internal/WF.lean
+++ b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -38,7 +38,7 @@ theorem toListModel_mkArray_nil {c} :
 @[simp]
 theorem computeSize_eq {buckets : Array (AssocList α β)} :
     computeSize buckets = (toListModel buckets).length := by
-  rw [computeSize, toListModel, List.flatMap_eq_foldl, Array.foldl_eq_foldl_toList]
+  rw [computeSize, toListModel, List.flatMap_eq_foldl, Array.foldl_toList]
   suffices ∀ (l : List (AssocList α β)) (l' : List ((a : α) × β a)),
       l.foldl (fun d b => d + b.toList.length) l'.length =
         (l.foldl (fun acc a => acc ++ a.toList) l').length
@@ -61,13 +61,13 @@ theorem isEmpty_eq_isEmpty [BEq α] [Hashable α] {m : Raw α β} (h : Raw.WFImp
 
 theorem fold_eq {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} :
     l.fold f init = l.buckets.foldl (fun acc l => l.foldl f acc) init := by
-  simp only [Raw.fold, Raw.foldM, Array.foldlM_eq_foldlM_toList, Array.foldl_eq_foldl_toList,
+  simp only [Raw.fold, Raw.foldM, ← Array.foldlM_toList, Array.foldl_toList,
     ← List.foldl_eq_foldlM, Id.run, AssocList.foldl]
 
 theorem fold_cons_apply {l : Raw α β} {acc : List γ} (f : (a : α) → β a → γ) :
     l.fold (fun acc k v => f k v :: acc) acc =
       ((toListModel l.buckets).reverse.map (fun p => f p.1 p.2)) ++ acc := by
-  rw [fold_eq, Array.foldl_eq_foldl_toList, toListModel]
+  rw [fold_eq, ← Array.foldl_toList, toListModel]
   generalize l.buckets.toList = l
   induction l generalizing acc with
   | nil => simp
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
index f72bda1ede..83f3d0770e 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
@@ -61,7 +61,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
   | nil => cases h1
   | cons hd tl ih =>
     unfold DefaultClause.ofArray at h2
-    rw [Array.foldr_eq_foldr_toList, List.toArray_toList] at h2
+    rw [← Array.foldr_toList, List.toArray_toList] at h2
     dsimp only [List.foldr] at h2
     split at h2
     · cases h2
@@ -77,7 +77,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
             · assumption
             · next heq _ _ =>
               unfold DefaultClause.ofArray
-              rw [Array.foldr_eq_foldr_toList, List.toArray_toList]
+              rw [← Array.foldr_toList, List.toArray_toList]
               exact heq
         · cases h1
           · simp only [← Option.some.inj h2]
@@ -89,7 +89,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
             apply ih
             assumption
             unfold DefaultClause.ofArray
-            rw [Array.foldr_eq_foldr_toList, List.toArray_toList]
+            rw [← Array.foldr_toList, List.toArray_toList]
             exact heq
 
 theorem CNF.Clause.convertLRAT_sat_of_sat (clause : CNF.Clause (PosFin n))
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
index c6bcc304f4..3b6cfa29e6 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
@@ -106,7 +106,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
   constructor
   · simp only [ofArray]
   · have hsize : (ofArray arr).assignments.size = n := by
-      simp only [ofArray, Array.foldl_eq_foldl_toList]
+      simp only [ofArray, ← Array.foldl_toList]
       have hb : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
       have hl (acc : Array Assignment) (ih : acc.size = n) (cOpt : Option (DefaultClause n)) (_cOpt_in_arr : cOpt ∈ arr.toList) :
         (ofArray_fold_fn acc cOpt).size = n := by rw [size_ofArray_fold_fn acc cOpt, ih]
@@ -187,7 +187,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
             exact ih i b h
     rcases List.foldlRecOn arr.toList ofArray_fold_fn (mkArray n unassigned) hb hl with ⟨_h_size, h'⟩
     intro i b h
-    simp only [ofArray, Array.foldl_eq_foldl_toList] at h
+    simp only [ofArray, ← Array.foldl_toList] at h
     exact h' i b h
 
 theorem readyForRatAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))) :
@@ -605,7 +605,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
 theorem readyForRupAdd_delete {n : Nat} (f : DefaultFormula n) (arr : Array Nat) :
     ReadyForRupAdd f → ReadyForRupAdd (delete f arr) := by
   intro h
-  rw [delete, Array.foldl_eq_foldl_toList]
+  rw [delete, ← Array.foldl_toList]
   constructor
   · have hb : f.rupUnits = #[] := h.1
     have hl (acc : DefaultFormula n) (ih : acc.rupUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.toList) :
@@ -625,7 +625,7 @@ theorem readyForRatAdd_delete {n : Nat} (f : DefaultFormula n) (arr : Array Nat)
     ReadyForRatAdd f → ReadyForRatAdd (delete f arr) := by
   intro h
   constructor
-  · rw [delete, Array.foldl_eq_foldl_toList]
+  · rw [delete, ← Array.foldl_toList]
     have hb : f.ratUnits = #[] := h.1
     have hl (acc : DefaultFormula n) (ih : acc.ratUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.toList) :
       (deleteOne acc id).ratUnits = #[] := by rw [deleteOne_preserves_ratUnits, ih]
@@ -659,7 +659,7 @@ theorem deleteOne_subset (f : DefaultFormula n) (id : Nat) (c : DefaultClause n)
 
 theorem delete_subset (f : DefaultFormula n) (arr : Array Nat) (c : DefaultClause n) :
     c ∈ toList (delete f arr) → c ∈ toList f := by
-  simp only [delete, Array.foldl_eq_foldl_toList]
+  simp only [delete, ← Array.foldl_toList]
   have hb : c ∈ toList f → c ∈ toList f := id
   have hl (f' : DefaultFormula n) (ih : c ∈ toList f' → c ∈ toList f) (id : Nat) (_ : id ∈ arr.toList) :
     c ∈ toList (deleteOne f' id) → c ∈ toList f := by intro h; exact ih <| deleteOne_subset f' id c h
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
index 1989bef8af..e4834892ae 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
@@ -739,7 +739,7 @@ theorem size_assignemnts_confirmRupHint {n : Nat} (clauses : Array (Option (Defa
 theorem size_assignments_performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) :
     (performRupCheck f rupHints).1.assignments.size = f.assignments.size := by
   simp only [performRupCheck]
-  rw [Array.foldl_eq_foldl_toList]
+  rw [← Array.foldl_toList]
   have hb : (f.assignments, ([] : CNF.Clause (PosFin n)), false, false).1.size = f.assignments.size := rfl
   have hl (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool) (hsize : acc.1.size = f.assignments.size)
     (id : Nat) (_ : id ∈ rupHints.toList) : (confirmRupHint f.clauses acc id).1.size = f.assignments.size := by
@@ -1288,7 +1288,7 @@ theorem restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_a
   have derivedLits_satisfies_invariant := derivedLitsInvariant_performRupCheck f f_assignments_size rupHints f'_assignments_size
   simp only at derivedLits_satisfies_invariant
   generalize (performRupCheck f rupHints).2.1 = derivedLits at *
-  rw [← f'_def, ← Array.foldl_eq_foldl_toList]
+  rw [← f'_def, Array.foldl_toList]
   let derivedLits_arr : Array (Literal (PosFin n)) := {toList := derivedLits}
   have derivedLits_arr_def : derivedLits_arr = {toList := derivedLits} := rfl
   have derivedLits_arr_nodup := nodup_derivedLits f f_assignments_size rupHints f'_assignments_size derivedLits
@@ -1301,7 +1301,7 @@ theorem restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_a
     clear_insert_inductive_case f f_assignments_size derivedLits_arr derivedLits_arr_nodup idx assignments ih
   rcases Array.foldl_induction motive h_base h_inductive with ⟨h_size, h⟩
   apply Array.ext
-  · rw [Array.foldl_eq_foldl_toList, size_clearUnit_foldl f'.assignments clearUnit size_clearUnit derivedLits,
+  · rw [← Array.foldl_toList, size_clearUnit_foldl f'.assignments clearUnit size_clearUnit derivedLits,
       f'_assignments_size, f_assignments_size]
   · intro i hi1 hi2
     rw [f_assignments_size] at hi2
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
index 052238e472..6e8fec9cdc 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
@@ -544,7 +544,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
     (∀ l : Literal (PosFin n), reduce c assignment = reducedToUnit l → ∀ (p : (PosFin n) → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l) := by
   let c_arr := c.clause.toArray
   have c_clause_rw : c.clause = c_arr.toList := by simp [c_arr]
-  rw [reduce, c_clause_rw, ← Array.foldl_eq_foldl_toList]
+  rw [reduce, c_clause_rw, Array.foldl_toList]
   let motive := ReducePostconditionInductionMotive c_arr assignment
   have h_base : motive 0 reducedToEmpty := by
     have : ∀ (a : PosFin n) (b : Bool), (reducedToEmpty = reducedToUnit (a, b)) = False := by intros; simp