diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
index f289a50d0a..8207f7b9bf 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
@@ -445,113 +445,292 @@ theorem Iter.toArray_mapWithPostcondition_mapWithPostcondition
   rw [IterM.toArray_mapWithPostcondition_mapWithPostcondition,
     instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
 
+section ForIn
+
+theorem Iter.forIn_filterMapWithPostcondition
+    [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadLiftT n o] [LawfulMonadLiftT n o] [Finite α Id]
+    [IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
+    {it : Iter (α := α) β} {f : β → PostconditionT n (Option β₂)} {init : γ}
+    {g : β₂ → γ → o (ForInStep γ)} :
+    forIn (it.filterMapWithPostcondition f) init g = forIn it init (fun out acc => do
+        match ← (f out).run with
+        | some c => g c acc
+        | none => return .yield acc) := by
+  simp [Iter.forIn_eq_forIn_toIterM, filterMapWithPostcondition, IterM.forIn_filterMapWithPostcondition,
+    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]; rfl
+
+theorem Iter.forIn_filterMapM
+    [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadAttach n] [WeaklyLawfulMonadAttach n]
+    [MonadLiftT n o] [LawfulMonadLiftT n o]
+    [Finite α Id] [IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
+    {it : Iter (α := α) β} {f : β → n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)} :
+    forIn (it.filterMapM f) init g = forIn it init (fun out acc => do
+        match ← f out with
+        | some c => g c acc
+        | none => return .yield acc) := by
+  simp [filterMapM, forIn_eq_forIn_toIterM, IterM.forIn_filterMapM,
+    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]; rfl
+
+theorem Iter.forIn_filterMap
+    [Monad n] [LawfulMonad n] [Finite α Id]
+    [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    {it : Iter (α := α) β} {f : β → Option β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} :
+    forIn (it.filterMap f) init g = forIn it init (fun out acc => do
+        match f out with
+        | some c => g c acc
+        | none => return .yield acc) := by
+  simp [filterMap, forIn_eq_forIn_toIterM, IterM.forIn_filterMap]; rfl
+
+theorem Iter.forIn_mapWithPostcondition
+    [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadLiftT n o] [LawfulMonadLiftT n o] [Finite α Id]
+    [IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
+    {it : Iter (α := α) β} {f : β → PostconditionT n β₂} {init : γ}
+    {g : β₂ → γ → o (ForInStep γ)} :
+    forIn (it.mapWithPostcondition f) init g =
+      forIn it init (fun out acc => do g (← (f out).run) acc) := by
+  simp [mapWithPostcondition, forIn_eq_forIn_toIterM, IterM.forIn_mapWithPostcondition,
+    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+
+theorem Iter.forIn_mapM
+    [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadAttach n] [WeaklyLawfulMonadAttach n]
+    [MonadLiftT n o] [LawfulMonadLiftT n o]
+    [Finite α Id]
+    [IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
+    {it : Iter (α := α) β} {f : β → n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)} :
+    forIn (it.mapM f) init g = forIn it init (fun out acc => do g (← f out) acc) := by
+  rw [mapM, forIn_eq_forIn_toIterM, IterM.forIn_mapM, instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+
+theorem Iter.forIn_map
+    [Monad n] [LawfulMonad n]
+    [Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    {it : Iter (α := α) β} {f : β → β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} :
+    forIn (it.map f) init g = forIn it init (fun out acc => do g (f out) acc) := by
+  simp [map, forIn_eq_forIn_toIterM, IterM.forIn_map]
+
+theorem Iter.forIn_filterWithPostcondition
+    [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadLiftT n o] [LawfulMonadLiftT n o]
+    [Finite α Id] [IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
+    {it : Iter (α := α) β} {f : β → PostconditionT n (ULift Bool)} {init : γ}
+    {g : β → γ → o (ForInStep γ)} :
+    haveI : MonadLift n o := ⟨monadLift⟩
+    forIn (it.filterWithPostcondition f) init g =
+      forIn it init (fun out acc => do if (← (f out).run).down then g out acc else return .yield acc) := by
+  simp [filterWithPostcondition, forIn_eq_forIn_toIterM, IterM.forIn_filterWithPostcondition,
+    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+
+theorem Iter.forIn_filterM
+    [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadAttach n] [WeaklyLawfulMonadAttach n]
+    [MonadLiftT n o] [LawfulMonadLiftT n o] [Finite α Id]
+    [IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
+    {it : Iter (α := α) β} {f : β → n (ULift Bool)} {init : γ} {g : β → γ → o (ForInStep γ)} :
+    forIn (it.filterM f) init g = forIn it init (fun out acc => do if (← f out).down then g out acc else return .yield acc) := by
+  simp [filterM, forIn_eq_forIn_toIterM, IterM.forIn_filterM,
+    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+
+theorem Iter.forIn_filter
+    [Monad n] [LawfulMonad n]
+    [Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    {it : Iter (α := α) β} {f : β → Bool} {init : γ} {g : β → γ → n (ForInStep γ)} :
+    forIn (it.filter f) init g = forIn it init (fun out acc => do if f out then g out acc else return .yield acc) := by
+  simp [filter, forIn_eq_forIn_toIterM, IterM.forIn_filter]
+
+end ForIn
+
 section Fold
 
-theorem Iter.foldM_filterMapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
-    [Iterator α Id β] [Finite α Id] [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m]
-    [Monad n] [LawfulMonad n]
-    [IteratorLoop α Id Id] [IteratorLoop α Id m] [IteratorLoop α Id n]
-    [MonadLiftT m n] [LawfulMonadLiftT m n]
-    [LawfulIteratorLoop α Id Id] [LawfulIteratorLoop α Id m] [LawfulIteratorLoop α Id n]
-    {f : β → m (Option γ)} {g : δ → γ → n δ} {init : δ} {it : Iter (α := α) β} :
+theorem Iter.foldM_filterMapWithPostcondition {α β γ δ : Type w}
+    {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad n] [Monad o] [LawfulMonad n] [LawfulMonad o]
+    [IteratorLoop α Id n] [IteratorLoop α Id o]
+    [LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
+    [MonadLiftT n o] [LawfulMonadLiftT n o]
+    {f : β → PostconditionT n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : Iter (α := α) β} :
+    (it.filterMapWithPostcondition f).foldM (init := init) g =
+      it.foldM (init := init) (fun d b => do
+          let some c ← (f b).run | pure d
+          g d c) := by
+  rw [filterMapWithPostcondition, IterM.foldM_filterMapWithPostcondition, foldM_eq_foldM_toIterM,
+    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]; rfl
+
+theorem Iter.foldM_filterMapM {α β γ δ : Type w}
+    {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
+    [Monad o] [LawfulMonad o]
+    [IteratorLoop α Id n] [IteratorLoop α Id o]
+    [LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
+    [MonadLiftT n o] [LawfulMonadLiftT n o]
+    {f : β → n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : Iter (α := α) β} :
     (it.filterMapM f).foldM (init := init) g =
       it.foldM (init := init) (fun d b => do
           let some c ← f b | pure d
           g d c) := by
-  rw [foldM_eq_foldM_toIterM, filterMapM_eq_toIter_filterMapM_toIterM, IterM.foldM_filterMapM]
-  congr
-  simp [instMonadLiftTOfMonadLift, Id.instMonadLiftTOfPure]
+  simp [filterMapM, IterM.foldM_filterMapM, foldM_eq_foldM_toIterM,
+    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]; rfl
 
-theorem Iter.foldM_mapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
-    [Iterator α Id β] [Finite α Id] [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m]
-    [Monad n] [LawfulMonad n] [IteratorLoop α Id m] [IteratorLoop α Id n]
-    [LawfulIteratorLoop α Id m] [LawfulIteratorLoop α Id n]
-    [MonadLiftT m n] [LawfulMonadLiftT m n]
-    {f : β → m γ} {g : δ → γ → n δ} {init : δ} {it : Iter (α := α) β} :
+theorem Iter.foldM_mapWithPostcondition {α β γ δ : Type w}
+    {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad m] [Monad n] [Monad o] [LawfulMonad m][LawfulMonad n] [LawfulMonad o]
+    [IteratorLoop α Id n] [IteratorLoop α Id o]
+    [LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
+    [MonadLiftT n o] [LawfulMonadLiftT n o]
+    {f : β → PostconditionT n γ} {g : δ → γ → o δ} {init : δ} {it : Iter (α := α) β} :
+    (it.mapWithPostcondition f).foldM (init := init) g =
+      it.foldM (init := init) (fun d b => do let c ← (f b).run; g d c) := by
+  simp [mapWithPostcondition, IterM.foldM_mapWithPostcondition, foldM_eq_foldM_toIterM,
+    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+
+theorem Iter.foldM_mapM {α β γ δ : Type w}
+    {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
+    [Monad o] [LawfulMonad o]
+    [IteratorLoop α Id n] [IteratorLoop α Id o]
+    [LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
+    [MonadLiftT n o] [LawfulMonadLiftT n o]
+    {f : β → n γ} {g : δ → γ → o δ} {init : δ} {it : Iter (α := α) β} :
+    haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
     (it.mapM f).foldM (init := init) g =
       it.foldM (init := init) (fun d b => do let c ← f b; g d c) := by
-  rw [foldM_eq_foldM_toIterM, mapM_eq_toIter_mapM_toIterM, IterM.foldM_mapM]
-  congr
-  simp [instMonadLiftTOfMonadLift, Id.instMonadLiftTOfPure]
+  simp [mapM, IterM.foldM_mapM, foldM_eq_foldM_toIterM,
+    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
 
-theorem Iter.foldM_filterMap {α β γ : Type w} {δ : Type x} {m : Type x → Type w'}
-    [Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m]
-    [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
-    {f : β → Option γ} {g : δ → γ → m δ} {init : δ} {it : Iter (α := α) β} :
+theorem Iter.foldM_filterWithPostcondition {α β δ : Type w}
+    {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad n] [Monad o] [LawfulMonad n] [LawfulMonad o]
+    [IteratorLoop α Id n] [IteratorLoop α Id o]
+    [LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
+    [MonadLiftT n o] [LawfulMonadLiftT n o]
+    {f : β → PostconditionT n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : Iter (α := α) β} :
+    (it.filterWithPostcondition f).foldM (init := init) g =
+      it.foldM (init := init) (fun d b => do if (← (f b).run).down then g d b else pure d) := by
+  simp [filterWithPostcondition, IterM.foldM_filterWithPostcondition, foldM_eq_foldM_toIterM,
+    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+
+theorem Iter.foldM_filterM {α β δ : Type w}
+    {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
+    [Monad o] [LawfulMonad o]
+    [IteratorLoop α Id n] [IteratorLoop α Id o]
+    [LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
+    [MonadLiftT n o] [LawfulMonadLiftT n o]
+    {f : β → n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : Iter (α := α) β} :
+    (it.filterM f).foldM (init := init) g =
+      it.foldM (init := init) (fun d b => do if (← f b).down then g d b else pure d) := by
+  simp [filterM, IterM.foldM_filterM, foldM_eq_foldM_toIterM,
+    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+
+theorem Iter.foldM_filterMap {α β γ δ : Type w} {n : Type w → Type w''}
+    [Iterator α Id β] [Finite α Id] [Monad n] [LawfulMonad n]
+    [IteratorLoop α Id n]
+    [LawfulIteratorLoop α Id n]
+    {f : β → Option γ} {g : δ → γ → n δ} {init : δ} {it : Iter (α := α) β} :
     (it.filterMap f).foldM (init := init) g =
       it.foldM (init := init) (fun d b => do
           let some c := f b | pure d
           g d c) := by
-  induction it using Iter.inductSteps generalizing init with | step it ihy ihs
-  rw [foldM_eq_match_step, foldM_eq_match_step, step_filterMap]
-  -- There seem to be some type dependencies that, combined with nested match expressions,
-  -- force us to split a lot.
-  split <;> rename_i h
-  · split at h
-    · split at h
-      · cases h
-      · cases h; simp [*, ihy ‹_›]
-    · cases h
-    · cases h
-  · split at h
-    · split at h
-      · cases h; simp [*, ihy ‹_›]
-      · cases h
-    · cases h; simp [*, ihs ‹_›]
-    · cases h
-  · split at h
-    · split at h
-      · cases h
-      · cases h
-    · cases h
-    · simp [*]
+  simp [filterMap, IterM.foldM_filterMap, foldM_eq_foldM_toIterM]; rfl
 
-theorem Iter.foldM_map {α β γ : Type w} {δ : Type x} {m : Type x → Type w'}
-    [Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m]
-    [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
-    {f : β → γ} {g : δ → γ → m δ} {init : δ} {it : Iter (α := α) β} :
+theorem Iter.foldM_map {α β γ δ : Type w} {n : Type w → Type w''}
+    [Iterator α Id β] [Finite α Id] [Monad n] [LawfulMonad n]
+    [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    {f : β → γ} {g : δ → γ → n δ} {init : δ} {it : Iter (α := α) β} :
     (it.map f).foldM (init := init) g =
-      it.foldM (init := init) (fun d b => g d (f b)) := by
-  induction it using Iter.inductSteps generalizing init with | step it ihy ihs
-  rw [foldM_eq_match_step, foldM_eq_match_step, step_map]
-  cases it.step using PlausibleIterStep.casesOn
-  · simp [*, ihy ‹_›]
-  · simp [*, ihs ‹_›]
-  · simp
+      it.foldM (init := init) (fun d b => do g d (f b)) := by
+  simp [foldM_eq_forIn, forIn_map]
 
-theorem Iter.fold_filterMapM {α β γ δ : Type w} {m : Type w → Type w'}
-    [Iterator α Id β] [Finite α Id] [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m]
-    [IteratorLoop α Id Id.{w}] [IteratorLoop α Id m]
-    [LawfulIteratorLoop α Id Id] [LawfulIteratorLoop α Id m]
-    {f : β → m (Option γ)} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} :
+theorem Iter.foldM_filter {α β δ : Type w} {n : Type w → Type w''}
+    [Iterator α Id β] [Finite α Id] [Monad n] [LawfulMonad n]
+    [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    {f : β → Bool} {g : δ → β → n δ} {init : δ} {it : Iter (α := α) β} :
+    (it.filter f).foldM (init := init) g =
+      it.foldM (init := init) (fun d b => if f b then g d b else pure d) := by
+  simp only [foldM_eq_forIn, forIn_filter]
+  congr 1; ext out acc
+  cases f out <;> simp
+
+theorem Iter.fold_filterMapWithPostcondition {α β γ δ : Type w} {n : Type w → Type w''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad n] [LawfulMonad n]
+    [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    {f : β → PostconditionT n (Option γ)} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} :
+    (it.filterMapWithPostcondition f).fold (init := init) g =
+      it.foldM (init := init) (fun d b => do
+          let some c ← (f b).run | pure d
+          return g d c) := by
+  simp [filterMapWithPostcondition, IterM.fold_filterMapWithPostcondition, foldM_eq_foldM_toIterM]
+  rfl
+
+theorem Iter.fold_filterMapM {α β γ δ : Type w} {n : Type w → Type w''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
+    [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    {f : β → n (Option γ)} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} :
     (it.filterMapM f).fold (init := init) g =
       it.foldM (init := init) (fun d b => do
           let some c ← f b | pure d
           return g d c) := by
-  rw [foldM_eq_foldM_toIterM, filterMapM_eq_toIter_filterMapM_toIterM, IterM.fold_filterMapM]
-  rfl
+  simp [filterMapM, IterM.fold_filterMapM, foldM_eq_foldM_toIterM]; rfl
 
-theorem Iter.fold_mapM {α β γ δ : Type w} {m : Type w → Type w'}
-    [Iterator α Id β] [Finite α Id] [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m]
-    [IteratorLoop α Id Id.{w}] [IteratorLoop α Id m]
-    [LawfulIteratorLoop α Id Id] [LawfulIteratorLoop α Id m]
-    {f : β → m γ} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} :
+theorem Iter.fold_mapWithPostcondition {α β γ δ : Type w} {n : Type w → Type w''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad n] [LawfulMonad n]
+    [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    {f : β → PostconditionT n γ} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} :
+    (it.mapWithPostcondition f).fold (init := init) g =
+      it.foldM (init := init) (fun d b => do let c ← (f b).run; return g d c) := by
+  simp [mapWithPostcondition, IterM.fold_mapWithPostcondition, foldM_eq_foldM_toIterM]
+
+theorem Iter.fold_mapM {α β γ δ : Type w} {n : Type w → Type w''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
+    [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    {f : β → n γ} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} :
     (it.mapM f).fold (init := init) g =
-      it.foldM (init := init) (fun d b => do return g d (← f b)) := by
-  rw [foldM_eq_foldM_toIterM, mapM_eq_toIter_mapM_toIterM, IterM.fold_mapM]
+      it.foldM (init := init) (fun d b => do let c ← f b; return g d c) := by
+  simp [mapM, IterM.fold_mapM, foldM_eq_foldM_toIterM]
 
-theorem Iter.fold_filterMap {α β γ : Type w} {δ : Type x}
-    [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+theorem Iter.fold_filterWithPostcondition {α β δ : Type w}
+    {n : Type w → Type w''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad n] [LawfulMonad n]
+    [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    {f : β → PostconditionT n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : Iter (α := α) β} :
+    (it.filterWithPostcondition f).fold (init := init) g =
+      it.foldM (init := init) (fun d b => return if (← (f b).run).down then g d b else d) := by
+  simp [filterWithPostcondition, IterM.fold_filterWithPostcondition, foldM_eq_foldM_toIterM]
+
+theorem Iter.fold_filterM {α β δ : Type w} {n : Type w → Type w''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
+    [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    {f : β → n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : Iter (α := α) β} :
+    (it.filterM f).fold (init := init) g =
+      it.foldM (init := init) (fun d b => return if (← f b).down then g d b else d) := by
+  simp [filterM, IterM.fold_filterM, foldM_eq_foldM_toIterM]
+
+theorem Iter.fold_filterMap {α β γ δ : Type w}
+    [Iterator α Id β] [Finite α Id]
+    [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
     {f : β → Option γ} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} :
     (it.filterMap f).fold (init := init) g =
       it.fold (init := init) (fun d b =>
           match f b with
           | some c => g d c
           | _ => d) := by
-  simp only [fold_eq_foldM, foldM_filterMap]
-  rfl
+  simp [filterMap, IterM.fold_filterMap, fold_eq_fold_toIterM]; rfl
 
-theorem Iter.fold_map {α β γ : Type w} {δ : Type x}
+theorem Iter.fold_map {α β γ δ : Type w}
     [Iterator α Id β] [Finite α Id]
     [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
     {f : β → γ} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} :
@@ -559,6 +738,14 @@ theorem Iter.fold_map {α β γ : Type w} {δ : Type x}
       it.fold (init := init) (fun d b => g d (f b)) := by
   simp [fold_eq_foldM, foldM_map]
 
+theorem Iter.fold_filter {α β δ : Type w}
+    [Iterator α Id β] [Finite α Id]
+    [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {f : β → Bool} {g : δ → β → δ} {init : δ} {it : Iter (α := α) β} :
+    (it.filter f).fold (init := init) g =
+      it.fold (init := init) (fun d b => if f b then g d b else d) := by
+  simp [filter, IterM.fold_filter, fold_eq_fold_toIterM]
+
 end Fold
 
 section Count
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
index bc4c23ece3..3e4c0f7fbe 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
@@ -1317,7 +1317,6 @@ end ToArray
 
 section ForIn
 
-@[spec]
 theorem IterM.forIn_filterMapWithPostcondition
     [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
     [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]
@@ -1349,7 +1348,6 @@ theorem IterM.forIn_filterMapWithPostcondition
   · simp [ihs ‹_›]
   · simp
 
-@[spec]
 theorem IterM.forIn_filterMapM
     [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
     [MonadAttach n] [WeaklyLawfulMonadAttach n]
@@ -1378,7 +1376,6 @@ theorem IterM.forIn_filterMap
   rw [filterMap, forIn_filterMapWithPostcondition]
   simp [PostconditionT.run_eq_map]
 
-@[spec]
 theorem IterM.forIn_mapWithPostcondition
     [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
     [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]
@@ -1393,7 +1390,6 @@ theorem IterM.forIn_mapWithPostcondition
     ← filterMapWithPostcondition, forIn_filterMapWithPostcondition]
   simp [PostconditionT.run_eq_map]
 
-@[spec]
 theorem IterM.forIn_mapM
     [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
     [MonadAttach n] [WeaklyLawfulMonadAttach n]
@@ -1415,7 +1411,6 @@ theorem IterM.forIn_map
   rw [map, forIn_mapWithPostcondition]
   simp [PostconditionT.run_eq_map]
 
-@[spec]
 theorem IterM.forIn_filterWithPostcondition
     [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
     [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]
@@ -1434,7 +1429,6 @@ theorem IterM.forIn_filterWithPostcondition
   apply bind_congr; intro fx
   cases fx.val.down <;> simp
 
-@[spec]
 theorem IterM.forIn_filterM
     [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
     [MonadAttach n] [WeaklyLawfulMonadAttach n]
@@ -1461,7 +1455,6 @@ end ForIn
 
 section Fold
 
-@[spec]
 theorem IterM.foldM_filterMapWithPostcondition {α β γ δ : Type w}
     {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
     [Iterator α m β] [Finite α m]
@@ -1481,7 +1474,6 @@ theorem IterM.foldM_filterMapWithPostcondition {α β γ δ : Type w}
   apply bind_congr; intro fx
   split <;> simp
 
-@[spec]
 theorem IterM.foldM_filterMapM {α β γ δ : Type w}
     {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
     [Iterator α m β] [Finite α m]
@@ -1499,7 +1491,6 @@ theorem IterM.foldM_filterMapM {α β γ δ : Type w}
           g d c) := by
   simp [filterMapM, foldM_filterMapWithPostcondition, PostconditionT.run_attachLift]
 
-@[spec]
 theorem IterM.foldM_mapWithPostcondition {α β γ δ : Type w}
     {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
     [Iterator α m β] [Finite α m]
@@ -1513,7 +1504,6 @@ theorem IterM.foldM_mapWithPostcondition {α β γ δ : Type w}
       it.foldM (init := init) (fun d b => do let c ← (f b).run; g d c) := by
   simp [foldM_eq_forIn, forIn_mapWithPostcondition]
 
-@[spec]
 theorem IterM.foldM_mapM {α β γ δ : Type w}
     {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
     [Iterator α m β] [Finite α m]
@@ -1529,10 +1519,45 @@ theorem IterM.foldM_mapM {α β γ δ : Type w}
       it.foldM (init := init) (fun d b => do let c ← f b; g d c) := by
   simp [foldM_eq_forIn, forIn_mapM]
 
+theorem IterM.foldM_filterWithPostcondition {α β δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α m β] [Finite α m]
+    [Monad m] [Monad n] [Monad o] [LawfulMonad m] [LawfulMonad n] [LawfulMonad o]
+    [IteratorLoop α m n] [IteratorLoop α m o]
+    [LawfulIteratorLoop α m n] [LawfulIteratorLoop α m o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    {f : β → PostconditionT n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : IterM (α := α) m β} :
+    haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
+    (it.filterWithPostcondition f).foldM (init := init) g =
+      it.foldM (init := init) (fun d b => do if (← (f b).run).down then g d b else pure d) := by
+  simp only [foldM_eq_forIn, forIn_filterWithPostcondition]
+  congr 1; ext out acc
+  simp only [map_bind]
+  apply bind_congr; intro fx
+  split <;> simp
+
+theorem IterM.foldM_filterM {α β δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α m β] [Finite α m]
+    [Monad m] [LawfulMonad m]
+    [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
+    [Monad o] [LawfulMonad o]
+    [IteratorLoop α m n] [IteratorLoop α m o]
+    [LawfulIteratorLoop α m n] [LawfulIteratorLoop α m o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    {f : β → n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : IterM (α := α) m β} :
+    haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
+    (it.filterM f).foldM (init := init) g =
+      it.foldM (init := init) (fun d b => do if (← f b).down then g d b else pure d) := by
+  simp [filterM, foldM_filterMapWithPostcondition, PostconditionT.run_attachLift]
+  congr 1; ext out acc
+  apply bind_congr; intro fx
+  cases fx.down <;> simp [PostconditionT.run_eq_map]
+
 theorem IterM.foldM_filterMap {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
     [Iterator α m β] [Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n]
-    [IteratorLoop α m m] [IteratorLoop α m n]
-    [LawfulIteratorLoop α m m] [LawfulIteratorLoop α m n]
+    [IteratorLoop α m n]
+    [LawfulIteratorLoop α m n]
     [MonadLiftT m n] [LawfulMonadLiftT m n]
     {f : β → Option γ} {g : δ → γ → n δ} {init : δ} {it : IterM (α := α) m β} :
     (it.filterMap f).foldM (init := init) g =
@@ -1545,21 +1570,44 @@ theorem IterM.foldM_filterMap {α β γ δ : Type w} {m : Type w → Type w'} {n
 
 theorem IterM.foldM_map {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
     [Iterator α m β] [Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n]
-    [IteratorLoop α m m] [IteratorLoop α m n]
-    [LawfulIteratorLoop α m m] [LawfulIteratorLoop α m n]
+    [IteratorLoop α m n] [LawfulIteratorLoop α m n]
     [MonadLiftT m n] [LawfulMonadLiftT m n]
     {f : β → γ} {g : δ → γ → n δ} {init : δ} {it : IterM (α := α) m β} :
     (it.map f).foldM (init := init) g =
       it.foldM (init := init) (fun d b => do g d (f b)) := by
   simp [foldM_eq_forIn, forIn_map]
 
-@[spec]
+theorem IterM.foldM_filter {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
+    [Iterator α m β] [Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n]
+    [IteratorLoop α m n]
+    [LawfulIteratorLoop α m n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    {f : β → Bool} {g : δ → β → n δ} {init : δ} {it : IterM (α := α) m β} :
+    (it.filter f).foldM (init := init) g =
+      it.foldM (init := init) (fun d b => if f b then g d b else pure d) := by
+  simp only [foldM_eq_forIn, forIn_filter]
+  congr 1; ext out acc
+  split <;> simp [*]
+
+theorem IterM.fold_filterMapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'}
+    {n : Type w → Type w''}
+    [Iterator α m β] [Finite α m]
+    [Monad m] [LawfulMonad m]
+    [Monad n] [LawfulMonad n]
+    [IteratorLoop α m n] [LawfulIteratorLoop α m n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    {f : β → PostconditionT n (Option γ)} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} :
+    (it.filterMapWithPostcondition f).fold (init := init) g =
+      it.foldM (init := init) (fun d b => do
+          let some c ← (f b).run | pure d
+          return g d c) := by
+  simp [fold_eq_foldM, foldM_filterMapWithPostcondition]
+
 theorem IterM.fold_filterMapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
     [Iterator α m β] [Finite α m]
     [Monad m] [LawfulMonad m]
     [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
-    [IteratorLoop α m m] [IteratorLoop α m n]
-    [LawfulIteratorLoop α m m] [LawfulIteratorLoop α m n]
+    [IteratorLoop α m n] [LawfulIteratorLoop α m n]
     [MonadLiftT m n] [LawfulMonadLiftT m n]
     {f : β → n (Option γ)} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} :
     (it.filterMapM f).fold (init := init) g =
@@ -1568,19 +1616,57 @@ theorem IterM.fold_filterMapM {α β γ δ : Type w} {m : Type w → Type w'} {n
           return g d c) := by
   simp [fold_eq_foldM, foldM_filterMapM]
 
-@[spec]
+theorem IterM.fold_mapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
+    [Iterator α m β] [Finite α m]
+    [Monad m] [LawfulMonad m]
+    [Monad n] [LawfulMonad n]
+    [IteratorLoop α m n] [LawfulIteratorLoop α m n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    {f : β → PostconditionT n γ} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} :
+    (it.mapWithPostcondition f).fold (init := init) g =
+      it.foldM (init := init) (fun d b => do let c ← (f b).run; return g d c) := by
+  simp [fold_eq_foldM, foldM_mapWithPostcondition]
+
 theorem IterM.fold_mapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
     [Iterator α m β] [Finite α m]
     [Monad m] [LawfulMonad m]
     [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
-    [IteratorLoop α m m] [IteratorLoop α m n]
-    [LawfulIteratorLoop α m m] [LawfulIteratorLoop α m n]
+    [IteratorLoop α m n] [LawfulIteratorLoop α m n]
     [MonadLiftT m n] [LawfulMonadLiftT m n]
     {f : β → n γ} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} :
     (it.mapM f).fold (init := init) g =
       it.foldM (init := init) (fun d b => do let c ← f b; return g d c) := by
   simp [fold_eq_foldM, foldM_mapM]
 
+theorem IterM.fold_filterWithPostcondition {α β δ : Type w} {m : Type w → Type w'}
+    {n : Type w → Type w''}
+    [Iterator α m β] [Finite α m]
+    [Monad m] [LawfulMonad m]
+    [Monad n] [LawfulMonad n]
+    [IteratorLoop α m n] [LawfulIteratorLoop α m n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    {f : β → PostconditionT n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : IterM (α := α) m β} :
+    (it.filterWithPostcondition f).fold (init := init) g =
+      it.foldM (init := init) (fun d b => return if (← (f b).run).down then g d b else d) := by
+  simp only [fold_eq_foldM, foldM_filterWithPostcondition, monadLift_self]
+  congr 1; ext out acc
+  apply bind_congr; intro fx
+  cases fx.down <;> simp
+
+theorem IterM.fold_filterM {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
+    [Iterator α m β] [Finite α m]
+    [Monad m] [LawfulMonad m]
+    [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
+    [IteratorLoop α m n] [LawfulIteratorLoop α m n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    {f : β → n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : IterM (α := α) m β} :
+    (it.filterM f).fold (init := init) g =
+      it.foldM (init := init) (fun d b => return if (← f b).down then g d b else d) := by
+  simp only [fold_eq_foldM, foldM_filterM]
+  congr 1; ext out acc
+  apply bind_congr; intro fx
+  cases fx.down <;> simp
+
 theorem IterM.fold_filterMap {α β γ δ : Type w} {m : Type w → Type w'}
     [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m]
     [IteratorLoop α m m] [LawfulIteratorLoop α m m]
@@ -1602,6 +1688,16 @@ theorem IterM.fold_map {α β γ δ : Type w} {m : Type w → Type w'}
       it.fold (init := init) (fun d b => g d (f b)) := by
   simp [fold_eq_foldM, foldM_map]
 
+theorem IterM.fold_filter {α β δ : Type w} {m : Type w → Type w'}
+    [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m]
+    [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {f : β → Bool} {g : δ → β → δ} {init : δ} {it : IterM (α := α) m β} :
+    (it.filter f).fold (init := init) g =
+      it.fold (init := init) (fun d b => if f b then g d b else d) := by
+  simp [fold_eq_foldM, foldM_filter]
+  congr; ext
+  split <;> simp
+
 end Fold
 
 section Count
diff --git a/src/Lean/Elab/Tactic/Do/Attr.lean b/src/Lean/Elab/Tactic/Do/Attr.lean
index 1909edd909..b7cc57da4a 100644
--- a/src/Lean/Elab/Tactic/Do/Attr.lean
+++ b/src/Lean/Elab/Tactic/Do/Attr.lean
@@ -216,7 +216,7 @@ def mkSpecAttr (ext : SpecExtension) : AttributeImpl where
   add   := fun declName stx attrKind => do
     let go : MetaM Unit := do
       let info ← getAsyncConstInfo declName
-      let prio ← getAttrParamOptPrio stx[3]
+      let prio ← if stx.getKind = ``Lean.Parser.Attr.spec then getAttrParamOptPrio stx[3] else getAttrParamOptPrio stx[1]
       try
         addSpecTheorem ext declName prio attrKind
       catch _ =>
diff --git a/src/Lean/Elab/Tactic/Do/Spec.lean b/src/Lean/Elab/Tactic/Do/Spec.lean
index 9f30855b48..43ad452ab6 100644
--- a/src/Lean/Elab/Tactic/Do/Spec.lean
+++ b/src/Lean/Elab/Tactic/Do/Spec.lean
@@ -28,7 +28,7 @@ public def findSpec (database : SpecTheorems) (wp : Expr) : MetaM SpecTheorem :=
   let prog := prog.headBeta
   let candidates ← database.specs.getMatch prog
   let candidates := candidates.filter fun spec => !database.erased.contains spec.proof
-  let candidates := candidates.insertionSort fun s₁ s₂ => s₁.priority < s₂.priority
+  let candidates := candidates.insertionSort fun s₁ s₂ => s₁.priority > s₂.priority
   trace[Elab.Tactic.Do.spec] "Candidates for {prog}: {candidates.map (·.proof)}"
   let specs ← candidates.filterM fun spec => do
     let (_, _, _, type) ← spec.proof.instantiate
diff --git a/src/Std/Do/Triple/SpecLemmas.lean b/src/Std/Do/Triple/SpecLemmas.lean
index 51c5e9f137..2634c90984 100644
--- a/src/Std/Do/Triple/SpecLemmas.lean
+++ b/src/Std/Do/Triple/SpecLemmas.lean
@@ -1163,8 +1163,10 @@ theorem Spec.forIn_slice {m : Type w → Type x} {ps : PostShape}
   simp only [← Slice.forIn_toList]
   exact Spec.forIn_list inv step
 
-open Std.Iterators in
-@[spec]
+section Iterators
+open Std.Iterators
+
+@[spec low]
 theorem Spec.forIn_iter {ps : PostShape} [Monad n] [WPMonad n ps]
     {α β γ} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
     [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
@@ -1182,8 +1184,7 @@ theorem Spec.forIn_iter {ps : PostShape} [Monad n] [WPMonad n ps]
   simp only [← Iter.forIn_toList]
   exact Spec.forIn_list inv step
 
-open Std.Iterators in
-@[spec]
+@[spec low]
 theorem Spec.forIn_iterM_id {ps : PostShape} [Monad n] [WPMonad n ps]
     {α β γ} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
     [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
@@ -1204,8 +1205,7 @@ theorem Spec.forIn_iterM_id {ps : PostShape} [Monad n] [WPMonad n ps]
       IterM.toList_toIter]
   exact Spec.forIn_list inv step
 
-open Std.Iterators in
-@[spec]
+@[spec low]
 theorem Spec.foldM_iter {ps : PostShape} [Monad n] [WPMonad n ps]
     {α β γ} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
     [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
@@ -1221,8 +1221,7 @@ theorem Spec.foldM_iter {ps : PostShape} [Monad n] [WPMonad n ps]
   rw [← Iter.foldlM_toList]
   exact Spec.foldlM_list inv step
 
-open Std.Iterators in
-@[spec]
+@[spec low]
 theorem Spec.foldM_iterM_id {ps : PostShape} [Monad n] [WPMonad n ps]
     {α β γ} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
     [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
@@ -1238,6 +1237,662 @@ theorem Spec.foldM_iterM_id {ps : PostShape} [Monad n] [WPMonad n ps]
   rw [← IterM.foldlM_toList]
   exact Spec.foldlM_list inv step
 
+@[spec]
+theorem Spec.IterM.forIn_filterMapWithPostcondition {m β ps}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
+    [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m]
+    [IteratorLoop α m o] [LawfulIteratorLoop α m o]
+    {it : IterM (α := α) m β} {f : β → PostconditionT n (Option β₂)} {init : γ}
+    {g : β₂ → γ → o (ForInStep γ)} {P Q}
+    (h :
+        haveI : MonadLift n o := ⟨monadLift⟩
+        Triple (m := o) (forIn it init (fun out acc => do
+          match ← (f out).run with
+          | some c => g c acc
+          | none => return .yield acc)) P Q) :
+    Triple (forIn (it.filterMapWithPostcondition f) init g) P Q := by
+  rwa [Std.IterM.forIn_filterMapWithPostcondition]
+
+@[spec]
+theorem Spec.IterM.forIn_filterMapM {m β ps}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
+    [MonadAttach n] [WeaklyLawfulMonadAttach n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m]
+    [IteratorLoop α m o] [LawfulIteratorLoop α m o]
+    {it : IterM (α := α) m β} {f : β → n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)}
+    {P Q}
+    (h :
+        haveI : MonadLift n o := ⟨monadLift⟩
+        Triple (forIn (m := o) it init (fun out acc => do
+          match ← f out with
+          | some c => g c acc
+          | none => return .yield acc)) P Q) :
+    Triple (forIn (it.filterMapM f) init g) P Q := by
+  rwa [Std.IterM.forIn_filterMapM]
+
+@[spec]
+theorem Spec.IterM.forIn_filterMap {m β ps}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [WPMonad n ps]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    [Iterator α m β] [Finite α m]
+    [IteratorLoop α m n] [LawfulIteratorLoop α m n]
+    {it : IterM (α := α) m β} {f : β → Option β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} {P Q}
+    (h :
+        Triple (forIn it init (fun out acc => do
+          match f out with
+          | some c => g c acc
+          | none => return .yield acc)) P Q) :
+    Triple (forIn (it.filterMap f) init g) P Q := by
+  rwa [Std.IterM.forIn_filterMap]
+
+@[spec]
+theorem Spec.IterM.forIn_mapWithPostcondition {m β ps}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
+    [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m]
+    [IteratorLoop α m o] [LawfulIteratorLoop α m o]
+    {it : IterM (α := α) m β} {f : β → PostconditionT n β₂} {init : γ}
+    {g : β₂ → γ → o (ForInStep γ)} {P Q}
+    (h :
+        haveI : MonadLift n o := ⟨monadLift⟩
+        Triple (forIn (m := o) it init (fun out acc => do g (← (f out).run) acc)) P Q) :
+    Triple (forIn (it.mapWithPostcondition f) init g) P Q := by
+  rwa [Std.IterM.forIn_mapWithPostcondition]
+
+@[spec]
+theorem Spec.IterM.forIn_mapM {m β ps}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
+    [MonadAttach n] [WeaklyLawfulMonadAttach n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m]
+    [IteratorLoop α m o] [LawfulIteratorLoop α m o]
+    {it : IterM (α := α) m β} {f : β → n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)} {P Q}
+    (h :
+        haveI : MonadLift n o := ⟨monadLift⟩
+        Triple (forIn (m := o) it init (fun out acc => do g (← f out) acc)) P Q) :
+    Triple (forIn (it.mapM f) init g) P Q := by
+  rwa [Std.IterM.forIn_mapM]
+
+@[spec]
+theorem Spec.IterM.forIn_map {m β ps}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [WPMonad n ps]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    [Iterator α m β] [Finite α m] [IteratorLoop α m n] [LawfulIteratorLoop α m n]
+    {it : IterM (α := α) m β} {f : β → β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} {P Q}
+    (h : Triple (forIn it init (fun out acc => do g (f out) acc)) P Q) :
+    Triple (forIn (it.map f) init g) P Q := by
+  rwa [Std.IterM.forIn_map]
+
+@[spec]
+theorem Spec.IterM.forIn_filterWithPostcondition {m β ps}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
+    [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m]
+    [IteratorLoop α m o] [LawfulIteratorLoop α m o]
+    {it : IterM (α := α) m β} {f : β → PostconditionT n (ULift Bool)} {init : γ}
+    {g : β → γ → o (ForInStep γ)} {P Q}
+    (h :
+        haveI : MonadLift n o := ⟨monadLift⟩
+        Triple (forIn (m := o) it init (fun out acc => do if (← (f out).run).down then g out acc else return .yield acc)) P Q) :
+    Triple (forIn (it.filterWithPostcondition f) init g) P Q := by
+  rwa [Std.IterM.forIn_filterWithPostcondition]
+
+@[spec]
+theorem Spec.IterM.forIn_filterM {m β ps}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
+    [MonadAttach n] [WeaklyLawfulMonadAttach n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m]
+    [IteratorLoop α m o] [LawfulIteratorLoop α m o]
+    {it : IterM (α := α) m β} {f : β → n (ULift Bool)} {init : γ} {g : β → γ → o (ForInStep γ)} {P Q}
+    (h :
+        haveI : MonadLift n o := ⟨monadLift⟩
+        Triple (forIn (m := o) it init (fun out acc => do if (← f out).down then g out acc else return .yield acc)) P Q):
+    Triple (forIn (it.filterM f) init g) P Q := by
+  rwa [Std.IterM.forIn_filterM]
+
+@[spec]
+theorem Spec.IterM.forIn_filter {m β ps}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [WPMonad n ps]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    [Iterator α m β] [Finite α m] [IteratorLoop α m n] [LawfulIteratorLoop α m n]
+    {it : IterM (α := α) m β} {f : β → Bool} {init : γ} {g : β → γ → n (ForInStep γ)} {P Q}
+    (h : Triple (forIn (m := n) it init (fun out acc => do if f out then g out acc else return .yield acc)) P Q) :
+    Triple (forIn (it.filter f) init g) P Q := by
+  rwa [Std.IterM.forIn_filter]
+
+@[spec]
+theorem Spec.IterM.foldM_filterMapWithPostcondition {α β γ δ : Type w} {ps}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α m β] [Finite α m]
+    [Monad m] [Monad n] [Monad o] [LawfulMonad m] [LawfulMonad n] [LawfulMonad o] [WPMonad o ps]
+    [IteratorLoop α m n] [IteratorLoop α m o]
+    [LawfulIteratorLoop α m n] [LawfulIteratorLoop α m o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    {f : β → PostconditionT n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : IterM (α := α) m β} {P Q}
+    (h :
+        haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
+        Triple (it.foldM (n := o) (init := init) (fun d b => do
+          let some c ← (f b).run | Pure.pure d
+          g d c)) P Q) :
+    Triple ((it.filterMapWithPostcondition f).foldM (init := init) g) P Q := by
+  rwa [Std.IterM.foldM_filterMapWithPostcondition]
+
+@[spec]
+theorem Spec.IterM.foldM_filterMapM {α β γ δ : Type w} {ps}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α m β] [Finite α m]
+    [Monad m] [LawfulMonad m]
+    [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
+    [Monad o] [LawfulMonad o] [WPMonad o ps]
+    [IteratorLoop α m n] [IteratorLoop α m o]
+    [LawfulIteratorLoop α m n] [LawfulIteratorLoop α m o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    {f : β → n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : IterM (α := α) m β} {P Q}
+    (h :
+        haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
+        Triple (it.foldM (n := o) (init := init) (fun d b => do
+          let some c ← f b | Pure.pure d
+          g d c)) P Q):
+    Triple ((it.filterMapM f).foldM (init := init) g) P Q := by
+  rwa [Std.IterM.foldM_filterMapM]
+
+@[spec]
+theorem Spec.IterM.foldM_mapWithPostcondition {α β γ δ : Type w} {ps}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α m β] [Finite α m]
+    [Monad m] [Monad n] [Monad o] [LawfulMonad m] [LawfulMonad n] [LawfulMonad o] [WPMonad o ps]
+    [IteratorLoop α m n] [IteratorLoop α m o]
+    [LawfulIteratorLoop α m n] [LawfulIteratorLoop α m o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    {f : β → PostconditionT n γ} {g : δ → γ → o δ} {init : δ} {it : IterM (α := α) m β} {P Q}
+    (h :
+        haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
+        Triple (it.foldM (n := o) (init := init) (fun d b => do let c ← (f b).run; g d c)) P Q):
+    Triple ((it.mapWithPostcondition f).foldM (init := init) g) P Q := by
+  rwa [Std.IterM.foldM_mapWithPostcondition]
+
+@[spec]
+theorem Spec.IterM.foldM_mapM {α β γ δ : Type w} {ps}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α m β] [Finite α m]
+    [Monad m] [LawfulMonad m]
+    [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
+    [Monad o] [LawfulMonad o] [WPMonad o ps]
+    [IteratorLoop α m n] [IteratorLoop α m o]
+    [LawfulIteratorLoop α m n] [LawfulIteratorLoop α m o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    {f : β → n γ} {g : δ → γ → o δ} {init : δ} {it : IterM (α := α) m β} {P Q}
+    (h :
+        haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
+        Triple (it.foldM (n := o) (init := init) (fun d b => do let c ← f b; g d c)) P Q) :
+    Triple ((it.mapM f).foldM (init := init) g) P Q := by
+  rwa [Std.IterM.foldM_mapM]
+
+@[spec]
+theorem Spec.IterM.foldM_filterWithPostcondition {α β δ : Type w} {ps}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α m β] [Finite α m]
+    [Monad m] [Monad n] [Monad o] [LawfulMonad m] [LawfulMonad n] [LawfulMonad o] [WPMonad o ps]
+    [IteratorLoop α m n] [IteratorLoop α m o]
+    [LawfulIteratorLoop α m n] [LawfulIteratorLoop α m o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    {f : β → PostconditionT n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : IterM (α := α) m β} {P Q}
+    (h :
+        haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
+        Triple (it.foldM (n := o) (init := init) (fun d b => do if (← (f b).run).down then g d b else Pure.pure d)) P Q):
+    Triple ((it.filterWithPostcondition f).foldM (init := init) g) P Q := by
+  rwa [Std.IterM.foldM_filterWithPostcondition]
+
+@[spec]
+theorem Spec.IterM.foldM_filterM {α β δ : Type w} {ps}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α m β] [Finite α m]
+    [Monad m] [LawfulMonad m]
+    [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
+    [Monad o] [LawfulMonad o] [WPMonad o ps]
+    [IteratorLoop α m n] [IteratorLoop α m o]
+    [LawfulIteratorLoop α m n] [LawfulIteratorLoop α m o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    {f : β → n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : IterM (α := α) m β} {P Q}
+    (h :
+        haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
+        Triple (it.foldM (n := o) (init := init) (fun d b => do if (← f b).down then g d b else Pure.pure d)) P Q) :
+    Triple ((it.filterM f).foldM (init := init) g) P Q := by
+  rwa [Std.IterM.foldM_filterM]
+
+@[spec]
+theorem Spec.IterM.foldM_filterMap {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {ps}
+    [Iterator α m β] [Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] [WPMonad n ps]
+    [IteratorLoop α m n]
+    [LawfulIteratorLoop α m n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    {f : β → Option γ} {g : δ → γ → n δ} {init : δ} {it : IterM (α := α) m β} {P Q}
+    (h : Triple (it.foldM (n := n) (init := init) (fun d b => do
+          let some c := f b | Pure.pure d
+          g d c)) P Q) :
+    Triple ((it.filterMap f).foldM (init := init) g) P Q := by
+  rwa [Std.IterM.foldM_filterMap]
+
+@[spec]
+theorem Spec.IterM.foldM_map {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {ps}
+    [Iterator α m β] [Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] [WPMonad n ps]
+    [IteratorLoop α m n] [LawfulIteratorLoop α m n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    {f : β → γ} {g : δ → γ → n δ} {init : δ} {it : IterM (α := α) m β} {P Q}
+    (h : Triple (it.foldM (init := init) (fun d b => do g d (f b))) P Q) :
+    Triple ((it.map f).foldM (init := init) g) P Q := by
+  rwa [Std.IterM.foldM_map]
+
+@[spec]
+theorem Spec.IterM.foldM_filter {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {ps}
+    [Iterator α m β] [Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] [WPMonad n ps]
+    [IteratorLoop α m n]
+    [LawfulIteratorLoop α m n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    {f : β → Bool} {g : δ → β → n δ} {init : δ} {it : IterM (α := α) m β} {P Q}
+    (h : Triple (it.foldM (init := init) (fun d b => if f b then g d b else Pure.pure d)) P Q) :
+    Triple ((it.filter f).foldM (init := init) g) P Q := by
+  rwa [Std.IterM.foldM_filter]
+
+@[spec]
+theorem Spec.IterM.fold_filterMapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'} {ps}
+    {n : Type w → Type w''}
+    [Iterator α m β] [Finite α m]
+    [Monad m] [LawfulMonad m]
+    [Monad n] [LawfulMonad n] [WPMonad n ps]
+    [IteratorLoop α m n] [LawfulIteratorLoop α m n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    {f : β → PostconditionT n (Option γ)} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} {P Q}
+    (h : Triple (it.foldM (n := n) (init := init) (fun d b => do
+          let some c ← (f b).run | Pure.pure d
+          return g d c)) P Q) :
+    Triple ((it.filterMapWithPostcondition f).fold (init := init) g) P Q := by
+  rwa [Std.IterM.fold_filterMapWithPostcondition]
+
+@[spec]
+theorem Spec.IterM.fold_filterMapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {ps}
+    [Iterator α m β] [Finite α m]
+    [Monad m] [LawfulMonad m]
+    [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [WPMonad n ps]
+    [IteratorLoop α m n] [LawfulIteratorLoop α m n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    {f : β → n (Option γ)} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} {P Q}
+    (h : Triple (it.foldM (init := init) (fun d b => do
+          let some c ← f b | Pure.pure d
+          return g d c)) P Q) :
+    Triple ((it.filterMapM f).fold (init := init) g) P Q := by
+  rwa [Std.IterM.fold_filterMapM]
+
+@[spec]
+theorem Spec.IterM.fold_mapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'}
+    {n : Type w → Type w''} {ps}
+    [Iterator α m β] [Finite α m]
+    [Monad m] [LawfulMonad m]
+    [Monad n] [LawfulMonad n] [WPMonad n ps]
+    [IteratorLoop α m n] [LawfulIteratorLoop α m n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    {f : β → PostconditionT n γ} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} {P Q}
+    (h : Triple (it.foldM (init := init) (fun d b => do let c ← (f b).run; return g d c)) P Q) :
+    Triple ((it.mapWithPostcondition f).fold (init := init) g) P Q := by
+  rwa [Std.IterM.fold_mapWithPostcondition]
+
+@[spec]
+theorem Spec.IterM.fold_mapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {ps}
+    [Iterator α m β] [Finite α m]
+    [Monad m] [LawfulMonad m]
+    [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [WPMonad n ps]
+    [IteratorLoop α m n] [LawfulIteratorLoop α m n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    {f : β → n γ} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} {P Q}
+    (h : Triple (it.foldM (init := init) (fun d b => do let c ← f b; return g d c)) P Q) :
+    Triple ((it.mapM f).fold (init := init) g) P Q := by
+  rwa [Std.IterM.fold_mapM]
+
+@[spec]
+theorem Spec.IterM.fold_filterWithPostcondition {α β δ : Type w} {m : Type w → Type w'} {ps}
+    {n : Type w → Type w''}
+    [Iterator α m β] [Finite α m]
+    [Monad m] [LawfulMonad m]
+    [Monad n] [LawfulMonad n] [WPMonad n ps]
+    [IteratorLoop α m n] [LawfulIteratorLoop α m n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    {f : β → PostconditionT n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : IterM (α := α) m β} {P Q}
+    (h : Triple (it.foldM (init := init) (fun d b => return if (← (f b).run).down then g d b else d)) P Q) :
+    Triple ((it.filterWithPostcondition f).fold (init := init) g) P Q := by
+  rwa [Std.IterM.fold_filterWithPostcondition]
+
+@[spec]
+theorem Spec.IterM.fold_filterM {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {ps}
+    [Iterator α m β] [Finite α m]
+    [Monad m] [LawfulMonad m]
+    [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [WPMonad n ps]
+    [IteratorLoop α m n] [LawfulIteratorLoop α m n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    {f : β → n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : IterM (α := α) m β} {P Q}
+    (h : Triple (it.foldM (init := init) (fun d b => return if (← f b).down then g d b else d)) P Q) :
+    Triple ((it.filterM f).fold (init := init) g) P Q := by
+  rwa [Std.IterM.fold_filterM]
+
+@[spec]
+theorem Spec.IterM.fold_filterMap {α β γ δ : Type w} {m : Type w → Type w'} {ps}
+    [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [WPMonad m ps]
+    [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {f : β → Option γ} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} {P Q}
+    (h : Triple (it.fold (init := init) (fun d b =>
+          match f b with
+          | some c => g d c
+          | _ => d)) P Q) :
+    Triple ((it.filterMap f).fold (init := init) g) P Q := by
+  rwa [Std.IterM.fold_filterMap]
+
+@[spec]
+theorem Spec.IterM.fold_map {α β γ δ : Type w} {m : Type w → Type w'} {ps}
+    [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [WPMonad m ps]
+    [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {f : β → γ} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} {P Q}
+    (h : Triple (it.fold (init := init) (fun d b => g d (f b))) P Q) :
+    Triple ((it.map f).fold (init := init) g) P Q := by
+  rwa [Std.IterM.fold_map]
+
+@[spec]
+theorem Spec.IterM.fold_filter {α β δ : Type w} {m : Type w → Type w'} {ps}
+    [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [WPMonad m ps]
+    [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {f : β → Bool} {g : δ → β → δ} {init : δ} {it : IterM (α := α) m β} {P Q}
+    (h : Triple (it.fold (init := init) (fun d b => if f b then g d b else d)) P Q) :
+    Triple ((it.filter f).fold (init := init) g) P Q := by
+  rwa [Std.IterM.fold_filter]
+
+variable {α β β₂ γ : Type w} [Iterator α Id β] {ps : PostShape}
+
+@[spec]
+theorem Spec.Iter.forIn_filterMapWithPostcondition
+    [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
+    [MonadLiftT n o] [LawfulMonadLiftT n o] [Finite α Id]
+    [IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
+    {it : Iter (α := α) β} {f : β → PostconditionT n (Option β₂)} {init : γ}
+    {g : β₂ → γ → o (ForInStep γ)} {P Q}
+    (h : Triple (forIn (m := o) it init (fun out acc => do
+        match ← (f out).run with
+        | some c => g c acc
+        | none => return .yield acc)) P Q) :
+    Triple (forIn (it.filterMapWithPostcondition f) init g) P Q := by
+  rwa [Std.Iter.forIn_filterMapWithPostcondition]
+
+@[spec]
+theorem Spec.Iter.forIn_filterMapM
+    [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
+    [MonadAttach n] [WeaklyLawfulMonadAttach n]
+    [MonadLiftT n o] [LawfulMonadLiftT n o]
+    [Finite α Id] [IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
+    {it : Iter (α := α) β} {f : β → n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)} {P Q}
+    (h : Triple (forIn (m := o) it init (fun out acc => do
+        match ← f out with
+        | some c => g c acc
+        | none => return .yield acc)) P Q) :
+    Triple (forIn (it.filterMapM f) init g) P Q := by
+  rwa [Std.Iter.forIn_filterMapM]
+
+@[spec]
+theorem Spec.Iter.forIn_filterMap
+    [Monad n] [LawfulMonad n] [WPMonad n ps] [Finite α Id]
+    [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    {it : Iter (α := α) β} {f : β → Option β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} {P Q}
+    (h : Triple (forIn it init (fun out acc => do
+        match f out with
+        | some c => g c acc
+        | none => return .yield acc)) P Q) :
+    Triple (forIn (it.filterMap f) init g) P Q := by
+  rwa [Std.Iter.forIn_filterMap]
+
+@[spec]
+theorem Spec.Iter.forIn_mapWithPostcondition
+    [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
+    [MonadLiftT n o] [LawfulMonadLiftT n o] [Finite α Id]
+    [IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
+    {it : Iter (α := α) β} {f : β → PostconditionT n β₂} {init : γ}
+    {g : β₂ → γ → o (ForInStep γ)} {P Q}
+    (h : Triple (forIn (m := o) it init (fun out acc => do g (← (f out).run) acc)) P Q) :
+    Triple (forIn (it.mapWithPostcondition f) init g) P Q := by
+  rwa [Std.Iter.forIn_mapWithPostcondition]
+
+@[spec]
+theorem Spec.Iter.forIn_mapM
+    [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
+    [MonadAttach n] [WeaklyLawfulMonadAttach n]
+    [MonadLiftT n o] [LawfulMonadLiftT n o]
+    [Finite α Id]
+    [IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
+    {it : Iter (α := α) β} {f : β → n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)} {P Q}
+    (h : Triple (forIn (m := o) it init (fun out acc => do g (← f out) acc)) P Q) :
+    Triple (forIn (it.mapM f) init g) P Q := by
+  rwa [Std.Iter.forIn_mapM]
+
+@[spec]
+theorem Spec.Iter.forIn_map
+    [Monad n] [LawfulMonad n] [WPMonad n ps]
+    [Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    {it : Iter (α := α) β} {f : β → β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} {P Q}
+    (h : Triple (forIn it init (fun out acc => do g (f out) acc)) P Q) :
+    Triple (forIn (it.map f) init g) P Q := by
+  rwa [Std.Iter.forIn_map]
+
+@[spec]
+theorem Spec.Iter.forIn_filterWithPostcondition
+    [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
+    [MonadLiftT n o] [LawfulMonadLiftT n o]
+    [Finite α Id] [IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
+    {it : Iter (α := α) β} {f : β → PostconditionT n (ULift Bool)} {init : γ}
+    {g : β → γ → o (ForInStep γ)} {P Q}
+    (h : Triple (forIn (m := o) it init (fun out acc => do if (← (f out).run).down then g out acc else return .yield acc)) P Q) :
+    Triple (forIn (it.filterWithPostcondition f) init g) P Q := by
+  rwa [Std.Iter.forIn_filterWithPostcondition]
+
+@[spec]
+theorem Spec.Iter.forIn_filterM
+    [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
+    [MonadAttach n] [WeaklyLawfulMonadAttach n]
+    [MonadLiftT n o] [LawfulMonadLiftT n o] [Finite α Id]
+    [IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
+    {it : Iter (α := α) β} {f : β → n (ULift Bool)} {init : γ} {g : β → γ → o (ForInStep γ)} {P Q}
+    (h : Triple (forIn (m := o) it init (fun out acc => do if (← f out).down then g out acc else return .yield acc)) P Q):
+    Triple (forIn (it.filterM f) init g) P Q := by
+  rwa [Std.Iter.forIn_filterM]
+
+@[spec]
+theorem Spec.Iter.forIn_filter
+    [Monad n] [LawfulMonad n] [WPMonad n ps]
+    [Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    {it : Iter (α := α) β} {f : β → Bool} {init : γ} {g : β → γ → n (ForInStep γ)} {P Q}
+    (h : Triple (forIn it init (fun out acc => do if f out then g out acc else return .yield acc)) P Q) :
+    Triple (forIn (it.filter f) init g) P Q := by
+  rwa [Std.Iter.forIn_filter]
+
+@[spec]
+theorem Iter.foldM_filterMapWithPostcondition {α β γ δ : Type w}
+    {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad n] [Monad o] [LawfulMonad n] [LawfulMonad o] [WPMonad o ps]
+    [IteratorLoop α Id n] [IteratorLoop α Id o]
+    [LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
+    [MonadLiftT n o] [LawfulMonadLiftT n o]
+    {f : β → PostconditionT n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : Iter (α := α) β} {P Q}
+    (h : Triple (it.foldM (m := o) (init := init) (fun d b => do
+          let some c ← (f b).run | pure d
+          g d c)) P Q) :
+    Triple ((it.filterMapWithPostcondition f).foldM (init := init) g) P Q := by
+  rwa [Std.Iter.foldM_filterMapWithPostcondition]
+
+@[spec]
+theorem Iter.foldM_filterMapM {α β γ δ : Type w}
+    {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
+    [Monad o] [LawfulMonad o] [WPMonad o ps]
+    [IteratorLoop α Id n] [IteratorLoop α Id o]
+    [LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
+    [MonadLiftT n o] [LawfulMonadLiftT n o]
+    {f : β → n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : Iter (α := α) β} {P Q}
+    (h : Triple (it.foldM (m := o) (init := init) (fun d b => do
+          let some c ← f b | Pure.pure d
+          g d c)) P Q) :
+    Triple ((it.filterMapM f).foldM (init := init) g) P Q := by
+  rwa [Std.Iter.foldM_filterMapM]
+
+@[spec]
+theorem Iter.foldM_mapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'}
+    {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad m] [Monad n] [Monad o] [LawfulMonad m][LawfulMonad n] [LawfulMonad o] [WPMonad o ps]
+    [IteratorLoop α Id n] [IteratorLoop α Id o]
+    [LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
+    [MonadLiftT n o] [LawfulMonadLiftT n o]
+    {f : β → PostconditionT n γ} {g : δ → γ → o δ} {init : δ} {it : Iter (α := α) β} {P Q}
+    (h : Triple (it.foldM (m := o) (init := init) (fun d b => do let c ← (f b).run; g d c)) P Q) :
+    Triple ((it.mapWithPostcondition f).foldM (init := init) g) P Q := by
+  rwa [Std.Iter.foldM_mapWithPostcondition (m := m)]
+
+@[spec]
+theorem Iter.foldM_mapM {α β γ δ : Type w}
+    {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
+    [Monad o] [LawfulMonad o] [WPMonad o ps]
+    [IteratorLoop α Id n] [IteratorLoop α Id o]
+    [LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
+    [MonadLiftT n o] [LawfulMonadLiftT n o]
+    {f : β → n γ} {g : δ → γ → o δ} {init : δ} {it : Iter (α := α) β} {P Q}
+    (h : Triple (it.foldM (m := o) (init := init) (fun d b => do let c ← f b; g d c)) P Q) :
+    Triple ((it.mapM f).foldM (init := init) g) P Q := by
+  rwa [Std.Iter.foldM_mapM]
+
+@[spec]
+theorem Iter.foldM_filterWithPostcondition {α β δ : Type w}
+    {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad n] [Monad o] [LawfulMonad n] [LawfulMonad o] [WPMonad o ps]
+    [IteratorLoop α Id n] [IteratorLoop α Id o]
+    [LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
+    [MonadLiftT n o] [LawfulMonadLiftT n o]
+    {f : β → PostconditionT n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : Iter (α := α) β} {P Q}
+    (h : Triple (it.foldM (m := o) (init := init) (fun d b => do if (← (f b).run).down then g d b else pure d)) P Q) :
+    Triple ((it.filterWithPostcondition f).foldM (init := init) g) P Q := by
+  rwa [Std.Iter.foldM_filterWithPostcondition]
+
+@[spec]
+theorem Iter.foldM_filterM {α β δ : Type w}
+    {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
+    [Monad o] [LawfulMonad o] [WPMonad o ps]
+    [IteratorLoop α Id n] [IteratorLoop α Id o]
+    [LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
+    [MonadLiftT n o] [LawfulMonadLiftT n o]
+    {f : β → n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : Iter (α := α) β} {P Q}
+    (h : Triple (it.foldM (m := o) (init := init) (fun d b => do if (← f b).down then g d b else pure d)) P Q) :
+    Triple ((it.filterM f).foldM (init := init) g) P Q := by
+  rwa [Std.Iter.foldM_filterM]
+
+@[spec]
+theorem Iter.foldM_filterMap {α β γ δ : Type w} {n : Type w → Type w''}
+    [Iterator α Id β] [Finite α Id] [Monad n] [LawfulMonad n] [WPMonad n ps]
+    [IteratorLoop α Id n]
+    [LawfulIteratorLoop α Id n]
+    {f : β → Option γ} {g : δ → γ → n δ} {init : δ} {it : Iter (α := α) β} {P Q}
+    (h : Triple (it.foldM (init := init) (fun d b => do
+          let some c := f b | pure d
+          g d c)) P Q) :
+    Triple ((it.filterMap f).foldM (init := init) g) P Q := by
+  rwa [Std.Iter.foldM_filterMap]
+
+@[spec]
+theorem Iter.foldM_map {α β γ δ : Type w} {n : Type w → Type w''}
+    [Iterator α Id β] [Finite α Id] [Monad n] [LawfulMonad n] [WPMonad n ps]
+    [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    {f : β → γ} {g : δ → γ → n δ} {init : δ} {it : Iter (α := α) β} {P Q}
+    (h : Triple (it.foldM (init := init) (fun d b => do g d (f b))) P Q) :
+    Triple ((it.map f).foldM (init := init) g) P Q := by
+  rwa [Std.Iter.foldM_map]
+
+@[spec]
+theorem Iter.foldM_filter {α β δ : Type w} {n : Type w → Type w''}
+    [Iterator α Id β] [Finite α Id] [Monad n] [LawfulMonad n] [WPMonad n ps]
+    [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    {f : β → Bool} {g : δ → β → n δ} {init : δ} {it : Iter (α := α) β} {P Q}
+    (h : Triple (it.foldM (init := init) (fun d b => if f b then g d b else pure d)) P Q) :
+    Triple ((it.filter f).foldM (init := init) g) P Q := by
+  rwa [Std.Iter.foldM_filter]
+
+@[spec]
+theorem Iter.fold_filterMapWithPostcondition {α β γ δ : Type w} {n : Type w → Type w''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad n] [LawfulMonad n] [WPMonad n ps]
+    [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    {f : β → PostconditionT n (Option γ)} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} {P Q}
+    (h : Triple (it.foldM (init := init) (fun d b => do
+          let some c ← (f b).run | pure d
+          return g d c)) P Q) :
+    Triple ((it.filterMapWithPostcondition f).fold (init := init) g) P Q := by
+  rwa [Std.Iter.fold_filterMapWithPostcondition]
+
+@[spec]
+theorem Iter.fold_filterMapM {α β γ δ : Type w} {n : Type w → Type w''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [WPMonad n ps]
+    [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    {f : β → n (Option γ)} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} {P Q}
+    (h : Triple (it.foldM (init := init) (fun d b => do
+          let some c ← f b | pure d
+          return g d c)) P Q) :
+    Triple ((it.filterMapM f).fold (init := init) g) P Q := by
+  rwa [Std.Iter.fold_filterMapM]
+
+@[spec]
+theorem Iter.fold_mapWithPostcondition {α β γ δ : Type w} {n : Type w → Type w''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad n] [LawfulMonad n] [WPMonad n ps]
+    [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    {f : β → PostconditionT n γ} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} {P Q}
+    (h : Triple (it.foldM (init := init) (fun d b => do let c ← (f b).run; return g d c)) P Q) :
+    Triple ((it.mapWithPostcondition f).fold (init := init) g) P Q := by
+  rwa [Std.Iter.fold_mapWithPostcondition]
+
+@[spec]
+theorem Iter.fold_mapM {α β γ δ : Type w} {n : Type w → Type w''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [WPMonad n ps]
+    [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    {f : β → n γ} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} {P Q}
+    (h : Triple (it.foldM (init := init) (fun d b => do let c ← f b; return g d c)) P Q) :
+    Triple ((it.mapM f).fold (init := init) g) P Q := by
+  rwa [Std.Iter.fold_mapM]
+
+@[spec]
+theorem Iter.fold_filterWithPostcondition {α β δ : Type w}
+    {n : Type w → Type w''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad n] [LawfulMonad n] [WPMonad n ps]
+    [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    {f : β → PostconditionT n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : Iter (α := α) β} {P Q}
+    (h : Triple (it.foldM (init := init) (fun d b => return if (← (f b).run).down then g d b else d)) P Q) :
+    Triple ((it.filterWithPostcondition f).fold (init := init) g) P Q := by
+  rwa [Std.Iter.fold_filterWithPostcondition]
+
+@[spec]
+theorem Iter.fold_filterM {α β δ : Type w} {n : Type w → Type w''}
+    [Iterator α Id β] [Finite α Id]
+    [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [WPMonad n ps]
+    [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    {f : β → n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : Iter (α := α) β} {P Q}
+    (h : Triple (it.foldM (init := init) (fun d b => return if (← f b).down then g d b else d)) P Q) :
+    Triple ((it.filterM f).fold (init := init) g) P Q := by
+  rwa [Std.Iter.fold_filterM]
+
+end Iterators
+
 @[spec]
 theorem Spec.forIn'_array {α β : Type u} {m : Type u → Type v} {ps : PostShape}
     [Monad m] [WPMonad m ps]
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..3120045992 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// Please update stage0 after merging #11716.
+
 namespace lean {
 options get_default_options() {
     options opts;
diff --git a/tests/lean/run/doLogicTests.lean b/tests/lean/run/doLogicTests.lean
index c1547ab1ed..819d9c944b 100644
--- a/tests/lean/run/doLogicTests.lean
+++ b/tests/lean/run/doLogicTests.lean
@@ -920,35 +920,28 @@ example  : (hp : ∀m, m = 42 → q → p) → (hinv : ∀ (inv : Nat → Prop),
 variable {m} [Monad m]
 open Std Std.Iterators
 
-theorem forIn_eq_sum (xs : Array Nat) {m ps} [Monad m] [WPMonad m ps] :
-    Triple (m := m) (do
-      let mut sum : Nat := 0
-      for n in xs.iter do
-        sum := sum + n
-      return sum) ⌜True⌝ (⇓r => ⌜r = xs.sum⌝) := by
-  mvcgen
-  case inv1 => exact ⇓⟨cur, n⟩ => ⌜n = cur.prefix.sum⌝
-  · simp only [List.sum_append_nat, List.sum_cons, List.sum_nil, Nat.add_zero,
-    Nat.add_right_cancel_iff, SPred.entails.refl]
-  · simp only [List.sum_nil, SPred.entails.refl]
-  · simp only [Array.toList_iter, Array.sum_eq_sum_toList, SPred.entails.refl]
-  · simp only [ExceptConds.entails.refl]
+-- TODO: enable after stage0 update, such that MPL priorities work
+-- theorem forIn_eq_sum (xs : Array Nat) {m ps} [Monad m] [WPMonad m ps] :
+--     Triple (m := m) (do
+--       let mut sum : Nat := 0
+--       for n in xs.iter do
+--         sum := sum + n
+--       return sum) ⌜True⌝ (⇓r => ⌜r = xs.sum⌝) := by
+--   mvcgen
+--   case inv1 => exact ⇓⟨cur, n⟩ => ⌜n = cur.prefix.sum⌝
+--   all_goals grind
 
-theorem forIn_map_eq_sum_add_size (xs : Array Nat) {m ps} [Monad m] [LawfulMonad m]
-    [WPMonad m ps] :
-    Triple (m := m) (do
-      let mut sum : Nat := 0
-      for n in (xs.iterM Id).map (· + 1) do
-        sum := sum + n
-      return sum) ⌜True⌝ (⇓r => ⌜r = xs.sum + xs.size⌝) := by
-  mvcgen
-  case inv1 => exact ⇓⟨cur, n⟩ => ⌜n = cur.prefix.sum⌝
-  all_goals (try grind)
-  apply SPred.pure_mono
-  simp only [IterM.toList_map, Array.toList_iterM, map_pure, Id.run_pure]
-  rw [← Array.sum_eq_sum_toList, ← Array.length_toList]
-  rename_i r
-  induction xs.toList generalizing r <;> grind
+-- TODO: enable after stage0 update, such that MPL priorities work
+-- theorem forIn_map_eq_sum_add_size (xs : Array Nat) {m ps} [Monad m] [LawfulMonad m]
+--     [WPMonad m ps] :
+--     Triple (m := m) (do
+--       let mut sum : Nat := 0
+--       for n in (xs.iterM Id).map (· + 1) do
+--         sum := sum + n
+--       return sum) ⌜True⌝ (⇓r => ⌜r = xs.sum + xs.size⌝) := by
+--   mvcgen
+--   case inv1 => exact ⇓⟨cur, n⟩ => ⌜n = cur.prefix.sum + cur.prefix.length⌝
+--   all_goals grind
 
 theorem forIn_mapM_eq_sum_add_size (xs : Array Nat) {m ps} [Monad m] [MonadAttach m]
     [LawfulMonad m] [WeaklyLawfulMonadAttach m] [WPMonad m ps] :
@@ -970,7 +963,7 @@ theorem forIn_filterMapM_eq_sum_add_size (xs : Array Nat) {m ps}
       return sum) ⌜True⌝ (⇓r => ⌜r = xs.sum + xs.size⌝) := by
   mvcgen
   case inv1 => exact ⇓⟨cur, n⟩ => ⌜n = cur.prefix.sum + cur.prefix.length⌝
-  all_goals (try grind)
+  all_goals grind
 
 theorem foldM_eq_sum (xs : Array Nat) {m ps} [Monad m] [LawfulMonad m]
     [WPMonad m ps] :
@@ -980,4 +973,4 @@ theorem foldM_eq_sum (xs : Array Nat) {m ps} [Monad m] [LawfulMonad m]
       (⇓r => ⌜r = xs.sum⌝) := by
   mvcgen
   case inv1 => exact ⇓⟨cur, n⟩ => ⌜n = cur.prefix.sum⌝
-  all_goals (try grind)
+  all_goals grind