theorem Std.Iterators.IterM.step_uLift {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} [Iterator α m β] [Monad n] {it : IterM m β} [MonadLiftT m (ULiftT n)] : (it.uLift n).step = do let __do_lift ← (monadLift it.step).run have step : it.Step := __do_lift.down pure ⟨Types.ULiftIterator.Monadic.modifyStep step.val, ⋯⟩

@[simp]

theorem Std.Iterators.IterM.toList_uLift {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} [Iterator α m β] [Monad m] [Monad n] {it : IterM m β} [MonadLiftT m (ULiftT n)] [Finite α m] [IteratorCollect α m m] [LawfulMonad m] [LawfulMonad n] [LawfulIteratorCollect α m m] [LawfulMonadLiftT m (ULiftT n)] : (it.uLift n).toList = (fun (l : ULift (List β)) => List.map ULift.up l.down) <$> (monadLift it.toList).run

@[simp]

theorem Std.Iterators.IterM.toListRev_uLift {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} [Iterator α m β] [Monad m] [Monad n] {it : IterM m β} [MonadLiftT m (ULiftT n)] [Finite α m] [IteratorCollect α m m] [LawfulMonad m] [LawfulMonad n] [LawfulIteratorCollect α m m] [LawfulMonadLiftT m (ULiftT n)] : (it.uLift n).toListRev = (fun (l : ULift (List β)) => List.map ULift.up l.down) <$> (monadLift it.toListRev).run

@[simp]

theorem Std.Iterators.IterM.toArray_uLift {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} [Iterator α m β] [Monad m] [Monad n] {it : IterM m β} [MonadLiftT m (ULiftT n)] [Finite α m] [IteratorCollect α m m] [LawfulMonad m] [LawfulMonad n] [LawfulIteratorCollect α m m] [LawfulMonadLiftT m (ULiftT n)] : (it.uLift n).toArray = (fun (l : ULift (Array β)) => Array.map ULift.up l.down) <$> (monadLift it.toArray).run