diff --git a/src/Init/Data.lean b/src/Init/Data.lean
index 0a5fa959c1..6fd13e88d4 100644
--- a/src/Init/Data.lean
+++ b/src/Init/Data.lean
@@ -48,3 +48,4 @@ import Init.Data.RArray
 import Init.Data.Vector
 import Init.Data.Iterators
 import Init.Data.Range.Polymorphic
+import Init.Data.Slice
diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean
index 8324678e25..2927c40737 100644
--- a/src/Init/Data/Array/Subarray.lean
+++ b/src/Init/Data/Array/Subarray.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 import Init.Data.Array.Basic
+import Init.Data.Slice.Basic
 
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 set_option linter.missingDocs true
@@ -14,14 +15,9 @@ set_option linter.missingDocs true
 universe u v w
 
 /--
-A region of some underlying array.
-
-A subarray contains an array together with the start and end indices of a region of interest.
-Subarrays can be used to avoid copying or allocating space, while being more convenient than
-tracking the bounds by hand. The region of interest consists of every index that is both greater
-than or equal to `start` and strictly less than `stop`.
+Internal representation of `Subarray`, which is an abbreviation for `Slice SubarrayData`.
 -/
-structure Subarray (α : Type u) where
+structure Std.Slice.Internal.SubarrayData (α : Type u) where
   /-- The underlying array. -/
   array : Array α
   /-- The starting index of the region of interest (inclusive). -/
@@ -42,6 +38,40 @@ structure Subarray (α : Type u) where
   -/
   stop_le_array_size : stop ≤ array.size
 
+open Std.Slice
+
+/--
+A region of some underlying array.
+
+A subarray contains an array together with the start and end indices of a region of interest.
+Subarrays can be used to avoid copying or allocating space, while being more convenient than
+tracking the bounds by hand. The region of interest consists of every index that is both greater
+than or equal to `start` and strictly less than `stop`.
+-/
+abbrev Subarray (α : Type u) := Std.Slice (Internal.SubarrayData α)
+
+instance {α : Type u} : Self (Std.Slice (Internal.SubarrayData α)) (Subarray α) where
+
+@[always_inline, inline, expose, inherit_doc Internal.SubarrayData.array]
+def Subarray.array (xs : Subarray α) : Array α :=
+  xs.internalRepresentation.array
+
+@[always_inline, inline, expose, inherit_doc Internal.SubarrayData.start]
+def Subarray.start (xs : Subarray α) : Nat :=
+  xs.internalRepresentation.start
+
+@[always_inline, inline, expose, inherit_doc Internal.SubarrayData.stop]
+def Subarray.stop (xs : Subarray α) : Nat :=
+  xs.internalRepresentation.stop
+
+@[always_inline, inline, expose, inherit_doc Internal.SubarrayData.start_le_stop]
+def Subarray.start_le_stop (xs : Subarray α) : xs.start ≤ xs.stop :=
+  xs.internalRepresentation.start_le_stop
+
+@[always_inline, inline, expose, inherit_doc Internal.SubarrayData.stop_le_array_size]
+def Subarray.stop_le_array_size (xs : Subarray α) : xs.stop ≤ xs.array.size :=
+  xs.internalRepresentation.stop_le_array_size
+
 namespace Subarray
 
 /--
@@ -51,7 +81,7 @@ def size (s : Subarray α) : Nat :=
   s.stop - s.start
 
 theorem size_le_array_size {s : Subarray α} : s.size ≤ s.array.size := by
-  let {array, start, stop, start_le_stop, stop_le_array_size} := s
+  let ⟨{array, start, stop, start_le_stop, stop_le_array_size}⟩ := s
   simp [size]
   apply Nat.le_trans (Nat.sub_le stop start)
   assumption
@@ -102,7 +132,9 @@ Examples:
 -/
 def popFront (s : Subarray α) : Subarray α :=
   if h : s.start < s.stop then
-    { s with start := s.start + 1, start_le_stop := Nat.le_of_lt_succ (Nat.add_lt_add_right h 1) }
+    ⟨{ s.internalRepresentation with
+        start := s.start + 1,
+        start_le_stop := Nat.le_of_lt_succ (Nat.add_lt_add_right h 1) }⟩
   else
     s
 
@@ -111,12 +143,13 @@ The empty subarray.
 
 This empty subarray is backed by an empty array.
 -/
-protected def empty : Subarray α where
-  array := #[]
-  start := 0
-  stop := 0
-  start_le_stop := Nat.le_refl 0
-  stop_le_array_size := Nat.le_refl 0
+protected def empty : Subarray α := ⟨{
+    array := #[]
+    start := 0
+    stop := 0
+    start_le_stop := Nat.le_refl 0
+    stop_le_array_size := Nat.le_refl 0
+  }⟩
 
 instance : EmptyCollection (Subarray α) :=
   ⟨Subarray.empty⟩
@@ -410,24 +443,24 @@ Additionally, the starting index is clamped to the ending index.
 def toSubarray (as : Array α) (start : Nat := 0) (stop : Nat := as.size) : Subarray α :=
   if h₂ : stop ≤ as.size then
     if h₁ : start ≤ stop then
-      { array := as, start := start, stop := stop,
-        start_le_stop := h₁, stop_le_array_size := h₂ }
+      ⟨{ array := as, start := start, stop := stop,
+         start_le_stop := h₁, stop_le_array_size := h₂ }⟩
     else
-      { array := as, start := stop, stop := stop,
-        start_le_stop := Nat.le_refl _, stop_le_array_size := h₂ }
+      ⟨{ array := as, start := stop, stop := stop,
+         start_le_stop := Nat.le_refl _, stop_le_array_size := h₂ }⟩
   else
     if h₁ : start ≤ as.size then
-      { array := as,
-        start := start,
-        stop := as.size,
-        start_le_stop := h₁,
-        stop_le_array_size := Nat.le_refl _ }
+      ⟨{ array := as,
+         start := start,
+         stop := as.size,
+         start_le_stop := h₁,
+         stop_le_array_size := Nat.le_refl _ }⟩
     else
-      { array := as,
-        start := as.size,
-        stop := as.size,
-        start_le_stop := Nat.le_refl _,
-        stop_le_array_size := Nat.le_refl _ }
+      ⟨{ array := as,
+         start := as.size,
+         stop := as.size,
+         start_le_stop := Nat.le_refl _,
+         stop_le_array_size := Nat.le_refl _ }⟩
 
 /--
 Allocates a new array that contains the contents of the subarray.
diff --git a/src/Init/Data/Array/Subarray/Split.lean b/src/Init/Data/Array/Subarray/Split.lean
index c431037fc3..331d4cbd8c 100644
--- a/src/Init/Data/Array/Subarray/Split.lean
+++ b/src/Init/Data/Array/Subarray/Split.lean
@@ -21,44 +21,24 @@ set_option linter.listVariables true -- Enforce naming conventions for `List`/`A
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Subarray
-/--
-Splits a subarray into two parts, the first of which contains the first `i` elements and the second
-of which contains the remainder.
--/
-def split (s : Subarray α) (i : Fin s.size.succ) : (Subarray α × Subarray α) :=
-  let ⟨i', isLt⟩ := i
-  have := s.start_le_stop
-  have := s.stop_le_array_size
-  have : s.start + i' ≤ s.stop := by
-    simp only [size] at isLt
-    omega
-  let pre := {s with
-    stop := s.start + i',
-    start_le_stop := by omega,
-    stop_le_array_size := by omega
-  }
-  let post := {s with
-    start := s.start + i'
-    start_le_stop := by assumption
-  }
-  (pre, post)
 
 /--
 Removes the first `i` elements of the subarray. If there are `i` or fewer elements, the resulting
 subarray is empty.
 -/
-def drop (arr : Subarray α) (i : Nat) : Subarray α where
+def drop (arr : Subarray α) (i : Nat) : Subarray α := ⟨{
   array := arr.array
   start := min (arr.start + i) arr.stop
   stop := arr.stop
   start_le_stop := by omega
   stop_le_array_size := arr.stop_le_array_size
+}⟩
 
 /--
 Keeps only the first `i` elements of the subarray. If there are `i` or fewer elements, the resulting
 subarray is empty.
 -/
-def take (arr : Subarray α) (i : Nat) : Subarray α where
+def take (arr : Subarray α) (i : Nat) : Subarray α := ⟨{
   array := arr.array
   start := arr.start
   stop := min (arr.start + i) arr.stop
@@ -68,3 +48,11 @@ def take (arr : Subarray α) (i : Nat) : Subarray α where
   stop_le_array_size := by
     have := arr.stop_le_array_size
     omega
+}⟩
+
+/--
+Splits a subarray into two parts, the first of which contains the first `i` elements and the second
+of which contains the remainder.
+-/
+def split (s : Subarray α) (i : Fin s.size.succ) : (Subarray α × Subarray α) :=
+  (s.take i, s.drop i)
diff --git a/src/Init/Data/Iterators.lean b/src/Init/Data/Iterators.lean
index 115a534b45..1fde41993b 100644
--- a/src/Init/Data/Iterators.lean
+++ b/src/Init/Data/Iterators.lean
@@ -9,7 +9,9 @@ prelude
 import Init.Data.Iterators.Basic
 import Init.Data.Iterators.PostconditionMonad
 import Init.Data.Iterators.Consumers
+import Init.Data.Iterators.Combinators
 import Init.Data.Iterators.Lemmas
+import Init.Data.Iterators.ToIterator
 import Init.Data.Iterators.Internal
 
 /-!
diff --git a/src/Init/Data/Iterators/Basic.lean b/src/Init/Data/Iterators/Basic.lean
index 571bee0f81..a6c011a839 100644
--- a/src/Init/Data/Iterators/Basic.lean
+++ b/src/Init/Data/Iterators/Basic.lean
@@ -401,6 +401,20 @@ theorem IterM.IsPlausibleIndirectSuccessorOf.trans {α β : Type w} {m : Type w
   case refl => exact h'
   case cons_right ih => exact IsPlausibleIndirectSuccessorOf.cons_right ih ‹_›
 
+theorem IterM.IsPlausibleIndirectSuccessorOf.single {α β : Type w} {m : Type w → Type w'}
+    [Iterator α m β] {it' it : IterM (α := α) m β}
+    (h : it'.IsPlausibleSuccessorOf it) :
+    it'.IsPlausibleIndirectSuccessorOf it :=
+  .cons_right (.refl _) h
+
+theorem IterM.IsPlausibleIndirectOutput.trans {α β : Type w} {m : Type w → Type w'}
+    [Iterator α m β]
+    {it' it : IterM (α := α) m β} {out : β} (h : it'.IsPlausibleIndirectSuccessorOf it)
+    (h' : it'.IsPlausibleIndirectOutput out) : it.IsPlausibleIndirectOutput out := by
+  induction h
+  case refl => exact h'
+  case cons_right ih => exact IsPlausibleIndirectOutput.indirect ‹_› ih
+
 /--
 The type of the step object returned by `Iter.step`, containing an `IterStep`
 and a proof that this is a plausible step for the given iterator.
diff --git a/src/Init/Data/Iterators/Combinators.lean b/src/Init/Data/Iterators/Combinators.lean
new file mode 100644
index 0000000000..0de4a9bee8
--- /dev/null
+++ b/src/Init/Data/Iterators/Combinators.lean
@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+import Init.Data.Iterators.Combinators.Monadic
+import Init.Data.Iterators.Combinators.FilterMap
diff --git a/src/Init/Data/Iterators/Combinators/Attach.lean b/src/Init/Data/Iterators/Combinators/Attach.lean
new file mode 100644
index 0000000000..cb596fbb57
--- /dev/null
+++ b/src/Init/Data/Iterators/Combinators/Attach.lean
@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+import Init.Data.Iterators.Combinators.Monadic.Attach
+import Init.Data.Iterators.Combinators.FilterMap
+
+namespace Std.Iterators
+
+@[always_inline, inline, inherit_doc IterM.attachWith]
+def Iter.attachWith {α β : Type w}
+    [Iterator α Id β]
+    (it : Iter (α := α) β) (P : β → Prop) (h : ∀ out, it.IsPlausibleIndirectOutput out → P out) :
+  Iter (α := Types.Attach α Id P) { out : β // P out } :=
+  (it.toIterM.attachWith P ?h).toIter
+where finally
+  case h =>
+    simp only [← isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM]
+    exact h
+
+end Std.Iterators
diff --git a/src/Std/Data/Iterators/Combinators/FilterMap.lean b/src/Init/Data/Iterators/Combinators/FilterMap.lean
similarity index 96%
rename from src/Std/Data/Iterators/Combinators/FilterMap.lean
rename to src/Init/Data/Iterators/Combinators/FilterMap.lean
index 3942526bc4..c0e21c30a0 100644
--- a/src/Std/Data/Iterators/Combinators/FilterMap.lean
+++ b/src/Init/Data/Iterators/Combinators/FilterMap.lean
@@ -3,8 +3,10 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
+module
+
 prelude
-import Std.Data.Iterators.Combinators.Monadic.FilterMap
+import Init.Data.Iterators.Combinators.Monadic.FilterMap
 
 /-!
 
@@ -75,7 +77,7 @@ postcondition is `fun x => x.isSome`; if `f` always fails, a suitable postcondit
 For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the
 returned `Option` value.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 def Iter.filterMapWithPostcondition {α β γ : Type w} [Iterator α Id β] {m : Type w → Type w'}
     [Monad m] (f : β → PostconditionT m (Option γ)) (it : Iter (α := α) β) :=
   (letI : MonadLift Id m := ⟨pure⟩; it.toIterM.filterMapWithPostcondition f : IterM m γ)
@@ -120,7 +122,7 @@ be `fun _ => False`.
 
 For each value emitted by the base iterator `it`, this combinator calls `f`.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 def Iter.filterWithPostcondition {α β : Type w} [Iterator α Id β] {m : Type w → Type w'}
     [Monad m] (f : β → PostconditionT m (ULift Bool)) (it : Iter (α := α) β) :=
   (letI : MonadLift Id m := ⟨pure⟩; it.toIterM.filterWithPostcondition f : IterM m β)
@@ -164,7 +166,7 @@ be `fun _ => False`.
 
 For each value emitted by the base iterator `it`, this combinator calls `f`.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 def Iter.mapWithPostcondition {α β γ : Type w} [Iterator α Id β] {m : Type w → Type w'}
     [Monad m] (f : β → PostconditionT m γ) (it : Iter (α := α) β) :=
   (letI : MonadLift Id m := ⟨pure⟩; it.toIterM.mapWithPostcondition f : IterM m γ)
@@ -205,7 +207,7 @@ possible to manually prove `Finite` and `Productive` instances depending on the
 For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the
 returned `Option` value.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 def Iter.filterMapM {α β γ : Type w} [Iterator α Id β] {m : Type w → Type w'}
     [Monad m] (f : β → m (Option γ)) (it : Iter (α := α) β) :=
   (letI : MonadLift Id m := ⟨pure⟩; it.toIterM.filterMapM f : IterM m γ)
@@ -242,7 +244,7 @@ manually prove `Finite` and `Productive` instances depending on the concrete cho
 
 For each value emitted by the base iterator `it`, this combinator calls `f`.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 def Iter.filterM {α β : Type w} [Iterator α Id β] {m : Type w → Type w'}
     [Monad m] (f : β → m (ULift Bool)) (it : Iter (α := α) β) :=
   (letI : MonadLift Id m := ⟨pure⟩; it.toIterM.filterM f : IterM m β)
@@ -281,22 +283,22 @@ manually prove `Finite` and `Productive` instances depending on the concrete cho
 
 For each value emitted by the base iterator `it`, this combinator calls `f`.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 def Iter.mapM {α β γ : Type w} [Iterator α Id β] {m : Type w → Type w'}
     [Monad m] (f : β → m γ) (it : Iter (α := α) β) :=
   (letI : MonadLift Id m := ⟨pure⟩; it.toIterM.mapM f : IterM m γ)
 
-@[always_inline, inline, inherit_doc IterM.filterMap]
+@[always_inline, inline, inherit_doc IterM.filterMap, expose]
 def Iter.filterMap {α : Type w} {β : Type w} {γ : Type w} [Iterator α Id β]
     (f : β → Option γ) (it : Iter (α := α) β) :=
   ((it.toIterM.filterMap f).toIter : Iter γ)
 
-@[always_inline, inline, inherit_doc IterM.filter]
+@[always_inline, inline, inherit_doc IterM.filter, expose]
 def Iter.filter {α : Type w} {β : Type w} [Iterator α Id β]
     (f : β → Bool) (it : Iter (α := α) β) :=
   ((it.toIterM.filter f).toIter : Iter β)
 
-@[always_inline, inline, inherit_doc IterM.map]
+@[always_inline, inline, inherit_doc IterM.map, expose]
 def Iter.map {α : Type w} {β : Type w} {γ : Type w} [Iterator α Id β]
     (f : β → γ) (it : Iter (α := α) β) :=
   ((it.toIterM.map f).toIter : Iter γ)
diff --git a/src/Init/Data/Iterators/Combinators/Monadic.lean b/src/Init/Data/Iterators/Combinators/Monadic.lean
new file mode 100644
index 0000000000..a35a85ce23
--- /dev/null
+++ b/src/Init/Data/Iterators/Combinators/Monadic.lean
@@ -0,0 +1,9 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+import Init.Data.Iterators.Combinators.Monadic.FilterMap
diff --git a/src/Init/Data/Iterators/Combinators/Monadic/Attach.lean b/src/Init/Data/Iterators/Combinators/Monadic/Attach.lean
new file mode 100644
index 0000000000..38275b7e88
--- /dev/null
+++ b/src/Init/Data/Iterators/Combinators/Monadic/Attach.lean
@@ -0,0 +1,136 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+import Init.Data.Iterators.Basic
+import Init.Data.Iterators.Internal.Termination
+import Init.Data.Iterators.Consumers.Collect
+import Init.Data.Iterators.Consumers.Loop
+
+namespace Std.Iterators.Types
+
+/--
+Internal state of the `attachWith` combinator. Do not depend on its internals.
+-/
+@[unbox]
+structure Attach (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β]
+    (P : β → Prop) where
+  inner : IterM (α := α) m β
+  invariant : ∀ out, inner.IsPlausibleIndirectOutput out → P out
+
+@[always_inline, inline]
+def Attach.modifyStep {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    {P : β → Prop}
+    (it : IterM (α := Attach α m P) m { out : β // P out })
+    (step : it.internalState.inner.Step (α := α) (m := m)) :
+    IterStep (IterM (α := Attach α m P) m { out : β // P out })
+        { out : β // P out } :=
+  match step with
+  | .yield it' out h =>
+    .yield ⟨it', fun out ho => it.internalState.invariant out (.indirect ⟨_, rfl, h⟩ ho)⟩
+      ⟨out, it.internalState.invariant out (.direct ⟨_, h⟩)⟩
+  | .skip it' h =>
+    .skip ⟨it', fun out ho => it.internalState.invariant out (.indirect ⟨_, rfl, h⟩ ho)⟩
+  | .done _ => .done
+
+instance Attach.instIterator {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] {P : β → Prop} :
+    Iterator (Attach α m P) m { out : β // P out } where
+  IsPlausibleStep it step := ∃ step', modifyStep it step' = step
+  step it := (fun step => ⟨modifyStep it step, step, rfl⟩) <$> it.internalState.inner.step
+
+def Attach.instFinitenessRelation {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [Finite α m] {P : β → Prop} :
+    FinitenessRelation (Attach α m P) m where
+  rel := InvImage WellFoundedRelation.rel fun it => it.internalState.inner.finitelyManySteps
+  wf := InvImage.wf _ WellFoundedRelation.wf
+  subrelation {it it'} h := by
+    apply Relation.TransGen.single
+    obtain ⟨_, hs, step, h', rfl⟩ := h
+    cases step using PlausibleIterStep.casesOn
+    · simp only [IterStep.successor, modifyStep, Option.some.injEq] at hs
+      simp only [← hs]
+      exact ⟨_, rfl, ‹_›⟩
+    · simp only [IterStep.successor, modifyStep, Option.some.injEq] at hs
+      simp only [← hs]
+      exact ⟨_, rfl, ‹_›⟩
+    · simp [IterStep.successor, modifyStep, reduceCtorEq] at hs
+
+instance Attach.instFinite {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [Finite α m] {P : β → Prop} : Finite (Attach α m P) m :=
+  .of_finitenessRelation instFinitenessRelation
+
+def Attach.instProductivenessRelation {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [Productive α m] {P : β → Prop} :
+    ProductivenessRelation (Attach α m P) m where
+  rel := InvImage WellFoundedRelation.rel fun it => it.internalState.inner.finitelyManySkips
+  wf := InvImage.wf _ WellFoundedRelation.wf
+  subrelation {it it'} h := by
+    apply Relation.TransGen.single
+    simp_wf
+    obtain ⟨step, hs⟩ := h
+    cases step using PlausibleIterStep.casesOn
+    · simp [modifyStep] at hs
+    · simp only [modifyStep, IterStep.skip.injEq] at hs
+      simp only [← hs]
+      assumption
+    · simp [modifyStep] at hs
+
+instance Attach.instProductive {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [Productive α m] {P : β → Prop} :
+    Productive (Attach α m P) m :=
+  .of_productivenessRelation instProductivenessRelation
+
+instance Attach.instIteratorCollect {α β : Type w} {m : Type w → Type w'} [Monad m] [Monad n]
+    {P : β → Prop} [Iterator α m β] :
+    IteratorCollect (Attach α m P) m n :=
+  .defaultImplementation
+
+instance Attach.instIteratorCollectPartial {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Monad n] {P : β → Prop} [Iterator α m β] :
+    IteratorCollectPartial (Attach α m P) m n :=
+  .defaultImplementation
+
+instance Attach.instIteratorLoop {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Monad n] {P : β → Prop} [Iterator α m β] [MonadLiftT m n] :
+    IteratorLoop (Attach α m P) m n :=
+  .defaultImplementation
+
+instance Attach.instIteratorLoopPartial {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Monad n] {P : β → Prop} [Iterator α m β] [MonadLiftT m n] :
+    IteratorLoopPartial (Attach α m P) m n :=
+  .defaultImplementation
+
+instance {α β : Type w} {m : Type w → Type w'} [Monad m]
+    {P : β → Prop} [Iterator α m β] [IteratorSize α m] :
+    IteratorSize (Attach α m P) m where
+  size it := IteratorSize.size it.internalState.inner
+
+instance {α β : Type w} {m : Type w → Type w'} [Monad m]
+    {P : β → Prop} [Iterator α m β] [IteratorSizePartial α m] :
+    IteratorSizePartial (Attach α m P) m where
+  size it := IteratorSizePartial.size it.internalState.inner
+
+end Types
+
+/--
+“Attaches” individual proofs to an iterator of values that satisfy a predicate `P`, returning an
+iterator with values in the corresponding subtype `{ x // P x }`.
+
+**Termination properties:**
+
+* `Finite` instance: only if the base iterator is finite
+* `Productive` instance: only if the base iterator is productive
+-/
+@[always_inline, inline]
+def IterM.attachWith {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] (it : IterM (α := α) m β) (P : β → Prop)
+    (h : ∀ out, it.IsPlausibleIndirectOutput out → P out) :
+    IterM (α := Types.Attach α m P) m { out : β // P out } :=
+  ⟨⟨it, h⟩⟩
+
+end Std.Iterators
diff --git a/src/Std/Data/Iterators/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
similarity index 96%
rename from src/Std/Data/Iterators/Combinators/Monadic/FilterMap.lean
rename to src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
index 412beb2357..5b19a49fcd 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/FilterMap.lean
+++ b/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
@@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
+module
+
 prelude
 import Init.Data.Iterators.Basic
 import Init.Data.Iterators.Consumers.Collect
@@ -45,19 +47,20 @@ structure FilterMap (α : Type w) {β γ : Type w}
 /--
 Internal state of the `map` combinator. Do not depend on its internals.
 -/
+@[expose]
 def Map (α : Type w) {β γ : Type w} (m : Type w → Type w') (n : Type w → Type w'')
     (lift : ⦃α : Type w⦄ → m α → n α) [Functor n]
     (f : β → PostconditionT n γ) :=
   FilterMap α m n lift (fun b => PostconditionT.map some (f b))
 
-@[always_inline, inline]
+@[always_inline, inline, expose]
 def IterM.InternalCombinators.filterMap {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} (lift : ⦃α : Type w⦄ → m α → n α)
     [Iterator α m β] (f : β → PostconditionT n (Option γ))
     (it : IterM (α := α) m β) : IterM (α := FilterMap α m n lift f) n γ :=
   toIterM ⟨it⟩ n γ
 
-@[always_inline, inline]
+@[always_inline, inline, expose]
 def IterM.InternalCombinators.map {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} [Monad n] (lift : ⦃α : Type w⦄ → m α → n α)
     [Iterator α m β] (f : β → PostconditionT n γ)
@@ -110,7 +113,7 @@ postcondition is `fun x => x.isSome`; if `f` always fails, a suitable postcondit
 For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the
 returned `Option` value.
 -/
-@[inline]
+@[inline, expose]
 def IterM.filterMapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
     [MonadLiftT m n] [Iterator α m β] (f : β → PostconditionT n (Option γ))
     (it : IterM (α := α) m β) : IterM (α := FilterMap α m n (fun ⦃_⦄ => monadLift) f) n γ :=
@@ -147,9 +150,9 @@ instance FilterMap.instIterator {α β γ : Type w} {m : Type w → Type w'} {n
       match ← it.internalState.inner.step with
       | .yield it' out h => do
         match ← (f out).operation with
-        | ⟨none, h'⟩ => pure <| .skip (it'.filterMapWithPostcondition f) (.yieldNone h h')
-        | ⟨some out', h'⟩ => pure <| .yield (it'.filterMapWithPostcondition f) out' (.yieldSome h h')
-      | .skip it' h => pure <| .skip (it'.filterMapWithPostcondition f) (.skip h)
+        | ⟨none, h'⟩ => pure <| .skip (it'.filterMapWithPostcondition f) (by exact .yieldNone h h')
+        | ⟨some out', h'⟩ => pure <| .yield (it'.filterMapWithPostcondition f) out' (by exact .yieldSome h h')
+      | .skip it' h => pure <| .skip (it'.filterMapWithPostcondition f) (by exact .skip h)
       | .done h => pure <| .done (.done h)
 
 instance {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β]
@@ -179,11 +182,13 @@ private def FilterMap.instFinitenessRelation {α β γ : Type w} {m : Type w →
     case done h' =>
       cases h
 
+@[no_expose]
 instance FilterMap.instFinite {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
     {f : β → PostconditionT n (Option γ)} [Finite α m] : Finite (FilterMap α m n lift f) n :=
   Finite.of_finitenessRelation FilterMap.instFinitenessRelation
 
+@[no_expose]
 instance {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β]
     {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} [Finite α m] :
     Finite (Map α m n lift f) n :=
@@ -202,6 +207,7 @@ private def Map.instProductivenessRelation {α β γ : Type w} {m : Type w → T
     case skip it' h =>
       exact h
 
+@[no_expose]
 instance Map.instProductive {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
     {f : β → PostconditionT n γ} [Productive α m] :
@@ -253,6 +259,7 @@ instance Map.instIteratorCollect {α β γ : Type w} {m : Type w → Type w'}
       (fun x => do g (← (f x).operation))
       it.internalState.inner (m := m)
 
+@[no_expose]
 instance Map.instIteratorCollectPartial {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β]
     {lift₁ : ⦃α : Type w⦄ → m α → n α}
@@ -318,7 +325,7 @@ be `fun _ => False`.
 
 For each value emitted by the base iterator `it`, this combinator calls `f`.
 -/
-@[inline]
+@[inline, expose]
 def IterM.mapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
     [Monad n] [MonadLiftT m n] [Iterator α m β] (f : β → PostconditionT n γ)
     (it : IterM (α := α) m β) : IterM (α := Map α m n (fun ⦃_⦄ => monadLift) f) n γ :=
@@ -365,7 +372,7 @@ be `fun _ => False`.
 
 For each value emitted by the base iterator `it`, this combinator calls `f`.
 -/
-@[inline]
+@[inline, expose]
 def IterM.filterWithPostcondition {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
     [Monad n] [MonadLiftT m n] [Iterator α m β] (f : β → PostconditionT n (ULift Bool))
     (it : IterM (α := α) m β) :=
@@ -411,7 +418,7 @@ possible to manually prove `Finite` and `Productive` instances depending on the
 For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the
 returned `Option` value.
 -/
-@[inline]
+@[inline, expose]
 def IterM.filterMapM {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
     [Iterator α m β] [Monad n] [MonadLiftT m n]
     (f : β → n (Option γ)) (it : IterM (α := α) m β) :=
@@ -451,7 +458,7 @@ manually prove `Finite` and `Productive` instances depending on the concrete cho
 
 For each value emitted by the base iterator `it`, this combinator calls `f`.
 -/
-@[inline]
+@[inline, expose]
 def IterM.mapM {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β]
     [Monad n] [MonadLiftT m n] (f : β → n γ) (it : IterM (α := α) m β) :=
   (it.filterMapWithPostcondition (fun b => some <$> PostconditionT.lift (f b)) : IterM n γ)
@@ -491,7 +498,7 @@ manually prove `Finite` and `Productive` instances depending on the concrete cho
 
 For each value emitted by the base iterator `it`, this combinator calls `f`.
 -/
-@[inline]
+@[inline, expose]
 def IterM.filterM {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β]
     [Monad n] [MonadLiftT m n] (f : β → n (ULift Bool)) (it : IterM (α := α) m β) :=
   (it.filterMapWithPostcondition
@@ -528,7 +535,7 @@ be proved manually.
 For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the
 returned `Option` value.
 -/
-@[inline]
+@[inline, expose]
 def IterM.filterMap {α β γ : Type w} {m : Type w → Type w'}
     [Iterator α m β] [Monad m] (f : β → Option γ) (it : IterM (α := α) m β) :=
   (it.filterMapWithPostcondition (fun b => pure (f b)) : IterM m γ)
@@ -557,7 +564,7 @@ it.map     ---a'--b'--c'--d'-e'----⊥
 
 For each value emitted by the base iterator `it`, this combinator calls `f`.
 -/
-@[inline]
+@[inline, expose]
 def IterM.map {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Monad m] (f : β → γ)
     (it : IterM (α := α) m β) :=
   (it.mapWithPostcondition (fun b => pure (f b)) : IterM m γ)
@@ -592,7 +599,7 @@ be proved manually.
 For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the
 returned value.
 -/
-@[inline]
+@[inline, expose]
 def IterM.filter {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Monad m]
     (f : β → Bool) (it : IterM (α := α) m β) :=
   (it.filterMap (fun b => if f b then some b else none) : IterM m β)
@@ -609,4 +616,18 @@ instance {α β γ : Type w} {m : Type w → Type w'}
     IteratorSizePartial (FilterMap α m n lift f) n :=
   .defaultImplementation
 
+instance {α β γ : Type w} {m : Type w → Type w'}
+    {n : Type w → Type w''} [Monad n] [Iterator α m β]
+    {lift : ⦃α : Type w⦄ → m α → n α}
+    {f : β → PostconditionT n γ} [IteratorSize α m] :
+    IteratorSize (Map α m n lift f) n where
+  size it := lift (IteratorSize.size it.internalState.inner)
+
+instance {α β γ : Type w} {m : Type w → Type w'}
+    {n : Type w → Type w''} [Monad n] [Iterator α m β]
+    {lift : ⦃α : Type w⦄ → m α → n α}
+    {f : β → PostconditionT n γ} [IteratorSizePartial α m] :
+    IteratorSizePartial (Map α m n lift f) n where
+  size it := lift (IteratorSizePartial.size it.internalState.inner)
+
 end Std.Iterators
diff --git a/src/Init/Data/Iterators/Lemmas.lean b/src/Init/Data/Iterators/Lemmas.lean
index 65a041ee83..6a4e33f659 100644
--- a/src/Init/Data/Iterators/Lemmas.lean
+++ b/src/Init/Data/Iterators/Lemmas.lean
@@ -7,3 +7,4 @@ module
 
 prelude
 import Init.Data.Iterators.Lemmas.Consumers
+import Init.Data.Iterators.Lemmas.Combinators
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators.lean b/src/Init/Data/Iterators/Lemmas/Combinators.lean
new file mode 100644
index 0000000000..f1f9970f19
--- /dev/null
+++ b/src/Init/Data/Iterators/Lemmas/Combinators.lean
@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+import Init.Data.Iterators.Lemmas.Combinators.Monadic
+import Init.Data.Iterators.Lemmas.Combinators.FilterMap
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
similarity index 99%
rename from src/Std/Data/Iterators/Lemmas/Combinators/FilterMap.lean
rename to src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
index 4f27015aa3..d4305c227d 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/FilterMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
@@ -3,10 +3,12 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
+module
+
 prelude
 import Init.Data.Iterators.Lemmas.Consumers
-import Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
-import Std.Data.Iterators.Combinators.FilterMap
+import Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
+import Init.Data.Iterators.Combinators.FilterMap
 
 namespace Std.Iterators
 
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean
new file mode 100644
index 0000000000..54440cf07d
--- /dev/null
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean
@@ -0,0 +1,9 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+import Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
new file mode 100644
index 0000000000..12c8e1ab55
--- /dev/null
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
@@ -0,0 +1,414 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
+import Init.Data.Iterators.Combinators.Monadic.FilterMap
+import Init.Data.Iterators.Lemmas.Consumers.Monadic
+import all Init.Data.Iterators.Consumers.Monadic.Collect
+
+namespace Std.Iterators
+open Std.Internal
+
+section Step
+
+variable {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
+  [Iterator α m β] {it : IterM (α := α) m β}
+
+theorem IterM.step_filterMapWithPostcondition {f : β → PostconditionT n (Option β')}
+    [Monad n] [LawfulMonad n] [MonadLiftT m n] :
+  (it.filterMapWithPostcondition f).step = (do
+    match ← it.step with
+    | .yield it' out h => do
+      match ← (f out).operation with
+      | ⟨none, h'⟩ =>
+        pure <| .skip (it'.filterMapWithPostcondition f) (.yieldNone (out := out) h h')
+      | ⟨some out', h'⟩ =>
+        pure <| .yield (it'.filterMapWithPostcondition f) out' (.yieldSome (out := out) h h')
+    | .skip it' h =>
+      pure <| .skip (it'.filterMapWithPostcondition f) (.skip h)
+    | .done h =>
+      pure <| .done (by exact .done h)) := by
+  apply bind_congr
+  intro step
+  match step with
+  | .yield it' out h =>
+    simp only [PlausibleIterStep.skip, PlausibleIterStep.yield]
+    apply bind_congr
+    intro step
+    rcases step with _ | _ <;> rfl
+  | .skip it' h => rfl
+  | .done h => rfl
+
+theorem IterM.step_filterWithPostcondition {f : β → PostconditionT n (ULift Bool)}
+    [Monad n] [LawfulMonad n] [MonadLiftT m n] :
+  (it.filterWithPostcondition f).step = (do
+    match ← it.step with
+    | .yield it' out h => do
+      match ← (f out).operation with
+      | ⟨.up false, h'⟩ =>
+        pure <| .skip (it'.filterWithPostcondition f) (.yieldNone (out := out) h ⟨⟨_, h'⟩, rfl⟩)
+      | ⟨.up true, h'⟩ =>
+        pure <| .yield (it'.filterWithPostcondition f) out (by exact .yieldSome (out := out) h ⟨⟨_, h'⟩, rfl⟩)
+    | .skip it' h =>
+      pure <| .skip (it'.filterWithPostcondition f) (by exact .skip h)
+    | .done h =>
+      pure <| .done (by exact .done h)) := by
+  apply bind_congr
+  intro step
+  match step with
+  | .yield it' out h =>
+    simp only [PostconditionT.operation_map, PlausibleIterStep.skip, PlausibleIterStep.yield,
+      bind_map_left]
+    apply bind_congr
+    intro step
+    rcases step with _ | _ <;> rfl
+  | .skip it' h => rfl
+  | .done h => rfl
+
+theorem IterM.step_mapWithPostcondition {γ : Type w} {f : β → PostconditionT n γ}
+    [Monad n] [LawfulMonad n] [MonadLiftT m n] :
+  (it.mapWithPostcondition f).step = (do
+    match ← it.step with
+    | .yield it' out h => do
+      let out' ← (f out).operation
+      pure <| .yield (it'.mapWithPostcondition f) out'.1 (.yieldSome h ⟨out', rfl⟩)
+    | .skip it' h =>
+      pure <| .skip (it'.mapWithPostcondition f) (.skip h)
+    | .done h =>
+      pure <| .done (.done h)) := by
+  apply bind_congr
+  intro step
+  match step with
+  | .yield it' out h =>
+    simp only [PostconditionT.operation_map, bind_map_left, bind_pure_comp]
+    rfl
+  | .skip it' h => rfl
+  | .done h => rfl
+
+theorem IterM.step_filterMapM {f : β → n (Option β')}
+    [Monad n] [LawfulMonad n] [MonadLiftT m n] :
+  (it.filterMapM f).step = (do
+    match ← it.step with
+    | .yield it' out h => do
+      match ← f out with
+      | none =>
+        pure <| .skip (it'.filterMapM f) (.yieldNone (out := out) h .intro)
+      | some out' =>
+        pure <| .yield (it'.filterMapM f) out' (.yieldSome (out := out) h .intro)
+    | .skip it' h =>
+      pure <| .skip (it'.filterMapM f) (.skip h)
+    | .done h =>
+      pure <| .done (.done h)) := by
+  apply bind_congr
+  intro step
+  match step with
+  | .yield it' out h =>
+    simp only [PostconditionT.lift, bind_map_left]
+    apply bind_congr
+    intro step
+    rcases step with _ | _ <;> rfl
+  | .skip it' h => rfl
+  | .done h => rfl
+
+theorem IterM.step_filterM {f : β → n (ULift Bool)}
+    [Monad n] [LawfulMonad n] [MonadLiftT m n] :
+  (it.filterM f).step = (do
+    match ← it.step with
+    | .yield it' out h => do
+      match ← f out with
+      | .up false =>
+        pure <| .skip (it'.filterM f) (.yieldNone (out := out) h ⟨⟨.up false, .intro⟩, rfl⟩)
+      | .up true =>
+        pure <| .yield (it'.filterM f) out (.yieldSome (out := out) h ⟨⟨.up true, .intro⟩, rfl⟩)
+    | .skip it' h =>
+      pure <| .skip (it'.filterM f) (.skip h)
+    | .done h =>
+      pure <| .done (.done h)) := by
+  apply bind_congr
+  intro step
+  match step with
+  | .yield it' out h =>
+    simp only [PostconditionT.lift, PostconditionT.operation_map, Functor.map_map,
+      PlausibleIterStep.skip, PlausibleIterStep.yield, bind_map_left]
+    apply bind_congr
+    intro step
+    rcases step with _ | _ <;> rfl
+  | .skip it' h => rfl
+  | .done h => rfl
+
+theorem IterM.step_mapM {γ : Type w} {f : β → n γ}
+    [Monad n] [LawfulMonad n] [MonadLiftT m n] :
+  (it.mapM f).step = (do
+    match ← it.step with
+    | .yield it' out h => do
+      let out' ← f out
+      pure <| .yield (it'.mapM f) out' (.yieldSome h ⟨⟨out', True.intro⟩, rfl⟩)
+    | .skip it' h =>
+      pure <| .skip (it'.mapM f) (.skip h)
+    | .done h =>
+      pure <| .done (.done h)) := by
+  apply bind_congr
+  intro step
+  match step with
+  | .yield it' out h =>
+    simp only [bind_pure_comp]
+    simp only [PostconditionT.lift, Functor.map]
+    simp only [PostconditionT.operation_map, Functor.map_map, PlausibleIterStep.skip,
+      PlausibleIterStep.yield, bind_map_left, bind_pure_comp]
+    rfl
+  | .skip it' h => rfl
+  | .done h => rfl
+
+theorem IterM.step_filterMap [Monad m] [LawfulMonad m] {f : β → Option β'} :
+  (it.filterMap f).step = (do
+    match ← it.step with
+    | .yield it' out h => do
+      match h' : f out with
+      | none =>
+        pure <| .skip (it'.filterMap f) (.yieldNone h h')
+      | some out' =>
+        pure <| .yield (it'.filterMap f) out' (.yieldSome h h')
+    | .skip it' h =>
+      pure <| .skip (it'.filterMap f) (.skip h)
+    | .done h =>
+      pure <| .done (.done h)) := by
+  simp only [IterM.filterMap, step_filterMapWithPostcondition, pure]
+  apply bind_congr
+  intro step
+  split
+  · simp only [PostconditionT.pure, PlausibleIterStep.skip, PlausibleIterStep.yield, pure_bind]
+    split <;> split <;> simp_all
+  · simp
+  · simp
+
+theorem IterM.step_map [Monad m] [LawfulMonad m] {f : β → β'} :
+  (it.map f).step = (do
+    match ← it.step with
+    | .yield it' out h =>
+      let out' := f out
+      pure <| .yield (it'.map f) out' (.yieldSome h ⟨⟨out', rfl⟩, rfl⟩)
+    | .skip it' h =>
+      pure <| .skip (it'.map f) (.skip h)
+    | .done h => pure <| .done (.done h)) := by
+  simp only [map, IterM.step_mapWithPostcondition]
+  apply bind_congr
+  intro step
+  split
+  · simp
+  · rfl
+  · rfl
+
+theorem IterM.step_filter [Monad m] [LawfulMonad m] {f : β → Bool} :
+  (it.filter f).step = (do
+    match ← it.step with
+    | .yield it' out h =>
+      if h' : f out = true then
+        pure <| .yield (it'.filter f) out (.yieldSome h (by simp [h']))
+      else
+        pure <| .skip (it'.filter f) (.yieldNone h (by simp [h']))
+    | .skip it' h =>
+      pure <| .skip (it'.filter f) (.skip h)
+    | .done h => pure <| .done (.done h)) := by
+  simp only [filter, IterM.step_filterMap]
+  apply bind_congr
+  intro step
+  split
+  · split
+    · split
+      · exfalso; simp_all
+      · rfl
+    · split
+      · congr; simp_all
+      · exfalso; simp_all
+  · rfl
+  · rfl
+
+end Step
+
+section Lawful
+
+@[no_expose]
+instance {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type x}
+    [Monad m] [Monad n] [Monad o] [LawfulMonad n] [LawfulMonad o] [Iterator α m β] [Finite α m]
+    [IteratorCollect α m o] [LawfulIteratorCollect α m o]
+    {lift : ⦃δ : Type w⦄ -> m δ → n δ} {f : β → PostconditionT n γ} [LawfulMonadLiftFunction lift] :
+    LawfulIteratorCollect (Map α m n lift f) n o where
+  lawful_toArrayMapped := by
+    intro δ lift' _ _
+    letI : MonadLift m n := ⟨lift (δ := _)⟩
+    letI : MonadLift n o := ⟨lift' (α := _)⟩
+    ext g it
+    have : it = IterM.mapWithPostcondition _ it.internalState.inner := by rfl
+    generalize it.internalState.inner = it at *
+    cases this
+    simp only [LawfulIteratorCollect.toArrayMapped_eq]
+    simp only [IteratorCollect.toArrayMapped]
+    rw [LawfulIteratorCollect.toArrayMapped_eq]
+    induction it using IterM.inductSteps with | step it ih_yield ih_skip =>
+    rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
+    rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
+    simp only [bind_assoc]
+    rw [IterM.step_mapWithPostcondition]
+    simp only [liftM_bind (m := n) (n := o), bind_assoc]
+    apply bind_congr
+    intro step
+    cases step using PlausibleIterStep.casesOn
+    · simp only [bind_pure_comp]
+      simp only [liftM_map, bind_map_left]
+      apply bind_congr
+      intro out'
+      simp only [← ih_yield ‹_›]
+      rfl
+    · simp only [bind_pure_comp, pure_bind, liftM_pure, pure_bind, ← ih_skip ‹_›]
+      simp only [IterM.mapWithPostcondition, IterM.InternalCombinators.map, internalState_toIterM]
+    · simp
+
+end Lawful
+
+section ToList
+
+theorem IterM.InternalConsumers.toList_filterMap {α β γ: Type w} {m : Type w → Type w'}
+    [Monad m] [LawfulMonad m]
+    [Iterator α m β] [IteratorCollect α m m] [LawfulIteratorCollect α m m] [Finite α m]
+    {f : β → Option γ} (it : IterM (α := α) m β) :
+    (it.filterMap f).toList = (fun x => x.filterMap f) <$> it.toList := by
+  induction it using IterM.inductSteps
+  rename_i it ihy ihs
+  rw [IterM.toList_eq_match_step, IterM.toList_eq_match_step]
+  simp only [bind_pure_comp, map_bind]
+  rw [step_filterMap]
+  simp only [bind_assoc, IterM.step, map_eq_pure_bind]
+  apply bind_congr
+  intro step
+  split
+  · simp only [List.filterMap_cons, bind_assoc, pure_bind]
+    split
+    · split
+      · simp only [bind_pure_comp, pure_bind]
+        exact ihy ‹_›
+      · simp_all
+    · split
+      · simp_all
+      · simp_all [ihy ‹_›]
+  · simp only [bind_pure_comp, pure_bind]
+    apply ihs
+    assumption
+  · simp
+
+theorem IterM.toList_filterMap {α β γ : Type w} {m : Type w → Type w'}
+    [Monad m] [LawfulMonad m]
+    [Iterator α m β] [IteratorCollect α m m] [LawfulIteratorCollect α m m] [Finite α m]
+    {f : β → Option γ} (it : IterM (α := α) m β) :
+    (it.filterMap f).toList = (fun x => x.filterMap f) <$> it.toList := by
+  induction it using IterM.inductSteps
+  rename_i it ihy ihs
+  rw [IterM.toList_eq_match_step, IterM.toList_eq_match_step]
+  simp only [bind_pure_comp, map_bind]
+  rw [step_filterMap]
+  simp only [bind_assoc, IterM.step, map_eq_pure_bind]
+  apply bind_congr
+  intro step
+  split
+  · simp only [List.filterMap_cons, bind_assoc, pure_bind]
+    split
+    · split
+      · simp only [bind_pure_comp, pure_bind]
+        exact ihy ‹_›
+      · simp_all
+    · split
+      · simp_all
+      · simp_all [ihy ‹_›]
+  · simp only [bind_pure_comp, pure_bind]
+    apply ihs
+    assumption
+  · simp
+
+theorem IterM.toList_map {α β β' : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
+    [Iterator α m β] [IteratorCollect α m m] [LawfulIteratorCollect α m m] [Finite α m] {f : β → β'}
+    (it : IterM (α := α) m β) :
+    (it.map f).toList = (fun x => x.map f) <$> it.toList := by
+  rw [LawfulIteratorCollect.toList_eq, ← List.filterMap_eq_map, ← toList_filterMap]
+  let t := type_of% (it.map f)
+  let t' := type_of% (it.filterMap (some ∘ f))
+  congr
+  · simp [Map]
+  · simp [instIteratorMap, inferInstanceAs]
+    congr
+    simp
+  · refine heq_of_eqRec_eq ?_ rfl
+    congr
+    simp only [Map, PostconditionT.map_pure, Function.comp_apply]
+    simp only [instIteratorMap, inferInstanceAs, Function.comp_apply]
+    congr
+    simp
+  · simp [Map]
+  · simp only [instIteratorMap, inferInstanceAs, Function.comp_apply]
+    congr
+    simp
+  · simp only [map, mapWithPostcondition, InternalCombinators.map, Function.comp_apply, filterMap,
+    filterMapWithPostcondition, InternalCombinators.filterMap]
+    congr
+    · simp [Map]
+    · simp
+
+theorem IterM.toList_filter {α : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
+    {β : Type w} [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {f : β → Bool} {it : IterM (α := α) m β} :
+    (it.filter f).toList = List.filter f <$> it.toList := by
+  simp only [filter, toList_filterMap, ← List.filterMap_eq_filter]
+  rfl
+
+end ToList
+
+section ToListRev
+
+theorem IterM.toListRev_filterMap {α β γ : Type w} {m : Type w → Type w'}
+    [Monad m] [LawfulMonad m]
+    [Iterator α m β] [IteratorCollect α m m] [LawfulIteratorCollect α m m] [Finite α m]
+    {f : β → Option γ} (it : IterM (α := α) m β) :
+    (it.filterMap f).toListRev = (fun x => x.filterMap f) <$> it.toListRev := by
+  simp [toListRev_eq, toList_filterMap]
+
+theorem IterM.toListRev_map {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
+    [Iterator α m β] [IteratorCollect α m m] [LawfulIteratorCollect α m m] [Finite α m] {f : β → γ}
+    (it : IterM (α := α) m β) :
+    (it.map f).toListRev = (fun x => x.map f) <$> it.toListRev := by
+  simp [toListRev_eq, toList_map]
+
+theorem IterM.toListRev_filter {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {f : β → Bool} {it : IterM (α := α) m β} :
+    (it.filter f).toListRev = List.filter f <$> it.toListRev := by
+  simp [toListRev_eq, toList_filter]
+
+end ToListRev
+
+section ToArray
+
+theorem IterM.toArray_filterMap {α β γ : Type w} {m : Type w → Type w'}
+    [Monad m] [LawfulMonad m]
+    [Iterator α m β] [IteratorCollect α m m] [LawfulIteratorCollect α m m] [Finite α m]
+    {f : β → Option γ} (it : IterM (α := α) m β) :
+    (it.filterMap f).toArray = (fun x => x.filterMap f) <$> it.toArray := by
+  simp [← toArray_toList, toList_filterMap]
+
+theorem IterM.toArray_map {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
+    [Iterator α m β] [IteratorCollect α m m] [LawfulIteratorCollect α m m] [Finite α m] {f : β → γ}
+    (it : IterM (α := α) m β) :
+    (it.map f).toArray = (fun x => x.map f) <$> it.toArray := by
+  simp [← toArray_toList, toList_map]
+
+theorem IterM.toArray_filter {α : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
+    {β : Type w} [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {f : β → Bool} {it : IterM (α := α) m β} :
+    (it.filter f).toArray = Array.filter f <$> it.toArray := by
+  simp [← toArray_toList, toList_filter]
+
+end ToArray
+
+end Std.Iterators
diff --git a/src/Init/Data/Iterators/PostconditionMonad.lean b/src/Init/Data/Iterators/PostconditionMonad.lean
index bd2e636798..923d2c6d1c 100644
--- a/src/Init/Data/Iterators/PostconditionMonad.lean
+++ b/src/Init/Data/Iterators/PostconditionMonad.lean
@@ -45,12 +45,12 @@ Caution: `lift` is not a lawful lift function.
 For example, `pure a : PostconditionT m α` is not the same as
 `PostconditionT.lift (pure a : m α)`.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 def PostconditionT.lift {α : Type w} {m : Type w → Type w'} [Functor m] (x : m α) :
     PostconditionT m α :=
   ⟨fun _ => True, (⟨·, .intro⟩) <$> x⟩
 
-@[always_inline, inline]
+@[always_inline, inline, expose]
 protected def PostconditionT.pure {m : Type w → Type w'} [Pure m] {α : Type w}
     (a : α) : PostconditionT m α :=
   ⟨fun y => a = y, pure <| ⟨a, rfl⟩⟩
@@ -70,7 +70,7 @@ turning `PostconditionT m` into a functor.
 The postcondition of the `x.map f` states that the return value is the image under `f` of some
 `a : α` satisfying the `x.Property`.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 protected def PostconditionT.map {m : Type w → Type w'} [Functor m] {α : Type w} {β : Type w}
     (f : α → β) (x : PostconditionT m α) : PostconditionT m β :=
   ⟨fun b => ∃ a : Subtype x.Property, f a.1 = b,
diff --git a/src/Init/Data/Iterators/ToIterator.lean b/src/Init/Data/Iterators/ToIterator.lean
new file mode 100644
index 0000000000..0d2451b628
--- /dev/null
+++ b/src/Init/Data/Iterators/ToIterator.lean
@@ -0,0 +1,110 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+import Init.Data.Iterators.Consumers
+
+/-!
+This module provides the typeclass `ToIterator`, which is implemented by types that can be
+converted into iterators.
+-/
+
+open Std.Iterators
+
+namespace Std.Iterators
+
+/--
+This typeclass provides an iterator for the given element `x : γ`. Usually, instances are provided
+for all elements of a type `γ`.
+-/
+class ToIterator {γ : Type u} (x : γ) (m : Type w → Type w') (β : outParam (Type w)) where
+  State : Type w
+  iterMInternal : IterM (α := State) m β
+
+/-- Converts `x` into a monadic iterator. -/
+@[always_inline, inline, expose]
+def ToIterator.iterM (x : γ) [ToIterator x m β] : IterM (α := ToIterator.State x m) m β :=
+  ToIterator.iterMInternal (x := x)
+
+/-- Converts `x` into a pure iterator. -/
+@[always_inline, inline, expose]
+def ToIterator.iter (x : γ) [ToIterator x Id β] : Iter (α := ToIterator.State x Id) β :=
+  ToIterator.iterM x |>.toIter
+
+/-- Creates a monadic `ToIterator` instance. -/
+@[always_inline, inline, expose]
+def ToIterator.ofM {x : γ} (State : Type w)
+    (iterM : IterM (α := State) m β) :
+    ToIterator x m β where
+  State := State
+  iterMInternal := iterM
+
+/-- Creates a pure `ToIterator` instance. -/
+@[always_inline, inline, expose]
+def ToIterator.of {x : γ} (State : Type w)
+    (iter : Iter (α := State) β) :
+    ToIterator x Id β where
+  State := State
+  iterMInternal := iter.toIterM
+
+/-!
+## Instance forwarding
+
+If the type defined as `ToIterator.State` implements an iterator typeclass, then this typeclass
+should also be available when the type is syntactically visible as `ToIteratorState`. The following
+instances are responsible for this forwarding.
+-/
+
+instance {x : γ} {State : Type w} {iter}
+    [Iterator State m β] :
+    letI i : ToIterator x m β := .ofM State iter
+    Iterator (α := i.State) m β :=
+  inferInstanceAs <| Iterator State m β
+
+instance {x : γ} {State : Type w} {iter}
+    [Iterator (α := State) m β] [Finite State m] :
+    letI i : ToIterator x m β := .ofM State iter
+    Finite (α := i.State) m :=
+  inferInstanceAs <| Finite (α := State) m
+
+instance {x : γ} {State : Type w} {iter}
+    [Iterator (α := State) m β] [IteratorCollect State m n] :
+    letI i : ToIterator x m β := .ofM State iter
+    IteratorCollect (α := i.State) m n :=
+  inferInstanceAs <| IteratorCollect (α := State) m n
+
+instance {x : γ} {State : Type w} {iter}
+    [Iterator (α := State) m β] [IteratorCollectPartial State m n] :
+    letI i : ToIterator x m β := .ofM State iter
+    IteratorCollectPartial (α := i.State) m n :=
+  inferInstanceAs <| IteratorCollectPartial (α := State) m n
+
+instance {x : γ} {State : Type w} {iter}
+    [Iterator (α := State) m β] [IteratorLoop State m n] :
+    letI i : ToIterator x m β := .ofM State iter
+    IteratorLoop (α := i.State) m n :=
+  inferInstanceAs <| IteratorLoop (α := State) m n
+
+instance {x : γ} {State : Type w} {iter}
+    [Iterator (α := State) m β] [IteratorLoopPartial State m n] :
+    letI i : ToIterator x m β := .ofM State iter
+    IteratorLoopPartial (α := i.State) m n :=
+  inferInstanceAs <| IteratorLoopPartial (α := State) m n
+
+instance {x : γ} {State : Type w} {iter}
+    [Iterator (α := State) m β] [IteratorSize State m] :
+    letI i : ToIterator x m β := .ofM State iter
+    IteratorSize (α := i.State) m :=
+  inferInstanceAs <| IteratorSize (α := State) m
+
+instance {x : γ} {State : Type w} {iter}
+    [Iterator (α := State) m β] [IteratorSizePartial State m] :
+    letI i : ToIterator x m β := .ofM State iter
+    IteratorSizePartial (α := i.State) m :=
+  inferInstanceAs <| IteratorSizePartial (α := State) m
+
+end Std.Iterators
diff --git a/src/Init/Data/Range/Polymorphic/Basic.lean b/src/Init/Data/Range/Polymorphic/Basic.lean
index 1364574483..370af75d89 100644
--- a/src/Init/Data/Range/Polymorphic/Basic.lean
+++ b/src/Init/Data/Range/Polymorphic/Basic.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 import Init.Data.Range.Polymorphic.RangeIterator
+import Init.Data.Iterators.Combinators.Attach
 
 open Std.Iterators
 
diff --git a/src/Init/Data/Range/Polymorphic/Nat.lean b/src/Init/Data/Range/Polymorphic/Nat.lean
index 4853aae7a2..f6a83b0ae4 100644
--- a/src/Init/Data/Range/Polymorphic/Nat.lean
+++ b/src/Init/Data/Range/Polymorphic/Nat.lean
@@ -145,4 +145,86 @@ instance : LawfulRangeSize .open Nat where
       Option.some.injEq] at hu h ⊢
     omega
 
+instance : ClosedOpenIntersection ⟨.open, .open⟩ Nat where
+  intersection r s := PRange.mk (max (r.lower + 1) s.lower) (min r.upper s.upper)
+
+example (h : b + 1 ≤ a) : b < a := by omega
+
+instance : LawfulClosedOpenIntersection ⟨.open, .open⟩ Nat where
+  mem_intersection_iff {a r s} := by
+    simp only [ClosedOpenIntersection.intersection, Membership.mem, SupportsLowerBound.IsSatisfied,
+      SupportsUpperBound.IsSatisfied, Nat.max_le, Nat.lt_min, Bound]
+    omega
+
+instance : ClosedOpenIntersection ⟨.open, .closed⟩ Nat where
+  intersection r s := PRange.mk (max (r.lower + 1) s.lower) (min (r.upper + 1) s.upper)
+
+instance : LawfulClosedOpenIntersection ⟨.open, .closed⟩ Nat where
+  mem_intersection_iff {a r s} := by
+    simp only [ClosedOpenIntersection.intersection, Membership.mem, SupportsLowerBound.IsSatisfied,
+      SupportsUpperBound.IsSatisfied, Nat.max_le, Nat.lt_min, Bound]
+    omega
+
+instance : ClosedOpenIntersection ⟨.open, .unbounded⟩ Nat where
+  intersection r s := PRange.mk (max (r.lower + 1) s.lower) s.upper
+
+instance : LawfulClosedOpenIntersection ⟨.open, .unbounded⟩ Nat where
+  mem_intersection_iff {a r s} := by
+    simp only [Membership.mem, SupportsLowerBound.IsSatisfied, Bound,
+      ClosedOpenIntersection.intersection, Nat.max_le, SupportsUpperBound.IsSatisfied, and_true]
+    omega
+
+instance : ClosedOpenIntersection ⟨.closed, .open⟩ Nat where
+  intersection r s := PRange.mk (max r.lower s.lower) (min r.upper s.upper)
+
+instance : LawfulClosedOpenIntersection ⟨.closed, .open⟩ Nat where
+  mem_intersection_iff {a r s} := by
+    simp only [ClosedOpenIntersection.intersection, Membership.mem, SupportsLowerBound.IsSatisfied,
+      SupportsUpperBound.IsSatisfied, Nat.max_le, Nat.lt_min, Bound]
+    omega
+
+instance : ClosedOpenIntersection ⟨.closed, .closed⟩ Nat where
+  intersection r s := PRange.mk (max r.lower s.lower) (min (r.upper + 1) s.upper)
+
+instance : LawfulClosedOpenIntersection ⟨.closed, .closed⟩ Nat where
+  mem_intersection_iff {a r s} := by
+    simp only [ClosedOpenIntersection.intersection, Membership.mem, SupportsLowerBound.IsSatisfied,
+      SupportsUpperBound.IsSatisfied, Nat.max_le, Nat.lt_min, Bound]
+    omega
+
+instance : ClosedOpenIntersection ⟨.closed, .unbounded⟩ Nat where
+  intersection r s := PRange.mk (max r.lower s.lower) s.upper
+
+instance : LawfulClosedOpenIntersection ⟨.closed, .unbounded⟩ Nat where
+  mem_intersection_iff {a r s} := by
+    simp only [Membership.mem, SupportsLowerBound.IsSatisfied, Bound,
+      ClosedOpenIntersection.intersection, Nat.max_le, SupportsUpperBound.IsSatisfied, and_true]
+    omega
+
+instance : ClosedOpenIntersection ⟨.unbounded, .open⟩ Nat where
+  intersection r s := PRange.mk s.lower (min r.upper s.upper)
+
+instance : LawfulClosedOpenIntersection ⟨.unbounded, .open⟩ Nat where
+  mem_intersection_iff {a r s} := by
+    simp only [Membership.mem, SupportsLowerBound.IsSatisfied, Bound,
+      ClosedOpenIntersection.intersection, SupportsUpperBound.IsSatisfied, true_and]
+    omega
+
+instance : ClosedOpenIntersection ⟨.unbounded, .closed⟩ Nat where
+  intersection r s := PRange.mk s.lower (min (r.upper + 1) s.upper)
+
+instance : LawfulClosedOpenIntersection ⟨.unbounded, .closed⟩ Nat where
+  mem_intersection_iff {a r s} := by
+    simp only [Membership.mem, SupportsLowerBound.IsSatisfied, Bound,
+      ClosedOpenIntersection.intersection, SupportsUpperBound.IsSatisfied, true_and]
+    omega
+
+instance : ClosedOpenIntersection ⟨.unbounded, .unbounded⟩ Nat where
+  intersection _ s := s
+
+instance : LawfulClosedOpenIntersection ⟨.unbounded, .unbounded⟩ Nat where
+  mem_intersection_iff {a r s} := by
+    simp [Membership.mem, SupportsLowerBound.IsSatisfied, Bound,
+      ClosedOpenIntersection.intersection, SupportsUpperBound.IsSatisfied]
+
 end Std.PRange
diff --git a/src/Init/Data/Range/Polymorphic/PRange.lean b/src/Init/Data/Range/Polymorphic/PRange.lean
index b57194d010..1ebd6cf3c5 100644
--- a/src/Init/Data/Range/Polymorphic/PRange.lean
+++ b/src/Init/Data/Range/Polymorphic/PRange.lean
@@ -7,12 +7,8 @@ module
 
 prelude
 import Init.Core
-import Init.NotationExtra
-import Init.Data.Iterators.Consumers
 import Init.Data.Range.Polymorphic.UpwardEnumerable
 
-open Std.Iterators
-
 namespace Std.PRange
 
 /--
@@ -299,4 +295,30 @@ instance {α} [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumer
 instance {α} [UpwardEnumerable α] : LawfulUnboundedUpperBound α where
   isSatisfied u a := by simp [SupportsUpperBound.IsSatisfied]
 
+/--
+This typeclass allows taking the intersection of ranges of the given shape and half-open ranges.
+
+An element should be contained in the intersection if and only if it is contained in both ranges.
+This is encoded in `LawfulClosedOpenIntersection`.
+-/
+class ClosedOpenIntersection (shape : RangeShape) (α : Type w) where
+  intersection : PRange shape α → PRange ⟨.closed, .open⟩ α → PRange ⟨.closed, .open⟩ α
+
+/--
+This typeclass ensures that the intersection according to `ClosedOpenIntersection shape α`
+of two ranges contains exactly those elements that are contained in both ranges.
+-/
+class LawfulClosedOpenIntersection (shape : RangeShape) (α : Type w)
+    [ClosedOpenIntersection shape α]
+    [SupportsLowerBound shape.lower α] [SupportsUpperBound shape.upper α]
+    [SupportsLowerBound .closed α]
+    [SupportsUpperBound .open α] where
+  /--
+  The intersection according to `ClosedOpenIntersection shapee α` of two ranges contains exactly
+  those elements that are contained in both ranges.
+  -/
+  mem_intersection_iff {a : α} {r : PRange ⟨shape.lower, shape.upper⟩ α}
+      {s : PRange ⟨.closed, .open⟩ α} :
+    a ∈ ClosedOpenIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s
+
 end Std.PRange
diff --git a/src/Init/Data/Range/Polymorphic/RangeIterator.lean b/src/Init/Data/Range/Polymorphic/RangeIterator.lean
index fd2c4bc6c6..e43dcae3ae 100644
--- a/src/Init/Data/Range/Polymorphic/RangeIterator.lean
+++ b/src/Init/Data/Range/Polymorphic/RangeIterator.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 import Init.Data.Iterators.Internal.Termination
+import Init.Data.Iterators.Consumers.Access
 import Init.Data.Iterators.Consumers.Loop
 import Init.Data.Iterators.Consumers.Collect
 import Init.Data.Range.Polymorphic.PRange
diff --git a/src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean b/src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean
index 9e8ff71ee6..a2ef3ede4d 100644
--- a/src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean
+++ b/src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean
@@ -10,7 +10,6 @@ import Init.Classical
 import Init.Core
 import Init.Data.Nat.Basic
 import Init.Data.Option.Lemmas
-import Init.NotationExtra
 
 namespace Std.PRange
 
@@ -67,7 +66,7 @@ The typeclass `Least? α` optionally provides a smallest element of `α`, `least
 The main use case of this typeclass is to use it in combination with `UpwardEnumerable` to
 obtain a (possibly infinite) ascending enumeration of all elements of `α`.
 -/
-class Least? (α : Type u) extends UpwardEnumerable α where
+class Least? (α : Type u) where
   /--
   Returns the smallest element of `α`, or none if `α` is empty.
 
diff --git a/src/Init/Data/Slice.lean b/src/Init/Data/Slice.lean
new file mode 100644
index 0000000000..cd1102591c
--- /dev/null
+++ b/src/Init/Data/Slice.lean
@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+import Init.Data.Slice.Basic
+import Init.Data.Slice.Notation
+import Init.Data.Slice.Operations
+import Init.Data.Slice.Array
+
+/-!
+# Polymorphic slices
+
+This module provides slices -- views on a subset of all elements of an array or other collection,
+demarcated by a range of indices.
+
+* `Init.Data.Slice.Basic` defines the `Slice` structure. All slices are of this type.
+* `Init.Data.Slice.Operations` provides functions on `Slice` via dot notation. Many of them are
+  implemented using iterators under the hood.
+* `Init.Data.Slice.Notation` provides slice notation based on ranges, relying on the `Sliceable`
+  typeclass.
+* `Init.Data.Slice.Array` provides the `Sliceable` instance for array slices.
+-/
diff --git a/src/Init/Data/Slice/Array.lean b/src/Init/Data/Slice/Array.lean
new file mode 100644
index 0000000000..76865966e0
--- /dev/null
+++ b/src/Init/Data/Slice/Array.lean
@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+import Init.Core
+import Init.Data.Array.Subarray
+import Init.Data.Iterators.Combinators.Attach
+import Init.Data.Iterators.Combinators.FilterMap
+import all Init.Data.Range.Polymorphic.Basic
+import Init.Data.Range.Polymorphic.Nat
+import Init.Data.Slice.Operations
+
+/-!
+This module provides slice notation for array slices (a.k.a. `Subarray`) and implements an iterator
+for those slices.
+-/
+
+open Std Slice PRange Iterators
+
+instance {shape} {α : Type u} [ClosedOpenIntersection shape Nat] :
+    Sliceable shape (Array α) Nat (Subarray α) where
+  mkSlice xs range :=
+    let halfOpenRange := ClosedOpenIntersection.intersection range (0)...<xs.size
+    (xs.toSubarray halfOpenRange.lower halfOpenRange.upper)
+
+instance {s : Subarray α} : ToIterator s Id α :=
+  .of _
+    (PRange.Internal.iter (s.internalRepresentation.start...<s.internalRepresentation.stop)
+      |>.attachWith (· < s.internalRepresentation.array.size) ?h
+      |>.map fun i => s.internalRepresentation.array[i.1])
+where finally
+  case h =>
+    simp only [Internal.isPlausibleIndirectOutput_iter_iff, Membership.mem,
+      SupportsUpperBound.IsSatisfied, and_imp]
+    intro out _ h
+    have := s.internalRepresentation.stop_le_array_size
+    omega
diff --git a/src/Init/Data/Slice/Basic.lean b/src/Init/Data/Slice/Basic.lean
new file mode 100644
index 0000000000..2a485daeef
--- /dev/null
+++ b/src/Init/Data/Slice/Basic.lean
@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+import Init.Core
+
+namespace Std.Slice
+
+/--
+Wrapper structure for slice types that makes generic slice functions available via dot notation.
+The implementation of the functions depends on the type `γ` of the internal representation.
+
+Usually, if `γ` is the internal representation of a slice of some type `α`, then `Slice γ` can be
+used directly, but one usually creates an abbreviation `AlphaSlice := Slice γ` and provides
+`Self (Slice γ) AlphaSlice` and `Sliceable shape α AlphaSlice` instances. Then `AlphaSlice` can
+be worked with without ever thinking of `Slice` and it is possible to extend the API with
+`α`/`γ`-specific functions.
+-/
+structure _root_.Std.Slice (γ : Type u) where
+  internalRepresentation : γ
+
+/--
+This typeclass determines that some type `α` is equal to `β` and that `β` should be used in APIs
+instead of `α`.
+
+`Self` is used in the polymorphic slice library.
+-/
+class Self (α : Type u) (β : outParam (Type u)) where
+  eq : α = β := by rfl
+
+end Std.Slice
diff --git a/src/Init/Data/Slice/Notation.lean b/src/Init/Data/Slice/Notation.lean
new file mode 100644
index 0000000000..39ec13b81f
--- /dev/null
+++ b/src/Init/Data/Slice/Notation.lean
@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+import Init.Data.Range.Polymorphic.PRange
+
+/-!
+# Slice notation
+
+This module provides the means to obtain a slice from a collection and a range of indices via
+slice notation.
+-/
+
+open Std PRange
+
+namespace Std.Slice
+
+/--
+This typeclass indicates how to obtain slices of `α` of type `γ`, given ranges of shape `shape` in
+the index type `β`.
+-/
+class Sliceable (shape : RangeShape) (α : Type u) (β : outParam (Type v))
+    (γ : outParam (Type w)) where
+  mkSlice (carrier : α) (range : PRange shape β) : γ
+
+macro_rules
+  | `($c[*...*]) => `(Sliceable.mkSlice $c *...*)
+  | `($c[$a...*]) => `(Sliceable.mkSlice $c $a...*)
+  | `($c[$a<...*]) => `(Sliceable.mkSlice $c $a<...*)
+  | `($c[*...<$b]) => `(Sliceable.mkSlice $c *...<$b)
+  | `($c[$a...<$b]) => `(Sliceable.mkSlice $c $a...<$b)
+  | `($c[$a<...<$b]) => `(Sliceable.mkSlice $c $a<...<$b)
+  | `($c[*...$b]) => `(Sliceable.mkSlice $c *...<$b)
+  | `($c[$a...$b]) => `(Sliceable.mkSlice $c $a...<$b)
+  | `($c[$a<...$b]) => `(Sliceable.mkSlice $c $a<...<$b)
+  | `($c[*...=$b]) => `(Sliceable.mkSlice $c *...=$b)
+  | `($c[$a...=$b]) => `(Sliceable.mkSlice $c $a...=$b)
+  | `($c[$a<...=$b]) => `(Sliceable.mkSlice $c $a<...=$b)
+
+end Std.Slice
diff --git a/src/Init/Data/Slice/Operations.lean b/src/Init/Data/Slice/Operations.lean
new file mode 100644
index 0000000000..4ab6d41bd1
--- /dev/null
+++ b/src/Init/Data/Slice/Operations.lean
@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+import Init.Data.Slice.Basic
+import Init.Data.Slice.Notation
+import Init.Data.Iterators
+
+open Std.Iterators
+
+namespace Std.Slice
+
+instance {x : γ} [ToIterator x m β] : ToIterator (Slice.mk x) m β where
+  State := ToIterator.State x m
+  iterMInternal := ToIterator.iterMInternal
+
+/--
+Internal function to obtain an iterator from a slice. Users should import `Std.Data.Iterators`
+and use `Std.Slice.iter` instead.
+-/
+@[always_inline, inline]
+def Internal.iter (s : Slice γ) [ToIterator s Id β] :=
+  ToIterator.iter s
+
+/--
+Returns the number of elements with distinct indices in the given slice.
+
+Example: `#[1, 1, 1][0...2].size = 2`.
+-/
+@[always_inline, inline]
+def size (s : Slice g) [ToIterator s Id β] [Iterator (ToIterator.State s Id) Id β]
+    [IteratorSize (ToIterator.State s Id) Id] :=
+  Internal.iter s |>.size
+
+/-- Allocates a new array that contains the elements of the slice. -/
+@[always_inline, inline]
+def toArray (s : Slice g) [ToIterator s Id β] [Iterator (ToIterator.State s Id) Id β]
+    [IteratorCollect (ToIterator.State s Id) Id Id] [Finite (ToIterator.State s Id) Id] : Array β :=
+  Internal.iter s |>.toArray
+
+/-- Allocates a new list that contains the elements of the slice. -/
+@[always_inline, inline]
+def toList (s : Slice g) [ToIterator s Id β] [Iterator (ToIterator.State s Id) Id β]
+    [IteratorCollect (ToIterator.State s Id) Id Id] [Finite (ToIterator.State s Id) Id] : List β :=
+  Internal.iter s |>.toList
+
+/-- Allocates a new list that contains the elements of the slice in reverse order. -/
+@[always_inline, inline]
+def toListRev (s : Slice g) [ToIterator s Id β] [Iterator (ToIterator.State s Id) Id β]
+    [IteratorCollect (ToIterator.State s Id) Id Id] [Finite (ToIterator.State s Id) Id] : List β :=
+  Internal.iter s |>.toListRev
+
+end Std.Slice
diff --git a/src/Init/Data/Stream.lean b/src/Init/Data/Stream.lean
index 843d9007a5..cd87363564 100644
--- a/src/Init/Data/Stream.lean
+++ b/src/Init/Data/Stream.lean
@@ -97,7 +97,7 @@ instance : Stream (Subarray α) α where
     if h : s.start < s.stop then
       have : s.start + 1 ≤ s.stop := Nat.succ_le_of_lt h
       some (s.array[s.start]'(Nat.lt_of_lt_of_le h s.stop_le_array_size),
-        { s with start := s.start + 1, start_le_stop := this })
+        ⟨{ s.internalRepresentation with start := s.start + 1, start_le_stop := this }⟩)
     else
       none
 
diff --git a/src/Std/Data/Iterators/Combinators.lean b/src/Std/Data/Iterators/Combinators.lean
index 9e9546f398..866303ff27 100644
--- a/src/Std/Data/Iterators/Combinators.lean
+++ b/src/Std/Data/Iterators/Combinators.lean
@@ -9,6 +9,5 @@ import Std.Data.Iterators.Combinators.Take
 import Std.Data.Iterators.Combinators.TakeWhile
 import Std.Data.Iterators.Combinators.Drop
 import Std.Data.Iterators.Combinators.DropWhile
-import Std.Data.Iterators.Combinators.FilterMap
 import Std.Data.Iterators.Combinators.StepSize
 import Std.Data.Iterators.Combinators.Zip
diff --git a/src/Std/Data/Iterators/Combinators/Monadic.lean b/src/Std/Data/Iterators/Combinators/Monadic.lean
index 8fc31c6ff4..6db558e4ca 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic.lean
@@ -8,6 +8,5 @@ import Std.Data.Iterators.Combinators.Monadic.Take
 import Std.Data.Iterators.Combinators.Monadic.TakeWhile
 import Std.Data.Iterators.Combinators.Monadic.Drop
 import Std.Data.Iterators.Combinators.Monadic.DropWhile
-import Std.Data.Iterators.Combinators.Monadic.FilterMap
 import Std.Data.Iterators.Combinators.Monadic.StepSize
 import Std.Data.Iterators.Combinators.Monadic.Zip
diff --git a/src/Std/Data/Iterators/Combinators/Monadic/Take.lean b/src/Std/Data/Iterators/Combinators/Monadic/Take.lean
index 1c46262aaa..97665a64ac 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/Take.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic/Take.lean
@@ -130,7 +130,7 @@ instance Take.instFinite [Monad m] [Iterator α m β] [Productive α m] :
     Finite (Take α m β) m :=
   Finite.of_finitenessRelation instFinitenessRelation
 
-instance Take.instIteratorCollect [Monad m] [Monad n] [Iterator α m β] [Productive α m] :
+instance Take.instIteratorCollect [Monad m] [Monad n] [Iterator α m β] :
     IteratorCollect (Take α m β) m n :=
   .defaultImplementation
 
@@ -139,12 +139,12 @@ instance Take.instIteratorCollectPartial [Monad m] [Monad n] [Iterator α m β]
   .defaultImplementation
 
 instance Take.instIteratorLoop [Monad m] [Monad n] [Iterator α m β]
-    [IteratorLoop α m n] [MonadLiftT m n] :
+    [MonadLiftT m n] :
     IteratorLoop (Take α m β) m n :=
   .defaultImplementation
 
 instance Take.instIteratorLoopPartial [Monad m] [Monad n] [Iterator α m β]
-    [IteratorLoopPartial α m n] [MonadLiftT m n] :
+    [MonadLiftT m n] :
     IteratorLoopPartial (Take α m β) m n :=
   .defaultImplementation
 
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators.lean b/src/Std/Data/Iterators/Lemmas/Combinators.lean
index d66dfd214b..df7f27f027 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators.lean
@@ -9,5 +9,4 @@ import Std.Data.Iterators.Lemmas.Combinators.Take
 import Std.Data.Iterators.Lemmas.Combinators.TakeWhile
 import Std.Data.Iterators.Lemmas.Combinators.Drop
 import Std.Data.Iterators.Lemmas.Combinators.DropWhile
-import Std.Data.Iterators.Lemmas.Combinators.FilterMap
 import Std.Data.Iterators.Lemmas.Combinators.Zip
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
index b716f7a6ee..6045a42435 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
@@ -4,414 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
 prelude
-import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
-import Std.Data.Iterators.Combinators.Monadic.FilterMap
-import Init.Data.Iterators.Lemmas.Consumers.Monadic
+import Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
 import Std.Data.Iterators.Lemmas.Equivalence.StepCongr
 
 namespace Std.Iterators
 open Std.Internal
 
-section Step
-
-variable {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
-  [Iterator α m β] {it : IterM (α := α) m β}
-
-theorem IterM.step_filterMapWithPostcondition {f : β → PostconditionT n (Option β')}
-    [Monad n] [LawfulMonad n] [MonadLiftT m n] :
-  (it.filterMapWithPostcondition f).step = (do
-    match ← it.step with
-    | .yield it' out h => do
-      match ← (f out).operation with
-      | ⟨none, h'⟩ =>
-        pure <| .skip (it'.filterMapWithPostcondition f) (.yieldNone (out := out) h h')
-      | ⟨some out', h'⟩ =>
-        pure <| .yield (it'.filterMapWithPostcondition f) out' (.yieldSome (out := out) h h')
-    | .skip it' h =>
-      pure <| .skip (it'.filterMapWithPostcondition f) (.skip h)
-    | .done h =>
-      pure <| .done (.done h)) := by
-  apply bind_congr
-  intro step
-  match step with
-  | .yield it' out h =>
-    simp only [PlausibleIterStep.skip, PlausibleIterStep.yield]
-    apply bind_congr
-    intro step
-    rcases step with _ | _ <;> rfl
-  | .skip it' h => rfl
-  | .done h => rfl
-
-theorem IterM.step_filterWithPostcondition {f : β → PostconditionT n (ULift Bool)}
-    [Monad n] [LawfulMonad n] [MonadLiftT m n] :
-  (it.filterWithPostcondition f).step = (do
-    match ← it.step with
-    | .yield it' out h => do
-      match ← (f out).operation with
-      | ⟨.up false, h'⟩ =>
-        pure <| .skip (it'.filterWithPostcondition f) (.yieldNone (out := out) h ⟨⟨_, h'⟩, rfl⟩)
-      | ⟨.up true, h'⟩ =>
-        pure <| .yield (it'.filterWithPostcondition f) out (.yieldSome (out := out) h ⟨⟨_, h'⟩, rfl⟩)
-    | .skip it' h =>
-      pure <| .skip (it'.filterWithPostcondition f) (.skip h)
-    | .done h =>
-      pure <| .done (.done h)) := by
-  apply bind_congr
-  intro step
-  match step with
-  | .yield it' out h =>
-    simp only [PostconditionT.operation_map, PlausibleIterStep.skip, PlausibleIterStep.yield,
-      bind_map_left]
-    apply bind_congr
-    intro step
-    rcases step with _ | _ <;> rfl
-  | .skip it' h => rfl
-  | .done h => rfl
-
-theorem IterM.step_mapWithPostcondition {γ : Type w} {f : β → PostconditionT n γ}
-    [Monad n] [LawfulMonad n] [MonadLiftT m n] :
-  (it.mapWithPostcondition f).step = (do
-    match ← it.step with
-    | .yield it' out h => do
-      let out' ← (f out).operation
-      pure <| .yield (it'.mapWithPostcondition f) out'.1 (.yieldSome h ⟨out', rfl⟩)
-    | .skip it' h =>
-      pure <| .skip (it'.mapWithPostcondition f) (.skip h)
-    | .done h =>
-      pure <| .done (.done h)) := by
-  apply bind_congr
-  intro step
-  match step with
-  | .yield it' out h =>
-    simp only [PostconditionT.operation_map, bind_map_left, bind_pure_comp]
-    rfl
-  | .skip it' h => rfl
-  | .done h => rfl
-
-theorem IterM.step_filterMapM {f : β → n (Option β')}
-    [Monad n] [LawfulMonad n] [MonadLiftT m n] :
-  (it.filterMapM f).step = (do
-    match ← it.step with
-    | .yield it' out h => do
-      match ← f out with
-      | none =>
-        pure <| .skip (it'.filterMapM f) (.yieldNone (out := out) h .intro)
-      | some out' =>
-        pure <| .yield (it'.filterMapM f) out' (.yieldSome (out := out) h .intro)
-    | .skip it' h =>
-      pure <| .skip (it'.filterMapM f) (.skip h)
-    | .done h =>
-      pure <| .done (.done h)) := by
-  apply bind_congr
-  intro step
-  match step with
-  | .yield it' out h =>
-    simp only [PostconditionT.lift, bind_map_left]
-    apply bind_congr
-    intro step
-    rcases step with _ | _ <;> rfl
-  | .skip it' h => rfl
-  | .done h => rfl
-
-theorem IterM.step_filterM {f : β → n (ULift Bool)}
-    [Monad n] [LawfulMonad n] [MonadLiftT m n] :
-  (it.filterM f).step = (do
-    match ← it.step with
-    | .yield it' out h => do
-      match ← f out with
-      | .up false =>
-        pure <| .skip (it'.filterM f) (.yieldNone (out := out) h ⟨⟨.up false, .intro⟩, rfl⟩)
-      | .up true =>
-        pure <| .yield (it'.filterM f) out (.yieldSome (out := out) h ⟨⟨.up true, .intro⟩, rfl⟩)
-    | .skip it' h =>
-      pure <| .skip (it'.filterM f) (.skip h)
-    | .done h =>
-      pure <| .done (.done h)) := by
-  apply bind_congr
-  intro step
-  match step with
-  | .yield it' out h =>
-    simp only [PostconditionT.lift,
-      PostconditionT.operation_map, Functor.map_map, PlausibleIterStep.skip,
-      PlausibleIterStep.yield, bind_map_left]
-    apply bind_congr
-    intro step
-    rcases step with _ | _ <;> rfl
-  | .skip it' h => rfl
-  | .done h => rfl
-
-theorem IterM.step_mapM {γ : Type w} {f : β → n γ}
-    [Monad n] [LawfulMonad n] [MonadLiftT m n] :
-  (it.mapM f).step = (do
-    match ← it.step with
-    | .yield it' out h => do
-      let out' ← f out
-      pure <| .yield (it'.mapM f) out' (.yieldSome h ⟨⟨out', True.intro⟩, rfl⟩)
-    | .skip it' h =>
-      pure <| .skip (it'.mapM f) (.skip h)
-    | .done h =>
-      pure <| .done (.done h)) := by
-  apply bind_congr
-  intro step
-  match step with
-  | .yield it' out h =>
-    simp only [bind_pure_comp]
-    simp only [PostconditionT.lift, Functor.map,
-      ]
-    simp only [PostconditionT.operation_map, Functor.map_map, PlausibleIterStep.skip,
-      PlausibleIterStep.yield, bind_map_left, bind_pure_comp]
-    rfl
-  | .skip it' h => rfl
-  | .done h => rfl
-
-theorem IterM.step_filterMap [Monad m] [LawfulMonad m] {f : β → Option β'} :
-  (it.filterMap f).step = (do
-    match ← it.step with
-    | .yield it' out h => do
-      match h' : f out with
-      | none =>
-        pure <| .skip (it'.filterMap f) (.yieldNone h h')
-      | some out' =>
-        pure <| .yield (it'.filterMap f) out' (.yieldSome h h')
-    | .skip it' h =>
-      pure <| .skip (it'.filterMap f) (.skip h)
-    | .done h =>
-      pure <| .done (.done h)) := by
-  simp only [IterM.filterMap, step_filterMapWithPostcondition, pure]
-  apply bind_congr
-  intro step
-  split
-  · simp only [PostconditionT.pure, PlausibleIterStep.skip, PlausibleIterStep.yield, pure_bind]
-    split <;> split <;> simp_all
-  · simp
-  · simp
-
-theorem IterM.step_map [Monad m] [LawfulMonad m] {f : β → β'} :
-  (it.map f).step = (do
-    match ← it.step with
-    | .yield it' out h =>
-      let out' := f out
-      pure <| .yield (it'.map f) out' (.yieldSome h ⟨⟨out', rfl⟩, rfl⟩)
-    | .skip it' h =>
-      pure <| .skip (it'.map f) (.skip h)
-    | .done h => pure <| .done (.done h)) := by
-  simp only [map, IterM.step_mapWithPostcondition]
-  apply bind_congr
-  intro step
-  split
-  · simp
-  · rfl
-  · rfl
-
-theorem IterM.step_filter [Monad m] [LawfulMonad m] {f : β → Bool} :
-  (it.filter f).step = (do
-    match ← it.step with
-    | .yield it' out h =>
-      if h' : f out = true then
-        pure <| .yield (it'.filter f) out (.yieldSome h (by simp [h']))
-      else
-        pure <| .skip (it'.filter f) (.yieldNone h (by simp [h']))
-    | .skip it' h =>
-      pure <| .skip (it'.filter f) (.skip h)
-    | .done h => pure <| .done (.done h)) := by
-  simp only [filter, IterM.step_filterMap]
-  apply bind_congr
-  intro step
-  split
-  · split
-    · split
-      · exfalso; simp_all
-      · rfl
-    · split
-      · congr; simp_all
-      · exfalso; simp_all
-  · rfl
-  · rfl
-
-end Step
-
-section Lawful
-
-instance {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type x}
-    [Monad m] [Monad n] [Monad o] [LawfulMonad n] [LawfulMonad o] [Iterator α m β] [Finite α m]
-    [IteratorCollect α m o] [LawfulIteratorCollect α m o]
-    {lift : ⦃δ : Type w⦄ -> m δ → n δ} {f : β → PostconditionT n γ} [LawfulMonadLiftFunction lift] :
-    LawfulIteratorCollect (Map α m n lift f) n o where
-  lawful_toArrayMapped := by
-    intro δ lift' _ _
-    letI : MonadLift m n := ⟨lift (δ := _)⟩
-    letI : MonadLift n o := ⟨lift' (α := _)⟩
-    ext g it
-    have : it = IterM.mapWithPostcondition _ it.internalState.inner := by rfl
-    generalize it.internalState.inner = it at *
-    cases this
-    simp only [LawfulIteratorCollect.toArrayMapped_eq]
-    simp only [IteratorCollect.toArrayMapped]
-    rw [LawfulIteratorCollect.toArrayMapped_eq]
-    induction it using IterM.inductSteps with | step it ih_yield ih_skip =>
-    rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
-    rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
-    simp only [bind_assoc]
-    rw [IterM.step_mapWithPostcondition]
-    simp only [liftM_bind (m := n) (n := o), bind_assoc]
-    apply bind_congr
-    intro step
-    cases step using PlausibleIterStep.casesOn
-    · simp only [bind_pure_comp]
-      simp only [liftM_map, bind_map_left]
-      apply bind_congr
-      intro out'
-      simp only [← ih_yield ‹_›]
-      rfl
-    · simp only [bind_pure_comp, pure_bind, liftM_pure, pure_bind, ← ih_skip ‹_›]
-      simp only [IterM.mapWithPostcondition, IterM.InternalCombinators.map, internalState_toIterM]
-    · simp
-
-end Lawful
-
-section ToList
-
-theorem IterM.InternalConsumers.toList_filterMap {α β γ: Type w} {m : Type w → Type w'}
-    [Monad m] [LawfulMonad m]
-    [Iterator α m β] [IteratorCollect α m m] [LawfulIteratorCollect α m m] [Finite α m]
-    {f : β → Option γ} (it : IterM (α := α) m β) :
-    (it.filterMap f).toList = (fun x => x.filterMap f) <$> it.toList := by
-  induction it using IterM.inductSteps
-  rename_i it ihy ihs
-  rw [IterM.toList_eq_match_step, IterM.toList_eq_match_step]
-  simp only [bind_pure_comp, map_bind]
-  rw [step_filterMap]
-  simp only [bind_assoc, IterM.step, map_eq_pure_bind]
-  apply bind_congr
-  intro step
-  split
-  · simp only [List.filterMap_cons, bind_assoc, pure_bind]
-    split
-    · split
-      · simp only [bind_pure_comp, pure_bind]
-        exact ihy ‹_›
-      · simp_all
-    · split
-      · simp_all
-      · simp_all [ihy ‹_›]
-  · simp only [bind_pure_comp, pure_bind]
-    apply ihs
-    assumption
-  · simp
-
-theorem IterM.toList_filterMap {α β γ : Type w} {m : Type w → Type w'}
-    [Monad m] [LawfulMonad m]
-    [Iterator α m β] [IteratorCollect α m m] [LawfulIteratorCollect α m m] [Finite α m]
-    {f : β → Option γ} (it : IterM (α := α) m β) :
-    (it.filterMap f).toList = (fun x => x.filterMap f) <$> it.toList := by
-  induction it using IterM.inductSteps
-  rename_i it ihy ihs
-  rw [IterM.toList_eq_match_step, IterM.toList_eq_match_step]
-  simp only [bind_pure_comp, map_bind]
-  rw [step_filterMap]
-  simp only [bind_assoc, IterM.step, map_eq_pure_bind]
-  apply bind_congr
-  intro step
-  split
-  · simp only [List.filterMap_cons, bind_assoc, pure_bind]
-    split
-    · split
-      · simp only [bind_pure_comp, pure_bind]
-        exact ihy ‹_›
-      · simp_all
-    · split
-      · simp_all
-      · simp_all [ihy ‹_›]
-  · simp only [bind_pure_comp, pure_bind]
-    apply ihs
-    assumption
-  · simp
-
-theorem IterM.toList_map {α β β' : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
-    [Iterator α m β] [IteratorCollect α m m] [LawfulIteratorCollect α m m] [Finite α m] {f : β → β'}
-    (it : IterM (α := α) m β) :
-    (it.map f).toList = (fun x => x.map f) <$> it.toList := by
-  rw [LawfulIteratorCollect.toList_eq, ← List.filterMap_eq_map, ← toList_filterMap]
-  let t := type_of% (it.map f)
-  let t' := type_of% (it.filterMap (some ∘ f))
-  congr
-  · simp [Map]
-  · simp [instIteratorMap, inferInstanceAs]
-    congr
-    simp
-  · refine heq_of_eqRec_eq ?_ rfl
-    congr
-    simp only [Map, PostconditionT.map_pure, Function.comp_apply]
-    simp only [instIteratorMap, inferInstanceAs, Function.comp_apply]
-    congr
-    simp
-  · simp [Map]
-  · simp only [instIteratorMap, inferInstanceAs, Function.comp_apply]
-    congr
-    simp
-  · simp only [map, mapWithPostcondition, InternalCombinators.map, Function.comp_apply, filterMap,
-    filterMapWithPostcondition, InternalCombinators.filterMap]
-    congr
-    · simp [Map]
-    · simp
-
-theorem IterM.toList_filter {α : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
-    {β : Type w} [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
-    {f : β → Bool} {it : IterM (α := α) m β} :
-    (it.filter f).toList = List.filter f <$> it.toList := by
-  simp only [filter, toList_filterMap, ← List.filterMap_eq_filter]
-  rfl
-
-end ToList
-
-section ToListRev
-
-theorem IterM.toListRev_filterMap {α β γ : Type w} {m : Type w → Type w'}
-    [Monad m] [LawfulMonad m]
-    [Iterator α m β] [IteratorCollect α m m] [LawfulIteratorCollect α m m] [Finite α m]
-    {f : β → Option γ} (it : IterM (α := α) m β) :
-    (it.filterMap f).toListRev = (fun x => x.filterMap f) <$> it.toListRev := by
-  simp [toListRev_eq, toList_filterMap]
-
-theorem IterM.toListRev_map {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
-    [Iterator α m β] [IteratorCollect α m m] [LawfulIteratorCollect α m m] [Finite α m] {f : β → γ}
-    (it : IterM (α := α) m β) :
-    (it.map f).toListRev = (fun x => x.map f) <$> it.toListRev := by
-  simp [toListRev_eq, toList_map]
-
-theorem IterM.toListRev_filter {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
-    [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
-    {f : β → Bool} {it : IterM (α := α) m β} :
-    (it.filter f).toListRev = List.filter f <$> it.toListRev := by
-  simp [toListRev_eq, toList_filter]
-
-end ToListRev
-
-section ToArray
-
-theorem IterM.toArray_filterMap {α β γ : Type w} {m : Type w → Type w'}
-    [Monad m] [LawfulMonad m]
-    [Iterator α m β] [IteratorCollect α m m] [LawfulIteratorCollect α m m] [Finite α m]
-    {f : β → Option γ} (it : IterM (α := α) m β) :
-    (it.filterMap f).toArray = (fun x => x.filterMap f) <$> it.toArray := by
-  simp [← toArray_toList, toList_filterMap]
-
-theorem IterM.toArray_map {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
-    [Iterator α m β] [IteratorCollect α m m] [LawfulIteratorCollect α m m] [Finite α m] {f : β → γ}
-    (it : IterM (α := α) m β) :
-    (it.map f).toArray = (fun x => x.map f) <$> it.toArray := by
-  simp [← toArray_toList, toList_map]
-
-theorem IterM.toArray_filter {α : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
-    {β : Type w} [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
-    {f : β → Bool} {it : IterM (α := α) m β} :
-    (it.filter f).toArray = Array.filter f <$> it.toArray := by
-  simp [← toArray_toList, toList_filter]
-
-end ToArray
-
-section Equivalence
-
 theorem stepAsHetT_filterMapWithPostcondition [Monad m] [LawfulMonad m] [Monad n]
     [LawfulMonad n] [Iterator α m β] [MonadLiftT m n] [LawfulMonadLiftT m n]
     {f : β → PostconditionT n (Option γ)} {it : IterM (α := α) m β} :
@@ -599,6 +197,4 @@ theorem IterM.Equiv.map {α₁ α₂ β γ : Type w}
     IterM.Equiv (ita.map f) (itb.map f) :=
   IterM.Equiv.filterMapWithPostcondition h
 
-end Equivalence
-
 end Std.Iterators
diff --git a/src/Std/Data/Iterators/Producers.lean b/src/Std/Data/Iterators/Producers.lean
index 0669c608e0..6c8e5d1292 100644
--- a/src/Std/Data/Iterators/Producers.lean
+++ b/src/Std/Data/Iterators/Producers.lean
@@ -10,3 +10,4 @@ import Std.Data.Iterators.Producers.Empty
 import Std.Data.Iterators.Producers.List
 import Std.Data.Iterators.Producers.Range
 import Std.Data.Iterators.Producers.Repeat
+import Std.Data.Iterators.Producers.Slice
diff --git a/src/Std/Data/Iterators/Producers/Slice.lean b/src/Std/Data/Iterators/Producers/Slice.lean
new file mode 100644
index 0000000000..f09f2a14de
--- /dev/null
+++ b/src/Std/Data/Iterators/Producers/Slice.lean
@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Init.Data.Slice.Operations
+
+/-!
+# Slice iterator
+
+This module provides iterators over slices from `Std.Slice` via `Std.Slice.iter`.
+-/
+
+open Std Slice Iterators
+
+/--
+Returns an iterator over the given slice. This iterator will emit the elements of the slice
+in increasing order of the indices.
+-/
+@[always_inline, inline]
+def Std.Slice.iter (s : Slice γ) [ToIterator s Id β] :=
+  (Internal.iter s : Iter β)
diff --git a/tests/lean/run/slice.lean b/tests/lean/run/slice.lean
new file mode 100644
index 0000000000..4fd8a41d60
--- /dev/null
+++ b/tests/lean/run/slice.lean
@@ -0,0 +1,31 @@
+import Std.Data.Iterators
+
+example : #[1, 2, 3][*...*].toList = [1, 2, 3] := by native_decide
+
+example : #[1, 2, 3][*...2].toList = [1, 2] := by native_decide
+
+example : #[1, 2, 3][*...<2].toList = [1, 2] := by native_decide
+
+example : #[1, 2, 3][*...=1].toList = [1, 2] := by native_decide
+
+example : #[1, 2, 3][0<...*].toList = [2, 3] := by native_decide
+
+example : #[1, 2, 3][0<...2].toList = [2] := by native_decide
+
+example : #[1, 2, 3][0<...<2].toList = [2] := by native_decide
+
+example : #[1, 2, 3][0<...=1].toList = [2] := by native_decide
+
+example : #[1, 2, 3][1...*].toList = [2, 3] := by native_decide
+
+example : #[1, 2, 3][1...2].toList = [2] := by native_decide
+
+example : #[1, 2, 3][1...<2].toList = [2] := by native_decide
+
+example : #[1, 2, 3][1...=1].toList = [2] := by native_decide
+
+example : #[1, 2, 3][1...<10].size = 2 := by native_decide
+
+example : (#[1, 2, 3][1...*].take 1).toList = [2] := by native_decide
+
+example : #[1, 1, 1][0...2].size = 2 := by native_decide