theorem Std.Iterators.Iter.takeWhile_eq {α β : Type u_1} [Iterator α Id β] {P : β → Bool} {it : Iter β} : takeWhile P it = (IterM.takeWhile P it.toIterM).toIter

theorem Std.Iterators.Iter.step_takeWhile {α β : Type u_1} [Iterator α Id β] {P : β → Bool} {it : Iter β} : (takeWhile P it).step = match it.step with | ⟨IterStep.yield it' out, h⟩ => match P out with | true => PlausibleIterStep.yield (takeWhile P it') out ⋯ | false => PlausibleIterStep.done ⋯ | ⟨IterStep.skip it', h⟩ => PlausibleIterStep.skip (takeWhile P it') ⋯ | ⟨IterStep.done, h⟩ => PlausibleIterStep.done ⋯

theorem Std.Iterators.Iter.atIdxSlow?_takeWhile {α β : Type u_1} [Iterator α Id β] [Productive α Id] {l : Nat} {it : Iter β} {P : β → Bool} : atIdxSlow? l (takeWhile P it) = if ∀ (k : Nat), k ≤ l → Option.any P (atIdxSlow? k it) = true then atIdxSlow? l it else none

@[simp]

theorem Std.Iterators.Iter.toList_takeWhile_of_finite {α β : Type u_1} [Iterator α Id β] {P : β → Bool} [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} : (takeWhile P it).toList = List.takeWhile P it.toList

@[simp]

theorem Std.Iterators.Iter.toListRev_takeWhile_of_finite {α β : Type u_1} [Iterator α Id β] {P : β → Bool} [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} : (takeWhile P it).toListRev = (List.takeWhile P it.toList).reverse

@[simp]

theorem Std.Iterators.Iter.toArray_takeWhile_of_finite {α β : Type u_1} [Iterator α Id β] {P : β → Bool} [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} : (takeWhile P it).toArray = Array.takeWhile P it.toArray