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

theorem Std.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 hP : 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.Iter.val_step_takeWhile {α β : Type u_1} [Iterator α Id β] {P : β → Bool} {it : Iter β} : (takeWhile P it).step.val = match it.step.val with | IterStep.yield it' out => match P out with | true => IterStep.yield (takeWhile P it') out | false => IterStep.done | IterStep.skip it' => IterStep.skip (takeWhile P it') | IterStep.done => IterStep.done

theorem Std.Iter.atIdxSlow?_takeWhile {α β : Type u_1} [Iterator α Id β] [Iterators.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.Iter.toList_takeWhile_of_finite {α β : Type u_1} [Iterator α Id β] {P : β → Bool} [Iterators.Finite α Id] {it : Iter β} : (takeWhile P it).toList = List.takeWhile P it.toList

@[simp]

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

@[simp]

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