theorem Std.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.Iter.unattach_toList_attachWith {α β : Type u_1} {P : β → Prop} [Iterator α Id β] {it : Iter β} {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [Iterators.Finite α Id] : (it.attachWith P hP).toList.unattach = it.toList

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Std.Iter.length_attachWith {α β : Type u_1} {P : β → Prop} [Iterator α Id β] {it : Iter β} {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] : (it.attachWith P hP).length = it.length

@[deprecated Std.Iter.length_attachWith (since := "2026-01-28")]

def Std.Iter.count_attachWith {α β : Type u_1} {P : β → Prop} [Iterator α Id β] {it : Iter β} {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] : (it.attachWith P hP).length = it.length

Equations

• @Std.Iter.count_attachWith = @Std.Iter.length_attachWith