theorem Std.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.Iter.toTake_eq_toIter_toTake_toIterM {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} : it.toTake = it.toIterM.toTake.toIter

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Std.Iter.step_toTake {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} : it.toTake.step = match it.step with | ⟨IterStep.yield it' out, h⟩ => PlausibleIterStep.yield it'.toTake out ⋯ | ⟨IterStep.skip it', h⟩ => PlausibleIterStep.skip it'.toTake ⋯ | ⟨IterStep.done, h⟩ => PlausibleIterStep.done ⋯

@[simp]

theorem Std.Iter.toList_toTake {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} : it.toTake.toList = it.toList