theorem Std.Iterators.Iter.take_eq_toIter_take_toIterM {α β : Type u_1} [Iterator α Id β] {n : Nat} {it : Iter β} : take n it = (IterM.take n it.toIterM).toIter

theorem Std.Iterators.Iter.step_take {α β : Type u_1} [Iterator α Id β] {n : Nat} {it : Iter β} : (take n it).step = match n with | 0 => PlausibleIterStep.done ⋯ | k.succ => match it.step with | ⟨IterStep.yield it' out, h⟩ => PlausibleIterStep.yield (take k it') out ⋯ | ⟨IterStep.skip it', h⟩ => PlausibleIterStep.skip (take (k + 1) it') ⋯ | ⟨IterStep.done, h⟩ => PlausibleIterStep.done ⋯

theorem Std.Iterators.Iter.atIdxSlow?_take {α β : Type u_1} [Iterator α Id β] [Productive α Id] {k l : Nat} {it : Iter β} : atIdxSlow? l (take k it) = if l < k then atIdxSlow? l it else none

@[simp]

theorem Std.Iterators.Iter.toList_take_of_finite {α β : Type u_1} [Iterator α Id β] {n : Nat} [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} : (take n it).toList = List.take n it.toList

@[simp]

theorem Std.Iterators.Iter.toListRev_take_of_finite {α β : Type u_1} [Iterator α Id β] {n : Nat} [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} : (take n it).toListRev = List.drop (it.toList.length - n) it.toListRev

@[simp]

theorem Std.Iterators.Iter.toArray_take_of_finite {α β : Type u_1} [Iterator α Id β] {n : Nat} [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} : (take n it).toArray = it.toArray.take n

@[simp]

theorem Std.Iterators.Iter.toList_take_zero {α β : Type u_1} [Iterator α Id β] [Finite (Take α Id β) Id] [IteratorCollect (Take α Id β) Id Id] [LawfulIteratorCollect (Take α Id β) Id Id] {it : Iter β} : (take 0 it).toList = []