theorem Std.IterM.toHashSet_eq_fold {α β : Type w} {x✝ : BEq β} {x✝¹ : Hashable β} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] {it : IterM m β} : it.toHashSet = fold (fun (acc : HashSet β) (a : β) => acc.insert a) ∅ it

@[simp]

theorem Std.IterM.toExtHashSet_eq_ofList {α β : Type w} {x✝ : BEq β} {x✝¹ : Hashable β} [EquivBEq β] [LawfulHashable β] {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} : it.toExtHashSet = ExtHashSet.ofList <$> it.toList

theorem Std.IterM.toTreeSet_eq_fold {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] {it : IterM m β} {cmp : β → β → Ordering} : it.toTreeSet cmp = fold (fun (acc : TreeSet β cmp) (a : β) => acc.insert a) ∅ it

@[simp]

theorem Std.IterM.toExtTreeSet_eq_ofList {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {cmp : β → β → Ordering} [TransCmp cmp] : it.toExtTreeSet cmp = (fun (x : List β) => ExtTreeSet.ofList x cmp) <$> it.toList