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 match __do_lift.down.inflate with | ⟨IterStep.yield it' out, h⟩ => pure (Shrink.deflate (PlausibleIterStep.yield (it'.uLift n) { down := out } ⋯)) | ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (it'.uLift n) ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))

@[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

@[simp]

theorem Std.Iterators.IterM.count_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] [IteratorLoop α m m] [LawfulMonad m] [LawfulMonad n] [LawfulIteratorLoop α m m] [LawfulMonadLiftT m (ULiftT n)] : (it.uLift n).count = (fun (x : ULift (ULift Nat)) => { down := x.down.down }) <$> (monadLift it.count).run