theorem Std.Iterators.Iter.uLift_eq_toIter_uLift_toIterM {α β : Type u} {it : Iter β} : it.uLift = (it.toIterM.uLift Id).toIter

theorem Std.Iterators.Iter.step_uLift {α β : Type u} [Iterator α Id β] {it : Iter β} : it.uLift.step = ⟨Types.ULiftIterator.modifyStep it.step.val, ⋯⟩

@[simp]

theorem Std.Iterators.Iter.toList_uLift {α β : Type u} [Iterator α Id β] {it : Iter β} [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] : it.uLift.toList = List.map ULift.up it.toList

@[simp]

theorem Std.Iterators.Iter.toListRev_uLift {α β : Type u} [Iterator α Id β] {it : Iter β} [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] : it.uLift.toListRev = List.map ULift.up it.toListRev

@[simp]

theorem Std.Iterators.Iter.toArray_uLift {α β : Type u} [Iterator α Id β] {it : Iter β} [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] : it.uLift.toArray = Array.map ULift.up it.toArray