theorem Std.Iterators.IterM.step_attachWith {α : Type w} {m : Type w → Type w'} {β : Type w} {P : β → Prop} [Iterator α m β] [Monad m] {it : IterM m β} {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} : (it.attachWith P hP).step = (fun (s : it.Step) => ⟨Types.Attach.Monadic.modifyStep (it.attachWith P hP) s, ⋯⟩) <$> it.step

@[simp]

theorem Std.Iterators.IterM.map_unattach_toList_attachWith {α : Type w} {m : Type w → Type w'} {β : Type w} {P : β → Prop} [Iterator α m β] [Monad m] {it : IterM m β} {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [Finite α m] [IteratorCollect α m m] [LawfulMonad m] [LawfulIteratorCollect α m m] : List.unattach <$> (it.attachWith P hP).toList = it.toList

@[simp]

theorem Std.Iterators.IterM.map_unattach_toListRev_attachWith {α : Type w} {m : Type w → Type w'} {β : Type w} {P : β → Prop} {n : Type u_1 → Type u_2} [Iterator α m β] [Monad m] [Monad n] {it : IterM m β} {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [Finite α m] [IteratorCollect α m m] [LawfulMonad m] [LawfulIteratorCollect α m m] : List.unattach <$> (it.attachWith P hP).toListRev = it.toListRev

@[simp]

theorem Std.Iterators.IterM.map_unattach_toArray_attachWith {α : Type w} {m : Type w → Type w'} {β : Type w} {P : β → Prop} {n : Type u_1 → Type u_2} [Iterator α m β] [Monad m] [Monad n] {it : IterM m β} {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [Finite α m] [IteratorCollect α m m] [LawfulMonad m] [LawfulIteratorCollect α m m] : (fun (x : Array { out : β // P out }) => Array.map Subtype.val x) <$> (it.attachWith P hP).toArray = it.toArray