theorem
Std.Iterators.IterM.step_take
{α : Type u_1}
{m : Type u_1 → Type u_2}
{β : Type u_1}
[Monad m]
[Iterator α m β]
{n : Nat}
{it : IterM m β}
:
(take n it).step = match n with
| 0 => pure (Shrink.deflate (PlausibleIterStep.done ⋯))
| k.succ => do
let __do_lift ← it.step
match __do_lift.inflate with
| ⟨IterStep.yield it' out, h⟩ => pure (Shrink.deflate (PlausibleIterStep.yield (take k it') out ⋯))
| ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (take (k + 1) it') ⋯))
| ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))