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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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