theorem Std.Slice.Internal.iter_eq_toIteratorIter {α β : Type v} {γ : Type u} [Iterators.ToIterator (Slice γ) Id α β] {s : Slice γ} : iter s = Iterators.ToIterator.iter s

theorem Std.Slice.forIn_internalIter {α : Type v} {γ : Type u} {β : Type v} {m : Type w → Type x} [Monad m] {δ : Type w} [Iterators.ToIterator (Slice γ) Id α β] [Iterators.Iterator α Id β] [Iterators.IteratorLoop α Id m] [Iterators.LawfulIteratorLoop α Id m] [Iterators.Finite α Id] {s : Slice γ} {init : δ} {f : β → δ → m (ForInStep δ)} : forIn (Internal.iter s) init f = forIn s init f

@[simp]

theorem Std.Slice.forIn_toList {α : Type v} {γ : Type u} {β : Type v} {m : Type w → Type x} [Monad m] [LawfulMonad m] {δ : Type w} [Iterators.ToIterator (Slice γ) Id α β] [Iterators.Iterator α Id β] [Iterators.IteratorLoop α Id m] [Iterators.LawfulIteratorLoop α Id m] [Iterators.IteratorCollect α Id Id] [Iterators.LawfulIteratorCollect α Id Id] [Iterators.Finite α Id] {s : Slice γ} {init : δ} {f : β → δ → m (ForInStep δ)} : forIn s.toList init f = forIn s init f

@[simp]

theorem Std.Slice.forIn_toArray {α : Type v} {γ : Type u} {β : Type v} {m : Type w → Type x} [Monad m] [LawfulMonad m] {δ : Type w} [Iterators.ToIterator (Slice γ) Id α β] [Iterators.Iterator α Id β] [Iterators.IteratorLoop α Id m] [Iterators.LawfulIteratorLoop α Id m] [Iterators.IteratorCollect α Id Id] [Iterators.LawfulIteratorCollect α Id Id] [Iterators.Finite α Id] {s : Slice γ} {init : δ} {f : β → δ → m (ForInStep δ)} : forIn s.toArray init f = forIn s init f

theorem Std.Slice.Internal.size_eq_count_iter {γ : Type u} {α β : Type v} [Iterators.ToIterator (Slice γ) Id α β] [Iterators.Iterator α Id β] [Iterators.Finite α Id] [Iterators.IteratorLoop α Id Id] [Iterators.LawfulIteratorLoop α Id Id] {s : Slice γ} [SliceSize γ] [LawfulSliceSize γ] : s.size = (iter s).count

theorem Std.Slice.Internal.toArray_eq_toArray_iter {γ : Type u} {α β : Type v} {s : Slice γ} [Iterators.ToIterator (Slice γ) Id α β] [Iterators.Iterator α Id β] [Iterators.IteratorCollect α Id Id] [Iterators.Finite α Id] : s.toArray = (iter s).toArray

theorem Std.Slice.Internal.toList_eq_toList_iter {γ : Type u} {α β : Type v} {s : Slice γ} [Iterators.ToIterator (Slice γ) Id α β] [Iterators.Iterator α Id β] [Iterators.IteratorCollect α Id Id] [Iterators.Finite α Id] : s.toList = (iter s).toList

theorem Std.Slice.Internal.toListRev_eq_toListRev_iter {γ : Type u} {α β : Type v} {s : Slice γ} [Iterators.ToIterator (Slice γ) Id α β] [Iterators.Iterator α Id β] [Iterators.Finite α Id] : s.toListRev = (iter s).toListRev

@[simp]

theorem Std.Slice.size_toArray_eq_size {γ : Type u} {α β : Type v} [Iterators.ToIterator (Slice γ) Id α β] [Iterators.Iterator α Id β] [SliceSize γ] [LawfulSliceSize γ] [Iterators.IteratorCollect α Id Id] [Iterators.Finite α Id] [Iterators.LawfulIteratorCollect α Id Id] {s : Slice γ} : s.toArray.size = s.size

@[simp]

theorem Std.Slice.length_toList_eq_size {γ : Type u} {α β : Type v} [Iterators.ToIterator (Slice γ) Id α β] [Iterators.Iterator α Id β] {s : Slice γ} [SliceSize γ] [LawfulSliceSize γ] [Iterators.IteratorCollect α Id Id] [Iterators.Finite α Id] [Iterators.LawfulIteratorCollect α Id Id] : s.toList.length = s.size

@[simp]

theorem Std.Slice.length_toListRev_eq_size {γ : Type u} {α β : Type v} [Iterators.ToIterator (Slice γ) Id α β] [Iterators.Iterator α Id β] {s : Slice γ} [Iterators.IteratorLoop α Id Id] [SliceSize γ] [LawfulSliceSize γ] [Iterators.Finite α Id] [Iterators.LawfulIteratorLoop α Id Id] : s.toListRev.length = s.size