theorem Std.Iterators.IterM.DefaultConsumers.toArrayMapped.go.aux₁ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃δ : Type w⦄ → m δ → n δ} {f : β → n γ} {it : IterM m β} [Monad n] [LawfulMonad n] [Iterator α m β] [Finite α m] {b : γ} {bs : Array γ} : go lift f it (#[b] ++ bs) = (fun (x : Array γ) => #[b] ++ x) <$> go lift f it bs

theorem Std.Iterators.IterM.DefaultConsumers.toArrayMapped.go.aux₂ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃δ : Type w⦄ → m δ → n δ} {f : β → n γ} {it : IterM m β} [Monad n] [LawfulMonad n] [Iterator α m β] [Finite α m] {acc : Array γ} : go lift f it acc = (fun (x : Array γ) => acc ++ x) <$> toArrayMapped lift f it

theorem Std.Iterators.IterM.DefaultConsumers.toArrayMapped_eq_match_step {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃δ : Type w⦄ → m δ → n δ} {f : β → n γ} {it : IterM m β} [Monad n] [LawfulMonad n] [Iterator α m β] [Finite α m] : toArrayMapped lift f it = do let __do_lift ← liftM it.step match __do_lift with | ⟨IterStep.yield it' out, property⟩ => do let __do_lift ← f out let __do_lift_1 ← toArrayMapped lift f it' pure (#[__do_lift] ++ __do_lift_1) | ⟨IterStep.skip it', property⟩ => toArrayMapped lift f it' | ⟨IterStep.done, property⟩ => pure #[]

theorem Std.Iterators.IterM.toArray_eq_match_step {α β : Type w} {m : Type w → Type w'} {it : IterM m β} [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m] : it.toArray = do let __do_lift ← it.step match __do_lift with | ⟨IterStep.yield it' out, property⟩ => do let __do_lift ← it'.toArray pure (#[out] ++ __do_lift) | ⟨IterStep.skip it', property⟩ => it'.toArray | ⟨IterStep.done, property⟩ => pure #[]

theorem Std.Iterators.IterM.toList_toArray {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Finite α m] [IteratorCollect α m m] {it : IterM m β} : Array.toList <$> it.toArray = it.toList

theorem Std.Iterators.IterM.toArray_toList {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m] [IteratorCollect α m m] {it : IterM m β} : List.toArray <$> it.toList = it.toArray

theorem Std.Iterators.IterM.toList_eq_match_step {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m] {it : IterM m β} : it.toList = do let __do_lift ← it.step match __do_lift with | ⟨IterStep.yield it' out, property⟩ => do let __do_lift ← it'.toList pure (out :: __do_lift) | ⟨IterStep.skip it', property⟩ => it'.toList | ⟨IterStep.done, property⟩ => pure []

theorem Std.Iterators.IterM.toListRev.go.aux₁ {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m] {it : IterM m β} {b : β} {bs : List β} : go it (bs ++ [b]) = (fun (x : List β) => x ++ [b]) <$> go it bs

theorem Std.Iterators.IterM.toListRev.go.aux₂ {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m] {it : IterM m β} {acc : List β} : go it acc = (fun (x : List β) => x ++ acc) <$> it.toListRev

theorem Std.Iterators.IterM.toListRev_eq_match_step {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m] {it : IterM m β} : it.toListRev = do let __do_lift ← it.step match __do_lift with | ⟨IterStep.yield it' out, property⟩ => do let __do_lift ← it'.toListRev pure (__do_lift ++ [out]) | ⟨IterStep.skip it', property⟩ => it'.toListRev | ⟨IterStep.done, property⟩ => pure []

theorem Std.Iterators.IterM.reverse_toListRev {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m] {it : IterM m β} : List.reverse <$> it.toListRev = it.toList

theorem Std.Iterators.IterM.toListRev_eq {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m] {it : IterM m β} : it.toListRev = List.reverse <$> it.toList

theorem Std.Iterators.LawfulIteratorCollect.toArray_eq {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Finite α m] [IteratorCollect α m m] [hl : LawfulIteratorCollect α m m] {it : IterM m β} : it.toArray = it.toArray

theorem Std.Iterators.LawfulIteratorCollect.toList_eq {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Finite α m] [IteratorCollect α m m] [hl : LawfulIteratorCollect α m m] {it : IterM m β} : it.toList = it.toList