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

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

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

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

@[simp]

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

@[deprecated Std.Slice.toArray_iter (since := "2025-11-13")]

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

@[simp]

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

@[deprecated Std.Slice.toList_iter (since := "2025-11-13")]

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

@[simp]

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

@[deprecated Std.Slice.toListRev_iter (since := "2025-11-13")]

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