theorem Std.Iterators.Iter.toArray_eq_toArray_toIterM {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} : it.toArray = it.toIterM.toArray.run

theorem Std.Iterators.Iter.toList_eq_toList_toIterM {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} : it.toList = it.toIterM.toList.run

theorem Std.Iterators.Iter.toListRev_eq_toListRev_toIterM {α β : Type u_1} [Iterator α Id β] [Finite α Id] {it : Iter β} : it.toListRev = it.toIterM.toListRev.run

@[simp]

theorem Std.Iterators.IterM.toList_toIter {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] {it : IterM Id β} : it.toIter.toList = it.toList.run

@[simp]

theorem Std.Iterators.IterM.toListRev_toIter {α β : Type u_1} [Iterator α Id β] [Finite α Id] {it : IterM Id β} : it.toIter.toListRev = it.toListRev.run

theorem Std.Iterators.Iter.toList_toArray {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} : it.toArray.toList = it.toList

theorem Std.Iterators.Iter.toArray_toList {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} : it.toList.toArray = it.toArray

@[simp]

theorem Std.Iterators.Iter.reverse_toListRev {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} : it.toListRev.reverse = it.toList

theorem Std.Iterators.Iter.toListRev_eq {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} : it.toListRev = it.toList.reverse

theorem Std.Iterators.Iter.toArray_eq_match_step {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} : it.toArray = match it.step.val with | IterStep.yield it' out => #[out] ++ it'.toArray | IterStep.skip it' => it'.toArray | IterStep.done => #[]

theorem Std.Iterators.Iter.toList_eq_match_step {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} : it.toList = match it.step.val with | IterStep.yield it' out => out :: it'.toList | IterStep.skip it' => it'.toList | IterStep.done => []

theorem Std.Iterators.Iter.toListRev_eq_match_step {α β : Type u_1} [Iterator α Id β] [Finite α Id] {it : Iter β} : it.toListRev = match it.step.val with | IterStep.yield it' out => it'.toListRev ++ [out] | IterStep.skip it' => it'.toListRev | IterStep.done => []

theorem Std.Iterators.Iter.getElem?_toList_eq_atIdxSlow? {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} {k : Nat} : it.toList[k]? = atIdxSlow? k it

theorem Std.Iterators.Iter.toList_eq_of_atIdxSlow?_eq {α₁ α₂ β : Type u_1} [Iterator α₁ Id β] [Finite α₁ Id] [IteratorCollect α₁ Id Id] [LawfulIteratorCollect α₁ Id Id] [Iterator α₂ Id β] [Finite α₂ Id] [IteratorCollect α₂ Id Id] [LawfulIteratorCollect α₂ Id Id] {it₁ : Iter β} {it₂ : Iter β} (h : ∀ (k : Nat), atIdxSlow? k it₁ = atIdxSlow? k it₂) : it₁.toList = it₂.toList

theorem Std.Iterators.Iter.isPlausibleIndirectOutput_of_mem_toList {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} {b : β} : b ∈ it.toList → it.IsPlausibleIndirectOutput b

theorem Std.Iterators.Iter.isPlausibleIndirectOutput_of_mem_toListRev {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} {b : β} : b ∈ it.toListRev → it.IsPlausibleIndirectOutput b