diff --git a/src/Init/Control/Lawful/Basic.lean b/src/Init/Control/Lawful/Basic.lean
index e389521c03..2cbbdb7d6e 100644
--- a/src/Init/Control/Lawful/Basic.lean
+++ b/src/Init/Control/Lawful/Basic.lean
@@ -252,6 +252,7 @@ instance : LawfulMonad Id := by
 @[simp] theorem run_map (x : Id α) (f : α → β) : (f <$> x).run = f x.run := rfl
 @[simp] theorem run_bind (x : Id α) (f : α → Id β) : (x >>= f).run = (f x.run).run := rfl
 @[simp] theorem run_pure (a : α) : (pure a : Id α).run = a := rfl
+@[simp] theorem pure_run (a : Id α) : pure a.run = a := rfl
 @[simp] theorem run_seqRight (x y : Id α) : (x *> y).run = y.run := rfl
 @[simp] theorem run_seqLeft (x y : Id α) : (x <* y).run = x.run := rfl
 @[simp] theorem run_seq (f : Id (α → β)) (x : Id α) : (f <*> x).run = f.run x.run := rfl
diff --git a/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
index 6e4d0afe0c..540c303d82 100644
--- a/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
+++ b/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
@@ -463,7 +463,7 @@ For each value emitted by the base iterator `it`, this combinator calls `f`.
 @[inline, expose]
 def IterM.mapM {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β]
     [Monad n] [MonadLiftT m n] (f : β → n γ) (it : IterM (α := α) m β) :=
-  (it.filterMapWithPostcondition (fun b => some <$> PostconditionT.lift (f b)) : IterM n γ)
+  (it.mapWithPostcondition (fun b => PostconditionT.lift (f b)) : IterM n γ)
 
 /--
 If `it` is an iterator, then `it.filterM f` is another iterator that applies a monadic
diff --git a/src/Init/Data/Iterators/Consumers/Loop.lean b/src/Init/Data/Iterators/Consumers/Loop.lean
index 4bfb754de2..1e0beebffc 100644
--- a/src/Init/Data/Iterators/Consumers/Loop.lean
+++ b/src/Init/Data/Iterators/Consumers/Loop.lean
@@ -139,6 +139,70 @@ def Iter.Partial.fold {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id
     (init : γ) (it : Iter.Partial (α := α) β) : γ :=
   ForIn.forIn (m := Id) it init (fun x acc => ForInStep.yield (f acc x))
 
+set_option doc.verso true in
+/--
+Returns {lean}`true` if the monadic predicate {name}`p` returns {lean}`true` for
+any element emitted by the iterator {name}`it`.
+
+{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
+examined in order of iteration.
+-/
+@[specialize]
+def Iter.anyM {α β : Type w} {m : Type → Type w'} [Monad m]
+    [Iterator α Id β] [IteratorLoop α Id m] [Finite α Id]
+    (p : β → m Bool) (it : Iter (α := α) β) : m Bool :=
+  ForIn.forIn it false (fun x _ => do
+    if ← p x then
+      return .done true
+    else
+      return .yield false)
+
+set_option doc.verso true in
+/--
+Returns {lean}`true` if the pure predicate {name}`p` returns {lean}`true` for
+any element emitted by the iterator {name}`it`.
+
+{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
+examined in order of iteration.
+-/
+@[inline]
+def Iter.any {α β : Type w}
+    [Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id]
+    (p : β → Bool) (it : Iter (α := α) β) : Bool :=
+  (it.anyM (fun x => pure (f := Id) (p x))).run
+
+set_option doc.verso true in
+/--
+Returns {lean}`true` if the monadic predicate {name}`p` returns {lean}`true` for
+all elements emitted by the iterator {name}`it`.
+
+{lit}`O(|xs|)`. Short-circuits upon encountering the first mismatch. The elements in {name}`it` are
+examined in order of iteration.
+-/
+@[specialize]
+def Iter.allM {α β : Type w} {m : Type → Type w'} [Monad m]
+    [Iterator α Id β] [IteratorLoop α Id m] [Finite α Id]
+    (p : β → m Bool) (it : Iter (α := α) β) : m Bool :=
+  ForIn.forIn it true (fun x _ => do
+    if ← p x then
+      return .yield true
+    else
+      return .done false)
+
+set_option doc.verso true in
+/--
+Returns {lean}`true` if the pure predicate {name}`p` returns {lean}`true` for
+all elements emitted by the iterator {name}`it`.
+
+{lit}`O(|xs|)`. Short-circuits upon encountering the first mismatch. The elements in {name}`it` are
+examined in order of iteration.
+-/
+@[inline]
+def Iter.all {α β : Type w}
+    [Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id]
+    (p : β → Bool) (it : Iter (α := α) β) : Bool :=
+  (it.allM (fun x => pure (f := Id) (p x))).run
+
 @[always_inline, inline, expose, inherit_doc IterM.size]
 def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSize α Id]
     (it : Iter (α := α) β) : Nat :=
diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean
index b7a8bddc0c..6176a5b8ec 100644
--- a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean
+++ b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean
@@ -416,6 +416,169 @@ def IterM.Partial.drain {α : Type w} {m : Type w → Type w'} [Monad m] {β : T
     m PUnit :=
   it.fold (γ := PUnit) (fun _ _ => .unit) .unit
 
+set_option doc.verso true in
+/--
+Returns {lean}`ULift.up true` if the monadic predicate {name}`p` returns {lean}`ULift.up true` for
+any element emitted by the iterator {name}`it`.
+
+{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
+examined in order of iteration.
+
+This function requires a {name}`Finite` instance proving that the iterator will finish after a
+finite number of steps. If the iterator is not finite or such an instance is not available,
+consider using {lit}`it.allowNontermination.anyM` instead of {lean}`it.anyM`. However, it is not
+possible to formally verify the behavior of the partial variant.
+-/
+@[specialize]
+def IterM.anyM {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [IteratorLoop α m m] [Finite α m]
+    (p : β → m (ULift Bool)) (it : IterM (α := α) m β) : m (ULift Bool) :=
+  ForIn.forIn it (ULift.up false) (fun x _ => do
+    if (← p x).down then
+      return .done (.up true)
+    else
+      return .yield (.up false))
+
+set_option doc.verso true in
+/--
+Returns {lean}`ULift.up true` if the monadic predicate {name}`p` returns {lean}`ULift.up true` for
+any element emitted by the iterator {name}`it`.
+
+{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
+examined in order of iteration.
+
+This is a partial, potentially nonterminating, function. It is not possible to formally verify
+its behavior. If the iterator has a {name}`Finite` instance, consider using {name}`IterM.anyM`
+instead.
+-/
+@[specialize]
+def IterM.Partial.anyM {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [IteratorLoopPartial α m m]
+    (p : β → m (ULift Bool)) (it : IterM.Partial (α := α) m β) : m (ULift Bool) :=
+  ForIn.forIn it (ULift.up false) (fun x _ => do
+    if (← p x).down then
+      return .done (.up true)
+    else
+      return .yield (.up false))
+
+set_option doc.verso true in
+/--
+Returns {lean}`ULift.up true` if the pure predicate {name}`p` returns {lean}`true` for
+any element emitted by the iterator {name}`it`.
+
+{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
+examined in order of iteration.
+
+This function requires a {name}`Finite` instance proving that the iterator will finish after a
+finite number of steps. If the iterator is not finite or such an instance is not available,
+consider using {lit}`it.allowNontermination.any` instead of {lean}`it.any`. However, it is not
+possible to formally verify the behavior of the partial variant.
+-/
+@[inline]
+def IterM.any {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [IteratorLoop α m m] [Finite α m]
+    (p : β → Bool) (it : IterM (α := α) m β) : m (ULift Bool) := do
+  it.anyM (fun x => pure (.up (p x)))
+
+set_option doc.verso true in
+/--
+Returns {lean}`ULift.up true` if the pure predicate {name}`p` returns {lean}`true` for
+any element emitted by the iterator {name}`it`.
+
+{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
+examined in order of iteration.
+
+This is a partial, potentially nonterminating, function. It is not possible to formally verify
+its behavior. If the iterator has a {name}`Finite` instance, consider using {name}`IterM.any`
+instead.
+-/
+@[inline]
+def IterM.Partial.any {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [IteratorLoopPartial α m m]
+    (p : β → Bool) (it : IterM.Partial (α := α) m β) : m (ULift Bool) := do
+  it.anyM (fun x => pure (.up (p x)))
+
+set_option doc.verso true in
+/--
+Returns {lean}`ULift.up true` if the monadic predicate {name}`p` returns {lean}`ULift.up true` for
+all elements emitted by the iterator {name}`it`.
+
+{lit}`O(|xs|)`. Short-circuits upon encountering the first mismatch. The elements in {name}`it` are
+examined in order of iteration.
+
+This function requires a {name}`Finite` instance proving that the iterator will finish after a
+finite number of steps. If the iterator is not finite or such an instance is not available,
+consider using {lit}`it.allowNontermination.allM` instead of {lean}`it.allM`. However, it is not
+possible to formally verify the behavior of the partial variant.
+-/
+@[specialize]
+def IterM.allM {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [IteratorLoop α m m] [Finite α m]
+    (p : β → m (ULift Bool)) (it : IterM (α := α) m β) : m (ULift Bool) := do
+  ForIn.forIn it (ULift.up true) (fun x _ => do
+    if (← p x).down then
+      return .yield (.up true)
+    else
+      return .done (.up false))
+set_option doc.verso true in
+/--
+Returns {lean}`ULift.up true` if the monadic predicate {name}`p` returns {lean}`ULift.up true` for
+all elements emitted by the iterator {name}`it`.
+
+{lit}`O(|xs|)`. Short-circuits upon encountering the first mismatch. The elements in {name}`it` are
+examined in order of iteration.
+
+This is a partial, potentially nonterminating, function. It is not possible to formally verify
+its behavior. If the iterator has a {name}`Finite` instance, consider using {name}`IterM.allM`
+instead.
+-/
+@[specialize]
+def IterM.Partial.allM {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [IteratorLoopPartial α m m]
+    (p : β → m (ULift Bool)) (it : IterM.Partial (α := α) m β) : m (ULift Bool) := do
+  ForIn.forIn it (ULift.up true) (fun x _ => do
+    if (← p x).down then
+      return .yield (.up true)
+    else
+      return .done (.up false))
+
+set_option doc.verso true in
+/--
+Returns {lean}`ULift.up true` if the pure predicate {name}`p` returns {lean}`true` for
+all elements emitted by the iterator {name}`it`.
+
+{lit}`O(|xs|)`. Short-circuits upon encountering the first mismatch. The elements in {name}`it` are
+examined in order of iteration.
+
+This function requires a {name}`Finite` instance proving that the iterator will finish after a
+finite number of steps. If the iterator is not finite or such an instance is not available,
+consider using {lit}`it.allowNontermination.all` instead of {lean}`it.all`. However, it is not
+possible to formally verify the behavior of the partial variant.
+-/
+@[inline]
+def IterM.all {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [IteratorLoop α m m] [Finite α m]
+    (p : β → Bool) (it : IterM (α := α) m β) : m (ULift Bool) := do
+  it.allM (fun x => pure (.up (p x)))
+
+set_option doc.verso true in
+/--
+Returns {lean}`ULift.up true` if the pure predicate {name}`p` returns {lean}`true` for
+all elements emitted by the iterator {name}`it`.
+
+{lit}`O(|xs|)`. Short-circuits upon encountering the first mismatch. The elements in {name}`it` are
+examined in order of iteration.
+
+This is a partial, potentially nonterminating, function. It is not possible to formally verify
+its behavior. If the iterator has a {name}`Finite` instance, consider using {name}`IterM.all`
+instead.
+-/
+@[inline]
+def IterM.Partial.all {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [IteratorLoopPartial α m m]
+    (p : β → Bool) (it : IterM.Partial (α := α) m β) : m (ULift Bool) := do
+  it.allM (fun x => pure (.up (p x)))
+
 section Size
 
 /--
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
index bccf7bbb0d..390419641a 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
@@ -179,7 +179,7 @@ theorem Iter.step_filterM {f : β → n (ULift Bool)}
   | .done h => rfl
 
 theorem Iter.step_mapM {f : β → n γ}
-    [Monad n] [LawfulMonad n] [MonadLiftT m n] :
+    [Monad n] [LawfulMonad n] :
   (it.mapM f).step = (do
     match it.step with
     | .yield it' out h => do
@@ -195,7 +195,6 @@ theorem Iter.step_mapM {f : β → n γ}
   match step with
   | .yield it' out h =>
     simp only [bind_pure_comp]
-    simp only [Functor.map]
     rfl
   | .skip it' h => rfl
   | .done h => rfl
@@ -222,6 +221,24 @@ theorem Iter.step_filterMap {f : β → Option γ} :
   · simp
   · simp
 
+/--
+a weaker version of `step_filterMap` that does not use dependent `match`
+-/
+theorem Iter.val_step_filterMap {f : β → Option γ} :
+    (it.filterMap f).step.val = match it.step.val with
+      | .yield it' out =>
+        match f out with
+        | none => .skip (it'.filterMap f)
+        | some out' => .yield (it'.filterMap f) out'
+      | .skip it' => .skip (it'.filterMap f)
+      | .done => .done := by
+  simp [step_filterMap]
+  cases it.step using PlausibleIterStep.casesOn
+  · simp only
+    split <;> simp_all
+  · simp
+  · simp
+
 theorem Iter.step_map {f : β → γ} :
     (it.map f).step = match it.step with
       | .yield it' out h =>
@@ -253,6 +270,25 @@ def Iter.step_filter {f : β → Bool} :
   · simp
   · simp
 
+def Iter.val_step_filter {f : β → Bool} :
+    (it.filter f).step.val = match it.step.val with
+      | .yield it' out =>
+        if f out = true then
+          .yield (it'.filter f) out
+        else
+          .skip (it'.filter f)
+      | .skip it' =>
+        .skip (it'.filter f)
+      | .done =>
+        .done := by
+  simp only [filter_eq_toIter_filter_toIterM, step, toIterM_toIter, IterM.step_filter, Id.run_bind]
+  generalize it.toIterM.step.run = step
+  cases step using PlausibleIterStep.casesOn
+  · simp only
+    split <;> simp [*]
+  · simp
+  · simp
+
 @[simp]
 theorem Iter.toList_filterMap
     [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] [Finite α Id]
@@ -431,4 +467,317 @@ theorem Iter.fold_map {α β γ : Type w} {δ : Type x}
 
 end Fold
 
+theorem Iter.anyM_filterMapM {α β β' : Type w} {m : Type w → Type w'}
+    [Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m]
+    {it : Iter (α := α) β} {f : β → m (Option β')} {p : β' → m (ULift Bool)} :
+    (it.filterMapM f).anyM p = (it.mapM (pure (f := m))).anyM (fun x => do
+      match ← f x with
+      | some fx => p fx
+      | none => return .up false) := by
+  simp only [filterMapM_eq_toIter_filterMapM_toIterM, IterM.anyM_filterMapM]
+  rfl
+
+-- There is hope to generalize the following theorem as soon there is a `Shrink` type.
+/--
+This lemma expresses `Iter.anyM` in terms of `IterM.anyM`.
+It requires all involved types to live in `Type 0`.
+-/
+theorem Iter.anyM_eq_anyM_mapM_pure {α β : Type} {m : Type → Type w'} [Iterator α Id β]
+    [Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    {it : Iter (α := α) β} {p : β → m Bool} :
+    it.anyM p = ULift.down <$> (it.mapM (α := α) (pure (f := m))).anyM (fun x => ULift.up <$> p x) := by
+  rw [anyM_eq_forIn, IterM.anyM_eq_forIn, map_eq_pure_bind]
+  induction it using Iter.inductSteps with | step it ihy ihs =>
+  rw [forIn_eq_match_step, IterM.forIn_eq_match_step, bind_assoc, step_mapM]
+  cases it.step using PlausibleIterStep.casesOn
+  · simp only [bind_assoc, liftM_pure, pure_bind, map_eq_pure_bind]
+    apply bind_congr; intro px
+    split
+    · simp
+    · simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
+theorem Iter.anyM_mapM {α β β' : Type w} {m : Type w → Type w'}
+    [Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m]
+    {it : Iter (α := α) β} {f : β → m β'} {p : β' → m (ULift Bool)} :
+    (it.mapM f).anyM p = (it.mapM (pure (f := m))).anyM (fun x => do p (← f x)) := by
+  rw [mapM_eq_toIter_mapM_toIterM, IterM.anyM_mapM, mapM_eq_toIter_mapM_toIterM]
+
+theorem Iter.anyM_filterM {α β : Type w} {m : Type w → Type w'}
+    [Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m]
+    {it : Iter (α := α) β} {f : β → m (ULift Bool)} {p : β → m (ULift Bool)} :
+    (it.filterM f).anyM p = (it.mapM (pure (f := m))).anyM (fun x => do
+        if (← f x).down then
+          p x
+        else
+          return .up false) := by
+  rw [filterM_eq_toIter_filterM_toIterM, IterM.anyM_filterM, mapM_eq_toIter_mapM_toIterM]
+
+theorem Iter.anyM_filterMap {α β β' : Type w} {m : Type → Type w'}
+    [Iterator α Id β] [Finite α Id] [Monad m] [IteratorLoop α Id m]
+    [LawfulMonad m] [LawfulIteratorLoop α Id m]
+    {it : Iter (α := α) β} {f : β → Option β'} {p : β' → m Bool} :
+    (it.filterMap f).anyM p = it.anyM (fun x => do
+      match f x with
+      | some fx => p fx
+      | none => return false) := by
+  induction it using Iter.inductSteps with | step it ihy ihs
+  rw [anyM_eq_match_step, anyM_eq_match_step, val_step_filterMap]
+  cases it.step using PlausibleIterStep.casesOn
+  · rename_i out _
+    simp only
+    cases f out
+    · simp [ihy ‹_›]
+    · apply bind_congr; intro px
+      split <;> simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
+theorem Iter.anyM_map {α β β' : Type w} {m : Type → Type w'}
+    [Iterator α Id β] [Finite α Id] [Monad m] [IteratorLoop α Id m]
+    [LawfulMonad m] [LawfulIteratorLoop α Id m]
+    {it : Iter (α := α) β} {f : β → β'} {p : β' → m Bool} :
+    (it.map f).anyM p = it.anyM (fun x => p (f x)) := by
+  induction it using Iter.inductSteps with | step it ihy ihs
+  rw [anyM_eq_match_step, anyM_eq_match_step, step_map]
+  cases it.step using PlausibleIterStep.casesOn
+  · simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
+theorem Iter.anyM_filter {α β : Type w} {m : Type → Type w'}
+    [Iterator α Id β] [Finite α Id] [Monad m][IteratorLoop α Id m]
+    [LawfulMonad m] [LawfulIteratorLoop α Id m]
+    {it : Iter (α := α) β} {f : β → Bool} {p : β → m Bool} :
+    (it.filter f).anyM p = it.anyM (fun x => do
+        if f x then
+          p x
+        else
+          return false) := by
+  induction it using Iter.inductSteps with | step it ihy ihs
+  rw [anyM_eq_match_step, anyM_eq_match_step, val_step_filter]
+  cases it.step using PlausibleIterStep.casesOn
+  · rename_i out _
+    simp only
+    cases f out <;> simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
+theorem Iter.any_filterMapM {α β β' : Type w} {m : Type w → Type w'}
+    [Iterator α Id β] [Finite α Id] [Monad m] [IteratorLoop α Id m]
+    [LawfulMonad m] [LawfulIteratorLoop α Id m]
+    {it : Iter (α := α) β} {f : β → m (Option β')} {p : β' → Bool} :
+    (it.filterMapM f).any p = (it.mapM (pure (f := m))).anyM (fun x => do
+      match ← f x with
+      | some fx => return .up (p fx)
+      | none => return .up false) := by
+  simp [IterM.any_eq_anyM, anyM_filterMapM]
+
+theorem Iter.any_mapM {α β β' : Type w} {m : Type w → Type w'}
+    [Iterator α Id β] [Finite α Id] [Monad m] [IteratorLoop α Id m]
+    [LawfulMonad m] [LawfulIteratorLoop α Id m]
+    {it : Iter (α := α) β} {f : β → m β'} {p : β' → Bool} :
+    (it.mapM f).any p = (it.mapM pure).anyM (fun x => (.up <| p ·) <$> (f x)) := by
+  simp [IterM.any_eq_anyM, anyM_mapM]
+
+theorem Iter.any_filterM {α β : Type w} {m : Type w → Type w'}
+    [Iterator α Id β] [Finite α Id] [Monad m] [IteratorLoop α Id m]
+    [LawfulMonad m] [LawfulIteratorLoop α Id m]
+    {it : Iter (α := α) β} {f : β → m (ULift Bool)} {p : β → Bool} :
+    (it.filterM f).any p = (it.mapM (pure (f := m))).anyM (fun x => do
+        if (← f x).down then
+          return .up (p x)
+        else
+          return .up false) := by
+  simp [IterM.any_eq_anyM, anyM_filterM]
+
+theorem Iter.any_filterMap {α β β' : Type w}
+    [Iterator α Id β] [Finite α Id][IteratorLoop α Id Id]
+    [LawfulIteratorLoop α Id Id]
+    {it : Iter (α := α) β} {f : β → Option β'} {p : β' → Bool} :
+    (it.filterMap f).any p = it.any (fun x =>
+      match f x with
+      | some fx => (p fx)
+      | none => false) := by
+  induction it using Iter.inductSteps with | step it ihy ihs
+  rw [any_eq_match_step, any_eq_match_step, val_step_filterMap]
+  cases it.step using PlausibleIterStep.casesOn
+  · rename_i out _
+    simp only
+    cases f out
+    · simp [*, ihy ‹_›]
+    · simp only
+      split <;> simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
+theorem Iter.any_map {α β β' : Type w}
+    [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id]
+    [LawfulIteratorLoop α Id Id]
+    {it : Iter (α := α) β} {f : β → β'} {p : β' → Bool} :
+    (it.map f).any p = it.any (fun x => p (f x)) := by
+  induction it using Iter.inductSteps with | step it ihy ihs
+  rw [any_eq_match_step, any_eq_match_step, step_map]
+  cases it.step using PlausibleIterStep.casesOn
+  · simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
+theorem Iter.allM_filterMapM {α β β' : Type w} {m : Type w → Type w'}
+    [Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m]
+    {it : Iter (α := α) β} {f : β → m (Option β')} {p : β' → m (ULift Bool)} :
+    (it.filterMapM f).allM p = (it.mapM (pure (f := m))).allM (fun x => do
+      match ← f x with
+      | some fx => p fx
+      | none => return .up true) := by
+  simp only [filterMapM_eq_toIter_filterMapM_toIterM, IterM.allM_filterMapM]
+  rfl
+
+/--
+This lemma expresses `Iter.allM` in terms of `IterM.allM`.
+It requires all involved types to live in `Type 0`.
+-/
+theorem Iter.allM_eq_allM_mapM_pure {α β : Type} {m : Type → Type w'} [Iterator α Id β]
+    [Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    {it : Iter (α := α) β} {p : β → m Bool} :
+    it.allM p = ULift.down <$> (it.mapM (α := α) (pure (f := m))).allM (fun x => ULift.up <$> p x) := by
+  rw [allM_eq_forIn, IterM.allM_eq_forIn, map_eq_pure_bind]
+  induction it using Iter.inductSteps with | step it ihy ihs =>
+  rw [forIn_eq_match_step, IterM.forIn_eq_match_step, bind_assoc, step_mapM]
+  cases it.step using PlausibleIterStep.casesOn
+  · simp only [bind_assoc, liftM_pure, pure_bind, map_eq_pure_bind]
+    apply bind_congr; intro px
+    split
+    · simp [ihy ‹_›]
+    · simp
+  · simp [ihs ‹_›]
+  · simp
+
+theorem Iter.allM_mapM {α β β' : Type w} {m : Type w → Type w'}
+    [Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m]
+    {it : Iter (α := α) β} {f : β → m β'} {p : β' → m (ULift Bool)} :
+    (it.mapM f).allM p = (it.mapM (pure (f := m))).allM (fun x => do p (← f x)) := by
+  rw [mapM_eq_toIter_mapM_toIterM, IterM.allM_mapM, mapM_eq_toIter_mapM_toIterM]
+
+theorem Iter.allM_filterM {α β : Type w} {m : Type w → Type w'}
+    [Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m]
+    {it : Iter (α := α) β} {f : β → m (ULift Bool)} {p : β → m (ULift Bool)} :
+    (it.filterM f).allM p = (it.mapM (pure (f := m))).allM (fun x => do
+        if (← f x).down then
+          p x
+        else
+          return .up true) := by
+  rw [filterM_eq_toIter_filterM_toIterM, IterM.allM_filterM, mapM_eq_toIter_mapM_toIterM]
+
+theorem Iter.allM_filterMap {α β β' : Type w} {m : Type → Type w'}
+    [Iterator α Id β] [Finite α Id] [Monad m] [IteratorLoop α Id m]
+    [LawfulMonad m] [LawfulIteratorLoop α Id m]
+    {it : Iter (α := α) β} {f : β → Option β'} {p : β' → m Bool} :
+    (it.filterMap f).allM p = it.allM (fun x => do
+      match f x with
+      | some fx => p fx
+      | none => return true) := by
+  induction it using Iter.inductSteps with | step it ihy ihs
+  rw [allM_eq_match_step, allM_eq_match_step, val_step_filterMap]
+  cases it.step using PlausibleIterStep.casesOn
+  · rename_i out _
+    simp only
+    cases f out
+    · simp [ihy ‹_›]
+    · apply bind_congr; intro px
+      split <;> simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
+theorem Iter.allM_map {α β β' : Type w} {m : Type → Type w'}
+    [Iterator α Id β] [Finite α Id] [Monad m] [IteratorLoop α Id m]
+    [LawfulMonad m] [LawfulIteratorLoop α Id m]
+    {it : Iter (α := α) β} {f : β → β'} {p : β' → m Bool} :
+    (it.map f).allM p = it.allM (fun x => p (f x)) := by
+  induction it using Iter.inductSteps with | step it ihy ihs
+  rw [allM_eq_match_step, allM_eq_match_step, step_map]
+  cases it.step using PlausibleIterStep.casesOn
+  · simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
+theorem Iter.allM_filter {α β : Type w} {m : Type → Type w'}
+    [Iterator α Id β] [Finite α Id] [Monad m][IteratorLoop α Id m]
+    [LawfulMonad m] [LawfulIteratorLoop α Id m]
+    {it : Iter (α := α) β} {f : β → Bool} {p : β → m Bool} :
+    (it.filter f).allM p = it.allM (fun x => do
+        if f x then
+          p x
+        else
+          return true) := by
+  induction it using Iter.inductSteps with | step it ihy ihs
+  rw [allM_eq_match_step, allM_eq_match_step, val_step_filter]
+  cases it.step using PlausibleIterStep.casesOn
+  · rename_i out _
+    simp only
+    cases f out <;> simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
+theorem Iter.all_filterMapM {α β β' : Type w} {m : Type w → Type w'}
+    [Iterator α Id β] [Finite α Id] [Monad m] [IteratorLoop α Id m]
+    [LawfulMonad m] [LawfulIteratorLoop α Id m]
+    {it : Iter (α := α) β} {f : β → m (Option β')} {p : β' → Bool} :
+    (it.filterMapM f).all p = (it.mapM (pure (f := m))).allM (fun x => do
+      match ← f x with
+      | some fx => return .up (p fx)
+      | none => return .up true) := by
+  simp [IterM.all_eq_allM, allM_filterMapM]
+
+theorem Iter.all_mapM {α β β' : Type w} {m : Type w → Type w'}
+    [Iterator α Id β] [Finite α Id] [Monad m] [IteratorLoop α Id m]
+    [LawfulMonad m] [LawfulIteratorLoop α Id m]
+    {it : Iter (α := α) β} {f : β → m β'} {p : β' → Bool} :
+    (it.mapM f).all p = (it.mapM pure).allM (fun x => (.up <| p ·) <$> (f x)) := by
+  simp [IterM.all_eq_allM, allM_mapM]
+
+theorem Iter.all_filterM {α β : Type w} {m : Type w → Type w'}
+    [Iterator α Id β] [Finite α Id] [Monad m] [IteratorLoop α Id m]
+    [LawfulMonad m] [LawfulIteratorLoop α Id m]
+    {it : Iter (α := α) β} {f : β → m (ULift Bool)} {p : β → Bool} :
+    (it.filterM f).all p = (it.mapM (pure (f := m))).allM (fun x => do
+        if (← f x).down then
+          return .up (p x)
+        else
+          return .up true) := by
+  simp [IterM.all_eq_allM, allM_filterM]
+
+theorem Iter.all_filterMap {α β β' : Type w}
+    [Iterator α Id β] [Finite α Id][IteratorLoop α Id Id]
+    [LawfulIteratorLoop α Id Id]
+    {it : Iter (α := α) β} {f : β → Option β'} {p : β' → Bool} :
+    (it.filterMap f).all p = it.all (fun x =>
+      match f x with
+      | some fx => (p fx)
+      | none => true) := by
+  induction it using Iter.inductSteps with | step it ihy ihs
+  rw [all_eq_match_step, all_eq_match_step, val_step_filterMap]
+  cases it.step using PlausibleIterStep.casesOn
+  · rename_i out _
+    simp only
+    cases f out
+    · simp [*, ihy ‹_›]
+    · simp only
+      split <;> simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
+theorem Iter.all_map {α β β' : Type w}
+    [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id]
+    [LawfulIteratorLoop α Id Id]
+    {it : Iter (α := α) β} {f : β → β'} {p : β' → Bool} :
+    (it.map f).all p = it.all (fun x => p (f x)) := by
+  induction it using Iter.inductSteps with | step it ihy ihs
+  rw [all_eq_match_step, all_eq_match_step, step_map]
+  cases it.step using PlausibleIterStep.casesOn
+  · simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
 end Std.Iterators
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
index 1ed1ceb549..c1b98f95de 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
@@ -160,7 +160,7 @@ theorem IterM.step_mapM {γ : Type w} {f : β → n γ}
   match step with
   | .yield it' out h =>
     simp only [bind_pure_comp]
-    simp only [PostconditionT.lift, Functor.map]
+    simp only [PostconditionT.lift]
     simp only [PostconditionT.operation_map, Functor.map_map, PlausibleIterStep.skip,
       PlausibleIterStep.yield, bind_map_left, bind_pure_comp]
     rfl
@@ -539,4 +539,356 @@ theorem IterM.fold_map {α β γ δ : Type w} {m : Type w → Type w'}
 
 end Fold
 
+section AnyAll
+
+theorem IterM.anyM_filterMapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
+    [Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n]
+    [LawfulMonad m] [LawfulMonad n]
+    {it : IterM (α := α) m β} {f : β → n (Option β')} {p : β' → n (ULift Bool)} :
+    (it.filterMapM f).anyM p = (it.mapM (pure (f := n))).anyM (fun x => do
+      match ← f x with
+      | some fx => p fx
+      | none => return .up false) := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [anyM_eq_match_step, anyM_eq_match_step, step_filterMapM, step_mapM, bind_assoc, bind_assoc]
+  apply bind_congr; intro step
+  split
+  · simp only [bind_assoc, pure_bind]
+    apply bind_congr; intro fx
+    split
+    · simp [ihy ‹_›]
+    · simp only [PlausibleIterStep.yield, pure_bind]
+      apply bind_congr; intro px
+      split <;> simp [ihy ‹_›]
+  · simp only [PlausibleIterStep.skip, pure_bind, bind_assoc]
+    simp [ihs ‹_›]
+  · simp
+
+theorem IterM.anyM_mapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
+    [Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n]
+    [LawfulMonad m] [LawfulMonad n]
+    {it : IterM (α := α) m β} {f : β → n β'} {p : β' → n (ULift Bool)} :
+    (it.mapM f).anyM p = (it.mapM (pure (f := n))).anyM (fun x => do p (← f x)) := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [anyM_eq_match_step, anyM_eq_match_step, step_mapM, step_mapM, bind_assoc, bind_assoc]
+  apply bind_congr; intro step
+  split
+  · simp only [bind_assoc, pure_bind]
+    apply bind_congr; intro fx
+    simp [ihy ‹_›]
+  · simp only [PlausibleIterStep.skip, pure_bind, bind_assoc]
+    simp [ihs ‹_›]
+  · simp
+
+theorem IterM.anyM_filterM {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
+    [Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n]
+    [LawfulMonad m] [LawfulMonad n]
+    {it : IterM (α := α) m β} {f : β → n (ULift Bool)} {p : β → n (ULift Bool)} :
+    (it.filterM f).anyM p = (it.mapM (pure (f := n))).anyM (fun x => do
+        if (← f x).down then
+          p x
+        else
+          return .up false) := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [anyM_eq_match_step, anyM_eq_match_step, step_mapM, step_filterM, bind_assoc, bind_assoc]
+  apply bind_congr; intro step
+  split
+  · simp only [bind_assoc, pure_bind]
+    apply bind_congr; intro fx
+    split <;> simp [ihy ‹_›]
+  · simp only [PlausibleIterStep.skip, pure_bind, bind_assoc]
+    simp [ihs ‹_›]
+  · simp
+
+theorem IterM.anyM_filterMap {α β β' : Type w} {m : Type w → Type w'}
+    [Iterator α m β] [Finite α m] [Monad m] [IteratorLoop α m m]
+    [LawfulMonad m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {f : β → Option β'} {p : β' → m (ULift Bool)} :
+    (it.filterMap f).anyM p = it.anyM (fun x => do
+      match f x with
+      | some fx => p fx
+      | none => return .up false) := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [anyM_eq_match_step, anyM_eq_match_step, step_filterMap, bind_assoc]
+  apply bind_congr; intro step
+  split
+  · split
+    · simp [*, ihy ‹_›]
+    · simp only [*, PlausibleIterStep.yield, pure_bind]
+      apply bind_congr; intro px
+      split <;> simp [ihy ‹_›]
+  · simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
+  · simp
+
+theorem IterM.anyM_map {α β β' : Type w} {m : Type w → Type w'}
+    [Iterator α m β] [Finite α m] [Monad m] [IteratorLoop α m m]
+    [LawfulMonad m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {f : β → β'} {p : β' → m (ULift Bool)} :
+    (it.map f).anyM p = it.anyM (fun x => p (f x)) := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [anyM_eq_match_step, anyM_eq_match_step, step_map, bind_assoc]
+  apply bind_congr; intro step
+  split
+  · simp only [pure_bind]
+    apply bind_congr; intro fx
+    simp [ihy ‹_›]
+  · simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
+  · simp
+
+theorem IterM.anyM_filter {α β : Type w} {m : Type w → Type w'}
+    [Iterator α m β] [Finite α m] [Monad m][IteratorLoop α m m]
+    [LawfulMonad m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {f : β → Bool} {p : β → m (ULift Bool)} :
+    (it.filter f).anyM p = it.anyM (fun x => do
+        if f x then
+          p x
+        else
+          return .up false) := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [anyM_eq_match_step, anyM_eq_match_step, step_filter, bind_assoc]
+  apply bind_congr; intro step
+  split
+  · simp only
+    split <;> simp [ihy ‹_›]
+  · simp only [PlausibleIterStep.skip, pure_bind]
+    simp [ihs ‹_›]
+  · simp
+
+theorem IterM.any_filterMapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
+    [Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n] [IteratorLoop α m m]
+    [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {f : β → n (Option β')} {p : β' → Bool} :
+    (it.filterMapM f).any p = (it.mapM (pure (f := n))).anyM (fun x => do
+      match ← f x with
+      | some fx => return .up (p fx)
+      | none => return .up false) := by
+  simp [any_eq_anyM, anyM_filterMapM]
+
+theorem IterM.any_mapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
+    [Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n] [IteratorLoop α m m]
+    [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {f : β → n β'} {p : β' → Bool} :
+    (it.mapM f).any p = (it.mapM (pure (f := n))).anyM (fun x => (.up <| p ·) <$> (f x)) := by
+  simp [any_eq_anyM, anyM_mapM]
+
+theorem IterM.any_filterM {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
+    [Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n] [IteratorLoop α m m]
+    [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {f : β → n (ULift Bool)} {p : β → Bool} :
+    (it.filterM f).any p = (it.mapM (pure (f := n))).anyM (fun x => do
+        if (← f x).down then
+          return .up (p x)
+        else
+          return .up false) := by
+  simp [any_eq_anyM, anyM_filterM]
+
+theorem IterM.any_filterMap {α β β' : Type w} {m : Type w → Type w'}
+    [Iterator α m β] [Finite α m] [Monad m] [IteratorLoop α m m]
+    [LawfulMonad m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {f : β → Option β'} {p : β' → Bool} :
+    (it.filterMap f).any p = it.any (fun x =>
+      match f x with
+      | some fx => (p fx)
+      | none => false) := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [any_eq_match_step, any_eq_match_step, step_filterMap, bind_assoc]
+  apply bind_congr; intro step
+  split
+  · split
+    · simp [*, ihy ‹_›]
+    · simp only [*, PlausibleIterStep.yield, pure_bind]
+      split <;> simp [ihy ‹_›]
+  · simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
+  · simp
+
+theorem IterM.any_map {α β β' : Type w} {m : Type w → Type w'}
+    [Iterator α m β] [Finite α m] [Monad m] [IteratorLoop α m m]
+    [LawfulMonad m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {f : β → β'} {p : β' → Bool} :
+    (it.map f).any p = it.any (fun x => p (f x)) := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [any_eq_match_step, any_eq_match_step, step_map, bind_assoc]
+  apply bind_congr; intro step
+  split
+  · simp only [pure_bind]
+    simp [ihy ‹_›]
+  · simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
+  · simp
+
+theorem IterM.allM_filterMapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
+    [Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n]
+    [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n]
+    {it : IterM (α := α) m β} {f : β → n (Option β')} {p : β' → n (ULift Bool)} :
+    (it.filterMapM f).allM p = (it.mapM (pure (f := n))).allM (fun x => do
+      match ← f x with
+      | some fx => p fx
+      | none => return .up true) := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [allM_eq_match_step, allM_eq_match_step, step_filterMapM, step_mapM, bind_assoc, bind_assoc]
+  apply bind_congr; intro step
+  split
+  · simp only [bind_assoc, pure_bind]
+    apply bind_congr; intro fx
+    split
+    · simp [ihy ‹_›]
+    · simp only [PlausibleIterStep.yield, pure_bind]
+      apply bind_congr; intro px
+      split <;> simp [ihy ‹_›]
+  · simp only [PlausibleIterStep.skip, pure_bind, bind_assoc]
+    simp [ihs ‹_›]
+  · simp
+
+theorem IterM.allM_mapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
+    [Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n]
+    [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n]
+    {it : IterM (α := α) m β} {f : β → n β'} {p : β' → n (ULift Bool)} :
+    (it.mapM f).allM p = (it.mapM (pure (f := n))).allM (fun x => do p (← f x)) := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [allM_eq_match_step, allM_eq_match_step, step_mapM, step_mapM, bind_assoc, bind_assoc]
+  apply bind_congr; intro step
+  split
+  · simp only [bind_assoc, pure_bind]
+    apply bind_congr; intro fx
+    simp [ihy ‹_›]
+  · simp only [PlausibleIterStep.skip, pure_bind, bind_assoc]
+    simp [ihs ‹_›]
+  · simp
+
+theorem IterM.allM_filterM {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
+    [Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n]
+    [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n]
+    {it : IterM (α := α) m β} {f : β → n (ULift Bool)} {p : β → n (ULift Bool)} :
+    (it.filterM f).allM p = (it.mapM (pure (f := n))).allM (fun x => do
+        if (← f x).down then
+          p x
+        else
+          return .up true) := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [allM_eq_match_step, allM_eq_match_step, step_mapM, step_filterM, bind_assoc, bind_assoc]
+  apply bind_congr; intro step
+  split
+  · simp only [bind_assoc, pure_bind]
+    apply bind_congr; intro fx
+    split <;> simp [ihy ‹_›]
+  · simp only [PlausibleIterStep.skip, pure_bind, bind_assoc]
+    simp [ihs ‹_›]
+  · simp
+
+theorem IterM.allM_filterMap {α β β' : Type w} {m : Type w → Type w'}
+    [Iterator α m β] [Finite α m] [Monad m] [IteratorLoop α m m]
+    [LawfulMonad m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {f : β → Option β'} {p : β' → m (ULift Bool)} :
+    (it.filterMap f).allM p = it.allM (fun x => do
+      match f x with
+      | some fx => p fx
+      | none => return .up true) := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [allM_eq_match_step, allM_eq_match_step, step_filterMap, bind_assoc]
+  apply bind_congr; intro step
+  split
+  · split
+    · simp [*, ihy ‹_›]
+    · simp only [*, PlausibleIterStep.yield, pure_bind]
+      apply bind_congr; intro px
+      split <;> simp [ihy ‹_›]
+  · simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
+  · simp
+
+theorem IterM.allM_map {α β β' : Type w} {m : Type w → Type w'}
+    [Iterator α m β] [Finite α m] [Monad m] [IteratorLoop α m m]
+    [LawfulMonad m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {f : β → β'} {p : β' → m (ULift Bool)} :
+    (it.map f).allM p = it.allM (fun x => p (f x)) := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [allM_eq_match_step, allM_eq_match_step, step_map, bind_assoc]
+  apply bind_congr; intro step
+  split
+  · simp only [pure_bind]
+    apply bind_congr; intro fx
+    simp [ihy ‹_›]
+  · simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
+  · simp
+
+theorem IterM.allM_filter {α β : Type w} {m : Type w → Type w'}
+    [Iterator α m β] [Finite α m] [Monad m][IteratorLoop α m m]
+    [LawfulMonad m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {f : β → Bool} {p : β → m (ULift Bool)} :
+    (it.filter f).allM p = it.allM (fun x => do
+        if f x then
+          p x
+        else
+          return .up true) := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [allM_eq_match_step, allM_eq_match_step, step_filter, bind_assoc]
+  apply bind_congr; intro step
+  split
+  · simp only
+    split <;> simp [ihy ‹_›]
+  · simp only [PlausibleIterStep.skip, pure_bind]
+    simp [ihs ‹_›]
+  · simp
+
+theorem IterM.all_filterMapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
+    [Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n] [IteratorLoop α m m]
+    [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {f : β → n (Option β')} {p : β' → Bool} :
+    (it.filterMapM f).all p = (it.mapM (pure (f := n))).allM (fun x => do
+      match ← f x with
+      | some fx => return .up (p fx)
+      | none => return .up true) := by
+  simp [all_eq_allM, allM_filterMapM]
+
+theorem IterM.all_mapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
+    [Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n] [IteratorLoop α m m]
+    [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {f : β → n β'} {p : β' → Bool} :
+    (it.mapM f).all p = (it.mapM (pure (f := n))).allM (fun x => (.up <| p ·) <$> (f x)) := by
+  simp [all_eq_allM, allM_mapM]
+
+theorem IterM.all_filterM {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
+    [Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n] [IteratorLoop α m m]
+    [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {f : β → n (ULift Bool)} {p : β → Bool} :
+    (it.filterM f).all p = (it.mapM (pure (f := n))).allM (fun x => do
+        if (← f x).down then
+          return .up (p x)
+        else
+          return .up true) := by
+  simp [all_eq_allM, allM_filterM]
+
+theorem IterM.all_filterMap {α β β' : Type w} {m : Type w → Type w'}
+    [Iterator α m β] [Finite α m] [Monad m] [IteratorLoop α m m]
+    [LawfulMonad m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {f : β → Option β'} {p : β' → Bool} :
+    (it.filterMap f).all p = it.all (fun x =>
+      match f x with
+      | some fx => (p fx)
+      | none => true) := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [all_eq_match_step, all_eq_match_step, step_filterMap, bind_assoc]
+  apply bind_congr; intro step
+  split
+  · split
+    · simp [*, ihy ‹_›]
+    · simp only [*, PlausibleIterStep.yield, pure_bind]
+      split <;> simp [ihy ‹_›]
+  · simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
+  · simp
+
+theorem IterM.all_map {α β β' : Type w} {m : Type w → Type w'}
+    [Iterator α m β] [Finite α m] [Monad m] [IteratorLoop α m m]
+    [LawfulMonad m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {f : β → β'} {p : β' → Bool} :
+    (it.map f).all p = it.all (fun x => p (f x)) := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [all_eq_match_step, all_eq_match_step, step_map, bind_assoc]
+  apply bind_congr; intro step
+  split
+  · simp only [pure_bind]
+    simp [ihy ‹_›]
+  · simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
+  · simp
+
+end AnyAll
+
 end Std.Iterators
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
index 377292bb8f..73dfedac31 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
@@ -497,4 +497,236 @@ theorem Iter.length_toListRev_eq_size {α β : Type w} [Iterator α Id β] [Fini
     it.toListRev.length = it.size := by
   rw [toListRev_eq, List.length_reverse, length_toList_eq_size]
 
+theorem Iter.anyM_eq_forIn {α β : Type w} {m : Type → Type w'} [Iterator α Id β]
+    [Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    {it : Iter (α := α) β} {p : β → m Bool} :
+    it.anyM p = (ForIn.forIn it false (fun x _ => do
+        if ← p x then
+          return .done true
+        else
+          return .yield false)) := by
+  rfl
+
+theorem Iter.anyM_eq_match_step {α β : Type w} {m : Type → Type w'} [Iterator α Id β]
+    [Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    {it : Iter (α := α) β} {p : β → m Bool} :
+    it.anyM p = (do
+      match it.step.val with
+      | .yield it' x =>
+        if (← p x) then
+          return true
+        else
+          it'.anyM p
+      | .skip it' => it'.anyM p
+      | .done => return false) := by
+  rw [anyM_eq_forIn, forIn_eq_match_step]
+  simp only [bind_assoc]
+  cases it.step using PlausibleIterStep.casesOn
+  · apply bind_congr; intro px
+    split
+    · simp
+    · simp [anyM_eq_forIn]
+  · simp [anyM_eq_forIn]
+  · simp
+
+theorem Iter.anyM_toList {α β : Type w} {m : Type → Type w'} [Iterator α Id β]
+    [Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : Iter (α := α) β} {p : β → m Bool} :
+    it.toList.anyM p = it.anyM p := by
+  induction it using Iter.inductSteps with | step it ihy ihs =>
+  rw [it.toList_eq_match_step, anyM_eq_match_step]
+  cases it.step using PlausibleIterStep.casesOn
+  · simp only [List.anyM_cons, ihy ‹_›]
+  · simp only [ihs ‹_›]
+  · simp only [List.anyM_nil]
+
+theorem Iter.anyM_toArray {α β : Type w} {m : Type → Type w'} [Iterator α Id β]
+    [Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : Iter (α := α) β} {p : β → m Bool} :
+    it.toArray.anyM p = it.anyM p := by
+  simp only [← Iter.toArray_toList, List.anyM_toArray, anyM_toList]
+
+theorem Iter.any_eq_anyM {α β : Type w} [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {it : Iter (α := α) β} {p : β → Bool} :
+    it.any p = (it.anyM (fun x => pure (f := Id) (p x))).run := by
+  rfl
+
+theorem Iter.anyM_pure {α β : Type w} [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {it : Iter (α := α) β} {p : β → Bool} :
+    it.anyM (fun x => pure (f := Id) (p x)) = pure (it.any (fun x => p x)) := by
+  simp [any_eq_anyM]
+
+theorem Iter.any_eq_match_step {α β : Type w} [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {it : Iter (α := α) β} {p : β → Bool} :
+    it.any p = (match it.step.val with
+      | .yield it' x =>
+        if p x then
+          true
+        else
+          it'.any p
+      | .skip it' => it'.any p
+      | .done => false) := by
+  rw [any_eq_anyM, anyM_eq_match_step]
+  split
+  · simp only [pure_bind, Bool.if_true_left, Bool.decide_eq_true, any_eq_anyM]
+    split <;> simp [*]
+  · simp [any_eq_anyM]
+  · simp
+
+theorem Iter.any_eq_forIn {α β : Type w} [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {it : Iter (α := α) β} {p : β → Bool} :
+    it.any p = (ForIn.forIn (m := Id) it false (fun x _ => do
+        if p x then
+          return .done true
+        else
+          return .yield false)).run := by
+  simp [any_eq_anyM, anyM_eq_forIn]
+
+theorem Iter.any_toList {α β : Type w} [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : Iter (α := α) β} {p : β → Bool} :
+    it.toList.any p = it.any p := by
+  induction it using Iter.inductSteps with | step it ihy ihs =>
+  rw [it.toList_eq_match_step, any_eq_match_step]
+  cases it.step using PlausibleIterStep.casesOn
+  · simp only [List.any_cons, ihy ‹_›]
+    split <;> simp [*]
+  · simp only [ihs ‹_›]
+  · simp only [List.any_nil]
+
+theorem Iter.any_toArray {α β : Type w} [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : Iter (α := α) β} {p : β → Bool} :
+    it.toArray.any p = it.any p := by
+  simp only [← Iter.toArray_toList, List.any_toArray, any_toList]
+
+theorem Iter.allM_eq_forIn {α β : Type w} {m : Type → Type w'} [Iterator α Id β]
+    [Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    {it : Iter (α := α) β} {p : β → m Bool} :
+    it.allM p = (ForIn.forIn it true (fun x _ => do
+        if ← p x then
+          return .yield true
+        else
+          return .done false)) := by
+  rfl
+
+theorem Iter.allM_eq_match_step {α β : Type w} {m : Type → Type w'} [Iterator α Id β]
+    [Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    {it : Iter (α := α) β} {p : β → m Bool} :
+    it.allM p = (do
+      match it.step.val with
+      | .yield it' x =>
+        if (← p x) then
+          it'.allM p
+        else
+          return false
+      | .skip it' => it'.allM p
+      | .done => return true) := by
+  rw [allM_eq_forIn, forIn_eq_match_step]
+  simp only [bind_assoc]
+  cases it.step using PlausibleIterStep.casesOn
+  · apply bind_congr; intro px
+    split
+    · simp [allM_eq_forIn]
+    · simp
+  · simp [allM_eq_forIn]
+  · simp
+
+theorem Iter.all_eq_allM {α β : Type w} [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {it : Iter (α := α) β} {p : β → Bool} :
+    it.all p = (it.allM (fun x => pure (f := Id) (p x))).run := by
+  rfl
+
+theorem Iter.allM_pure {α β : Type w} [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {it : Iter (α := α) β} {p : β → Bool} :
+    it.allM (fun x => pure (f := Id) (p x)) = pure (it.all (fun x => p x)) := by
+  simp [all_eq_allM]
+
+theorem Iter.all_eq_match_step {α β : Type w} [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {it : Iter (α := α) β} {p : β → Bool} :
+    it.all p = (match it.step.val with
+      | .yield it' x =>
+        if p x then
+          it'.all p
+        else
+          false
+      | .skip it' => it'.all p
+      | .done => true) := by
+  rw [all_eq_allM, allM_eq_match_step]
+  split
+  · simp only [pure_bind, all_eq_allM, Bool.if_false_right, Bool.decide_eq_true]
+    split <;> simp [*]
+  · simp [all_eq_allM]
+  · simp
+
+theorem Iter.all_eq_forIn {α β : Type w} [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {it : Iter (α := α) β} {p : β → Bool} :
+    it.all p = (ForIn.forIn (m := Id) it true (fun x _ => do
+        if p x then
+          return .yield true
+        else
+          return .done false)).run := by
+  simp [all_eq_allM, allM_eq_forIn]
+
+theorem Iter.all_toList {α β : Type w} [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : Iter (α := α) β} {p : β → Bool} :
+    it.toList.all p = it.all p := by
+  induction it using Iter.inductSteps with | step it ihy ihs =>
+  rw [it.toList_eq_match_step, all_eq_match_step]
+  cases it.step using PlausibleIterStep.casesOn
+  · simp only [List.all_cons, ihy ‹_›]
+    split <;> simp [*]
+  · simp only [ihs ‹_›]
+  · simp only [List.all_nil]
+
+theorem Iter.all_toArray {α β : Type w} [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : Iter (α := α) β} {p : β → Bool} :
+    it.toArray.all p = it.all p := by
+  simp only [← Iter.toArray_toList, List.all_toArray, all_toList]
+
+theorem Iter.allM_eq_not_anyM_not {α β : Type w} {m : Type → Type w'} [Iterator α Id β]
+    [Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    {it : Iter (α := α) β} {p : β → m Bool} :
+    it.allM p = (! ·) <$> it.anyM ((! ·) <$> p ·) := by
+  induction it using Iter.inductSteps with | step it ihy ihs =>
+  rw [allM_eq_match_step, anyM_eq_match_step, map_eq_pure_bind]
+  cases it.step using PlausibleIterStep.casesOn
+  · simp only [map_eq_pure_bind, bind_assoc, pure_bind]
+    apply bind_congr; intro px
+    split
+    · simp [*, ihy ‹_›]
+    · simp [*]
+  · simp [ihs ‹_›]
+  · simp
+
+theorem Iter.all_eq_not_any_not {α β : Type w} [Iterator α Id β]
+    [Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {it : Iter (α := α) β} {p : β → Bool} :
+    it.all p = ! it.any (! p ·) := by
+  induction it using Iter.inductSteps with | step it ihy ihs =>
+  rw [all_eq_match_step, any_eq_match_step]
+  cases it.step using PlausibleIterStep.casesOn
+  · simp only
+    split
+    · simp [*, ihy ‹_›]
+    · simp [*]
+  · simp [ihs ‹_›]
+  · simp
+
 end Std.Iterators
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
index b20c93a749..c0a731000e 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
@@ -334,4 +334,183 @@ theorem IterM.drain_eq_map_toArray {α β : Type w} {m : Type w → Type w'} [It
     it.drain = (fun _ => .unit) <$> it.toList := by
   simp [IterM.drain_eq_map_toList]
 
+theorem IterM.anyM_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {p : β → m (ULift Bool)} :
+    it.anyM p = (ForIn.forIn it (.up false) (fun x _ => do
+        if (← p x).down then
+          return .done (.up true)
+        else
+          return .yield (.up false))) := by
+  rfl
+
+theorem IterM.anyM_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {p : β → m (ULift Bool)} :
+    it.anyM p = (do
+      match (← it.step).val with
+      | .yield it' x =>
+        if (← p x).down then
+          return .up true
+        else
+          it'.anyM p
+      | .skip it' => it'.anyM p
+      | .done => return .up false) := by
+  rw [anyM_eq_forIn, forIn_eq_match_step]
+  simp only [monadLift_self, bind_assoc]
+  apply bind_congr; intro step
+  split
+  · apply bind_congr; intro px
+    split
+    · simp
+    · simp [anyM_eq_forIn]
+  · simp [anyM_eq_forIn]
+  · simp
+
+theorem IterM.any_eq_anyM {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {p : β → Bool} :
+    it.any p = it.anyM (fun x => pure (.up (p x))) := by
+  rfl
+
+theorem IterM.anyM_pure {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {p : β → ULift Bool} :
+    it.anyM (fun x => pure (p x)) = it.any (fun x => (p x).down) := by
+  simp [any_eq_anyM]
+
+theorem IterM.any_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {p : β → Bool} :
+    it.any p = (do
+      match (← it.step).val with
+      | .yield it' x =>
+        if p x then
+          return .up true
+        else
+          it'.any p
+      | .skip it' => it'.any p
+      | .done => return .up false) := by
+  rw [any_eq_anyM, anyM_eq_match_step]
+  apply bind_congr; intro step
+  split
+  · simp [any_eq_anyM]
+  · simp [any_eq_anyM]
+  · simp
+
+theorem IterM.any_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {p : β → Bool} :
+    it.any p = (ForIn.forIn it (.up false) (fun x _ => do
+        if p x then
+          return .done (.up true)
+        else
+          return .yield (.up false))) := by
+  simp [any_eq_anyM, anyM_eq_forIn]
+
+theorem IterM.allM_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {p : β → m (ULift Bool)} :
+    it.allM p = (ForIn.forIn it (.up true) (fun x _ => do
+        if (← p x).down then
+          return .yield (.up true)
+        else
+          return .done (.up false))) := by
+  rfl
+
+theorem IterM.allM_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {p : β → m (ULift Bool)} :
+    it.allM p = (do
+      match (← it.step).val with
+      | .yield it' x =>
+        if (← p x).down then
+          it'.allM p
+        else
+          return .up false
+      | .skip it' => it'.allM p
+      | .done => return .up true) := by
+  rw [allM_eq_forIn, forIn_eq_match_step]
+  simp only [monadLift_self, bind_assoc]
+  apply bind_congr; intro step
+  split
+  · apply bind_congr; intro px
+    split
+    · simp [allM_eq_forIn]
+    · simp
+  · simp [allM_eq_forIn]
+  · simp
+
+theorem IterM.all_eq_allM {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {p : β → Bool} :
+    it.all p = it.allM (fun x => pure (.up (p x))) := by
+  rfl
+
+theorem IterM.allM_pure {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {p : β → ULift Bool} :
+    it.allM (fun x => pure (p x)) = it.all (fun x => (p x).down) := by
+  simp [all_eq_allM]
+
+theorem IterM.all_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {p : β → Bool} :
+    it.all p = (do
+      match (← it.step).val with
+      | .yield it' x =>
+        if p x then
+          it'.all p
+        else
+          return .up false
+      | .skip it' => it'.all p
+      | .done => return .up true) := by
+  rw [all_eq_allM, allM_eq_match_step]
+  apply bind_congr; intro step
+  split
+  · simp [all_eq_allM]
+  · simp [all_eq_allM]
+  · simp
+
+theorem IterM.all_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {p : β → Bool} :
+    it.all p = (ForIn.forIn it (.up true) (fun x _ => do
+        if p x then
+          return .yield (.up true)
+        else
+          return .done (.up false))) := by
+  simp [all_eq_allM, allM_eq_forIn]
+
+theorem IterM.allM_eq_not_anyM_not {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {p : β → m (ULift Bool)} :
+    it.allM p = (fun x => .up !x.down) <$> it.anyM ((fun x => .up !x.down) <$> p ·) := by
+  induction it using IterM.inductSteps with | step it ihy ihs =>
+  rw [allM_eq_match_step, anyM_eq_match_step, map_eq_pure_bind, bind_assoc]
+  apply bind_congr; intro step
+  cases step using PlausibleIterStep.casesOn
+  · simp only [map_eq_pure_bind, bind_assoc, pure_bind]
+    apply bind_congr; intro px
+    split
+    · simp [*, ihy ‹_›]
+    · simp [*]
+  · simp [ihs ‹_›]
+  · simp
+
+theorem IterM.all_eq_not_any_not {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {p : β → Bool} :
+    it.all p = (fun x => .up !x.down) <$> it.any (! p ·) := by
+  induction it using IterM.inductSteps with | step it ihy ihs =>
+  rw [all_eq_match_step, any_eq_match_step, map_eq_pure_bind, bind_assoc]
+  apply bind_congr; intro step
+  cases step using PlausibleIterStep.casesOn
+  · simp only
+    split
+    · simp [*, ihy ‹_›]
+    · simp [*]
+  · simp [ihs ‹_›]
+  · simp
+
 end Std.Iterators
diff --git a/src/Init/Data/List/Monadic.lean b/src/Init/Data/List/Monadic.lean
index 60659157ac..09e92b73d9 100644
--- a/src/Init/Data/List/Monadic.lean
+++ b/src/Init/Data/List/Monadic.lean
@@ -481,10 +481,38 @@ theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] {p : α → m Bool} {as :
     simp only [anyM, ih, pure_bind]
     split <;> simp_all
 
+@[simp] theorem anyM_nil [Monad m] {p : α → m Bool} :
+    ([] : List α).anyM p = pure false :=
+  (rfl)
+
+@[simp] theorem anyM_cons [Monad m] {p : α → m Bool} {x : α} {xs : List α} :
+    (x :: xs).anyM p = (do
+      if (← p x) then
+        return true
+      else
+        xs.anyM p) := by
+  rw [anyM]
+  apply bind_congr; intro px
+  split <;> simp
+
 @[simp] theorem allM_pure [Monad m] [LawfulMonad m] {p : α → Bool} {as : List α} :
     as.allM (m := m) (pure <| p ·) = pure (as.all p) := by
   simp [allM_eq_not_anyM_not, all_eq_not_any_not]
 
+@[simp] theorem allM_nil [Monad m] {p : α → m Bool} :
+    ([] : List α).allM p = pure true :=
+  (rfl)
+
+@[simp] theorem allM_cons [Monad m] {p : α → m Bool} {x : α} {xs : List α} :
+    (x :: xs).allM p = (do
+      if (← p x) then
+        xs.allM p
+      else
+        return false) := by
+  rw [allM]
+  apply bind_congr; intro px
+  split <;> simp
+
 /-! ### Recognizing higher order functions using a function that only depends on the value. -/
 
 /--