feat: introduce iterator combinators takeWhile and dropWhile (#8493)

This PR provides the iterator combinators `takeWhile` (forwarding all
emitted values of another iterator until a predicate becomes false)
`dropWhile` (dropping values until some predicate on these values
becomes false, then forwarding all the others).

src/Std/Data/Iterators/Combinators.lean

@@ -6,5 +6,7 @@ Authors: Paul Reichert
 prelude
 import Std.Data.Iterators.Combinators.Monadic
 import Std.Data.Iterators.Combinators.Take
+import Std.Data.Iterators.Combinators.TakeWhile
+import Std.Data.Iterators.Combinators.DropWhile
 import Std.Data.Iterators.Combinators.FilterMap
 import Std.Data.Iterators.Combinators.Zip

src/Std/Data/Iterators/Combinators/DropWhile.lean

@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Std.Data.Iterators.Combinators.Monadic.DropWhile
+
+namespace Std.Iterators
+
+/--
+Constructs intermediate states of an iterator created with the combinator `Iter.dropWhile`.
+When `it.dropWhile P` has stopped dropping elements, its new state cannot be created
+directly with `Iter.dropWhile` but only with `Intermediate.dropWhile`.
+
+`Intermediate.dropWhile` is meant to be used only for internally or for verification purposes.
+-/
+@[always_inline, inline]
+def Iter.Intermediate.dropWhile (P : β → Bool) (dropping : Bool)
+    (it : Iter (α := α) β) :=
+  ((IterM.Intermediate.dropWhile P dropping it.toIterM).toIter : Iter β)
+
+/--
+Given an iterator `it` and a predicate `P`, `it.dropWhile P` is an iterator that
+emits the values emitted by `it` starting from the first value that is rejected by `P`.
+The elements before are dropped.
+
+In situations where `P` is monadic, use `dropWhileM` instead.
+
+**Marble diagram:**
+
+Assuming that the predicate `P` accepts `a` and `b` but rejects `c`:
+
+```text
+it               ---a----b---c--d-e--⊥
+it.dropWhile P   ------------c--d-e--⊥
+
+it               ---a----⊥
+it.dropWhile P   --------⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: only if `it` is finite
+* `Productive` instance: only if `it` is finite
+
+Depending on `P`, it is possible that `it.dropWhileM P` is productive although
+`it` is not. In this case, the `Productive` instance needs to be proved manually.
+
+**Performance:**
+
+This combinator calls `P` on each output of `it` until the predicate evaluates to false. After
+that, the combinator incurs an addictional O(1) cost for each value emitted by `it`.
+-/
+@[always_inline, inline]
+def Iter.dropWhile {α : Type w} {β : Type w} (P : β → Bool) (it : Iter (α := α) β) :=
+  (it.toIterM.dropWhile P |>.toIter : Iter β)
+
+end Std.Iterators

src/Std/Data/Iterators/Combinators/FilterMap.lean

@@ -47,7 +47,7 @@ of `f`.
 **Marble diagram (without monadic effects):**
 
 ```text
-it                        ---a --b--c --d-e--⊥
+it                                ---a --b--c --d-e--⊥
 it.filterMapWithPostcondition     ---a'-----c'-------⊥
 ```
 
@@ -96,7 +96,7 @@ of `f`.
 **Marble diagram (without monadic effects):**
 
 ```text
-it                     ---a--b--c--d-e--⊥
+it                             ---a--b--c--d-e--⊥
 it.filterWithPostcondition     ---a-----c-------⊥
 ```
 
@@ -141,7 +141,7 @@ of `f`.
 **Marble diagram (without monadic effects):**
 
 ```text
-it                  ---a --b --c --d -e ----⊥
+it                          ---a --b --c --d -e ----⊥
 it.mapWithPostcondition     ---a'--b'--c'--d'-e'----⊥
 ```
 

src/Std/Data/Iterators/Combinators/Monadic.lean

@@ -5,5 +5,7 @@ Authors: Paul Reichert
 -/
 prelude
 import Std.Data.Iterators.Combinators.Monadic.Take
+import Std.Data.Iterators.Combinators.Monadic.TakeWhile
+import Std.Data.Iterators.Combinators.Monadic.DropWhile
 import Std.Data.Iterators.Combinators.Monadic.FilterMap
 import Std.Data.Iterators.Combinators.Monadic.Zip

src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean

@@ -0,0 +1,289 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Init.Data.Nat.Lemmas
+import Init.RCases
+import Std.Data.Iterators.Basic
+import Std.Data.Iterators.Consumers.Monadic.Collect
+import Std.Data.Iterators.Consumers.Monadic.Loop
+import Std.Data.Iterators.Internal.Termination
+import Std.Data.Iterators.PostConditionMonad
+
+/-!
+# Monadic `dropWhile` iterator combinator
+
+This module provides the iterator combinator `IterM.dropWhile` that will drop all values emitted
+by a given iterator until a given predicate on these values becomes false the first fime. Beginning
+with that moment, the combinator will forward all emitted values.
+
+Several variants of this combinator are provided:
+
+* `M` suffix: Instead of a pure function, this variant takes a monadic function. Given a suitable
+  `MonadLiftT` instance, it will also allow lifting the iterator to another monad first and then
+  applying the mapping function in this monad.
+* `WithPostcondition` suffix: This variant takes a monadic function where the return type in the
+  monad is a subtype. This variant is in rare cases necessary for the intrinsic verification of an
+  iterator, and particularly for specialized termination proofs. If possible, avoid this.
+-/
+
+namespace Std.Iterators
+
+variable {α : Type w} {m : Type w → Type w'} {β : Type w}
+
+/--
+Internal state of the `dropWhile` combinator. Do not depend on its internals.
+-/
+@[unbox]
+structure DropWhile (α : Type w) (m : Type w → Type w') (β : Type w)
+    (P : β → PostconditionT m (ULift Bool)) where
+  /-- Internal implementation detail of the iterator library. -/
+  dropping : Bool
+  /-- Internal implementation detail of the iterator library. -/
+  inner : IterM (α := α) m β
+
+/--
+Constructs intermediate states of an iterator created with the combinator
+`IterM.dropWhileWithPostcondition`.
+When `it.dropWhileWithPostcondition P` has stopped dropping elements, its new state cannot be
+created directly with `IterM.dropWhileWithPostcondition` but only with
+`Intermediate.dropWhileWithPostcondition`.
+
+`Intermediate.dropWhileWithPostcondition` is meant to be used only for internally or for
+verification purposes.
+-/
+@[always_inline, inline]
+def IterM.Intermediate.dropWhileWithPostcondition (P : β → PostconditionT m (ULift Bool))
+    (dropping : Bool) (it : IterM (α := α) m β) :=
+  (toIterM (DropWhile.mk (P := P) dropping it) m β : IterM m β)
+
+/--
+Constructs intermediate states of an iterator created with the combinator `IterM.dropWhileM`.
+When `it.dropWhileM P` has stopped dropping elements, its new state cannot be created
+directly with `IterM.dropWhileM` but only with `Intermediate.dropWhileM`.
+
+`Intermediate.dropWhileM` is meant to be used only for internally or for verification purposes.
+-/
+@[always_inline, inline]
+def IterM.Intermediate.dropWhileM [Monad m] (P : β → m (ULift Bool)) (dropping : Bool)
+    (it : IterM (α := α) m β) :=
+  (IterM.Intermediate.dropWhileWithPostcondition (PostconditionT.lift ∘ P) dropping it : IterM m β)
+
+/--
+Constructs intermediate states of an iterator created with the combinator `IterM.dropWhile`.
+When `it.dropWhile P` has stopped dropping elements, its new state cannot be created
+directly with `IterM.dropWhile` but only with `Intermediate.dropWhile`.
+
+`Intermediate.dropWhile` is meant to be used only for internally or for verification purposes.
+-/
+@[always_inline, inline]
+def IterM.Intermediate.dropWhile [Monad m] (P : β → Bool) (dropping : Bool)
+    (it : IterM (α := α) m β) :=
+  (IterM.Intermediate.dropWhileM (pure ∘ ULift.up ∘ P) dropping it : IterM m β)
+
+/--
+*Note: This is a very general combinator that requires an advanced understanding of monads,
+dependent types and termination proofs. The variants `dropWhile` and `dropWhileM` are easier to use
+and sufficient for most use cases.*
+
+Given an iterator `it` and a monadic predicate `P`, `it.dropWhileWithPostcondition P` is an iterator
+that emits the values emitted by `it` starting from the first value that is rejected by `P`.
+The elements before are dropped.
+
+`P` is expected to return `PostconditionT m (ULift Bool)`. The `PostconditionT` transformer allows
+the caller to intrinsically prove properties about `P`'s return value in the monad `m`, enabling
+termination proofs depending on the specific behavior of `P`.
+
+**Marble diagram (ignoring monadic effects):**
+
+Assuming that the predicate `P` accepts `a` and `b` but rejects `c`:
+
+```text
+it                                ---a----b---c--d-e--⊥
+it.dropWhileWithPostcondition P   ------------c--d-e--⊥
+
+it                                ---a----⊥
+it.dropWhileWithPostcondition P   --------⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: only if `it` is finite
+* `Productive` instance: only if `it` is finite
+
+Depending on `P`, it is possible that `it.dropWhileWithPostcondition P` is finite (or productive) although
+`it` is not. In this case, the `Finite` (or `Productive`) instance needs to be proved manually.
+
+**Performance:**
+
+This combinator calls `P` on each output of `it` until the predicate evaluates to false. After
+that, the combinator incurs an addictional O(1) cost for each value emitted by `it`.
+-/
+@[always_inline, inline]
+def IterM.dropWhileWithPostcondition (P : β → PostconditionT m (ULift Bool)) (it : IterM (α := α) m β) :=
+  (Intermediate.dropWhileWithPostcondition P true it : IterM m β)
+
+/--
+Given an iterator `it` and a monadic predicate `P`, `it.dropWhileM P` is an iterator that
+emits the values emitted by `it` starting from the first value that is rejected by `P`.
+The elements before are dropped.
+
+If `P` is pure, then the simpler variant `dropWhile` can be used instead.
+
+**Marble diagram (ignoring monadic effects):**
+
+Assuming that the predicate `P` accepts `a` and `b` but rejects `c`:
+
+```text
+it                ---a----b---c--d-e--⊥
+it.dropWhileM P   ------------c--d-e--⊥
+
+it                ---a----⊥
+it.dropWhileM P   --------⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: only if `it` is finite
+* `Productive` instance: only if `it` is finite
+
+Depending on `P`, it is possible that `it.dropWhileM P` is finite (or productive) although
+`it` is not. In this case, the `Finite` (or `Productive`) instance needs to be proved manually.
+Use `dropWhileWithPostcondition` if the termination behavior depends on `P`'s behavior.
+
+**Performance:**
+
+This combinator calls `P` on each output of `it` until the predicate evaluates to false. After
+that, the combinator incurs an addictional O(1) cost for each value emitted by `it`.
+-/
+@[always_inline, inline]
+def IterM.dropWhileM [Monad m] (P : β → m (ULift Bool)) (it : IterM (α := α) m β) :=
+  (Intermediate.dropWhileM P true it : IterM m β)
+
+/--
+Given an iterator `it` and a predicate `P`, `it.dropWhile P` is an iterator that
+emits the values emitted by `it` starting from the first value that is rejected by `P`.
+The elements before are dropped.
+
+In situations where `P` is monadic, use `dropWhileM` instead.
+
+**Marble diagram (ignoring monadic effects):**
+
+Assuming that the predicate `P` accepts `a` and `b` but rejects `c`:
+
+```text
+it               ---a----b---c--d-e--⊥
+it.dropWhile P   ------------c--d-e--⊥
+
+it               ---a----⊥
+it.dropWhile P   --------⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: only if `it` is finite
+* `Productive` instance: only if `it` is finite
+
+Depending on `P`, it is possible that `it.dropWhileM P` is productive although
+`it` is not. In this case, the `Productive` instance needs to be proved manually.
+
+**Performance:**
+
+This combinator calls `P` on each output of `it` until the predicate evaluates to false. After
+that, the combinator incurs an addictional O(1) cost for each value emitted by `it`.
+-/
+@[always_inline, inline]
+def IterM.dropWhile [Monad m] (P : β → Bool) (it : IterM (α := α) m β) :=
+  (Intermediate.dropWhile P true it: IterM m β)
+
+/--
+`it.PlausibleStep step` is the proposition that `step` is a possible next step from the
+`dropWhile` iterator `it`. This is mostly internally relevant, except if one needs to manually
+prove termination (`Finite` or `Productive` instances, for example) of a `dropWhile` iterator.
+-/
+inductive DropWhile.PlausibleStep [Iterator α m β] {P} (it : IterM (α := DropWhile α m β P) m β) :
+    (step : IterStep (IterM (α := DropWhile α m β P) m β) β) → Prop where
+  | yield : ∀ {it' out}, it.internalState.inner.IsPlausibleStep (.yield it' out) →
+      it.internalState.dropping = false →
+      PlausibleStep it (.yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out)
+  | skip : ∀ {it'}, it.internalState.inner.IsPlausibleStep (.skip it') →
+      PlausibleStep it (.skip (IterM.Intermediate.dropWhileWithPostcondition P it.internalState.dropping it'))
+  | done : it.internalState.inner.IsPlausibleStep .done → PlausibleStep it .done
+  | start : ∀ {it' out}, it.internalState.inner.IsPlausibleStep (.yield it' out) →
+      it.internalState.dropping = true → (P out).Property (.up false) →
+      PlausibleStep it (.yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out)
+  | dropped : ∀ {it' out}, it.internalState.inner.IsPlausibleStep (.yield it' out) →
+      it.internalState.dropping = true → (P out).Property (.up true) →
+      PlausibleStep it (.skip (IterM.Intermediate.dropWhileWithPostcondition P true it'))
+
+@[always_inline, inline]
+instance DropWhile.instIterator [Monad m] [Iterator α m β] {P} :
+    Iterator (DropWhile α m β P) m β where
+  IsPlausibleStep := DropWhile.PlausibleStep
+  step it := do
+    match ← it.internalState.inner.step with
+    | .yield it' out h =>
+      if h' : it.internalState.dropping = true then
+        match ← (P out).operation with
+        | ⟨.up true, h''⟩ =>
+          return .skip (IterM.Intermediate.dropWhileWithPostcondition P true it') (.dropped h h' h'')
+        | ⟨.up false, h''⟩ =>
+          return .yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out (.start h h' h'')
+      else
+        return .yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out
+            (.yield h (Bool.not_eq_true _ ▸ h'))
+    | .skip it' h =>
+      return .skip (IterM.Intermediate.dropWhileWithPostcondition P it.internalState.dropping it') (.skip h)
+    | .done h =>
+      return .done (.done h)
+
+private def DropWhile.instFinitenessRelation [Monad m] [Iterator α m β]
+    [Finite α m] {P} :
+    FinitenessRelation (DropWhile α m β P) m where
+  rel := InvImage WellFoundedRelation.rel
+      (IterM.finitelyManySteps ∘ DropWhile.inner ∘ IterM.internalState)
+  wf := by
+    apply InvImage.wf
+    exact WellFoundedRelation.wf
+  subrelation {it it'} h := by
+    obtain ⟨step, h, h'⟩ := h
+    cases h'
+    case yield it' out k h' h'' =>
+      cases h
+      exact IterM.TerminationMeasures.Finite.rel_of_yield h'
+    case skip it' out h' =>
+      cases h
+      exact IterM.TerminationMeasures.Finite.rel_of_skip h'
+    case done _ =>
+      cases h
+    case start it' out h' h'' h''' =>
+      cases h
+      exact IterM.TerminationMeasures.Finite.rel_of_yield h'
+    case dropped it' out h' h'' h''' =>
+      cases h
+      exact IterM.TerminationMeasures.Finite.rel_of_yield h'
+
+instance DropWhile.instFinite [Monad m] [Iterator α m β] [Finite α m] {P} :
+    Finite (DropWhile α m β P) m :=
+  Finite.of_finitenessRelation instFinitenessRelation
+
+instance DropWhile.instIteratorCollect [Monad m] [Monad n] [Iterator α m β] [Productive α m] {P} :
+    IteratorCollect (DropWhile α m β P) m n :=
+  .defaultImplementation
+
+instance DropWhile.instIteratorCollectPartial [Monad m] [Monad n] [Iterator α m β] {P} :
+    IteratorCollectPartial (DropWhile α m β P) m n :=
+  .defaultImplementation
+
+instance DropWhile.instIteratorLoop [Monad m] [Monad n] [Iterator α m β] :
+    IteratorLoop α m n :=
+  .defaultImplementation
+
+instance DropWhile.instIteratorForPartial [Monad m] [Monad n] [Iterator α m β]
+    [IteratorLoopPartial α m n] [MonadLiftT m n] {P} :
+    IteratorLoopPartial (DropWhile α m β P) m n :=
+  .defaultImplementation
+
+end Std.Iterators

src/Std/Data/Iterators/Combinators/Monadic/FilterMap.lean

@@ -39,6 +39,7 @@ Internal state of the `filterMap` combinator. Do not depend on its internals.
 structure FilterMap (α : Type w) {β γ : Type w}
     (m : Type w → Type w') (n : Type w → Type w'') (lift : ⦃α : Type w⦄ → m α → n α)
     (f : β → PostconditionT n (Option γ)) where
+  /-- Internal implementation detail of the iterator library. -/
   inner : IterM (α := α) m β
 
 /--
@@ -81,7 +82,7 @@ of `f`.
 **Marble diagram (without monadic effects):**
 
 ```text
-it                        ---a --b--c --d-e--⊥
+it                                ---a --b--c --d-e--⊥
 it.filterMapWithPostcondition     ---a'-----c'-------⊥
 ```
 
@@ -294,7 +295,7 @@ of `f`.
 **Marble diagram (without monadic effects):**
 
 ```text
-it                  ---a --b --c --d -e ----⊥
+it                          ---a --b --c --d -e ----⊥
 it.mapWithPostcondition     ---a'--b'--c'--d'-e'----⊥
 ```
 
@@ -340,7 +341,7 @@ of `f`.
 **Marble diagram (without monadic effects):**
 
 ```text
-it                     ---a--b--c--d-e--⊥
+it                             ---a--b--c--d-e--⊥
 it.filterWithPostcondition     ---a-----c-------⊥
 ```
 

src/Std/Data/Iterators/Combinators/Monadic/Take.lean

@@ -52,7 +52,7 @@ it.take 3   ---a--⊥
 
 This combinator incurs an additional O(1) cost with each output of `it`.
 -/
-@[inline]
+@[always_inline, inline]
 def IterM.take (n : Nat) (it : IterM (α := α) m β) :=
   toIterM (Take.mk n it) m β
 

src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean

@@ -0,0 +1,289 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Init.Data.Nat.Lemmas
+import Init.RCases
+import Std.Data.Iterators.Basic
+import Std.Data.Iterators.Consumers.Monadic.Collect
+import Std.Data.Iterators.Consumers.Monadic.Loop
+import Std.Data.Iterators.Internal.Termination
+import Std.Data.Iterators.PostConditionMonad
+
+/-!
+# Monadic `takeWhile` iterator combinator
+
+This module provides the iterator combinator `IterM.takeWhile` that will take all values emitted
+by a given iterator until a given predicate on these values becomes false the first fime. Then
+the combinator will terminate.
+
+Several variants of this combinator are provided:
+
+* `M` suffix: Instead of a pure function, this variant takes a monadic function. Given a suitable
+  `MonadLiftT` instance, it will also allow lifting the iterator to another monad first and then
+  applying the mapping function in this monad.
+* `WithPostcondition` suffix: This variant takes a monadic function where the return type in the
+  monad is a subtype. This variant is in rare cases necessary for the intrinsic verification of an
+  iterator, and particularly for specialized termination proofs. If possible, avoid this.
+-/
+
+namespace Std.Iterators
+
+variable {α : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {β : Type w}
+
+/--
+Internal state of the `takeWhile` combinator. Do not depend on its internals.
+-/
+@[unbox]
+structure TakeWhile (α : Type w) (m : Type w → Type w') (β : Type w)
+    (P : β → PostconditionT m (ULift Bool)) where
+  /-- Internal implementation detail of the iterator library. -/
+  inner : IterM (α := α) m β
+
+/--
+*Note: This is a very general combinator that requires an advanced understanding of monads,
+dependent types and termination proofs. The variants `takeWhile` and `takeWhileM` are easier to use
+and sufficient for most use cases.*
+
+Given an iterator `it` and a monadic predicate `P`, `it.takeWhileWithPostcondition P` is an iterator
+that emits the values emitted by `it` until one of those values is rejected by `P`.
+If some emitted value is rejected by `P`, the value is dropped and the iterator terminates.
+
+`P` is expected to return `PostconditionT m (ULift Bool)`. The `PostconditionT` transformer allows
+the caller to intrinsically prove properties about `P`'s return value in the monad `m`, enabling
+termination proofs depending on the specific behavior of `P`.
+
+**Marble diagram (ignoring monadic effects):**
+
+Assuming that the predicate `P` accepts `a` and `b` but rejects `c`:
+
+```text
+it                                ---a----b---c--d-e--⊥
+it.takeWhileWithPostcondition P   ---a----b---⊥
+
+it                                ---a----⊥
+it.takeWhileWithPostcondition P   ---a----⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: only if `it` is finite
+* `Productive` instance: only if `it` is productive
+
+Depending on `P`, it is possible that `it.takeWhileWithPostcondition P` is finite (or productive)
+although `it` is not. In this case, the `Finite` (or `Productive`) instance needs to be proved
+manually.
+
+**Performance:**
+
+This combinator calls `P` on each output of `it` until the predicate evaluates to false. Then
+it terminates.
+-/
+@[always_inline, inline]
+def IterM.takeWhileWithPostcondition (P : β → PostconditionT m (ULift Bool)) (it : IterM (α := α) m β) :=
+  (toIterM (TakeWhile.mk (P := P) it) m β : IterM m β)
+
+/--
+Given an iterator `it` and a monadic predicate `P`, `it.takeWhileM P` is an iterator that outputs
+the values emitted by `it` until one of those values is rejected by `P`.
+If some emitted value is rejected by `P`, the value is dropped and the iterator terminates.
+
+If `P` is pure, then the simpler variant `takeWhile` can be used instead.
+
+**Marble diagram (ignoring monadic effects):**
+
+Assuming that the predicate `P` accepts `a` and `b` but rejects `c`:
+
+```text
+it                ---a----b---c--d-e--⊥
+it.takeWhileM P   ---a----b---⊥
+
+it                ---a----⊥
+it.takeWhileM P   ---a----⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: only if `it` is finite
+* `Productive` instance: only if `it` is productive
+
+Depending on `P`, it is possible that `it.takeWhileM P` is finite (or productive) although `it` is not.
+In this case, the `Finite` (or `Productive`) instance needs to be proved manually.
+
+**Performance:**
+
+This combinator calls `P` on each output of `it` until the predicate evaluates to false. Then
+it terminates.
+-/
+@[always_inline, inline]
+def IterM.takeWhileM [Monad m] (P : β → m (ULift Bool)) (it : IterM (α := α) m β) :=
+  (it.takeWhileWithPostcondition (PostconditionT.lift ∘ P) : IterM m β)
+
+/--
+Given an iterator `it` and a predicate `P`, `it.takeWhile P` is an iterator that outputs
+the values emitted by `it` until one of those values is rejected by `P`.
+If some emitted value is rejected by `P`, the value is dropped and the iterator terminates.
+
+In situations where `P` is monadic, use `takeWhileM` instead.
+
+**Marble diagram (ignoring monadic effects):**
+
+Assuming that the predicate `P` accepts `a` and `b` but rejects `c`:
+
+```text
+it               ---a----b---c--d-e--⊥
+it.takeWhile P   ---a----b---⊥
+
+it               ---a----⊥
+it.takeWhile P   ---a----⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: only if `it` is finite
+* `Productive` instance: only if `it` is productive
+
+Depending on `P`, it is possible that `it.takeWhile P` is finite (or productive) although `it` is not.
+In this case, the `Finite` (or `Productive`) instance needs to be proved manually.
+
+**Performance:**
+
+This combinator calls `P` on each output of `it` until the predicate evaluates to false. Then
+it terminates.
+-/
+@[always_inline, inline]
+def IterM.takeWhile [Monad m] (P : β → Bool) (it : IterM (α := α) m β) :=
+  (it.takeWhileM (pure ∘ ULift.up ∘ P) : IterM m β)
+
+/--
+`it.PlausibleStep step` is the proposition that `step` is a possible next step from the
+`takeWhile` iterator `it`. This is mostly internally relevant, except if one needs to manually
+prove termination (`Finite` or `Productive` instances, for example) of a `takeWhile` iterator.
+-/
+inductive TakeWhile.PlausibleStep [Iterator α m β] {P} (it : IterM (α := TakeWhile α m β P) m β) :
+    (step : IterStep (IterM (α := TakeWhile α m β P) m β) β) → Prop where
+  | yield : ∀ {it' out}, it.internalState.inner.IsPlausibleStep (.yield it' out) →
+      (P out).Property (.up true) → PlausibleStep it (.yield (it'.takeWhileWithPostcondition P) out)
+  | skip : ∀ {it'}, it.internalState.inner.IsPlausibleStep (.skip it') →
+      PlausibleStep it (.skip (it'.takeWhileWithPostcondition P))
+  | done : it.internalState.inner.IsPlausibleStep .done → PlausibleStep it .done
+  | rejected : ∀ {it' out}, it.internalState.inner.IsPlausibleStep (.yield it' out) →
+      (P out).Property (.up false) → PlausibleStep it .done
+
+@[always_inline, inline]
+instance TakeWhile.instIterator [Monad m] [Iterator α m β] {P} :
+    Iterator (TakeWhile α m β P) m β where
+  IsPlausibleStep := TakeWhile.PlausibleStep
+  step it := do
+    match ← it.internalState.inner.step with
+    | .yield it' out h => match ← (P out).operation with
+      | ⟨.up true, h'⟩ => pure <| .yield (it'.takeWhileWithPostcondition P) out (.yield h h')
+      | ⟨.up false, h'⟩ => pure <| .done (.rejected h h')
+    | .skip it' h => pure <| .skip (it'.takeWhileWithPostcondition P) (.skip h)
+    | .done h => pure <| .done (.done h)
+
+private def TakeWhile.instFinitenessRelation [Monad m] [Iterator α m β]
+    [Finite α m] {P} :
+    FinitenessRelation (TakeWhile α m β P) m where
+  rel := InvImage WellFoundedRelation.rel (IterM.finitelyManySteps ∘ TakeWhile.inner ∘ IterM.internalState)
+  wf := by
+    apply InvImage.wf
+    exact WellFoundedRelation.wf
+  subrelation {it it'} h := by
+    obtain ⟨step, h, h'⟩ := h
+    cases h'
+    case yield it' out k h' h'' =>
+      cases h
+      exact IterM.TerminationMeasures.Finite.rel_of_yield h'
+    case skip it' out h' =>
+      cases h
+      exact IterM.TerminationMeasures.Finite.rel_of_skip h'
+    case done _ =>
+      cases h
+    case rejected _ =>
+      cases h
+
+instance TakeWhile.instFinite [Monad m] [Iterator α m β] [Finite α m] {P} :
+    Finite (TakeWhile α m β P) m :=
+  Finite.of_finitenessRelation instFinitenessRelation
+
+private def TakeWhile.instProductivenessRelation [Monad m] [Iterator α m β]
+    [Productive α m] {P} :
+    ProductivenessRelation (TakeWhile α m β P) m where
+  rel := InvImage WellFoundedRelation.rel (IterM.finitelyManySkips ∘ TakeWhile.inner ∘ IterM.internalState)
+  wf := by
+    apply InvImage.wf
+    exact WellFoundedRelation.wf
+  subrelation {it it'} h := by
+    cases h
+    exact IterM.TerminationMeasures.Productive.rel_of_skip ‹_›
+
+instance TakeWhile.instProductive [Monad m] [Iterator α m β] [Productive α m] {P} :
+    Productive (TakeWhile α m β P) m :=
+  Productive.of_productivenessRelation instProductivenessRelation
+
+instance TakeWhile.instIteratorCollect [Monad m] [Monad n] [Iterator α m β] [Productive α m] {P} :
+    IteratorCollect (TakeWhile α m β P) m n :=
+  .defaultImplementation
+
+instance TakeWhile.instIteratorCollectPartial [Monad m] [Monad n] [Iterator α m β] {P} :
+    IteratorCollectPartial (TakeWhile α m β P) m n :=
+  .defaultImplementation
+
+private def TakeWhile.PlausibleForInStep {β : Type u} {γ : Type v}
+    (P : β → PostconditionT m (ULift Bool))
+    (f : β → γ → ForInStep γ → Prop) :
+    β → γ → (ForInStep γ) → Prop
+  | out, c, ForInStep.yield c' => (P out).Property (.up true) ∧ f out c (.yield c')
+  | _, _, .done _ => True
+
+private def TakeWhile.wellFounded_plausibleForInStep {α β : Type w} {m : Type w → Type w'}
+    [Monad m] [Iterator α m β] {γ : Type x} {P}
+    {f : β → γ → ForInStep γ → Prop} (wf : IteratorLoop.WellFounded (TakeWhile α m β P) m f) :
+    IteratorLoop.WellFounded α m (PlausibleForInStep P f) := by
+      simp only [IteratorLoop.WellFounded] at ⊢ wf
+      letI : WellFoundedRelation _ := ⟨_, wf⟩
+      apply Subrelation.wf
+        (r := InvImage WellFoundedRelation.rel fun p => (p.1.takeWhileWithPostcondition P, p.2))
+        (fun {p q} h => by
+          simp only [InvImage, WellFoundedRelation.rel, this, IteratorLoop.rel,
+            IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+          obtain ⟨out, h, h'⟩ | ⟨h, h'⟩ := h
+          · apply Or.inl
+            exact ⟨out, .yield h h'.1, h'.2⟩
+          · apply Or.inr
+            refine ⟨?_, h'⟩
+            exact PlausibleStep.skip h)
+      apply InvImage.wf
+      exact WellFoundedRelation.wf
+
+instance TakeWhile.instIteratorLoop [Monad m] [Monad n] [Iterator α m β]
+    [IteratorLoop α m n] [MonadLiftT m n] :
+    IteratorLoop (TakeWhile α m β P) m n where
+  forIn lift {γ} Plausible wf it init f := by
+    refine IteratorLoop.forIn lift (γ := γ)
+        (PlausibleForInStep P Plausible)
+        (wellFounded_plausibleForInStep wf)
+        it.internalState.inner
+        init
+        fun out acc => do match ← (P out).operation with
+          | ⟨.up true, h⟩ => match ← f out acc with
+            | ⟨.yield c, h'⟩ => pure ⟨.yield c, h, h'⟩
+            | ⟨.done c, h'⟩ => pure ⟨.done c, .intro⟩
+          | ⟨.up false, h⟩ => pure ⟨.done acc, .intro⟩
+
+instance TakeWhile.instIteratorForPartial [Monad m] [Monad n] [Iterator α m β]
+    [IteratorLoopPartial α m n] [MonadLiftT m n] {P} :
+    IteratorLoopPartial (TakeWhile α m β P) m n where
+  forInPartial lift {γ} it init f := do
+    IteratorLoopPartial.forInPartial lift it.internalState.inner (γ := γ)
+        init
+        fun out acc => do match ← (P out).operation with
+          | ⟨.up true, _⟩ => match ← f out acc with
+            | .yield c => pure (.yield c)
+            | .done c => pure (.done c)
+          | ⟨.up false, _⟩ => pure (.done acc)
+
+end Std.Iterators

src/Std/Data/Iterators/Combinators/TakeWhile.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Std.Data.Iterators.Combinators.Monadic.TakeWhile
+
+namespace Std.Iterators
+
+/--
+Given an iterator `it` and a predicate `P`, `it.takeWhile P` is an iterator that outputs
+the values emitted by `it` until one of those values is rejected by `P`.
+If some emitted value is rejected by `P`, the value is dropped and the iterator terminates.
+
+**Marble diagram:**
+
+Assuming that the predicate `P` accepts `a` and `b` but rejects `c`:
+
+```text
+it               ---a----b---c--d-e--⊥
+it.takeWhile P   ---a----b---⊥
+
+it               ---a----⊥
+it.takeWhile P   ---a----⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: only if `it` is finite
+* `Productive` instance: only if `it` is productive
+
+Depending on `P`, it is possible that `it.takeWhile P` is finite (or productive) although `it` is not.
+In this case, the `Finite` (or `Productive`) instance needs to be proved manually.
+
+**Performance:**
+
+This combinator calls `P` on each output of `it` until the predicate evaluates to false. Then
+it terminates.
+-/
+@[always_inline, inline]
+def Iter.takeWhile {α : Type w} {β : Type w} (P : β → Bool) (it : Iter (α := α) β) :=
+  (it.toIterM.takeWhile P |>.toIter : Iter β)
+
+end Std.Iterators

src/Std/Data/Iterators/Lemmas/Combinators.lean

@@ -6,5 +6,7 @@ Authors: Paul Reichert
 prelude
 import Std.Data.Iterators.Lemmas.Combinators.Monadic
 import Std.Data.Iterators.Lemmas.Combinators.Take
+import Std.Data.Iterators.Lemmas.Combinators.TakeWhile
+import Std.Data.Iterators.Lemmas.Combinators.DropWhile
 import Std.Data.Iterators.Lemmas.Combinators.FilterMap
 import Std.Data.Iterators.Lemmas.Combinators.Zip

src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean

@@ -0,0 +1,124 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Std.Data.Iterators.Combinators.DropWhile
+import Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
+import Std.Data.Iterators.Lemmas.Consumers
+
+namespace Std.Iterators
+
+theorem Iter.dropWhile_eq_intermediateDropWhile {α β} [Iterator α Id β] {P}
+    {it : Iter (α := α) β} :
+    it.dropWhile P = Intermediate.dropWhile P true it :=
+  rfl
+
+theorem Iter.Intermediate.dropWhile_eq_dropWhile_toIterM {α β} [Iterator α Id β] {P}
+    {it : Iter (α := α) β} {dropping} :
+    Intermediate.dropWhile P dropping it =
+      (IterM.Intermediate.dropWhile P dropping it.toIterM).toIter :=
+  rfl
+
+theorem Iter.dropWhile_eq_dropWhile_toIterM {α β} [Iterator α Id β] {P}
+    {it : Iter (α := α) β} :
+    it.dropWhile P = (it.toIterM.dropWhile P).toIter :=
+  rfl
+
+theorem Iter.step_intermediateDropWhile {α β} [Iterator α Id β]
+    {it : Iter (α := α) β} {P} {dropping} :
+    (Iter.Intermediate.dropWhile P dropping it).step = (match it.step with
+      | .yield it' out h =>
+        if h' : dropping = true then
+          match P out with
+          | true =>
+            .skip (Intermediate.dropWhile P true it') (.dropped h h' True.intro)
+          | false =>
+            .yield (Intermediate.dropWhile P false it') out (.start h h' True.intro)
+        else
+          .yield (Intermediate.dropWhile P false it') out
+              (.yield h (Bool.not_eq_true _ ▸ h'))
+      | .skip it' h =>
+        .skip (Intermediate.dropWhile P dropping it') (.skip h)
+      | .done h =>
+        .done (.done h)) := by
+  simp [Intermediate.dropWhile_eq_dropWhile_toIterM, Iter.step, IterM.step_intermediateDropWhile]
+  cases it.toIterM.step.run using PlausibleIterStep.casesOn
+  · simp only [IterM.Step.toPure_yield, PlausibleIterStep.yield, toIter_toIterM, toIterM_toIter]
+    split
+    · split
+      · split
+        · rfl
+        · exfalso; simp_all
+      · split
+        · exfalso; simp_all
+        · rfl
+    · rfl
+  · rfl
+  · rfl
+
+theorem Iter.step_dropWhile {α β} [Iterator α Id β] {P}
+    {it : Iter (α := α) β} :
+    (it.dropWhile P).step = (match it.step with
+    | .yield it' out h =>
+        match P out with
+        | true =>
+          .skip (Intermediate.dropWhile P true it') (.dropped h rfl True.intro)
+        | false =>
+          .yield (Intermediate.dropWhile P false it') out (.start h rfl True.intro)
+    | .skip it' h =>
+      .skip (Intermediate.dropWhile P true it') (.skip h)
+    | .done h =>
+      .done (.done h)) := by
+  simp [dropWhile_eq_intermediateDropWhile, step_intermediateDropWhile]
+
+theorem Iter.toList_intermediateDropWhile_of_finite {α β} [Iterator α Id β] {P dropping}
+    [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : Iter (α := α) β} :
+    (Intermediate.dropWhile P dropping it).toList =
+      if dropping = true then it.toList.dropWhile P else it.toList := by
+  induction it using Iter.inductSteps generalizing dropping with | step it ihy ihs =>
+  rw [toList_eq_match_step, toList_eq_match_step, step_intermediateDropWhile]
+  cases it.step using PlausibleIterStep.casesOn
+  · rename_i hp
+    simp [List.dropWhile_cons]
+    cases P _
+    · cases dropping
+      · specialize ihy hp (dropping := false)
+        rw [if_neg (by simp)] at ihy
+        simp [ihy]
+      · specialize ihy hp (dropping := false)
+        rw [if_neg (by simp)] at ihy
+        simp [ihy]
+    · cases dropping
+      · specialize ihy hp (dropping := false)
+        simp [ihy]
+      · specialize ihy hp (dropping := true)
+        simp [ihy]
+  · rename_i hp
+    simp [ihs hp]
+  · simp
+
+@[simp]
+theorem Iter.toList_dropWhile_of_finite {α β} [Iterator α Id β] {P}
+    [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : Iter (α := α) β} :
+    (it.dropWhile P).toList = it.toList.dropWhile P := by
+  simp [dropWhile_eq_intermediateDropWhile, toList_intermediateDropWhile_of_finite]
+
+@[simp]
+theorem Iter.toArray_dropWhile_of_finite {α β} [Iterator α Id β] {P}
+    [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : Iter (α := α) β} :
+    (it.dropWhile P).toArray = (it.toList.dropWhile P).toArray := by
+  simp only [← toArray_toList, toList_dropWhile_of_finite]
+
+@[simp]
+theorem Iter.toListRev_dropWhile_of_finite {α β} [Iterator α Id β] {P}
+    [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : Iter (α := α) β} :
+    (it.dropWhile P).toListRev = (it.toList.dropWhile P).reverse := by
+  rw [toListRev_eq, toList_dropWhile_of_finite]
+
+end Std.Iterators

src/Std/Data/Iterators/Lemmas/Combinators/Monadic.lean

@@ -5,5 +5,7 @@ Authors: Paul Reichert
 -/
 prelude
 import Std.Data.Iterators.Lemmas.Combinators.Monadic.Take
+import Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
+import Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
 import Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
 import Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip

src/Std/Data/Iterators/Lemmas/Combinators/Monadic/DropWhile.lean

@@ -0,0 +1,172 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Std.Data.Iterators.Combinators.Monadic.DropWhile
+import Std.Data.Iterators.Lemmas.Consumers.Monadic
+
+namespace Std.Iterators
+
+theorem IterM.Intermediate.dropWhileM_eq_dropWhileWithPostcondition {α m β} [Monad m]
+    [Iterator α m β] {it : IterM (α := α) m β} {P dropping} :
+    Intermediate.dropWhileM P dropping it =
+      Intermediate.dropWhileWithPostcondition (PostconditionT.lift ∘ P) dropping it :=
+  rfl
+
+theorem IterM.Intermediate.dropWhile_eq_dropWhileM {α m β} [Monad m]
+    [Iterator α m β] {it : IterM (α := α) m β} {P} :
+    Intermediate.dropWhile P dropping it =
+      Intermediate.dropWhileM (pure ∘ ULift.up ∘ P) dropping it :=
+  rfl
+
+theorem IterM.dropWhileWithPostcondition_eq_intermediateDropWhileWithPostcondition {α m β}
+    [Iterator α m β] {it : IterM (α := α) m β} {P} :
+    it.dropWhileWithPostcondition P = Intermediate.dropWhileWithPostcondition P true it :=
+  rfl
+
+theorem IterM.dropWhileM_eq_intermediateDropWhileM {α m β} [Monad m]
+    [Iterator α m β] {it : IterM (α := α) m β} {P} :
+    it.dropWhileM P = Intermediate.dropWhileM P true it :=
+  rfl
+
+theorem IterM.dropWhile_eq_intermediateDropWhile {α m β} [Monad m]
+    [Iterator α m β] {it : IterM (α := α) m β} {P} :
+    it.dropWhile P = Intermediate.dropWhile P true it :=
+  rfl
+
+theorem IterM.step_intermediateDropWhileWithPostcondition {α m β} [Monad m] [Iterator α m β]
+    {it : IterM (α := α) m β} {P} {dropping} :
+    (IterM.Intermediate.dropWhileWithPostcondition P dropping it).step = (do
+    match ← it.step with
+    | .yield it' out h =>
+      if h' : dropping = true then
+        match ← (P out).operation with
+        | ⟨.up true, h''⟩ =>
+          return .skip (IterM.Intermediate.dropWhileWithPostcondition P true it') (.dropped h h' h'')
+        | ⟨.up false, h''⟩ =>
+          return .yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out (.start h h' h'')
+      else
+        return .yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out
+            (.yield h (Bool.not_eq_true _ ▸ h'))
+    | .skip it' h =>
+      return .skip (IterM.Intermediate.dropWhileWithPostcondition P dropping it') (.skip h)
+    | .done h =>
+      return .done (.done h)) := by
+  simp only [dropWhileWithPostcondition, step, Iterator.step, internalState_toIterM]
+  apply bind_congr
+  intro step
+  cases step using PlausibleIterStep.casesOn <;> rfl
+
+theorem IterM.step_dropWhileWithPostcondition {α m β} [Monad m] [Iterator α m β]
+    {it : IterM (α := α) m β} {P} :
+    (it.dropWhileWithPostcondition P).step = (do
+    match ← it.step with
+    | .yield it' out h =>
+        match ← (P out).operation with
+        | ⟨.up true, h''⟩ =>
+          return .skip (IterM.Intermediate.dropWhileWithPostcondition P true it') (.dropped h rfl h'')
+        | ⟨.up false, h''⟩ =>
+          return .yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out (.start h rfl h'')
+    | .skip it' h =>
+      return .skip (IterM.Intermediate.dropWhileWithPostcondition P true it') (.skip h)
+    | .done h =>
+      return .done (.done h)) := by
+  simp [dropWhileWithPostcondition_eq_intermediateDropWhileWithPostcondition, step_intermediateDropWhileWithPostcondition]
+
+theorem IterM.step_intermediateDropWhileM {α m β} [Monad m] [LawfulMonad m] [Iterator α m β]
+    {it : IterM (α := α) m β} {P} {dropping} :
+    (IterM.Intermediate.dropWhileM P dropping it).step = (do
+    match ← it.step with
+    | .yield it' out h =>
+      if h' : dropping = true then
+        match ← P out with
+        | .up true =>
+          return .skip (IterM.Intermediate.dropWhileM P true it') (.dropped h h' True.intro)
+        | .up false =>
+          return .yield (IterM.Intermediate.dropWhileM P false it') out (.start h h' True.intro)
+      else
+        return .yield (IterM.Intermediate.dropWhileM P false it') out
+            (.yield h (Bool.not_eq_true _ ▸ h'))
+    | .skip it' h =>
+      return .skip (IterM.Intermediate.dropWhileM P dropping it') (.skip h)
+    | .done h =>
+      return .done (.done h)) := by
+  simp only [Intermediate.dropWhileM_eq_dropWhileWithPostcondition, step_intermediateDropWhileWithPostcondition]
+  apply bind_congr
+  intro step
+  cases step using PlausibleIterStep.casesOn
+  · simp only [Function.comp_apply, PostconditionT.operation_lift, PlausibleIterStep.skip,
+    PlausibleIterStep.yield, bind_map_left]
+    split
+    · apply bind_congr
+      rintro ⟨x⟩
+      cases x <;> rfl
+    · rfl
+  · rfl
+  · rfl
+
+theorem IterM.step_dropWhileM {α m β} [Monad m] [LawfulMonad m] [Iterator α m β]
+    {it : IterM (α := α) m β} {P} :
+    (it.dropWhileM P).step = (do
+    match ← it.step with
+    | .yield it' out h =>
+      match ← P out with
+      | .up true =>
+        return .skip (IterM.Intermediate.dropWhileM P true it') (.dropped h rfl True.intro)
+      | .up false =>
+        return .yield (IterM.Intermediate.dropWhileM P false it') out (.start h rfl True.intro)
+    | .skip it' h =>
+      return .skip (IterM.Intermediate.dropWhileM P true it') (.skip h)
+    | .done h =>
+      return .done (.done h)) := by
+  simp [dropWhileM_eq_intermediateDropWhileM, step_intermediateDropWhileM]
+
+theorem IterM.step_intermediateDropWhile {α m β} [Monad m] [LawfulMonad m] [Iterator α m β]
+    {it : IterM (α := α) m β} {P} {dropping} :
+    (IterM.Intermediate.dropWhile P dropping it).step = (do
+    match ← it.step with
+    | .yield it' out h =>
+      if h' : dropping = true then
+        match P out with
+        | true =>
+          return .skip (IterM.Intermediate.dropWhile P true it') (.dropped h h' True.intro)
+        | false =>
+          return .yield (IterM.Intermediate.dropWhile P false it') out (.start h h' True.intro)
+      else
+        return .yield (IterM.Intermediate.dropWhile P false it') out
+            (.yield h (Bool.not_eq_true _ ▸ h'))
+    | .skip it' h =>
+      return .skip (IterM.Intermediate.dropWhile P dropping it') (.skip h)
+    | .done h =>
+      return .done (.done h)) := by
+  simp only [Intermediate.dropWhile_eq_dropWhileM, step_intermediateDropWhileM]
+  apply bind_congr
+  intro step
+  cases step using PlausibleIterStep.casesOn
+  · simp only [Function.comp_apply, PostconditionT.operation_lift, PlausibleIterStep.skip,
+    PlausibleIterStep.yield, bind_map_left]
+    split
+    · cases P _ <;> simp
+    · rfl
+  · rfl
+  · rfl
+
+theorem IterM.step_dropWhile {α m β} [Monad m] [LawfulMonad m] [Iterator α m β]
+    {it : IterM (α := α) m β} {P} :
+    (it.dropWhile P).step = (do
+    match ← it.step with
+    | .yield it' out h =>
+        match P out with
+        | true =>
+          return .skip (IterM.Intermediate.dropWhile P true it') (.dropped h rfl True.intro)
+        | false =>
+          return .yield (IterM.Intermediate.dropWhile P false it') out (.start h rfl True.intro)
+    | .skip it' h =>
+      return .skip (IterM.Intermediate.dropWhile P true it') (.skip h)
+    | .done h =>
+      return .done (.done h)) := by
+  simp [dropWhile_eq_intermediateDropWhile, step_intermediateDropWhile]
+
+end Std.Iterators

src/Std/Data/Iterators/Lemmas/Combinators/Monadic/TakeWhile.lean

@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Std.Data.Iterators.Combinators.Monadic.TakeWhile
+import Std.Data.Iterators.Lemmas.Consumers.Monadic
+
+namespace Std.Iterators
+
+theorem IterM.step_takeWhileWithPostcondition {α m β} [Monad m] [Iterator α m β]
+    {it : IterM (α := α) m β} {P} :
+    (it.takeWhileWithPostcondition P).step = (do
+      match ← it.step with
+      | .yield it' out h => match ← (P out).operation with
+        | ⟨.up true, h'⟩ => pure <| .yield (it'.takeWhileWithPostcondition P) out (.yield h h')
+        | ⟨.up false, h'⟩ => pure <| .done (.rejected h h')
+      | .skip it' h => pure <| .skip (it'.takeWhileWithPostcondition P) (.skip h)
+      | .done h => pure <| .done (.done h)) := by
+  simp only [takeWhileWithPostcondition, step, Iterator.step, internalState_toIterM]
+  apply bind_congr
+  intro step
+  cases step using PlausibleIterStep.casesOn <;> rfl
+
+theorem IterM.step_takeWhileM {α m β} [Monad m] [LawfulMonad m] [Iterator α m β]
+    {it : IterM (α := α) m β} {P} :
+    (it.takeWhileM P).step = (do
+      match ← it.step with
+      | .yield it' out h => match ← P out with
+        | .up true => pure <| .yield (it'.takeWhileM P) out (.yield h True.intro)
+        | .up false => pure <| .done (.rejected h True.intro)
+      | .skip it' h => pure <| .skip (it'.takeWhileM P) (.skip h)
+      | .done h => pure <| .done (.done h)) := by
+  simp only [takeWhileM, step_takeWhileWithPostcondition]
+  apply bind_congr
+  intro step
+  cases step using PlausibleIterStep.casesOn
+  · simp only [Function.comp_apply, PostconditionT.operation_lift, PlausibleIterStep.yield,
+    PlausibleIterStep.done, bind_map_left]
+    apply bind_congr
+    rintro ⟨x⟩
+    cases x <;> rfl
+  · simp
+  · simp
+
+theorem IterM.step_takeWhile {α m β} [Monad m] [LawfulMonad m] [Iterator α m β]
+    {it : IterM (α := α) m β} {P} :
+    (it.takeWhile P).step = (do
+      match ← it.step with
+      | .yield it' out h => match P out with
+        | true => pure <| .yield (it'.takeWhile P) out (.yield h True.intro)
+        | false => pure <| .done (.rejected h True.intro)
+      | .skip it' h => pure <| .skip (it'.takeWhile P) (.skip h)
+      | .done h => pure <| .done (.done h)) := by
+  simp only [takeWhile, step_takeWhileM]
+  apply bind_congr
+  intro step
+  cases step using PlausibleIterStep.casesOn
+  · simp only [Function.comp_apply, PlausibleIterStep.yield, PlausibleIterStep.done, pure_bind]
+    cases P _ <;> rfl
+  · simp
+  · simp
+
+end Std.Iterators

src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean

@@ -0,0 +1,134 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Std.Data.Iterators.Combinators.TakeWhile
+import Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
+import Std.Data.Iterators.Lemmas.Consumers
+
+namespace Std.Iterators
+
+theorem Iter.takeWhile_eq {α β} [Iterator α Id β] {P}
+    {it : Iter (α := α) β} :
+    it.takeWhile P = (it.toIterM.takeWhile P).toIter :=
+  rfl
+
+theorem Iter.step_takeWhile {α β} [Iterator α Id β] {P}
+    {it : Iter (α := α) β} :
+    (it.takeWhile P).step = (match it.step with
+      | .yield it' out h => match P out with
+        | true => .yield (it'.takeWhile P) out (.yield h True.intro)
+        | false => .done (.rejected h True.intro)
+      | .skip it' h => .skip (it'.takeWhile P) (.skip h)
+      | .done h => .done (.done h)) := by
+  simp [Iter.takeWhile_eq, Iter.step, toIterM_toIter, IterM.step_takeWhile]
+  generalize it.toIterM.step.run = step
+  cases step using PlausibleIterStep.casesOn
+  · simp only [IterM.Step.toPure_yield, PlausibleIterStep.yield, toIter_toIterM, toIterM_toIter]
+    cases P _ <;> rfl
+  · simp
+  · simp
+
+theorem Iter.atIdxSlow?_takeWhile {α β}
+    [Iterator α Id β] [Productive α Id] {l : Nat}
+    {it : Iter (α := α) β} {P} :
+    (it.takeWhile P).atIdxSlow? l = if ∀ k, k ≤ l → (it.atIdxSlow? k).any P then it.atIdxSlow? l else none := by
+  fun_induction it.atIdxSlow? l
+  case case1 it it' out h h' =>
+    simp only [atIdxSlow?.eq_def (it := it.takeWhile P), step_takeWhile, h',
+      PlausibleIterStep.yield, PlausibleIterStep.done, Nat.le_zero_eq, forall_eq]
+    rw [atIdxSlow?, h']
+    simp only [Option.any_some]
+    apply Eq.symm
+    split
+    · cases h' : P out
+      · exfalso; simp_all
+      · simp
+    · cases h' : P out
+      · simp
+      · exfalso; simp_all
+  case case2 it it' out h h' l ih =>
+    simp only [Nat.succ_eq_add_one, atIdxSlow?.eq_def (it := it.takeWhile P), step_takeWhile, h']
+    simp only [atIdxSlow?.eq_def (it := it), h']
+    cases hP : P out
+    · simp
+      intro h
+      specialize h 0 (Nat.zero_le _)
+      simp at h
+      exfalso; simp_all
+    · simp [ih]
+      split
+      · rename_i h
+        rw [if_pos]
+        intro k hk
+        split
+        · exact hP
+        · simp at hk
+          exact h _ hk
+      · rename_i hl
+        rw [if_neg]
+        intro hl'
+        apply hl
+        intro k hk
+        exact hl' (k + 1) (Nat.succ_le_succ hk)
+  case case3 l it it' h h' ih =>
+    simp only [atIdxSlow?.eq_def (it := it.takeWhile P), step_takeWhile, h', ih]
+    simp only [atIdxSlow?.eq_def (it := it), h']
+  case case4 l it h h' =>
+    simp only [atIdxSlow?.eq_def (it := it), atIdxSlow?.eq_def (it := it.takeWhile P), h',
+      step_takeWhile]
+    split <;> rfl
+
+private theorem List.getElem?_takeWhile {l : List α} {P : α → Bool} {k} :
+    (l.takeWhile P)[k]? = if ∀ k' : Nat, k' ≤ k → l[k']?.any P then l[k]? else none := by
+  induction l generalizing k
+  · simp
+  · rename_i x xs ih
+    rw [List.takeWhile_cons]
+    split
+    · cases k
+      · simp [*]
+      · simp [ih]
+        split
+        · rw [if_pos]
+          intro k' hk'
+          cases k'
+          · simp [*]
+          · simp_all
+        · rename_i hP
+          rw [if_neg]
+          intro hP'
+          apply hP
+          intro k' hk'
+          specialize hP' (k' + 1) (by omega)
+          simp_all
+    · simp
+      intro h
+      specialize h 0
+      simp_all
+
+@[simp]
+theorem Iter.toList_takeWhile_of_finite {α β} [Iterator α Id β] {P}
+    [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : Iter (α := α) β} :
+    (it.takeWhile P).toList = it.toList.takeWhile P := by
+  ext
+  simp only [getElem?_toList_eq_atIdxSlow?, atIdxSlow?_takeWhile, List.getElem?_takeWhile]
+
+@[simp]
+theorem Iter.toListRev_takeWhile_of_finite {α β} [Iterator α Id β] {P}
+    [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : Iter (α := α) β} :
+    (it.takeWhile P).toListRev = (it.toList.takeWhile P).reverse := by
+  rw [toListRev_eq, toList_takeWhile_of_finite]
+
+@[simp]
+theorem Iter.toArray_takeWhile_of_finite {α β} [Iterator α Id β] {P}
+    [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : Iter (α := α) β} :
+    (it.takeWhile P).toArray = it.toArray.takeWhile P := by
+  rw [← toArray_toList, ← toArray_toList, List.takeWhile_toArray, toList_takeWhile_of_finite]
+
+end Std.Iterators

src/Std/Data/Iterators/PostConditionMonad.lean

@@ -171,4 +171,9 @@ theorem PostconditionT.operation_map {m : Type w → Type w'} [Functor m] {α :
     (x.map f).operation = (fun a => ⟨_, a, rfl⟩) <$> x.operation :=
   rfl
 
+@[simp]
+theorem PostconditionT.operation_lift {m : Type w →Type w'} [Functor m] {α : Type w}
+    {x : m α} : (lift x : PostconditionT m α).operation = (⟨·, True.intro⟩) <$> x :=
+  rfl
+
 end Std.Iterators

tests/lean/run/iterators.lean

@@ -182,3 +182,29 @@ example : ([1, 2, 3].iter.zip ["one", "two"].iter).toArray =
   simp
 
 end Zip
+
+section TakeWhile
+
+example : ([1, 2, 3, 4].iter.takeWhile (· ≠ 3)).toList = [1, 2] := by
+  simp
+
+example : ([1, 2, 3, 4].iter.takeWhile (· ≠ 3)).toArray = #[1, 2] := by
+  simp
+
+example : ([1, 2, 3, 4].iter.takeWhile (· ≠ 3)).toListRev = [2, 1] := by
+  simp
+
+end TakeWhile
+
+section DropWhile
+
+example : ([1, 2, 3, 4].iter.dropWhile (· ≠ 3)).toList = [3, 4] := by
+  simp
+
+example : ([1, 2, 3, 4].iter.dropWhile (· ≠ 3)).toArray = #[3, 4] := by
+  simp
+
+example : ([1, 2, 3, 4].iter.dropWhile (· ≠ 3)).toListRev = [4, 3] := by
+  simp
+
+end DropWhile