theorem Std.Iterators.Iter.unattach_eq_toIter_unattach_toIterM {α β : Type u_1} {P : β → Prop} [Iterator α Id β] {it : Iter β} {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} : it.attachWith P hP = (it.toIterM.attachWith P ⋯).toIter

theorem Std.Iterators.Iter.unattach_toList_attachWith {α β : Type u_1} {P : β → Prop} [Iterator α Id β] {it : Iter β} {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] : (it.attachWith P hP).toList.unattach = it.toList

@[simp]

theorem Std.Iterators.Iter.toList_attachWith {α β : Type u_1} {P : β → Prop} [Iterator α Id β] {it : Iter β} {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] : (it.attachWith P hP).toList = it.toList.attachWith P ⋯

theorem Std.Iterators.Iter.unattach_toListRev_attachWith {α β : Type u_1} {P : β → Prop} [Iterator α Id β] {it : Iter β} {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] : (it.attachWith P hP).toListRev.unattach = it.toListRev

@[simp]

theorem Std.Iterators.Iter.toListRev_attachWith {α β : Type u_1} {P : β → Prop} [Iterator α Id β] {it : Iter β} {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] : (it.attachWith P hP).toListRev = it.toListRev.attachWith P ⋯

@[simp]

theorem Std.Iterators.Iter.unattach_toArray_attachWith {α β : Type u_1} {P : β → Prop} [Iterator α Id β] {it : Iter β} {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] : (it.attachWith P hP).toListRev.unattach = it.toListRev