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

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 with | ⟨IterStep.yield it' out, property⟩ => #[out] ++ it'.toArray | ⟨IterStep.skip it', property⟩ => it'.toArray | ⟨IterStep.done, property⟩ => #[]

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 with | ⟨IterStep.yield it' out, property⟩ => out :: it'.toList | ⟨IterStep.skip it', property⟩ => it'.toList | ⟨IterStep.done, property⟩ => []

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

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