theorem Std.Iter.toHashSet_equiv_ofList {α β : Type w} {x✝ : BEq β} {x✝¹ : Hashable β} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} : it.toHashSet.Equiv (HashSet.ofList it.toList)

@[simp]

theorem Std.Iter.toExtHashSet_eq_ofList {α β : Type w} {x✝ : BEq β} {x✝¹ : Hashable β} [EquivBEq β] [LawfulHashable β] [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} : it.toExtHashSet = ExtHashSet.ofList it.toList

theorem Std.Iter.toTreeSet_equiv_ofList {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} {cmp : β → β → Ordering} : (it.toTreeSet cmp).Equiv (TreeSet.ofList it.toList cmp)

@[simp]

theorem Std.Iter.toExtTreeSet_eq_ofList {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} {cmp : β → β → Ordering} [TransCmp cmp] : it.toExtTreeSet cmp = ExtTreeSet.ofList it.toList cmp