diff --git a/src/Std/Data/Iterators.lean b/src/Std/Data/Iterators.lean
index cb4bbcf0ce..7531c9666d 100644
--- a/src/Std/Data/Iterators.lean
+++ b/src/Std/Data/Iterators.lean
@@ -10,6 +10,7 @@ public import Init.Data.Iterators.Internal
 public import Std.Data.Iterators.Producers
 public import Std.Data.Iterators.Combinators
 public import Std.Data.Iterators.Lemmas
+public import Std.Data.Iterators.Consumers
 
 @[expose] public section
 
diff --git a/src/Std/Data/Iterators/Consumers.lean b/src/Std/Data/Iterators/Consumers.lean
new file mode 100644
index 0000000000..54f056a04e
--- /dev/null
+++ b/src/Std/Data/Iterators/Consumers.lean
@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Std.Data.Iterators.Consumers.Monadic
+public import Std.Data.Iterators.Consumers.Set
diff --git a/src/Std/Data/Iterators/Consumers/Monadic.lean b/src/Std/Data/Iterators/Consumers/Monadic.lean
new file mode 100644
index 0000000000..ae23a669ea
--- /dev/null
+++ b/src/Std/Data/Iterators/Consumers/Monadic.lean
@@ -0,0 +1,9 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Std.Data.Iterators.Consumers.Monadic.Set
diff --git a/src/Std/Data/Iterators/Consumers/Monadic/Set.lean b/src/Std/Data/Iterators/Consumers/Monadic/Set.lean
new file mode 100644
index 0000000000..96f6fda8c1
--- /dev/null
+++ b/src/Std/Data/Iterators/Consumers/Monadic/Set.lean
@@ -0,0 +1,141 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.Iterators.Consumers.Monadic.Loop
+public import Std.Data.HashSet.Basic
+public import Std.Data.ExtHashSet.Basic
+public import Std.Data.TreeSet.Basic
+public import Std.Data.ExtTreeSet.Basic
+import Init.Data.Iterators.Consumers.Monadic.Loop
+
+set_option doc.verso true
+
+namespace Std
+open Iterators
+
+set_option doc.verso false
+
+/--
+Traverses the given iterator and stores the emitted values in a {name}`HashSet`.
+
+If the iterator is not finite, this function might run forever. Given {givenInstance}`Finite α m`,
+the variant {lean}`it.ensureTermination.toHashSet` always terminates after finitely many steps.
+-/
+@[inline]
+public def IterM.toHashSet {α β : Type w} [BEq β] [Hashable β] {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [IteratorLoop α m m] (it : IterM (α := α) m β) : m (HashSet β) :=
+  it.fold (init := ∅) fun acc a => acc.insert a
+
+set_option doc.verso true
+
+/--
+Traverses the given iterator and stores the emitted values in a {name}`HashSet`.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using {name}`IterM.toHashSet`.
+-/
+@[inline]
+public def IterM.Total.toHashSet {α β : Type w} [BEq β] [Hashable β] {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [Finite α m] [IteratorLoop α m m] (it : IterM.Total (α := α) m β) :
+    m (HashSet β) :=
+  it.it.toHashSet
+
+docs_to_verso IterM.toHashSet
+
+set_option doc.verso false
+
+/--
+Traverses the given iterator and stores the emitted values in a {name}`ExtHashSet`.
+
+If the iterator is not finite, this function might run forever. Given {givenInstance}`Finite α m`,
+the variant {lean}`it.ensureTermination.toExtHashSet` always terminates after finitely many steps.
+-/
+@[inline]
+public def IterM.toExtHashSet {α β : Type w} [BEq β] [Hashable β] [EquivBEq β] [LawfulHashable β]
+    {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m]
+    (it : IterM (α := α) m β) : m (ExtHashSet β) :=
+  it.fold (init := ∅) fun acc a => acc.insert a
+
+set_option doc.verso true
+
+/--
+Traverses the given iterator and stores the emitted values in a {name}`ExtHashSet`.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using {name}`IterM.toExtHashSet`.
+-/
+@[inline]
+public def IterM.Total.toExtHashSet {α β : Type w} [BEq β] [Hashable β] [EquivBEq β] [LawfulHashable β]
+    {m : Type w → Type w'} [Monad m] [Iterator α m β] [Finite α m] [IteratorLoop α m m]
+    (it : IterM.Total (α := α) m β) : m (ExtHashSet β) :=
+  it.it.toExtHashSet
+
+docs_to_verso IterM.toExtHashSet
+
+set_option doc.verso false
+
+/--
+Traverses the given iterator and stores the emitted values in a {name}`TreeSet`.
+
+If the iterator is not finite, this function might run forever. Given {givenInstance}`Finite α m`,
+the variant {lean}`it.ensureTermination.toTreeSet` always terminates after finitely many steps.
+-/
+@[inline]
+public def IterM.toTreeSet {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [IteratorLoop α m m] (it : IterM (α := α) m β) (cmp : β → β → Ordering) :
+    m (TreeSet β cmp) :=
+  it.fold (init := ∅) fun acc a => acc.insert a
+
+set_option doc.verso true
+
+/--
+Traverses the given iterator and stores the emitted values in a {name}`TreeSet`.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using {name}`IterM.toTreeSet`.
+-/
+@[inline]
+public def IterM.Total.toTreeSet {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [Finite α m] [IteratorLoop α m m] (it : IterM.Total (α := α) m β)
+    (cmp : β → β → Ordering) : m (TreeSet β cmp) :=
+  it.it.toTreeSet cmp
+
+docs_to_verso IterM.toTreeSet
+
+set_option doc.verso false
+
+/--
+Traverses the given iterator and stores the emitted values in a {name}`ExtTreeSet`.
+
+If the iterator is not finite, this function might run forever. Given {givenInstance}`Finite α m`,
+the variant {lean}`it.ensureTermination.toExtTreeSet cmp` always terminates after finitely
+many steps.
+-/
+@[inline]
+public def IterM.toExtTreeSet {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
+    [IteratorLoop α m m] (it : IterM (α := α) m β) (cmp : β → β → Ordering := by exact compare)
+    [TransCmp cmp] : m (ExtTreeSet β cmp) :=
+  it.fold (init := ∅) fun acc a => acc.insert a
+
+set_option doc.verso true
+
+/--
+Traverses the given iterator and stores the emitted values in a {name}`ExtTreeSet`.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using {name}`IterM.toExtTreeSet`.
+-/
+@[inline]
+public def IterM.Total.toExtTreeSet {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
+    [Finite α m] [IteratorLoop α m m] (it : IterM.Total (α := α) m β)
+    (cmp : β → β → Ordering := by exact compare) [TransCmp cmp] : m (ExtTreeSet β cmp) :=
+  it.it.toExtTreeSet cmp
+
+docs_to_verso IterM.toExtTreeSet
+
+end Std
diff --git a/src/Std/Data/Iterators/Consumers/Set.lean b/src/Std/Data/Iterators/Consumers/Set.lean
new file mode 100644
index 0000000000..87d16cdcb8
--- /dev/null
+++ b/src/Std/Data/Iterators/Consumers/Set.lean
@@ -0,0 +1,133 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Std.Data.Iterators.Consumers.Monadic.Set
+public import Init.Data.Iterators.Consumers.Total
+
+set_option doc.verso true
+
+namespace Std
+open Iterators
+
+set_option doc.verso false
+
+/--
+Traverses the given iterator and stores the emitted values in a {name}`HashSet`.
+
+If the iterator is not finite, this function might run forever. Given {givenInstance}`Finite α Id`,
+the variant {lean}`it.ensureTermination.toHashSet` always terminates after finitely many steps.
+-/
+@[inline]
+public def Iter.toHashSet {α β : Type w} [BEq β] [Hashable β] [Iterator α Id β]
+    [IteratorLoop α Id Id] (it : Iter (α := α) β) : HashSet β :=
+  it.toIterM.toHashSet.run
+
+set_option doc.verso true
+
+/--
+Traverses the given iterator and stores the emitted values in a {name}`HashSet`.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using {name}`Iter.toHashSet`.
+-/
+@[inline]
+public def Iter.Total.toHashSet {α β : Type w} [BEq β] [Hashable β] [Iterator α Id β] [Finite α Id]
+    [IteratorLoop α Id Id] (it : Total (α := α) β) : HashSet β :=
+  it.it.toHashSet
+
+docs_to_verso Iter.toHashSet
+
+set_option doc.verso false
+
+/--
+Traverses the given iterator and stores the emitted values in a {name}`ExtHashSet`.
+
+If the iterator is not finite, this function might run forever. Given {givenInstance}`Finite α Id`,
+the variant {lean}`it.ensureTermination.toExtHashSet` always terminates after finitely many steps.
+-/
+@[inline]
+public def Iter.toExtHashSet {α β : Type w} [BEq β] [Hashable β] [EquivBEq β] [LawfulHashable β]
+    [Iterator α Id β] [IteratorLoop α Id Id] (it : Iter (α := α) β) : ExtHashSet β :=
+  it.toIterM.toExtHashSet.run
+
+set_option doc.verso true
+
+/--
+Traverses the given iterator and stores the emitted values in a {name}`ExtHashSet`.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using {name}`Iter.toExtHashSet`.
+-/
+@[inline]
+public def Iter.Total.toExtHashSet {α β : Type w} [BEq β] [Hashable β] [EquivBEq β]
+    [LawfulHashable β] [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id]
+    (it : Total (α := α) β) : ExtHashSet β :=
+  it.it.toExtHashSet
+
+docs_to_verso Iter.toExtHashSet
+
+set_option doc.verso false
+
+/--
+Traverses the given iterator and stores the emitted values in a {name}`TreeSet`.
+
+If the iterator is not finite, this function might run forever. Given {givenInstance}`Finite α Id`,
+the variant {lean}`it.ensureTermination.toTreeSet cmp` always terminates after finitely many steps.
+-/
+@[inline]
+public def Iter.toTreeSet {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
+    (it : Iter (α := α) β) (cmp : β → β → Ordering := by exact compare) : TreeSet β cmp :=
+  it.toIterM.toTreeSet cmp |>.run
+
+set_option doc.verso true
+
+/--
+Traverses the given iterator and stores the emitted values in a {name}`TreeSet`.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using {name}`Iter.toTreeSet`.
+-/
+@[inline]
+public def Iter.Total.toTreeSet {α β : Type w} [Iterator α Id β] [Finite α Id]
+    [IteratorLoop α Id Id] (it : Total (α := α) β) (cmp : β → β → Ordering := by exact compare) :
+    TreeSet β cmp :=
+  it.it.toTreeSet cmp
+
+docs_to_verso Iter.toTreeSet
+
+set_option doc.verso false
+
+/--
+Traverses the given iterator and stores the emitted values in a {name}`ExtTreeSet`.
+
+If the iterator is not finite, this function might run forever. Given {givenInstance}`Finite α Id`,
+the variant {lean}`it.ensureTermination.toExtTreeSet cmp` always terminates after finitely many steps.
+-/
+@[inline]
+public def Iter.toExtTreeSet {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
+    (it : Iter (α := α) β) (cmp : β → β → Ordering := by exact compare) [TransCmp cmp] :
+    ExtTreeSet β cmp :=
+  it.toIterM.toExtTreeSet cmp |>.run
+
+set_option doc.verso true
+
+/--
+Traverses the given iterator and stores the emitted values in a {name}`ExtTreeSet`.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using {name}`Iter.toExtTreeSet`.
+-/
+@[inline]
+public def Iter.Total.toExtTreeSet {α β : Type w} [Iterator α Id β] [Finite α Id]
+    [IteratorLoop α Id Id] (it : Total (α := α) β) (cmp : β → β → Ordering := by exact compare)
+    [TransCmp cmp] : ExtTreeSet β cmp :=
+  it.it.toExtTreeSet cmp
+
+docs_to_verso Iter.toExtTreeSet
+
+end Std
diff --git a/src/Std/Data/Iterators/Lemmas/Consumers.lean b/src/Std/Data/Iterators/Lemmas/Consumers.lean
index c7c89d0c98..1be90022fd 100644
--- a/src/Std/Data/Iterators/Lemmas/Consumers.lean
+++ b/src/Std/Data/Iterators/Lemmas/Consumers.lean
@@ -10,3 +10,4 @@ public import Init.Data.Iterators.Lemmas.Consumers
 public import Std.Data.Iterators.Lemmas.Consumers.Monadic
 public import Std.Data.Iterators.Lemmas.Consumers.Collect
 public import Std.Data.Iterators.Lemmas.Consumers.Loop
+public import Std.Data.Iterators.Lemmas.Consumers.Set
diff --git a/src/Std/Data/Iterators/Lemmas/Consumers/Monadic.lean b/src/Std/Data/Iterators/Lemmas/Consumers/Monadic.lean
index 5c8d58c4b6..7621b447b2 100644
--- a/src/Std/Data/Iterators/Lemmas/Consumers/Monadic.lean
+++ b/src/Std/Data/Iterators/Lemmas/Consumers/Monadic.lean
@@ -8,3 +8,4 @@ module
 prelude
 public import Std.Data.Iterators.Lemmas.Consumers.Monadic.Collect
 public import Std.Data.Iterators.Lemmas.Consumers.Monadic.Loop
+public import Std.Data.Iterators.Lemmas.Consumers.Monadic.Set
diff --git a/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Set.lean b/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Set.lean
new file mode 100644
index 0000000000..a0b60a1cc0
--- /dev/null
+++ b/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Set.lean
@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Std.Data.Iterators.Consumers.Monadic.Set
+public import Init.Data.Iterators.Consumers.Monadic.Collect
+import all Std.Data.Iterators.Consumers.Monadic.Set
+import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
+import Std.Data.ExtHashSet.Lemmas
+import Std.Data.ExtTreeSet.Lemmas
+
+public section
+
+namespace Std
+open Iterators
+
+theorem IterM.toHashSet_eq_fold {α β : Type w} {_ : BEq β} {_ : Hashable β} {m : Type w → Type w'}
+    [Monad m] [Iterator α m β] [IteratorLoop α m m] {it : IterM (α := α) m β} :
+    it.toHashSet = it.fold (init := ∅) fun acc a => acc.insert a := (rfl)
+
+@[simp]
+theorem IterM.toExtHashSet_eq_ofList {α β : Type w} {_ : BEq β} {_ : Hashable β} [EquivBEq β]
+    [LawfulHashable β] {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β]
+    [Finite α m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM (α := α) m β} :
+    it.toExtHashSet = ExtHashSet.ofList <$> it.toList := by
+  simp only [toExtHashSet, ← foldl_toList, ← ExtHashSet.ofList_eq_foldl]
+
+theorem 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 = it.fold (init := ∅) fun acc a => acc.insert a := (rfl)
+
+@[simp]
+theorem IterM.toExtTreeSet_eq_ofList {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
+    [Iterator α m β] [Finite α m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {cmp : β → β → Ordering} [TransCmp cmp] :
+    it.toExtTreeSet cmp = (ExtTreeSet.ofList · cmp) <$> it.toList := by
+  simp only [toExtTreeSet, ← foldl_toList, ← ExtTreeSet.ofList_eq_foldl]
+
+end Std
diff --git a/src/Std/Data/Iterators/Lemmas/Consumers/Set.lean b/src/Std/Data/Iterators/Lemmas/Consumers/Set.lean
new file mode 100644
index 0000000000..75a0050516
--- /dev/null
+++ b/src/Std/Data/Iterators/Lemmas/Consumers/Set.lean
@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Std.Data.Iterators.Consumers.Set
+public import Init.Data.Iterators.Consumers.Collect
+import all Std.Data.Iterators.Consumers.Set
+import Std.Data.Iterators.Lemmas.Consumers.Monadic.Set
+import Init.Data.Iterators.Lemmas.Consumers.Loop
+import Std.Data.HashSet.Lemmas
+import Std.Data.TreeSet.Lemmas
+import Init.Data.Iterators.Lemmas.Consumers.Collect
+
+public section
+
+namespace Std
+open Iterators
+
+open HashSet in
+theorem Iter.toHashSet_equiv_ofList {α β : Type w} {_ : BEq β} {_ : Hashable β} [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter (α := α) β} :
+    it.toHashSet ~m HashSet.ofList it.toList := by
+  simpa [toHashSet, IterM.toHashSet_eq_fold, ← fold_eq_fold_toIterM,
+    ← foldl_toList] using ofList_equiv_foldl.symm
+
+@[simp]
+theorem Iter.toExtHashSet_eq_ofList {α β : Type w} {_ : BEq β} {_ : Hashable β} [EquivBEq β]
+    [LawfulHashable β] [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id]
+    [LawfulIteratorLoop α Id Id] {it : Iter (α := α) β} :
+    it.toExtHashSet = ExtHashSet.ofList it.toList := by
+  simp [toExtHashSet, ← toList_eq_toList_toIterM]
+
+open TreeSet in
+theorem Iter.toTreeSet_equiv_ofList {α β : Type w} [Iterator α Id β] [Finite α Id]
+    [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter (α := α) β}
+    {cmp : β → β → Ordering} : it.toTreeSet cmp ~m TreeSet.ofList it.toList cmp := by
+  simpa [toTreeSet, IterM.toTreeSet_eq_fold, ← fold_eq_fold_toIterM,
+    ← foldl_toList] using ofList_equiv_foldl.symm
+
+@[simp]
+theorem Iter.toExtTreeSet_eq_ofList {α β : Type w} [Iterator α Id β] [Finite α Id]
+    [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter (α := α) β}
+    {cmp : β → β → Ordering} [TransCmp cmp] :
+    it.toExtTreeSet cmp = ExtTreeSet.ofList it.toList cmp := by
+  simp [toExtTreeSet, ← toList_eq_toList_toIterM]
+
+end Std