theorem Std.IterM.step_filterMapWithPostcondition {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] {it : IterM m β} {f : β → Iterators.PostconditionT n (Option β')} [Monad n] [LawfulMonad n] [MonadLiftT m n] : (filterMapWithPostcondition f it).step = do let __do_lift ← liftM it.step match __do_lift.inflate with | ⟨IterStep.yield it' out, h⟩ => do let __do_lift ← (f out).operation match __do_lift with | ⟨none, h'⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (filterMapWithPostcondition f it') ⋯)) | ⟨some out', h'⟩ => pure (Shrink.deflate (PlausibleIterStep.yield (filterMapWithPostcondition f it') out' ⋯)) | ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (filterMapWithPostcondition f it') ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))

theorem Std.IterM.step_filterWithPostcondition {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] {it : IterM m β} {f : β → Iterators.PostconditionT n (ULift Bool)} [Monad n] [LawfulMonad n] [MonadLiftT m n] : (filterWithPostcondition f it).step = do let __do_lift ← liftM it.step match __do_lift.inflate with | ⟨IterStep.yield it' out, h⟩ => do let __do_lift ← (f out).operation match __do_lift with | ⟨{ down := false }, h'⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (filterWithPostcondition f it') ⋯)) | ⟨{ down := true }, h'⟩ => pure (Shrink.deflate (PlausibleIterStep.yield (filterWithPostcondition f it') out ⋯)) | ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (filterWithPostcondition f it') ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))

theorem Std.IterM.step_mapWithPostcondition {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] {it : IterM m β} {γ : Type w} {f : β → Iterators.PostconditionT n γ} [Monad n] [LawfulMonad n] [MonadLiftT m n] : (mapWithPostcondition f it).step = do let __do_lift ← liftM it.step match __do_lift.inflate with | ⟨IterStep.yield it' out, h⟩ => do let out' ← (f out).operation pure (Shrink.deflate (PlausibleIterStep.yield (mapWithPostcondition f it') out'.val ⋯)) | ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (mapWithPostcondition f it') ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))

theorem Std.IterM.step_filterMapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] {it : IterM m β} {f : β → n (Option β')} [Monad n] [MonadAttach n] [LawfulMonad n] [MonadLiftT m n] : (filterMapM f it).step = do let __do_lift ← liftM it.step match __do_lift.inflate with | ⟨IterStep.yield it' out, h⟩ => do let __do_lift ← MonadAttach.attach (f out) match __do_lift with | ⟨none, hf⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (filterMapM f it') ⋯)) | ⟨some out', hf⟩ => pure (Shrink.deflate (PlausibleIterStep.yield (filterMapM f it') out' ⋯)) | ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (filterMapM f it') ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))

theorem Std.IterM.step_filterM {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] {it : IterM m β} {f : β → n (ULift Bool)} [Monad n] [MonadAttach n] [LawfulMonad n] [MonadLiftT m n] : (filterM f it).step = do let __do_lift ← liftM it.step match __do_lift.inflate with | ⟨IterStep.yield it' out, h⟩ => do let __do_lift ← MonadAttach.attach (f out) match __do_lift with | ⟨{ down := false }, hf⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (filterM f it') ⋯)) | ⟨{ down := true }, hf⟩ => pure (Shrink.deflate (PlausibleIterStep.yield (filterM f it') out ⋯)) | ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (filterM f it') ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))

theorem Std.IterM.step_mapM {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] {it : IterM m β} {γ : Type w} {f : β → n γ} [Monad n] [MonadAttach n] [LawfulMonad n] [MonadLiftT m n] : (mapM f it).step = do let __do_lift ← liftM it.step match __do_lift.inflate with | ⟨IterStep.yield it' out, h⟩ => do let out' ← MonadAttach.attach (f out) pure (Shrink.deflate (PlausibleIterStep.yield (mapM f it') out'.val ⋯)) | ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (mapM f it') ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))

theorem Std.IterM.step_filterMap {α β β' : Type w} {m : Type w → Type w'} [Iterator α m β] {it : IterM m β} [Monad m] [LawfulMonad m] {f : β → Option β'} : (filterMap f it).step = do let __do_lift ← it.step match __do_lift.inflate with | ⟨IterStep.yield it' out, h⟩ => match h' : f out with | none => pure (Shrink.deflate (PlausibleIterStep.skip (filterMap f it') ⋯)) | some out' => pure (Shrink.deflate (PlausibleIterStep.yield (filterMap f it') out' ⋯)) | ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (filterMap f it') ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))

theorem Std.IterM.step_map {α β β' : Type w} {m : Type w → Type w'} [Iterator α m β] {it : IterM m β} [Monad m] [LawfulMonad m] {f : β → β'} : (map f it).step = do let __do_lift ← it.step match __do_lift.inflate with | ⟨IterStep.yield it' out, h⟩ => let out' := f out; pure (Shrink.deflate (PlausibleIterStep.yield (map f it') out' ⋯)) | ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (map f it') ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))

theorem Std.IterM.step_filter {α β : Type w} {m : Type w → Type w'} [Iterator α m β] {it : IterM m β} [Monad m] [LawfulMonad m] {f : β → Bool} : (filter f it).step = do let __do_lift ← it.step match __do_lift.inflate with | ⟨IterStep.yield it' out, h⟩ => if h' : f out = true then pure (Shrink.deflate (PlausibleIterStep.yield (filter f it') out ⋯)) else pure (Shrink.deflate (PlausibleIterStep.skip (filter f it') ⋯)) | ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (filter f it') ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))

theorem Std.IterM.InternalConsumers.toList_filterMap {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] {f : β → Option γ} (it : IterM m β) : (filterMap f it).toList = (fun (x : List β) => List.filterMap f x) <$> it.toList

theorem Std.IterM.toList_mapWithPostcondition_eq_toList_filterMapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] {f : β → Iterators.PostconditionT n γ} {it : IterM m β} : (mapWithPostcondition f it).toList = (filterMapWithPostcondition (fun (x : β) => Iterators.PostconditionT.map some (f x)) it).toList

theorem Std.IterM.toList_filterMapM_eq_toList_filterMapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] {f : β → n (Option γ)} {it : IterM m β} : (filterMapM f it).toList = (filterMapWithPostcondition (fun (b : β) => Iterators.PostconditionT.attachLift (f b)) it).toList

theorem Std.IterM.toList_mapM_eq_toList_mapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] {f : β → n γ} {it : IterM m β} : (mapM f it).toList = (mapWithPostcondition (fun (b : β) => Iterators.PostconditionT.attachLift (f b)) it).toList

theorem Std.IterM.toList_mapM_eq_toList_filterMapM {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] {f : β → n γ} {it : IterM m β} : (mapM f it).toList = (filterMapM (fun (b : β) => some <$> f b) it).toList

theorem Std.IterM.toList_map_eq_toList_mapM {α β γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Iterator α m β] [Iterators.Finite α m] {f : β → γ} {it : IterM m β} : (map f it).toList = (mapM (fun (b : β) => pure (f b)) it).toList

theorem Std.IterM.toList_map_eq_toList_filterMapM {α β γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Iterator α m β] [Iterators.Finite α m] {f : β → γ} {it : IterM m β} : (map f it).toList = (filterMapM (fun (b : β) => pure (some (f b))) it).toList

@[simp]

theorem Std.IterM.toList_filterMapWithPostcondition_filterMapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] {f : β → Iterators.PostconditionT n (Option γ)} {g : γ → Iterators.PostconditionT o (Option δ)} {it : IterM m β} : (filterMapWithPostcondition g (filterMapWithPostcondition f it)).toList = (filterMapWithPostcondition (fun (b : β) => do let __do_lift ← liftM (f b) match __do_lift with | none => pure none | some fb => g fb) it).toList

@[simp]

theorem Std.IterM.toList_mapWithPostcondition_mapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] {f : β → Iterators.PostconditionT n γ} {g : γ → Iterators.PostconditionT o δ} {it : IterM m β} : (mapWithPostcondition g (mapWithPostcondition f it)).toList = (mapWithPostcondition (fun (x : β) => liftM (f x) >>= g) it).toList

@[simp]

theorem Std.IterM.toList_filterMapM_filterMapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] {f : β → Iterators.PostconditionT n (Option γ)} {g : γ → o (Option δ)} {it : IterM m β} : (filterMapM g (filterMapWithPostcondition f it)).toList = (filterMapM (fun (b : β) => do let __do_lift ← liftM (f b).run match __do_lift with | none => pure none | some fb => g fb) it).toList

@[simp]

theorem Std.IterM.toList_filterMapM_filterMapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] {f : β → n (Option γ)} {g : γ → o (Option δ)} {it : IterM m β} : (filterMapM g (filterMapM f it)).toList = (filterMapM (fun (b : β) => do let __do_lift ← liftM (f b) match __do_lift with | none => pure none | some fb => g fb) it).toList

@[simp]

theorem Std.IterM.toList_filterMapM_mapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] {f : β → n γ} {g : γ → o (Option δ)} {it : IterM m β} : (filterMapM g (mapM f it)).toList = (filterMapM (fun (b : β) => do let __do_lift ← liftM (f b) g __do_lift) it).toList

@[simp]

theorem Std.IterM.toList_filterMapM_map {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] {f : β → γ} {g : γ → n (Option δ)} {it : IterM m β} : (filterMapM g (map f it)).toList = (filterMapM (fun (b : β) => g (f b)) it).toList

@[simp]

theorem Std.IterM.toList_mapM_filterMapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] {f : β → n (Option γ)} {g : γ → o δ} {it : IterM m β} : (mapM g (filterMapM f it)).toList = (filterMapM (fun (b : β) => do let __do_lift ← liftM (f b) match __do_lift with | none => pure none | some fb => some <$> g fb) it).toList

@[simp]

theorem Std.IterM.toList_mapM_mapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] {f : β → n γ} {g : γ → o δ} {it : IterM m β} : (mapM g (mapM f it)).toList = (mapM (fun (b : β) => do let __do_lift ← liftM (f b) g __do_lift) it).toList

@[simp]

theorem Std.IterM.toList_mapM_map {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] {f : β → γ} {g : γ → n δ} {it : IterM m β} : (mapM g (map f it)).toList = (mapM (fun (b : β) => g (f b)) it).toList

@[simp]

theorem Std.IterM.toList_map_mapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] {f : β → n γ} {g : γ → δ} {it : IterM m β} : (map g (mapM f it)).toList = (mapM (fun (b : β) => do let __do_lift ← f b pure (g __do_lift)) it).toList

@[simp]

theorem Std.IterM.toList_filterMapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α Id β] [Iterators.Finite α Id] {f : β → Iterators.PostconditionT m (Option γ)} (it : IterM Id β) : (filterMapWithPostcondition f it).toList = List.filterMapM (fun (x : β) => (f x).run) it.toList.run

@[simp]

theorem Std.IterM.toList_mapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α Id β] [Iterators.Finite α Id] {f : β → Iterators.PostconditionT m γ} (it : IterM Id β) : (mapWithPostcondition f it).toList = List.mapM (fun (x : β) => (f x).run) it.toList.run

@[simp]

theorem Std.IterM.toList_filterMapM {α β γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Iterator α Id β] [Iterators.Finite α Id] {f : β → m (Option γ)} (it : IterM Id β) : (filterMapM f it).toList = List.filterMapM f it.toList.run

@[simp]

theorem Std.IterM.toList_mapM {α β γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Iterator α Id β] [Iterators.Finite α Id] {f : β → m γ} (it : IterM Id β) : (mapM f it).toList = List.mapM f it.toList.run

@[simp]

theorem Std.IterM.toList_filterMap {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] {f : β → Option γ} (it : IterM m β) : (filterMap f it).toList = (fun (x : List β) => List.filterMap f x) <$> it.toList

@[simp]

theorem Std.IterM.toList_map {α β β' : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] {f : β → β'} (it : IterM m β) : (map f it).toList = (fun (x : List β) => List.map f x) <$> it.toList

@[simp]

theorem Std.IterM.toList_filter {α : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {β : Type w} [Iterator α m β] [Iterators.Finite α m] {f : β → Bool} {it : IterM m β} : (filter f it).toList = List.filter f <$> it.toList

theorem Std.IterM.toListRev_mapWithPostcondition_eq_toListRev_filterMapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] {f : β → Iterators.PostconditionT n γ} {it : IterM m β} : (mapWithPostcondition f it).toListRev = (filterMapWithPostcondition (fun (x : β) => Iterators.PostconditionT.map some (f x)) it).toListRev

theorem Std.IterM.toListRev_filterMapM_eq_toListRev_filterMapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] {f : β → n (Option γ)} {it : IterM m β} : (filterMapM f it).toListRev = (filterMapWithPostcondition (fun (b : β) => Iterators.PostconditionT.attachLift (f b)) it).toListRev

theorem Std.IterM.toListRev_mapM_eq_toListRev_mapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] {f : β → n γ} {it : IterM m β} : (mapM f it).toListRev = (mapWithPostcondition (fun (b : β) => Iterators.PostconditionT.attachLift (f b)) it).toListRev

theorem Std.IterM.toListRev_mapM_eq_toListRev_filterMapM {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] {f : β → n γ} {it : IterM m β} : (mapM f it).toListRev = (filterMapM (fun (b : β) => some <$> f b) it).toListRev

theorem Std.IterM.toListRev_map_eq_toListRev_mapM {α β γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Iterator α m β] [Iterators.Finite α m] {f : β → γ} {it : IterM m β} : (map f it).toListRev = (mapM (fun (b : β) => pure (f b)) it).toListRev

theorem Std.IterM.toListRev_map_eq_toListRev_filterMapM {α β γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Iterator α m β] [Iterators.Finite α m] {f : β → γ} {it : IterM m β} : (map f it).toListRev = (filterMapM (fun (b : β) => pure (some (f b))) it).toListRev

@[simp]

theorem Std.IterM.toListRev_filterMapWithPostcondition_filterMapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] {f : β → Iterators.PostconditionT n (Option γ)} {g : γ → Iterators.PostconditionT o (Option δ)} {it : IterM m β} : (filterMapWithPostcondition g (filterMapWithPostcondition f it)).toListRev = (filterMapWithPostcondition (fun (b : β) => do let __do_lift ← liftM (f b) match __do_lift with | none => pure none | some fb => g fb) it).toListRev

@[simp]

theorem Std.IterM.toListRev_mapWithPostcondition_mapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] {f : β → Iterators.PostconditionT n γ} {g : γ → Iterators.PostconditionT o δ} {it : IterM m β} : (mapWithPostcondition g (mapWithPostcondition f it)).toListRev = (mapWithPostcondition (fun (x : β) => liftM (f x) >>= g) it).toListRev

@[simp]

theorem Std.IterM.toListRev_filterMapM_filterMapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] {f : β → Iterators.PostconditionT n (Option γ)} {g : γ → o (Option δ)} {it : IterM m β} : (filterMapM g (filterMapWithPostcondition f it)).toListRev = (filterMapM (fun (b : β) => do let __do_lift ← liftM (f b).run match __do_lift with | none => pure none | some fb => g fb) it).toListRev

@[simp]

theorem Std.IterM.toListRev_filterMapM_filterMapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] {f : β → n (Option γ)} {g : γ → o (Option δ)} {it : IterM m β} : (filterMapM g (filterMapM f it)).toListRev = (filterMapM (fun (b : β) => do let __do_lift ← liftM (f b) match __do_lift with | none => pure none | some fb => g fb) it).toListRev

@[simp]

theorem Std.IterM.toListRev_filterMapM_mapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] {f : β → n γ} {g : γ → o (Option δ)} {it : IterM m β} : (filterMapM g (mapM f it)).toListRev = (filterMapM (fun (b : β) => do let __do_lift ← liftM (f b) g __do_lift) it).toListRev

@[simp]

theorem Std.IterM.toListRev_filterMapM_map {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] {f : β → γ} {g : γ → n (Option δ)} {it : IterM m β} : (filterMapM g (map f it)).toListRev = (filterMapM (fun (b : β) => g (f b)) it).toListRev

@[simp]

theorem Std.IterM.toListRev_mapM_filterMapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] {f : β → n (Option γ)} {g : γ → o δ} {it : IterM m β} : (mapM g (filterMapM f it)).toListRev = (filterMapM (fun (b : β) => do let __do_lift ← liftM (f b) match __do_lift with | none => pure none | some fb => some <$> g fb) it).toListRev

@[simp]

theorem Std.IterM.toListRev_mapM_mapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] {f : β → n γ} {g : γ → o δ} {it : IterM m β} : (mapM g (mapM f it)).toListRev = (mapM (fun (b : β) => do let __do_lift ← liftM (f b) g __do_lift) it).toListRev

@[simp]

theorem Std.IterM.toListRev_mapM_map {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] {f : β → γ} {g : γ → n δ} {it : IterM m β} : (mapM g (map f it)).toListRev = (mapM (fun (b : β) => g (f b)) it).toListRev

@[simp]

theorem Std.IterM.toListRev_map_mapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] {f : β → n γ} {g : γ → δ} {it : IterM m β} : (map g (mapM f it)).toListRev = (mapM (fun (b : β) => do let __do_lift ← f b pure (g __do_lift)) it).toListRev

@[simp]

theorem Std.IterM.toListRev_filterMapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α Id β] [Iterators.Finite α Id] {f : β → Iterators.PostconditionT m (Option γ)} (it : IterM Id β) : (filterMapWithPostcondition f it).toListRev = List.reverse <$> List.filterMapM (fun (x : β) => (f x).run) it.toList.run

@[simp]

theorem Std.IterM.toListRev_mapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α Id β] [Iterators.Finite α Id] {f : β → Iterators.PostconditionT m γ} (it : IterM Id β) : (mapWithPostcondition f it).toListRev = List.reverse <$> List.mapM (fun (x : β) => (f x).run) it.toList.run

@[simp]

theorem Std.IterM.toListRev_filterMapM {α β γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Iterator α Id β] [Iterators.Finite α Id] {f : β → m (Option γ)} (it : IterM Id β) : (filterMapM f it).toListRev = List.reverse <$> List.filterMapM f it.toList.run

@[simp]

theorem Std.IterM.toListRev_mapM {α β γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Iterator α Id β] [Iterators.Finite α Id] {f : β → m γ} (it : IterM Id β) : (mapM f it).toListRev = List.reverse <$> List.mapM f it.toList.run

@[simp]

theorem Std.IterM.toListRev_filterMap {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] {f : β → Option γ} (it : IterM m β) : (filterMap f it).toListRev = (fun (x : List β) => List.filterMap f x) <$> it.toListRev

@[simp]

theorem Std.IterM.toListRev_map {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] {f : β → γ} (it : IterM m β) : (map f it).toListRev = (fun (x : List β) => List.map f x) <$> it.toListRev

@[simp]

theorem Std.IterM.toListRev_filter {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] {f : β → Bool} {it : IterM m β} : (filter f it).toListRev = List.filter f <$> it.toListRev

theorem Std.IterM.toArray_mapWithPostcondition_eq_toArray_filterMapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] {f : β → Iterators.PostconditionT n γ} {it : IterM m β} : (mapWithPostcondition f it).toArray = (filterMapWithPostcondition (fun (x : β) => Iterators.PostconditionT.map some (f x)) it).toArray

theorem Std.IterM.toArray_filterMapM_eq_toArray_filterMapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] {f : β → n (Option γ)} {it : IterM m β} : (filterMapM f it).toArray = (filterMapWithPostcondition (fun (b : β) => Iterators.PostconditionT.attachLift (f b)) it).toArray

theorem Std.IterM.toArray_mapM_eq_toArray_mapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] {f : β → n γ} {it : IterM m β} : (mapM f it).toArray = (mapWithPostcondition (fun (b : β) => Iterators.PostconditionT.attachLift (f b)) it).toArray

theorem Std.IterM.toArray_mapM_eq_toArray_filterMapM {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] {f : β → n γ} {it : IterM m β} : (mapM f it).toArray = (filterMapM (fun (b : β) => some <$> f b) it).toArray

theorem Std.IterM.toArray_map_eq_toArray_mapM {α β γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Iterator α m β] [Iterators.Finite α m] {f : β → γ} {it : IterM m β} : (map f it).toArray = (mapM (fun (b : β) => pure (f b)) it).toArray

theorem Std.IterM.toArray_map_eq_toArray_filterMapM {α β γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Iterator α m β] [Iterators.Finite α m] {f : β → γ} {it : IterM m β} : (map f it).toArray = (filterMapM (fun (b : β) => pure (some (f b))) it).toArray

@[simp]

theorem Std.IterM.toArray_filterMapWithPostcondition_filterMapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] {f : β → Iterators.PostconditionT n (Option γ)} {g : γ → Iterators.PostconditionT o (Option δ)} {it : IterM m β} : (filterMapWithPostcondition g (filterMapWithPostcondition f it)).toArray = (filterMapWithPostcondition (fun (b : β) => do let __do_lift ← liftM (f b) match __do_lift with | none => pure none | some fb => g fb) it).toArray

@[simp]

theorem Std.IterM.toArray_mapWithPostcondition_mapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] {f : β → Iterators.PostconditionT n γ} {g : γ → Iterators.PostconditionT o δ} {it : IterM m β} : (mapWithPostcondition g (mapWithPostcondition f it)).toArray = (mapWithPostcondition (fun (x : β) => liftM (f x) >>= g) it).toArray

@[simp]

theorem Std.IterM.toArray_filterMapM_filterMapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] {f : β → Iterators.PostconditionT n (Option γ)} {g : γ → o (Option δ)} {it : IterM m β} : (filterMapM g (filterMapWithPostcondition f it)).toArray = (filterMapM (fun (b : β) => do let __do_lift ← liftM (f b).run match __do_lift with | none => pure none | some fb => g fb) it).toArray

@[simp]

theorem Std.IterM.toArray_filterMapM_filterMapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] {f : β → n (Option γ)} {g : γ → o (Option δ)} {it : IterM m β} : (filterMapM g (filterMapM f it)).toArray = (filterMapM (fun (b : β) => do let __do_lift ← liftM (f b) match __do_lift with | none => pure none | some fb => g fb) it).toArray

@[simp]

theorem Std.IterM.toArray_filterMapM_mapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] {f : β → n γ} {g : γ → o (Option δ)} {it : IterM m β} : (filterMapM g (mapM f it)).toArray = (filterMapM (fun (b : β) => do let __do_lift ← liftM (f b) g __do_lift) it).toArray

@[simp]

theorem Std.IterM.toArray_filterMapM_map {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] {f : β → γ} {g : γ → n (Option δ)} {it : IterM m β} : (filterMapM g (map f it)).toArray = (filterMapM (fun (b : β) => g (f b)) it).toArray

@[simp]

theorem Std.IterM.toArray_mapM_filterMapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] {f : β → n (Option γ)} {g : γ → o δ} {it : IterM m β} : (mapM g (filterMapM f it)).toArray = (filterMapM (fun (b : β) => do let __do_lift ← liftM (f b) match __do_lift with | none => pure none | some fb => some <$> g fb) it).toArray

@[simp]

theorem Std.IterM.toArray_mapM_mapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] {f : β → n γ} {g : γ → o δ} {it : IterM m β} : (mapM g (mapM f it)).toArray = (mapM (fun (b : β) => do let __do_lift ← liftM (f b) g __do_lift) it).toArray

@[simp]

theorem Std.IterM.toArray_mapM_map {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] {f : β → γ} {g : γ → n δ} {it : IterM m β} : (mapM g (map f it)).toArray = (mapM (fun (b : β) => g (f b)) it).toArray

@[simp]

theorem Std.IterM.toArray_map_mapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] {f : β → n γ} {g : γ → δ} {it : IterM m β} : (map g (mapM f it)).toArray = (mapM (fun (b : β) => do let __do_lift ← f b pure (g __do_lift)) it).toArray

@[simp]

theorem Std.IterM.toArray_filterMapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α Id β] [Iterators.Finite α Id] {f : β → Iterators.PostconditionT m (Option γ)} (it : IterM Id β) : (filterMapWithPostcondition f it).toArray = Array.filterMapM (fun (x : β) => (f x).run) it.toArray.run

@[simp]

theorem Std.IterM.toArray_mapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α Id β] [Iterators.Finite α Id] {f : β → Iterators.PostconditionT m γ} (it : IterM Id β) : (mapWithPostcondition f it).toArray = Array.mapM (fun (x : β) => (f x).run) it.toArray.run

@[simp]

theorem Std.IterM.toArray_filterMapM {α β γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Iterator α Id β] [Iterators.Finite α Id] {f : β → m (Option γ)} (it : IterM Id β) : (filterMapM f it).toArray = Array.filterMapM f it.toArray.run

@[simp]

theorem Std.IterM.toArray_mapM {α β γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Iterator α Id β] [Iterators.Finite α Id] {f : β → m γ} (it : IterM Id β) : (mapM f it).toArray = Array.mapM f it.toArray.run

@[simp]

theorem Std.IterM.toArray_filterMap {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] {f : β → Option γ} (it : IterM m β) : (filterMap f it).toArray = (fun (x : Array β) => Array.filterMap f x) <$> it.toArray

@[simp]

theorem Std.IterM.toArray_map {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] {f : β → γ} (it : IterM m β) : (map f it).toArray = (fun (x : Array β) => Array.map f x) <$> it.toArray

@[simp]

theorem Std.IterM.toArray_filter {α : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {β : Type w} [Iterator α m β] [Iterators.Finite α m] {f : β → Bool} {it : IterM m β} : (filter f it).toArray = (fun (as : Array β) => Array.filter f as) <$> it.toArray

theorem Std.IterM.forIn_filterMapWithPostcondition {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {o : Type u_1 → Type u_4} {α β β₂ γ : Type u_1} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m o] [LawfulIteratorLoop α m o] {it : IterM m β} {f : β → Iterators.PostconditionT n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)} : forIn (filterMapWithPostcondition f it) init g = forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out).run match __do_lift with | some c => g c acc | none => pure (ForInStep.yield acc)

theorem Std.IterM.forIn_filterMapM {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {o : Type u_1 → Type u_4} {α β β₂ γ : Type u_1} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [MonadAttach n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m o] [LawfulIteratorLoop α m o] {it : IterM m β} {f : β → n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)} : forIn (filterMapM f it) init g = forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out) match __do_lift with | some c => g c acc | none => pure (ForInStep.yield acc)

theorem Std.IterM.forIn_filterMap {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α β β₂ γ : Type u_1} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m n] [LawfulIteratorLoop α m n] {it : IterM m β} {f : β → Option β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} : forIn (filterMap f it) init g = forIn it init fun (out : β) (acc : γ) => match f out with | some c => g c acc | none => pure (ForInStep.yield acc)

theorem Std.IterM.forIn_mapWithPostcondition {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {o : Type u_1 → Type u_4} {α β β₂ γ : Type u_1} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m o] [LawfulIteratorLoop α m o] {it : IterM m β} {f : β → Iterators.PostconditionT n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)} : forIn (mapWithPostcondition f it) init g = forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out).run g __do_lift acc

theorem Std.IterM.forIn_mapM {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {o : Type u_1 → Type u_4} {α β β₂ γ : Type u_1} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [MonadAttach n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m o] [LawfulIteratorLoop α m o] {it : IterM m β} {f : β → n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)} : forIn (mapM f it) init g = forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out) g __do_lift acc

theorem Std.IterM.forIn_map {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α β β₂ γ : Type u_1} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m n] [LawfulIteratorLoop α m n] {it : IterM m β} {f : β → β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} : forIn (map f it) init g = forIn it init fun (out : β) (acc : γ) => g (f out) acc

theorem Std.IterM.forIn_filterWithPostcondition {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {o : Type u_1 → Type u_4} {α β γ : Type u_1} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m o] [LawfulIteratorLoop α m o] {it : IterM m β} {f : β → Iterators.PostconditionT n (ULift Bool)} {init : γ} {g : β → γ → o (ForInStep γ)} : forIn (filterWithPostcondition f it) init g = forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out).run if __do_lift.down = true then g out acc else pure (ForInStep.yield acc)

theorem Std.IterM.forIn_filterM {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {o : Type u_1 → Type u_4} {α β γ : Type u_1} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [MonadAttach n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m o] [LawfulIteratorLoop α m o] {it : IterM m β} {f : β → n (ULift Bool)} {init : γ} {g : β → γ → o (ForInStep γ)} : forIn (filterM f it) init g = forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out) if __do_lift.down = true then g out acc else pure (ForInStep.yield acc)

theorem Std.IterM.forIn_filter {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α β γ : Type u_1} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m n] [LawfulIteratorLoop α m n] {it : IterM m β} {f : β → Bool} {init : γ} {g : β → γ → n (ForInStep γ)} : forIn (filter f it) init g = forIn it init fun (out : β) (acc : γ) => if f out = true then g out acc else pure (ForInStep.yield acc)

theorem Std.IterM.foldM_filterMapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Iterator α m β] [Iterators.Finite α m] [Monad m] [Monad n] [Monad o] [LawfulMonad m] [LawfulMonad n] [LawfulMonad o] [IteratorLoop α m n] [IteratorLoop α m o] [LawfulIteratorLoop α m n] [LawfulIteratorLoop α m o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] {f : β → Iterators.PostconditionT n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : IterM m β} : foldM g init (filterMapWithPostcondition f it) = foldM (fun (d : δ) (b : β) => do let __discr ← liftM (f b).run match __discr with | some c => g d c | x => pure d) init it

theorem Std.IterM.foldM_filterMapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [LawfulMonad o] [IteratorLoop α m n] [IteratorLoop α m o] [LawfulIteratorLoop α m n] [LawfulIteratorLoop α m o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] {f : β → n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : IterM m β} : foldM g init (filterMapM f it) = foldM (fun (d : δ) (b : β) => do let __discr ← liftM (f b) match __discr with | some c => g d c | x => pure d) init it

theorem Std.IterM.foldM_mapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Iterator α m β] [Iterators.Finite α m] [Monad m] [Monad n] [Monad o] [LawfulMonad m] [LawfulMonad n] [LawfulMonad o] [IteratorLoop α m n] [IteratorLoop α m o] [LawfulIteratorLoop α m n] [LawfulIteratorLoop α m o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] {f : β → Iterators.PostconditionT n γ} {g : δ → γ → o δ} {init : δ} {it : IterM m β} : foldM g init (mapWithPostcondition f it) = foldM (fun (d : δ) (b : β) => do let c ← liftM (f b).run g d c) init it

theorem Std.IterM.foldM_mapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [LawfulMonad o] [IteratorLoop α m n] [IteratorLoop α m o] [LawfulIteratorLoop α m n] [LawfulIteratorLoop α m o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] {f : β → n γ} {g : δ → γ → o δ} {init : δ} {it : IterM m β} : foldM g init (mapM f it) = foldM (fun (d : δ) (b : β) => do let c ← liftM (f b) g d c) init it

theorem Std.IterM.foldM_filterWithPostcondition {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Iterator α m β] [Iterators.Finite α m] [Monad m] [Monad n] [Monad o] [LawfulMonad m] [LawfulMonad n] [LawfulMonad o] [IteratorLoop α m n] [IteratorLoop α m o] [LawfulIteratorLoop α m n] [LawfulIteratorLoop α m o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] {f : β → Iterators.PostconditionT n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : IterM m β} : foldM g init (filterWithPostcondition f it) = foldM (fun (d : δ) (b : β) => do let __do_lift ← liftM (f b).run if __do_lift.down = true then g d b else pure d) init it

theorem Std.IterM.foldM_filterM {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [LawfulMonad o] [IteratorLoop α m n] [IteratorLoop α m o] [LawfulIteratorLoop α m n] [LawfulIteratorLoop α m o] [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] {f : β → n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : IterM m β} : foldM g init (filterM f it) = foldM (fun (d : δ) (b : β) => do let __do_lift ← liftM (f b) if __do_lift.down = true then g d b else pure d) init it

theorem Std.IterM.foldM_filterMap {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Iterators.Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Option γ} {g : δ → γ → n δ} {init : δ} {it : IterM m β} : foldM g init (filterMap f it) = foldM (fun (d : δ) (b : β) => match f b with | some c => g d c | x => pure d) init it

theorem Std.IterM.foldM_map {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Iterators.Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → γ} {g : δ → γ → n δ} {init : δ} {it : IterM m β} : foldM g init (map f it) = foldM (fun (d : δ) (b : β) => g d (f b)) init it

theorem Std.IterM.foldM_filter {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Iterators.Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Bool} {g : δ → β → n δ} {init : δ} {it : IterM m β} : foldM g init (filter f it) = foldM (fun (d : δ) (b : β) => if f b = true then g d b else pure d) init it

theorem Std.IterM.fold_filterMapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Iterators.PostconditionT n (Option γ)} {g : δ → γ → δ} {init : δ} {it : IterM m β} : fold g init (filterMapWithPostcondition f it) = foldM (fun (d : δ) (b : β) => do let __discr ← (f b).run match __discr with | some c => pure (g d c) | x => pure d) init it

theorem Std.IterM.fold_filterMapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n (Option γ)} {g : δ → γ → δ} {init : δ} {it : IterM m β} : fold g init (filterMapM f it) = foldM (fun (d : δ) (b : β) => do let __discr ← f b match __discr with | some c => pure (g d c) | x => pure d) init it

theorem Std.IterM.fold_mapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Iterators.PostconditionT n γ} {g : δ → γ → δ} {init : δ} {it : IterM m β} : fold g init (mapWithPostcondition f it) = foldM (fun (d : δ) (b : β) => do let c ← (f b).run pure (g d c)) init it

theorem Std.IterM.fold_mapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n γ} {g : δ → γ → δ} {init : δ} {it : IterM m β} : fold g init (mapM f it) = foldM (fun (d : δ) (b : β) => do let c ← f b pure (g d c)) init it

theorem Std.IterM.fold_filterWithPostcondition {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Iterators.PostconditionT n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : IterM m β} : fold g init (filterWithPostcondition f it) = foldM (fun (d : δ) (b : β) => do let __do_lift ← (f b).run pure (if __do_lift.down = true then g d b else d)) init it

theorem Std.IterM.fold_filterM {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : IterM m β} : fold g init (filterM f it) = foldM (fun (d : δ) (b : β) => do let __do_lift ← f b pure (if __do_lift.down = true then g d b else d)) init it

theorem Std.IterM.fold_filterMap {α β γ δ : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {f : β → Option γ} {g : δ → γ → δ} {init : δ} {it : IterM m β} : fold g init (filterMap f it) = fold (fun (d : δ) (b : β) => match f b with | some c => g d c | x => d) init it

theorem Std.IterM.fold_map {α β γ δ : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {f : β → γ} {g : δ → γ → δ} {init : δ} {it : IterM m β} : fold g init (map f it) = fold (fun (d : δ) (b : β) => g d (f b)) init it

theorem Std.IterM.fold_filter {α β δ : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {f : β → Bool} {g : δ → β → δ} {init : δ} {it : IterM m β} : fold g init (filter f it) = fold (fun (d : δ) (b : β) => if f b = true then g d b else d) init it

@[simp]

theorem Std.IterM.count_map {α β β' : Type w} {m : Type w → Type w'} [Iterator α m β] [Monad m] [IteratorLoop α m m] [Iterators.Finite α m] [LawfulMonad m] [LawfulIteratorLoop α m m] {it : IterM m β} {f : β → β'} : (map f it).count = it.count

theorem Std.IterM.anyM_filterMapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Iterators.Finite α m] [MonadLiftT m n] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] {it : IterM m β} {f : β → n (Option β')} {p : β' → n (ULift Bool)} : anyM p (filterMapM f it) = anyM (fun (x : β) => do let __do_lift ← f x match __do_lift with | some fx => p fx | none => pure { down := false }) (mapM pure it)

theorem Std.IterM.anyM_mapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Iterators.Finite α m] [MonadLiftT m n] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] {it : IterM m β} {f : β → n β'} {p : β' → n (ULift Bool)} : anyM p (mapM f it) = anyM (fun (x : β) => do let __do_lift ← f x p __do_lift) (mapM pure it)

theorem Std.IterM.anyM_filterM {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Iterators.Finite α m] [MonadLiftT m n] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] {it : IterM m β} {f p : β → n (ULift Bool)} : anyM p (filterM f it) = anyM (fun (x : β) => do let __do_lift ← f x if __do_lift.down = true then p x else pure { down := false }) (mapM pure it)

theorem Std.IterM.anyM_filterMap {α β β' : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [IteratorLoop α m m] [LawfulMonad m] [LawfulIteratorLoop α m m] {it : IterM m β} {f : β → Option β'} {p : β' → m (ULift Bool)} : anyM p (filterMap f it) = anyM (fun (x : β) => match f x with | some fx => p fx | none => pure { down := false }) it

theorem Std.IterM.anyM_map {α β β' : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [IteratorLoop α m m] [LawfulMonad m] [LawfulIteratorLoop α m m] {it : IterM m β} {f : β → β'} {p : β' → m (ULift Bool)} : anyM p (map f it) = anyM (fun (x : β) => p (f x)) it

theorem Std.IterM.anyM_filter {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [IteratorLoop α m m] [LawfulMonad m] [LawfulIteratorLoop α m m] {it : IterM m β} {f : β → Bool} {p : β → m (ULift Bool)} : anyM p (filter f it) = anyM (fun (x : β) => if f x = true then p x else pure { down := false }) it

theorem Std.IterM.any_filterMapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Iterators.Finite α m] [MonadLiftT m n] [IteratorLoop α m m] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [LawfulMonadLiftT m n] [LawfulIteratorLoop α m m] {it : IterM m β} {f : β → n (Option β')} {p : β' → Bool} : any p (filterMapM f it) = anyM (fun (x : β) => do let __do_lift ← f x match __do_lift with | some fx => pure { down := p fx } | none => pure { down := false }) (mapM pure it)

theorem Std.IterM.any_mapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Iterators.Finite α m] [MonadLiftT m n] [IteratorLoop α m m] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [LawfulMonadLiftT m n] [LawfulIteratorLoop α m m] {it : IterM m β} {f : β → n β'} {p : β' → Bool} : any p (mapM f it) = anyM (fun (x : β) => (fun (x : β') => { down := p x }) <$> f x) (mapM pure it)

theorem Std.IterM.any_filterM {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Iterators.Finite α m] [MonadLiftT m n] [IteratorLoop α m m] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [LawfulMonadLiftT m n] [LawfulIteratorLoop α m m] {it : IterM m β} {f : β → n (ULift Bool)} {p : β → Bool} : any p (filterM f it) = anyM (fun (x : β) => do let __do_lift ← f x if __do_lift.down = true then pure { down := p x } else pure { down := false }) (mapM pure it)

theorem Std.IterM.any_filterMap {α β β' : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [IteratorLoop α m m] [LawfulMonad m] [LawfulIteratorLoop α m m] {it : IterM m β} {f : β → Option β'} {p : β' → Bool} : any p (filterMap f it) = any (fun (x : β) => match f x with | some fx => p fx | none => false) it

theorem Std.IterM.any_map {α β β' : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [IteratorLoop α m m] [LawfulMonad m] [LawfulIteratorLoop α m m] {it : IterM m β} {f : β → β'} {p : β' → Bool} : any p (map f it) = any (fun (x : β) => p (f x)) it

theorem Std.IterM.allM_filterMapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Iterators.Finite α m] [MonadLiftT m n] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [LawfulMonadLiftT m n] {it : IterM m β} {f : β → n (Option β')} {p : β' → n (ULift Bool)} : allM p (filterMapM f it) = allM (fun (x : β) => do let __do_lift ← f x match __do_lift with | some fx => p fx | none => pure { down := true }) (mapM pure it)

theorem Std.IterM.allM_mapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Iterators.Finite α m] [MonadLiftT m n] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [LawfulMonadLiftT m n] {it : IterM m β} {f : β → n β'} {p : β' → n (ULift Bool)} : allM p (mapM f it) = allM (fun (x : β) => do let __do_lift ← f x p __do_lift) (mapM pure it)

theorem Std.IterM.allM_filterM {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Iterators.Finite α m] [MonadLiftT m n] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [LawfulMonadLiftT m n] {it : IterM m β} {f p : β → n (ULift Bool)} : allM p (filterM f it) = allM (fun (x : β) => do let __do_lift ← f x if __do_lift.down = true then p x else pure { down := true }) (mapM pure it)

theorem Std.IterM.allM_filterMap {α β β' : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [IteratorLoop α m m] [LawfulMonad m] [LawfulIteratorLoop α m m] {it : IterM m β} {f : β → Option β'} {p : β' → m (ULift Bool)} : allM p (filterMap f it) = allM (fun (x : β) => match f x with | some fx => p fx | none => pure { down := true }) it

theorem Std.IterM.allM_map {α β β' : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [IteratorLoop α m m] [LawfulMonad m] [LawfulIteratorLoop α m m] {it : IterM m β} {f : β → β'} {p : β' → m (ULift Bool)} : allM p (map f it) = allM (fun (x : β) => p (f x)) it

theorem Std.IterM.allM_filter {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [IteratorLoop α m m] [LawfulMonad m] [LawfulIteratorLoop α m m] {it : IterM m β} {f : β → Bool} {p : β → m (ULift Bool)} : allM p (filter f it) = allM (fun (x : β) => if f x = true then p x else pure { down := true }) it

theorem Std.IterM.all_filterMapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Iterators.Finite α m] [MonadLiftT m n] [IteratorLoop α m m] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [LawfulMonadLiftT m n] [LawfulIteratorLoop α m m] {it : IterM m β} {f : β → n (Option β')} {p : β' → Bool} : all p (filterMapM f it) = allM (fun (x : β) => do let __do_lift ← f x match __do_lift with | some fx => pure { down := p fx } | none => pure { down := true }) (mapM pure it)

theorem Std.IterM.all_mapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Iterators.Finite α m] [MonadLiftT m n] [IteratorLoop α m m] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [LawfulMonadLiftT m n] [LawfulIteratorLoop α m m] {it : IterM m β} {f : β → n β'} {p : β' → Bool} : all p (mapM f it) = allM (fun (x : β) => (fun (x : β') => { down := p x }) <$> f x) (mapM pure it)

theorem Std.IterM.all_filterM {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Iterators.Finite α m] [MonadLiftT m n] [IteratorLoop α m m] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [LawfulMonadLiftT m n] [LawfulIteratorLoop α m m] {it : IterM m β} {f : β → n (ULift Bool)} {p : β → Bool} : all p (filterM f it) = allM (fun (x : β) => do let __do_lift ← f x if __do_lift.down = true then pure { down := p x } else pure { down := true }) (mapM pure it)

theorem Std.IterM.all_filterMap {α β β' : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [IteratorLoop α m m] [LawfulMonad m] [LawfulIteratorLoop α m m] {it : IterM m β} {f : β → Option β'} {p : β' → Bool} : all p (filterMap f it) = all (fun (x : β) => match f x with | some fx => p fx | none => true) it

theorem Std.IterM.all_map {α β β' : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [IteratorLoop α m m] [LawfulMonad m] [LawfulIteratorLoop α m m] {it : IterM m β} {f : β → β'} {p : β' → Bool} : all p (map f it) = all (fun (x : β) => p (f x)) it