diff --git a/src/Init/Data/Iterators/Basic.lean b/src/Init/Data/Iterators/Basic.lean
index b19a60d74e..62cc100b1a 100644
--- a/src/Init/Data/Iterators/Basic.lean
+++ b/src/Init/Data/Iterators/Basic.lean
@@ -12,18 +12,80 @@ public import Init.Ext
 public import Init.NotationExtra
 public import Init.TacticsExtra
 
+set_option doc.verso true
+
 public section
 
 /-!
-### Definition of iterators
+# Definition of iterators
 
 This module defines iterators and what it means for an iterator to be finite and productive.
 -/
 
 namespace Std
 
+private opaque Internal.idOpaque {α} : { f : α → α // f = id } := ⟨id, rfl⟩
+
+/--
+Currently, {lean}`Shrink α` is just a wrapper around {lean}`α`.
+
+In the future, {name}`Shrink` should allow shrinking {lean}`α` into a potentially smaller universe,
+given a proof that {name}`α` is actually small, just like Mathlib's {lit}`Shrink`, except that
+the latter's conversion functions are noncomputable. Until then, {lean}`Shrink α` is always in the
+same universe as {name}`α`.
+
+This no-op type exists so that fewer breaking changes will be needed when the
+real {lit}`Shrink` type is available and the iterators will be made more flexible with regard to
+universes.
+
+The conversion functions {name (scope := "Init.Data.Iterators.Basic")}`Shrink.deflate` and
+{name (scope := "Init.Data.Iterators.Basic")}`Shrink.inflate` form an equivalence between
+{name}`α` and {lean}`Shrink α`, but this equivalence is intentionally not definitional.
+-/
+public def Shrink (α : Type u) : Type u := Internal.idOpaque.1 α
+
+/-- Converts elements of {name}`α` into elements of {lean}`Shrink α`. -/
+@[always_inline]
+public def Shrink.deflate {α} (x : α) : Shrink α :=
+  cast (by simp [Shrink, Internal.idOpaque.property]) x
+
+/-- Converts elements of {lean}`Shrink α` into elements of {name}`α`. -/
+@[always_inline]
+public def Shrink.inflate {α} (x : Shrink α) : α :=
+  cast (by simp [Shrink, Internal.idOpaque.property]) x
+
+@[simp, grind =]
+public theorem Shrink.deflate_inflate {α} {x : Shrink α} :
+    Shrink.deflate x.inflate = x := by
+  simp [deflate, inflate]
+
+@[simp, grind =]
+public theorem Shrink.inflate_deflate {α} {x : α} :
+    (Shrink.deflate x).inflate = x := by
+  simp [deflate, inflate]
+
+public theorem Shrink.inflate_inj {α} {x y : Shrink α} :
+    x.inflate = y.inflate ↔ x = y := by
+  apply Iff.intro
+  · intro h
+    simpa using congrArg Shrink.deflate h
+  · rintro rfl
+    rfl
+
+public theorem Shrink.deflate_inj {α} {x y : α} :
+    Shrink.deflate x = Shrink.deflate y ↔ x = y := by
+  apply Iff.intro
+  · intro h
+    simpa using congrArg Shrink.inflate h
+  · rintro rfl
+    rfl
+
 namespace Iterators
 
+-- It is not fruitful to move the following docstrings to verso right now because there are lots of
+-- forward references that cannot be realized nicely.
+set_option doc.verso false
+
 /--
 An iterator that sequentially emits values of type `β` in the monad `m`. It may be finite
 or infinite.
@@ -284,7 +346,7 @@ step object is bundled with a proof that it is a "plausible" step for the given
 -/
 class Iterator (α : Type w) (m : Type w → Type w') (β : outParam (Type w)) where
   IsPlausibleStep : IterM (α := α) m β → IterStep (IterM (α := α) m β) β → Prop
-  step : (it : IterM (α := α) m β) → m (PlausibleIterStep <| IsPlausibleStep it)
+  step : (it : IterM (α := α) m β) → m (Shrink <| PlausibleIterStep <| IsPlausibleStep it)
 
 section Monadic
 
@@ -358,7 +420,7 @@ the termination measures `it.finitelyManySteps` and `it.finitelyManySkips`.
 -/
 @[always_inline, inline, expose]
 def IterM.step {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
-    (it : IterM (α := α) m β) : m it.Step :=
+    (it : IterM (α := α) m β) : m (Shrink it.Step) :=
   Iterator.step it
 
 end Monadic
@@ -582,7 +644,7 @@ the termination measures `it.finitelyManySteps` and `it.finitelyManySkips`.
 -/
 @[always_inline, inline, expose]
 def Iter.step {α β : Type w} [Iterator α Id β] (it : Iter (α := α) β) : it.Step :=
-  it.toIterM.step.run.toPure
+  it.toIterM.step.run.inflate.toPure
 
 end Pure
 
diff --git a/src/Init/Data/Iterators/Combinators/Monadic/Attach.lean b/src/Init/Data/Iterators/Combinators/Monadic/Attach.lean
index ec3a185f61..946526e31f 100644
--- a/src/Init/Data/Iterators/Combinators/Monadic/Attach.lean
+++ b/src/Init/Data/Iterators/Combinators/Monadic/Attach.lean
@@ -43,7 +43,8 @@ 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', Monadic.modifyStep it step' = step
-  step it := (fun step => ⟨Monadic.modifyStep it step, step, rfl⟩) <$> it.internalState.inner.step
+  step it := (fun step => .deflate ⟨Monadic.modifyStep it step.inflate, step.inflate, rfl⟩) <$>
+      it.internalState.inner.step
 
 def Attach.instFinitenessRelation {α β : Type w} {m : Type w → Type w'} [Monad m]
     [Iterator α m β] [Finite α m] {P : β → Prop} :
diff --git a/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
index 540c303d82..42561ff763 100644
--- a/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
+++ b/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
@@ -149,13 +149,13 @@ instance FilterMap.instIterator {α β γ : Type w} {m : Type w → Type w'} {n
   step it :=
     letI : MonadLift m n := ⟨lift (α := _)⟩
     do
-      match ← it.internalState.inner.step with
+      match (← it.internalState.inner.step).inflate with
       | .yield it' out h => do
         match ← (f out).operation with
-        | ⟨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)
+        | ⟨none, h'⟩ => pure <| .deflate <| .skip (it'.filterMapWithPostcondition f) (by exact .yieldNone h h')
+        | ⟨some out', h'⟩ => pure <| .deflate <| .yield (it'.filterMapWithPostcondition f) out' (by exact .yieldSome h h')
+      | .skip it' h => pure <| .deflate <| .skip (it'.filterMapWithPostcondition f) (by exact .skip h)
+      | .done h => pure <| .deflate <| .done (.done h)
 
 instance {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β]
     {lift : ⦃α : Type w⦄ → m α → n α}
diff --git a/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean b/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean
index 6b22828659..30540315c4 100644
--- a/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean
+++ b/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean
@@ -90,9 +90,9 @@ instance Types.ULiftIterator.instIterator [Iterator α m β] [Monad n] :
       step = ULiftIterator.Monadic.modifyStep step'
   step it := do
     let step := (← (lift it.internalState.inner.step).run).down
-    return ⟨Monadic.modifyStep step.val, ?hp⟩
+    return .deflate ⟨Monadic.modifyStep step.inflate.val, ?hp⟩
   where finally
-    case hp => exact ⟨step.val, step.property, rfl⟩
+    case hp => exact ⟨step.inflate.val, step.inflate.property, rfl⟩
 
 def Types.ULiftIterator.instFinitenessRelation [Iterator α m β] [Finite α m] [Monad n] :
     FinitenessRelation (ULiftIterator α m n β lift) n where
diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Collect.lean b/src/Init/Data/Iterators/Consumers/Monadic/Collect.lean
index 1bb519cc62..3627a18393 100644
--- a/src/Init/Data/Iterators/Consumers/Monadic/Collect.lean
+++ b/src/Init/Data/Iterators/Consumers/Monadic/Collect.lean
@@ -91,7 +91,7 @@ def IterM.DefaultConsumers.toArrayMapped {α β : Type w} {m : Type w → Type w
 where
   @[specialize]
   go [Monad n] [Finite α m] (it : IterM (α := α) m β) a := letI : MonadLift m n := ⟨lift (α := _)⟩; do
-    match ← it.step with
+    match (← it.step).inflate with
     | .yield it' b _ => go it' (a.push (← f b))
     | .skip it' _ => go it' a
     | .done _ => return a
@@ -150,7 +150,7 @@ partial def IterM.DefaultConsumers.toArrayMappedPartial {α β : Type w} {m : Ty
 where
   @[specialize]
   go [Monad n] (it : IterM (α := α) m β) a := letI : MonadLift m n := ⟨lift⟩; do
-    match ← it.step with
+    match (← it.step).inflate with
     | .yield it' b _ => go it' (a.push (← f b))
     | .skip it' _ => go it' a
     | .done _ => return a
@@ -209,7 +209,7 @@ def IterM.toListRev {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type
   go it []
 where
   go [Finite α m] it bs := do
-    match ← it.step with
+    match (← it.step).inflate with
     | .yield it' b _ => go it' (b :: bs)
     | .skip it' _ => go it' bs
     | .done _ => return bs
@@ -229,7 +229,7 @@ partial def IterM.Partial.toListRev {α : Type w} {m : Type w → Type w'} [Mona
 where
   @[specialize]
   go it bs := do
-    match ← it.step with
+    match (← it.step).inflate with
     | .yield it' b _ => go it' (b :: bs)
     | .skip it' _ => go it' bs
     | .done _ => return bs
diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean
index 6176a5b8ec..0927700ffd 100644
--- a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean
+++ b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean
@@ -142,7 +142,8 @@ def IterM.DefaultConsumers.forIn' {m : Type w → Type w'} {α : Type w} {β : T
     (P : β → Prop) (hP : ∀ b, it.IsPlausibleIndirectOutput b → P b)
     (f : (b : β) → P b → (c : γ) → n (Subtype (plausible_forInStep b c))) : n γ :=
   haveI : WellFounded _ := wf
-  (lift _ _ · it.step) fun
+  (lift _ _ · it.step) fun s =>
+    match s.inflate with
     | .yield it' out h => do
       match ← f out (hP _ <| .direct ⟨_, h⟩) init with
       | ⟨.yield c, _⟩ =>
@@ -220,7 +221,8 @@ partial def IterM.DefaultConsumers.forInPartial {m : Type w → Type w'} {α : T
     (lift : ∀ γ δ, (γ → n δ) → m γ → n δ) (γ : Type x)
     (it : IterM (α := α) m β) (init : γ)
     (f : (b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (ForInStep γ)) : n γ :=
-  (lift _ _ · it.step) fun
+  (lift _ _ · it.step) fun s =>
+      match s.inflate with
       | .yield it' out h => do
         match ← f out (.direct ⟨_, h⟩) init with
         | .yield c =>
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
index 390419641a..282c7d6eb9 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
@@ -62,18 +62,18 @@ theorem Iter.step_filterMapWithPostcondition {f : β → PostconditionT n (Optio
     | .yield it' out h => do
       match ← (f out).operation with
       | ⟨none, h'⟩ =>
-        pure <| .skip (it'.filterMapWithPostcondition f) (.yieldNone (out := out) h h')
+        pure <| .deflate <| .skip (it'.filterMapWithPostcondition f) (.yieldNone (out := out) h h')
       | ⟨some out', h'⟩ =>
-        pure <| .yield (it'.filterMapWithPostcondition f) out' (.yieldSome (out := out) h h')
+        pure <| .deflate <| .yield (it'.filterMapWithPostcondition f) out' (.yieldSome (out := out) h h')
     | .skip it' h =>
-      pure <| .skip (it'.filterMapWithPostcondition f) (.skip h)
+      pure <| .deflate <| .skip (it'.filterMapWithPostcondition f) (.skip h)
     | .done h =>
-      pure <| .done (.done h)) := by
+      pure <| .deflate <| .done (.done h)) := by
   simp only [filterMapWithPostcondition_eq_toIter_filterMapWithPostcondition_toIterM, IterM.step_filterMapWithPostcondition,
     step]
   simp only [liftM, monadLift, pure_bind]
   generalize it.toIterM.step = step
-  match step with
+  match step.inflate with
   | .yield it' out h =>
     apply bind_congr
     intro step
@@ -88,17 +88,17 @@ theorem Iter.step_filterWithPostcondition {f : β → PostconditionT n (ULift Bo
     | .yield it' out h => do
       match ← (f out).operation with
       | ⟨.up false, h'⟩ =>
-        pure <| .skip (it'.filterWithPostcondition f) (.yieldNone (out := out) h ⟨⟨_, h'⟩, rfl⟩)
+        pure <| .deflate <| .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⟩)
+        pure <| .deflate <| .yield (it'.filterWithPostcondition f) out (.yieldSome (out := out) h ⟨⟨_, h'⟩, rfl⟩)
     | .skip it' h =>
-      pure <| .skip (it'.filterWithPostcondition f) (.skip h)
+      pure <| .deflate <| .skip (it'.filterWithPostcondition f) (.skip h)
     | .done h =>
-      pure <| .done (.done h)) := by
+      pure <| .deflate <| .done (.done h)) := by
   simp only [filterWithPostcondition_eq_toIter_filterMapWithPostcondition_toIterM, IterM.step_filterWithPostcondition, step]
   simp only [liftM, monadLift, pure_bind]
   generalize it.toIterM.step = step
-  match step with
+  match step.inflate with
   | .yield it' out h =>
     apply bind_congr
     intro step
@@ -112,15 +112,15 @@ theorem Iter.step_mapWithPostcondition {f : β → PostconditionT n γ}
     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⟩)
+      pure <| .deflate <| .yield (it'.mapWithPostcondition f) out'.1 (.yieldSome h ⟨out', rfl⟩)
     | .skip it' h =>
-      pure <| .skip (it'.mapWithPostcondition f) (.skip h)
+      pure <| .deflate <| .skip (it'.mapWithPostcondition f) (.skip h)
     | .done h =>
-      pure <| .done (.done h)) := by
+      pure <| .deflate <| .done (.done h)) := by
   simp only [mapWithPostcondition_eq_toIter_mapWithPostcondition_toIterM, IterM.step_mapWithPostcondition, step]
   simp only [liftM, monadLift, pure_bind]
   generalize it.toIterM.step = step
-  match step with
+  match step.inflate with
   | .yield it' out h =>
     simp only [bind_pure_comp]
     rfl
@@ -134,17 +134,17 @@ theorem Iter.step_filterMapM {β' : Type w} {f : β → n (Option β')}
     | .yield it' out h => do
       match ← f out with
       | none =>
-        pure <| .skip (it'.filterMapM f) (.yieldNone (out := out) h .intro)
+        pure <| .deflate <| .skip (it'.filterMapM f) (.yieldNone (out := out) h .intro)
       | some out' =>
-        pure <| .yield (it'.filterMapM f) out' (.yieldSome (out := out) h .intro)
+        pure <| .deflate <| .yield (it'.filterMapM f) out' (.yieldSome (out := out) h .intro)
     | .skip it' h =>
-      pure <| .skip (it'.filterMapM f) (.skip h)
+      pure <| .deflate <| .skip (it'.filterMapM f) (.skip h)
     | .done h =>
-      pure <| .done (.done h)) := by
+      pure <| .deflate <| .done (.done h)) := by
   simp only [filterMapM_eq_toIter_filterMapM_toIterM, IterM.step_filterMapM, step]
   simp only [liftM, monadLift, pure_bind]
   generalize it.toIterM.step = step
-  match step with
+  match step.inflate with
   | .yield it' out h =>
     apply bind_congr
     intro step
@@ -159,17 +159,17 @@ theorem Iter.step_filterM {f : β → n (ULift Bool)}
     | .yield it' out h => do
       match ← f out with
       | .up false =>
-        pure <| .skip (it'.filterM f) (.yieldNone (out := out) h ⟨⟨.up false, .intro⟩, rfl⟩)
+        pure <| .deflate <| .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⟩)
+        pure <| .deflate <| .yield (it'.filterM f) out (.yieldSome (out := out) h ⟨⟨.up true, .intro⟩, rfl⟩)
     | .skip it' h =>
-      pure <| .skip (it'.filterM f) (.skip h)
+      pure <| .deflate <| .skip (it'.filterM f) (.skip h)
     | .done h =>
-      pure <| .done (.done h)) := by
+      pure <| .deflate <| .done (.done h)) := by
   simp only [filterM_eq_toIter_filterM_toIterM, IterM.step_filterM, step]
   simp only [liftM, monadLift, pure_bind]
   generalize it.toIterM.step = step
-  match step with
+  match step.inflate with
   | .yield it' out h =>
     simp [PostconditionT.lift]
     apply bind_congr
@@ -184,15 +184,15 @@ theorem Iter.step_mapM {f : β → n γ}
     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⟩)
+      pure <| .deflate <| .yield (it'.mapM f) out' (.yieldSome h ⟨⟨out', True.intro⟩, rfl⟩)
     | .skip it' h =>
-      pure <| .skip (it'.mapM f) (.skip h)
+      pure <| .deflate <| .skip (it'.mapM f) (.skip h)
     | .done h =>
-      pure <| .done (.done h)) := by
+      pure <| .deflate <| .done (.done h)) := by
   simp only [mapM_eq_toIter_mapM_toIterM, IterM.step_mapM, step]
   simp only [liftM, monadLift, pure_bind]
   generalize it.toIterM.step = step
-  match step with
+  match step.inflate with
   | .yield it' out h =>
     simp only [bind_pure_comp]
     rfl
@@ -210,14 +210,14 @@ theorem Iter.step_filterMap {f : β → Option γ} :
   simp only [filterMap_eq_toIter_filterMap_toIterM, toIterM_toIter, IterM.step_filterMap, step]
   simp only [monadLift, Id.run_bind]
   generalize it.toIterM.step.run = step
-  cases step using PlausibleIterStep.casesOn
+  cases step.inflate using PlausibleIterStep.casesOn
   · simp only [IterM.Step.toPure_yield, toIter_toIterM, toIterM_toIter]
     split <;> split <;> (try exfalso; simp_all; done)
-    · rfl
+    · simp
     · rename_i h₁ _ h₂
       rw [h₁] at h₂
       cases h₂
-      rfl
+      simp
   · simp
   · simp
 
@@ -249,7 +249,7 @@ theorem Iter.step_map {f : β → γ} :
         .done (.done h) := by
   simp only [map_eq_toIter_map_toIterM, step, toIterM_toIter, IterM.step_map, Id.run_bind]
   generalize it.toIterM.step.run = step
-  cases step using PlausibleIterStep.casesOn <;> simp
+  cases step.inflate using PlausibleIterStep.casesOn <;> simp
 
 def Iter.step_filter {f : β → Bool} :
     (it.filter f).step = match it.step with
@@ -264,7 +264,7 @@ def Iter.step_filter {f : β → Bool} :
         .done (.done h) := by
   simp only [filter_eq_toIter_filter_toIterM, step, toIterM_toIter, IterM.step_filter, Id.run_bind]
   generalize it.toIterM.step.run = step
-  cases step using PlausibleIterStep.casesOn
+  cases step.inflate using PlausibleIterStep.casesOn
   · simp only
     split <;> simp [*]
   · simp
@@ -283,7 +283,7 @@ def Iter.val_step_filter {f : β → Bool} :
         .done := by
   simp only [filter_eq_toIter_filter_toIterM, step, toIterM_toIter, IterM.step_filter, Id.run_bind]
   generalize it.toIterM.step.run = step
-  cases step using PlausibleIterStep.casesOn
+  cases step.inflate using PlausibleIterStep.casesOn
   · simp only
     split <;> simp [*]
   · simp
@@ -490,7 +490,7 @@ theorem Iter.anyM_eq_anyM_mapM_pure {α β : Type} {m : Type → Type w'} [Itera
   induction it using Iter.inductSteps with | step it ihy ihs =>
   rw [forIn_eq_match_step, IterM.forIn_eq_match_step, bind_assoc, step_mapM]
   cases it.step using PlausibleIterStep.casesOn
-  · simp only [bind_assoc, liftM_pure, pure_bind, map_eq_pure_bind]
+  · simp only [bind_assoc, liftM_pure, pure_bind, map_eq_pure_bind, Shrink.inflate_deflate]
     apply bind_congr; intro px
     split
     · simp
@@ -646,7 +646,7 @@ theorem Iter.allM_eq_allM_mapM_pure {α β : Type} {m : Type → Type w'} [Itera
   induction it using Iter.inductSteps with | step it ihy ihs =>
   rw [forIn_eq_match_step, IterM.forIn_eq_match_step, bind_assoc, step_mapM]
   cases it.step using PlausibleIterStep.casesOn
-  · simp only [bind_assoc, liftM_pure, pure_bind, map_eq_pure_bind]
+  · simp only [bind_assoc, liftM_pure, pure_bind, map_eq_pure_bind, Shrink.inflate_deflate]
     apply bind_congr; intro px
     split
     · simp [ihy ‹_›]
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean
index 90f41a0523..0491529b79 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean
@@ -18,7 +18,7 @@ variable {α : Type w} {m : Type w → Type w'} {β : Type w} {P : β → Prop}
 
 theorem IterM.step_attachWith [Iterator α m β] [Monad m] {it : IterM (α := α) m β} {hP} :
     (it.attachWith P hP).step =
-      (fun s => ⟨Types.Attach.Monadic.modifyStep (it.attachWith P hP) s, s, rfl⟩) <$> it.step :=
+      (fun s => .deflate ⟨Types.Attach.Monadic.modifyStep (it.attachWith P hP) s.inflate, s.inflate, rfl⟩) <$> it.step :=
   rfl
 
 @[simp]
@@ -32,7 +32,7 @@ theorem IterM.map_unattach_toList_attachWith [Iterator α m β] [Monad m]
   simp only [bind_pure_comp, bind_map_left, map_bind]
   apply bind_congr
   intro step
-  cases step using PlausibleIterStep.casesOn
+  cases step.inflate using PlausibleIterStep.casesOn
   · rename_i it' out hp
     simp only [IterM.attachWith] at ihy
     simp [Types.Attach.Monadic.modifyStep,
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
index c1b98f95de..d0896ebe1e 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
@@ -25,20 +25,20 @@ variable {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
 theorem IterM.step_filterMapWithPostcondition {f : β → PostconditionT n (Option β')}
     [Monad n] [LawfulMonad n] [MonadLiftT m n] :
   (it.filterMapWithPostcondition f).step = (do
-    match ← it.step with
+    match (← it.step).inflate with
     | .yield it' out h => do
       match ← (f out).operation with
       | ⟨none, h'⟩ =>
-        pure <| .skip (it'.filterMapWithPostcondition f) (.yieldNone (out := out) h h')
+        pure <| .deflate <| .skip (it'.filterMapWithPostcondition f) (.yieldNone (out := out) h h')
       | ⟨some out', h'⟩ =>
-        pure <| .yield (it'.filterMapWithPostcondition f) out' (.yieldSome (out := out) h h')
+        pure <| .deflate <| .yield (it'.filterMapWithPostcondition f) out' (.yieldSome (out := out) h h')
     | .skip it' h =>
-      pure <| .skip (it'.filterMapWithPostcondition f) (.skip h)
+      pure <| .deflate <| .skip (it'.filterMapWithPostcondition f) (.skip h)
     | .done h =>
-      pure <| .done (by exact .done h)) := by
+      pure <| .deflate <| .done (by exact .done h)) := by
   apply bind_congr
   intro step
-  match step with
+  match step.inflate with
   | .yield it' out h =>
     simp only [PlausibleIterStep.skip, PlausibleIterStep.yield]
     apply bind_congr
@@ -50,20 +50,20 @@ theorem IterM.step_filterMapWithPostcondition {f : β → PostconditionT n (Opti
 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
+    match (← it.step).inflate 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⟩)
+        pure <| .deflate <| .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⟩)
+        pure <| .deflate <| .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)
+      pure <| .deflate <| .skip (it'.filterWithPostcondition f) (by exact .skip h)
     | .done h =>
-      pure <| .done (by exact .done h)) := by
+      pure <| .deflate <| .done (by exact .done h)) := by
   apply bind_congr
   intro step
-  match step with
+  match step.inflate with
   | .yield it' out h =>
     simp only [PostconditionT.operation_map, PlausibleIterStep.skip, PlausibleIterStep.yield,
       bind_map_left]
@@ -76,17 +76,17 @@ theorem IterM.step_filterWithPostcondition {f : β → PostconditionT n (ULift B
 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
+    match (← it.step).inflate with
     | .yield it' out h => do
       let out' ← (f out).operation
-      pure <| .yield (it'.mapWithPostcondition f) out'.1 (.yieldSome h ⟨out', rfl⟩)
+      pure <| .deflate <| .yield (it'.mapWithPostcondition f) out'.1 (.yieldSome h ⟨out', rfl⟩)
     | .skip it' h =>
-      pure <| .skip (it'.mapWithPostcondition f) (.skip h)
+      pure <| .deflate <| .skip (it'.mapWithPostcondition f) (.skip h)
     | .done h =>
-      pure <| .done (.done h)) := by
+      pure <| .deflate <| .done (.done h)) := by
   apply bind_congr
   intro step
-  match step with
+  match step.inflate with
   | .yield it' out h =>
     simp only [PostconditionT.operation_map, bind_map_left, bind_pure_comp]
     rfl
@@ -96,20 +96,20 @@ theorem IterM.step_mapWithPostcondition {γ : Type w} {f : β → PostconditionT
 theorem IterM.step_filterMapM {f : β → n (Option β')}
     [Monad n] [LawfulMonad n] [MonadLiftT m n] :
   (it.filterMapM f).step = (do
-    match ← it.step with
+    match (← it.step).inflate with
     | .yield it' out h => do
       match ← f out with
       | none =>
-        pure <| .skip (it'.filterMapM f) (.yieldNone (out := out) h .intro)
+        pure <| .deflate <| .skip (it'.filterMapM f) (.yieldNone (out := out) h .intro)
       | some out' =>
-        pure <| .yield (it'.filterMapM f) out' (.yieldSome (out := out) h .intro)
+        pure <| .deflate <| .yield (it'.filterMapM f) out' (.yieldSome (out := out) h .intro)
     | .skip it' h =>
-      pure <| .skip (it'.filterMapM f) (.skip h)
+      pure <| .deflate <| .skip (it'.filterMapM f) (.skip h)
     | .done h =>
-      pure <| .done (.done h)) := by
+      pure <| .deflate <| .done (.done h)) := by
   apply bind_congr
   intro step
-  match step with
+  match step.inflate with
   | .yield it' out h =>
     simp only [PostconditionT.lift, bind_map_left]
     apply bind_congr
@@ -121,20 +121,20 @@ theorem IterM.step_filterMapM {f : β → n (Option β')}
 theorem IterM.step_filterM {f : β → n (ULift Bool)}
     [Monad n] [LawfulMonad n] [MonadLiftT m n] :
   (it.filterM f).step = (do
-    match ← it.step with
+    match (← it.step).inflate 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⟩)
+        pure <| .deflate <| .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⟩)
+        pure <| .deflate <| .yield (it'.filterM f) out (.yieldSome (out := out) h ⟨⟨.up true, .intro⟩, rfl⟩)
     | .skip it' h =>
-      pure <| .skip (it'.filterM f) (.skip h)
+      pure <| .deflate <| .skip (it'.filterM f) (.skip h)
     | .done h =>
-      pure <| .done (.done h)) := by
+      pure <| .deflate <| .done (.done h)) := by
   apply bind_congr
   intro step
-  match step with
+  match step.inflate with
   | .yield it' out h =>
     simp only [PostconditionT.lift, PostconditionT.operation_map, Functor.map_map,
       PlausibleIterStep.skip, PlausibleIterStep.yield, bind_map_left]
@@ -147,17 +147,17 @@ theorem IterM.step_filterM {f : β → n (ULift Bool)}
 theorem IterM.step_mapM {γ : Type w} {f : β → n γ}
     [Monad n] [LawfulMonad n] [MonadLiftT m n] :
   (it.mapM f).step = (do
-    match ← it.step with
+    match (← it.step).inflate with
     | .yield it' out h => do
       let out' ← f out
-      pure <| .yield (it'.mapM f) out' (.yieldSome h ⟨⟨out', True.intro⟩, rfl⟩)
+      pure <| .deflate <| .yield (it'.mapM f) out' (.yieldSome h ⟨⟨out', True.intro⟩, rfl⟩)
     | .skip it' h =>
-      pure <| .skip (it'.mapM f) (.skip h)
+      pure <| .deflate <| .skip (it'.mapM f) (.skip h)
     | .done h =>
-      pure <| .done (.done h)) := by
+      pure <| .deflate <| .done (.done h)) := by
   apply bind_congr
   intro step
-  match step with
+  match step.inflate with
   | .yield it' out h =>
     simp only [bind_pure_comp]
     simp only [PostconditionT.lift]
@@ -169,17 +169,17 @@ theorem IterM.step_mapM {γ : Type w} {f : β → n γ}
 
 theorem IterM.step_filterMap [Monad m] [LawfulMonad m] {f : β → Option β'} :
   (it.filterMap f).step = (do
-    match ← it.step with
+    match (← it.step).inflate with
     | .yield it' out h => do
       match h' : f out with
       | none =>
-        pure <| .skip (it'.filterMap f) (.yieldNone h h')
+        pure <| .deflate <| .skip (it'.filterMap f) (.yieldNone h h')
       | some out' =>
-        pure <| .yield (it'.filterMap f) out' (.yieldSome h h')
+        pure <| .deflate <| .yield (it'.filterMap f) out' (.yieldSome h h')
     | .skip it' h =>
-      pure <| .skip (it'.filterMap f) (.skip h)
+      pure <| .deflate <| .skip (it'.filterMap f) (.skip h)
     | .done h =>
-      pure <| .done (.done h)) := by
+      pure <| .deflate <| .done (.done h)) := by
   simp only [IterM.filterMap, step_filterMapWithPostcondition, pure]
   apply bind_congr
   intro step
@@ -191,13 +191,13 @@ theorem IterM.step_filterMap [Monad m] [LawfulMonad m] {f : β → Option β'} :
 
 theorem IterM.step_map [Monad m] [LawfulMonad m] {f : β → β'} :
   (it.map f).step = (do
-    match ← it.step with
+    match (← it.step).inflate with
     | .yield it' out h =>
       let out' := f out
-      pure <| .yield (it'.map f) out' (.yieldSome h ⟨⟨out', rfl⟩, rfl⟩)
+      pure <| .deflate <| .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
+      pure <| .deflate <| .skip (it'.map f) (.skip h)
+    | .done h => pure <| .deflate <| .done (.done h)) := by
   simp only [map, IterM.step_mapWithPostcondition]
   apply bind_congr
   intro step
@@ -208,15 +208,15 @@ theorem IterM.step_map [Monad m] [LawfulMonad m] {f : β → β'} :
 
 theorem IterM.step_filter [Monad m] [LawfulMonad m] {f : β → Bool} :
   (it.filter f).step = (do
-    match ← it.step with
+    match (← it.step).inflate with
     | .yield it' out h =>
       if h' : f out = true then
-        pure <| .yield (it'.filter f) out (.yieldSome h (by simp [h']))
+        pure <| .deflate <| .yield (it'.filter f) out (.yieldSome h (by simp [h']))
       else
-        pure <| .skip (it'.filter f) (.yieldNone h (by simp [h']))
+        pure <| .deflate <| .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
+      pure <| .deflate <| .skip (it'.filter f) (.skip h)
+    | .done h => pure <| .deflate <| .done (.done h)) := by
   simp only [filter, IterM.step_filterMap]
   apply bind_congr
   intro step
@@ -260,14 +260,15 @@ instance {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
     simp only [liftM_bind (m := n) (n := o), bind_assoc]
     apply bind_congr
     intro step
-    cases step using PlausibleIterStep.casesOn
+    cases step.inflate using PlausibleIterStep.casesOn
     · simp only [bind_pure_comp]
       simp only [liftM_map, bind_map_left]
       apply bind_congr
       intro out'
-      simp only [← ih_yield ‹_›]
+      simp only [Shrink.inflate_deflate, ← ih_yield ‹_›]
       rfl
-    · simp only [bind_pure_comp, pure_bind, liftM_pure, pure_bind, ← ih_skip ‹_›]
+    · simp only [bind_pure_comp, pure_bind, liftM_pure, pure_bind, ← ih_skip ‹_›,
+        Shrink.inflate_deflate]
       simp only [IterM.mapWithPostcondition, IterM.InternalCombinators.map, internalState_toIterM]
     · simp
 
@@ -288,17 +289,17 @@ theorem IterM.InternalConsumers.toList_filterMap {α β γ: Type w} {m : Type w
   simp only [bind_assoc, IterM.step, map_eq_pure_bind]
   apply bind_congr
   intro step
-  split
+  cases step.inflate using PlausibleIterStep.casesOn
   · simp only [List.filterMap_cons, bind_assoc, pure_bind]
     split
     · split
-      · simp only [bind_pure_comp, pure_bind]
+      · simp only [bind_pure_comp, pure_bind, Shrink.inflate_deflate]
         exact ihy ‹_›
       · simp_all
     · split
       · simp_all
       · simp_all [ihy ‹_›]
-  · simp only [bind_pure_comp, pure_bind]
+  · simp only [bind_pure_comp, pure_bind, Shrink.inflate_deflate]
     apply ihs
     assumption
   · simp
@@ -316,17 +317,17 @@ theorem IterM.toList_filterMap {α β γ : Type w} {m : Type w → Type w'}
   simp only [bind_assoc, IterM.step, map_eq_pure_bind]
   apply bind_congr
   intro step
-  split
+  cases step.inflate using PlausibleIterStep.casesOn
   · simp only [List.filterMap_cons, bind_assoc, pure_bind]
     split
     · split
-      · simp only [bind_pure_comp, pure_bind]
+      · simp only [bind_pure_comp, pure_bind, Shrink.inflate_deflate]
         exact ihy ‹_›
       · simp_all
     · split
       · simp_all
       · simp_all [ihy ‹_›]
-  · simp only [bind_pure_comp, pure_bind]
+  · simp only [bind_pure_comp, pure_bind, Shrink.inflate_deflate]
     apply ihs
     assumption
   · simp
@@ -433,7 +434,7 @@ theorem IterM.foldM_filterMapM {α β γ δ : Type w}
   induction it using IterM.inductSteps generalizing init with | step it ihy ihs
   rw [foldM_eq_match_step, foldM_eq_match_step, step_filterMapM, liftM_bind, bind_assoc]
   apply bind_congr; intro step
-  split
+  cases step.inflate using PlausibleIterStep.casesOn
   · simp only [PlausibleIterStep.skip, PlausibleIterStep.yield, liftM_bind, bind_assoc]
     apply bind_congr; intro c?
     split <;> simp [ihy ‹_›]
@@ -455,7 +456,7 @@ theorem IterM.foldM_mapM {α β γ δ : Type w}
   induction it using IterM.inductSteps generalizing init with | step it ihy ihs
   rw [foldM_eq_match_step, foldM_eq_match_step, step_mapM, liftM_bind, bind_assoc]
   apply bind_congr; intro step
-  split
+  cases step.inflate using PlausibleIterStep.casesOn
   · simp [ihy ‹_›]
   · simp [ihs ‹_›]
   · simp
@@ -473,8 +474,9 @@ theorem IterM.foldM_filterMap {α β γ δ : Type w} {m : Type w → Type w'} {n
   induction it using IterM.inductSteps generalizing init with | step it ihy ihs
   rw [foldM_eq_match_step, foldM_eq_match_step, step_filterMap, liftM_bind, bind_assoc]
   apply bind_congr; intro step
-  split
-  · split <;> simp [ihy ‹_›, *]
+  cases step.inflate using PlausibleIterStep.casesOn
+  · simp only [PlausibleIterStep.skip, PlausibleIterStep.yield]
+    split <;> simp [ihy ‹_›, *]
   · simp [ihs ‹_›]
   · simp
 
@@ -489,7 +491,7 @@ theorem IterM.foldM_map {α β γ δ : Type w} {m : Type w → Type w'} {n : Typ
   induction it using IterM.inductSteps generalizing init with | step it ihy ihs
   rw [foldM_eq_match_step, foldM_eq_match_step, step_map, liftM_bind, bind_assoc]
   apply bind_congr; intro step
-  split
+  cases step.inflate using PlausibleIterStep.casesOn
   · simp [ihy ‹_›]
   · simp [ihs ‹_›]
   · simp
@@ -553,11 +555,11 @@ theorem IterM.anyM_filterMapM {α β β' : Type w} {m : Type w → Type w'} {n :
   rw [anyM_eq_match_step, anyM_eq_match_step, step_filterMapM, step_mapM, bind_assoc, bind_assoc]
   apply bind_congr; intro step
   split
-  · simp only [bind_assoc, pure_bind]
+  · simp only [bind_assoc, pure_bind, Shrink.inflate_deflate]
     apply bind_congr; intro fx
     split
     · simp [ihy ‹_›]
-    · simp only [PlausibleIterStep.yield, pure_bind]
+    · simp only [PlausibleIterStep.yield, pure_bind, Shrink.inflate_deflate]
       apply bind_congr; intro px
       split <;> simp [ihy ‹_›]
   · simp only [PlausibleIterStep.skip, pure_bind, bind_assoc]
@@ -573,7 +575,7 @@ theorem IterM.anyM_mapM {α β β' : Type w} {m : Type w → Type w'} {n : Type
   rw [anyM_eq_match_step, anyM_eq_match_step, step_mapM, step_mapM, bind_assoc, bind_assoc]
   apply bind_congr; intro step
   split
-  · simp only [bind_assoc, pure_bind]
+  · simp only [bind_assoc, pure_bind, Shrink.inflate_deflate]
     apply bind_congr; intro fx
     simp [ihy ‹_›]
   · simp only [PlausibleIterStep.skip, pure_bind, bind_assoc]
@@ -593,7 +595,7 @@ theorem IterM.anyM_filterM {α β : Type w} {m : Type w → Type w'} {n : Type w
   rw [anyM_eq_match_step, anyM_eq_match_step, step_mapM, step_filterM, bind_assoc, bind_assoc]
   apply bind_congr; intro step
   split
-  · simp only [bind_assoc, pure_bind]
+  · simp only [bind_assoc, pure_bind, Shrink.inflate_deflate]
     apply bind_congr; intro fx
     split <;> simp [ihy ‹_›]
   · simp only [PlausibleIterStep.skip, pure_bind, bind_assoc]
@@ -611,10 +613,11 @@ theorem IterM.anyM_filterMap {α β β' : Type w} {m : Type w → Type w'}
   induction it using IterM.inductSteps with | step it ihy ihs
   rw [anyM_eq_match_step, anyM_eq_match_step, step_filterMap, bind_assoc]
   apply bind_congr; intro step
-  split
-  · split
+  cases step.inflate using PlausibleIterStep.casesOn
+  · simp only
+    split
     · simp [*, ihy ‹_›]
-    · simp only [*, PlausibleIterStep.yield, pure_bind]
+    · simp only [*, PlausibleIterStep.yield, pure_bind, Shrink.inflate_deflate]
       apply bind_congr; intro px
       split <;> simp [ihy ‹_›]
   · simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
@@ -628,8 +631,8 @@ theorem IterM.anyM_map {α β β' : Type w} {m : Type w → Type w'}
   induction it using IterM.inductSteps with | step it ihy ihs
   rw [anyM_eq_match_step, anyM_eq_match_step, step_map, bind_assoc]
   apply bind_congr; intro step
-  split
-  · simp only [pure_bind]
+  cases step.inflate using PlausibleIterStep.casesOn
+  · simp only [pure_bind, Shrink.inflate_deflate]
     apply bind_congr; intro fx
     simp [ihy ‹_›]
   · simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
@@ -647,7 +650,7 @@ theorem IterM.anyM_filter {α β : Type w} {m : Type w → Type w'}
   induction it using IterM.inductSteps with | step it ihy ihs
   rw [anyM_eq_match_step, anyM_eq_match_step, step_filter, bind_assoc]
   apply bind_congr; intro step
-  split
+  cases step.inflate using PlausibleIterStep.casesOn
   · simp only
     split <;> simp [ihy ‹_›]
   · simp only [PlausibleIterStep.skip, pure_bind]
@@ -693,10 +696,11 @@ theorem IterM.any_filterMap {α β β' : Type w} {m : Type w → Type w'}
   induction it using IterM.inductSteps with | step it ihy ihs
   rw [any_eq_match_step, any_eq_match_step, step_filterMap, bind_assoc]
   apply bind_congr; intro step
-  split
-  · split
+  cases step.inflate using PlausibleIterStep.casesOn
+  · simp only
+    split
     · simp [*, ihy ‹_›]
-    · simp only [*, PlausibleIterStep.yield, pure_bind]
+    · simp only [*, PlausibleIterStep.yield, pure_bind, Shrink.inflate_deflate]
       split <;> simp [ihy ‹_›]
   · simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
   · simp
@@ -709,7 +713,7 @@ theorem IterM.any_map {α β β' : Type w} {m : Type w → Type w'}
   induction it using IterM.inductSteps with | step it ihy ihs
   rw [any_eq_match_step, any_eq_match_step, step_map, bind_assoc]
   apply bind_congr; intro step
-  split
+  cases step.inflate using PlausibleIterStep.casesOn
   · simp only [pure_bind]
     simp [ihy ‹_›]
   · simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
@@ -727,11 +731,11 @@ theorem IterM.allM_filterMapM {α β β' : Type w} {m : Type w → Type w'} {n :
   rw [allM_eq_match_step, allM_eq_match_step, step_filterMapM, step_mapM, bind_assoc, bind_assoc]
   apply bind_congr; intro step
   split
-  · simp only [bind_assoc, pure_bind]
+  · simp only [bind_assoc, pure_bind, Shrink.inflate_deflate]
     apply bind_congr; intro fx
     split
     · simp [ihy ‹_›]
-    · simp only [PlausibleIterStep.yield, pure_bind]
+    · simp only [PlausibleIterStep.yield, pure_bind, Shrink.inflate_deflate]
       apply bind_congr; intro px
       split <;> simp [ihy ‹_›]
   · simp only [PlausibleIterStep.skip, pure_bind, bind_assoc]
@@ -747,7 +751,7 @@ theorem IterM.allM_mapM {α β β' : Type w} {m : Type w → Type w'} {n : Type
   rw [allM_eq_match_step, allM_eq_match_step, step_mapM, step_mapM, bind_assoc, bind_assoc]
   apply bind_congr; intro step
   split
-  · simp only [bind_assoc, pure_bind]
+  · simp only [bind_assoc, pure_bind, Shrink.inflate_deflate]
     apply bind_congr; intro fx
     simp [ihy ‹_›]
   · simp only [PlausibleIterStep.skip, pure_bind, bind_assoc]
@@ -767,7 +771,7 @@ theorem IterM.allM_filterM {α β : Type w} {m : Type w → Type w'} {n : Type w
   rw [allM_eq_match_step, allM_eq_match_step, step_mapM, step_filterM, bind_assoc, bind_assoc]
   apply bind_congr; intro step
   split
-  · simp only [bind_assoc, pure_bind]
+  · simp only [bind_assoc, pure_bind, Shrink.inflate_deflate]
     apply bind_congr; intro fx
     split <;> simp [ihy ‹_›]
   · simp only [PlausibleIterStep.skip, pure_bind, bind_assoc]
@@ -785,10 +789,11 @@ theorem IterM.allM_filterMap {α β β' : Type w} {m : Type w → Type w'}
   induction it using IterM.inductSteps with | step it ihy ihs
   rw [allM_eq_match_step, allM_eq_match_step, step_filterMap, bind_assoc]
   apply bind_congr; intro step
-  split
-  · split
+  cases step.inflate using PlausibleIterStep.casesOn
+  · simp only
+    split
     · simp [*, ihy ‹_›]
-    · simp only [*, PlausibleIterStep.yield, pure_bind]
+    · simp only [*, PlausibleIterStep.yield, pure_bind, Shrink.inflate_deflate]
       apply bind_congr; intro px
       split <;> simp [ihy ‹_›]
   · simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
@@ -802,8 +807,8 @@ theorem IterM.allM_map {α β β' : Type w} {m : Type w → Type w'}
   induction it using IterM.inductSteps with | step it ihy ihs
   rw [allM_eq_match_step, allM_eq_match_step, step_map, bind_assoc]
   apply bind_congr; intro step
-  split
-  · simp only [pure_bind]
+  cases step.inflate using PlausibleIterStep.casesOn
+  · simp only [pure_bind, Shrink.inflate_deflate]
     apply bind_congr; intro fx
     simp [ihy ‹_›]
   · simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
@@ -821,7 +826,7 @@ theorem IterM.allM_filter {α β : Type w} {m : Type w → Type w'}
   induction it using IterM.inductSteps with | step it ihy ihs
   rw [allM_eq_match_step, allM_eq_match_step, step_filter, bind_assoc]
   apply bind_congr; intro step
-  split
+  cases step.inflate using PlausibleIterStep.casesOn
   · simp only
     split <;> simp [ihy ‹_›]
   · simp only [PlausibleIterStep.skip, pure_bind]
@@ -867,10 +872,11 @@ theorem IterM.all_filterMap {α β β' : Type w} {m : Type w → Type w'}
   induction it using IterM.inductSteps with | step it ihy ihs
   rw [all_eq_match_step, all_eq_match_step, step_filterMap, bind_assoc]
   apply bind_congr; intro step
-  split
-  · split
+  cases step.inflate using PlausibleIterStep.casesOn
+  · simp only
+    split
     · simp [*, ihy ‹_›]
-    · simp only [*, PlausibleIterStep.yield, pure_bind]
+    · simp only [*, PlausibleIterStep.yield, pure_bind, Shrink.inflate_deflate]
       split <;> simp [ihy ‹_›]
   · simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
   · simp
@@ -883,7 +889,7 @@ theorem IterM.all_map {α β β' : Type w} {m : Type w → Type w'}
   induction it using IterM.inductSteps with | step it ihy ihs
   rw [all_eq_match_step, all_eq_match_step, step_map, bind_assoc]
   apply bind_congr; intro step
-  split
+  cases step.inflate using PlausibleIterStep.casesOn
   · simp only [pure_bind]
     simp [ihy ‹_›]
   · simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean
index f6d6a71d60..5855ae74b8 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean
@@ -21,7 +21,7 @@ theorem IterM.step_uLift [Iterator α m β] [Monad n] {it : IterM (α := α) m 
     [MonadLiftT m (ULiftT n)] :
     (it.uLift n).step = (do
       let step := (← (monadLift it.step : ULiftT n _).run).down
-      return ⟨Types.ULiftIterator.Monadic.modifyStep step.val, step.val, step.property, rfl⟩) :=
+      return .deflate ⟨Types.ULiftIterator.Monadic.modifyStep step.inflate.val, step.inflate.val, step.inflate.property, rfl⟩) :=
   rfl
 
 @[simp]
@@ -37,7 +37,7 @@ theorem IterM.toList_uLift [Iterator α m β] [Monad m] [Monad n] {it : IterM (
   apply bind_congr
   intro step
   simp [Types.ULiftIterator.Monadic.modifyStep]
-  cases step.down using PlausibleIterStep.casesOn
+  cases step.down.inflate using PlausibleIterStep.casesOn
   · simp only [uLift] at ihy
     simp [ihy ‹_›]
   · exact ihs ‹_›
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean
index 56927df870..807e226631 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean
@@ -77,7 +77,7 @@ theorem Iter.toArray_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [I
   simp only [Iter.toArray_eq_toArray_toIterM, Iter.step]
   rw [IterM.toArray_eq_match_step, Id.run_bind]
   generalize it.toIterM.step.run = step
-  cases step using PlausibleIterStep.casesOn <;> simp
+  cases step.inflate using PlausibleIterStep.casesOn <;> simp
 
 theorem Iter.toList_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
     [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
@@ -95,7 +95,7 @@ theorem Iter.toListRev_eq_match_step {α β} [Iterator α Id β] [Finite α Id]
       | .done => [] := by
   rw [Iter.toListRev_eq_toListRev_toIterM, IterM.toListRev_eq_match_step, Iter.step, Id.run_bind]
   generalize it.toIterM.step.run = step
-  cases step using PlausibleIterStep.casesOn <;> simp
+  cases step.inflate using PlausibleIterStep.casesOn <;> simp
 
 theorem Iter.getElem?_toList_eq_atIdxSlow? {α β}
     [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
index 73dfedac31..574915cb83 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
@@ -112,7 +112,7 @@ theorem Iter.forIn'_eq_match_step {α β : Type w} [Iterator α Id β]
   simp only [forIn'_eq]
   rw [IterM.DefaultConsumers.forIn'_eq_match_step]
   simp only [bind_map_left, Iter.step]
-  cases it.toIterM.step.run using PlausibleIterStep.casesOn
+  cases it.toIterM.step.run.inflate using PlausibleIterStep.casesOn
   · simp only [IterM.Step.toPure_yield, PlausibleIterStep.yield, toIter_toIterM, toIterM_toIter]
     apply bind_congr
     intro forInStep
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean
index c27e8e49f0..5b333ae73d 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean
@@ -46,7 +46,7 @@ theorem IterM.DefaultConsumers.toArrayMapped.go.aux₂ [Monad n] [LawfulMonad n]
 theorem IterM.DefaultConsumers.toArrayMapped_eq_match_step [Monad n] [LawfulMonad n]
     [Iterator α m β] [Finite α m] :
     IterM.DefaultConsumers.toArrayMapped lift f it (m := m) = letI : MonadLift m n := ⟨lift (δ := _)⟩; (do
-      match (← it.step).val with
+      match (← it.step).inflate.val with
       | .yield it' out =>
         return #[← f out] ++ (← IterM.DefaultConsumers.toArrayMapped lift f it' (m := m))
       | .skip it' => IterM.DefaultConsumers.toArrayMapped lift f it' (m := m)
@@ -54,12 +54,13 @@ theorem IterM.DefaultConsumers.toArrayMapped_eq_match_step [Monad n] [LawfulMona
   rw [IterM.DefaultConsumers.toArrayMapped, IterM.DefaultConsumers.toArrayMapped.go]
   apply bind_congr
   intro step
-  split <;> simp [IterM.DefaultConsumers.toArrayMapped.go.aux₂]
+  cases step.inflate using PlausibleIterStep.casesOn <;>
+    simp [IterM.DefaultConsumers.toArrayMapped.go.aux₂]
 
 theorem IterM.toArray_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     [IteratorCollect α m m] [LawfulIteratorCollect α m m] :
     it.toArray = (do
-      match (← it.step).val with
+      match (← it.step).inflate.val with
       | .yield it' out => return #[out] ++ (← it'.toArray)
       | .skip it' => it'.toArray
       | .done => return #[]) := by
@@ -82,7 +83,7 @@ theorem IterM.toArray_toList [Monad m] [LawfulMonad m] [Iterator α m β] [Finit
 theorem IterM.toList_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     [IteratorCollect α m m] [LawfulIteratorCollect α m m] {it : IterM (α := α) m β} :
     it.toList = (do
-      match (← it.step).val with
+      match (← it.step).inflate.val with
       | .yield it' out => return out :: (← it'.toList)
       | .skip it' => it'.toList
       | .done => return []) := by
@@ -114,7 +115,7 @@ theorem IterM.toListRev.go.aux₂ [Monad m] [LawfulMonad m] [Iterator α m β] [
 theorem IterM.toListRev_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     {it : IterM (α := α) m β} :
     it.toListRev = (do
-      match (← it.step).val with
+      match (← it.step).inflate.val with
       | .yield it' out => return (← it'.toListRev) ++ [out]
       | .skip it' => it'.toListRev
       | .done => return []) := by
@@ -122,7 +123,7 @@ theorem IterM.toListRev_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m 
   rw [toListRev.go]
   apply bind_congr
   intro step
-  cases step using PlausibleIterStep.casesOn <;> simp [IterM.toListRev.go.aux₂]
+  cases step.inflate using PlausibleIterStep.casesOn <;> simp [IterM.toListRev.go.aux₂]
 
 theorem IterM.reverse_toListRev [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     [IteratorCollect α m m] [LawfulIteratorCollect α m m]
@@ -134,7 +135,7 @@ theorem IterM.reverse_toListRev [Monad m] [LawfulMonad m] [Iterator α m β] [Fi
   rw [toListRev_eq_match_step, toList_eq_match_step, map_eq_pure_bind, bind_assoc]
   apply bind_congr
   intro step
-  cases step using PlausibleIterStep.casesOn <;> simp (discharger := assumption) [ihy, ihs]
+  cases step.inflate using PlausibleIterStep.casesOn <;> simp (discharger := assumption) [ihy, ihs]
 
 theorem IterM.toListRev_eq [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     [IteratorCollect α m m] [LawfulIteratorCollect α m m]
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
index c0a731000e..2338f7058e 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
@@ -23,7 +23,8 @@ theorem IterM.DefaultConsumers.forIn'_eq_match_step {α β : Type w} {m : Type w
     {it : IterM (α := α) m β} {init : γ}
     {P hP} {f : (b : β) → P b → (c : γ) → n (Subtype (plausible_forInStep b c))} :
     IterM.DefaultConsumers.forIn' lift γ plausible_forInStep wf it init P hP f =
-      (lift _ _ · it.step) (fun
+      (lift _ _ · it.step) (fun s =>
+          match s.inflate with
           | .yield it' out h => do
             match ← f out (hP _ <| .direct ⟨_, h⟩) init with
             | ⟨.yield c, _⟩ =>
@@ -36,7 +37,7 @@ theorem IterM.DefaultConsumers.forIn'_eq_match_step {α β : Type w} {m : Type w
           | .done _ => return init) := by
   rw [forIn']
   congr; ext step
-  cases step using PlausibleIterStep.casesOn <;> rfl
+  cases step.inflate using PlausibleIterStep.casesOn <;> rfl
 
 theorem IterM.forIn'_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
     {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n]
@@ -95,7 +96,7 @@ theorem IterM.forIn'_eq_match_step {α β : Type w} {m : Type w → Type w'} [It
     {f : (out : β) → _ → γ → n (ForInStep γ)} :
     letI : ForIn' n (IterM (α := α) m β) β _ := IterM.instForIn'
     ForIn'.forIn' it init f = (do
-      match ← it.step with
+      match (← it.step).inflate with
       | .yield it' out h =>
         match ← f out (.direct ⟨_, h⟩) init with
         | .yield c =>
@@ -109,7 +110,7 @@ theorem IterM.forIn'_eq_match_step {α β : Type w} {m : Type w → Type w'} [It
   rw [IterM.forIn'_eq, DefaultConsumers.forIn'_eq_match_step]
   apply bind_congr
   intro step
-  cases step using PlausibleIterStep.casesOn
+  cases step.inflate using PlausibleIterStep.casesOn
   · simp only [map_eq_pure_bind, bind_assoc]
     apply bind_congr
     intro forInStep
@@ -129,7 +130,7 @@ theorem IterM.forIn_eq_match_step {α β : Type w} {m : Type w → Type w'} [Ite
     [MonadLiftT m n] [LawfulMonadLiftT m n] {γ : Type w} {it : IterM (α := α) m β} {init : γ}
     {f : β → γ → n (ForInStep γ)} :
     ForIn.forIn it init f = (do
-      match ← it.step with
+      match (← it.step).inflate with
       | .yield it' out _ =>
         match ← f out init with
         | .yield c => ForIn.forIn it' c f
@@ -153,7 +154,7 @@ theorem IterM.forM_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iter
     [MonadLiftT m n] [LawfulMonadLiftT m n] {it : IterM (α := α) m β}
     {f : β → n PUnit} :
     ForM.forM it f = (do
-      match ← it.step with
+      match (← it.step).inflate with
       | .yield it' out _ =>
         f out
         ForM.forM it' f
@@ -162,7 +163,7 @@ theorem IterM.forM_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iter
   rw [forM_eq_forIn, forIn_eq_match_step]
   apply bind_congr
   intro step
-  cases step using PlausibleIterStep.casesOn <;> simp [forM_eq_forIn]
+  cases step.inflate using PlausibleIterStep.casesOn <;> simp [forM_eq_forIn]
 
 theorem IterM.foldM_eq_forIn {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
     {n : Type w → Type w''} [Monad n] [IteratorLoop α m n] [MonadLiftT m n] {f : γ → β → n γ}
@@ -183,14 +184,14 @@ theorem IterM.foldM_eq_match_step {α β γ : Type w} {m : Type w → Type w'} [
     [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n]
     {f : γ → β → n γ} {init : γ} {it : IterM (α := α) m β} :
     it.foldM (init := init) f = (do
-      match ← it.step with
+      match (← it.step).inflate with
       | .yield it' out _ => it'.foldM (init := ← f init out) f
       | .skip it' _ => it'.foldM (init := init) f
       | .done _ => return init) := by
   rw [IterM.foldM_eq_forIn, IterM.forIn_eq_match_step]
   apply bind_congr
   intro step
-  cases step using PlausibleIterStep.casesOn <;> simp [foldM_eq_forIn]
+  cases step.inflate using PlausibleIterStep.casesOn <;> simp [foldM_eq_forIn]
 
 theorem IterM.fold_eq_forIn {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β]
     [Finite α m] [Monad m]
@@ -218,7 +219,7 @@ theorem IterM.fold_eq_match_step {α β γ : Type w} {m : Type w → Type w'} [I
     [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
     {f : γ → β → γ} {init : γ} {it : IterM (α := α) m β} :
     it.fold (init := init) f = (do
-      match ← it.step with
+      match (← it.step).inflate with
       | .yield it' out _ => it'.fold (init := f init out) f
       | .skip it' _ => it'.fold (init := init) f
       | .done _ => return init) := by
@@ -226,7 +227,7 @@ theorem IterM.fold_eq_match_step {α β γ : Type w} {m : Type w → Type w'} [I
   simp only [fold_eq_foldM]
   apply bind_congr
   intro step
-  cases step using PlausibleIterStep.casesOn <;> simp
+  cases step.inflate using PlausibleIterStep.casesOn <;> simp
 
 -- The argument `f : γ₁ → γ₂` is intentionally explicit, as it is sometimes not found by unification.
 theorem IterM.fold_hom {m : Type w → Type w'} [Iterator α m β] [Finite α m]
@@ -260,7 +261,7 @@ theorem IterM.toList_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator
   simp only [map_eq_pure_bind, bind_assoc]
   apply bind_congr
   intro step
-  cases step using PlausibleIterStep.casesOn
+  cases step.inflate using PlausibleIterStep.casesOn
   · rename_i it' out h
     specialize ihy h (l' ++ [out])
     simpa using ihy
@@ -296,7 +297,7 @@ theorem IterM.drain_eq_match_step {α β : Type w} {m : Type w → Type w'} [Ite
     [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
     {it : IterM (α := α) m β} :
     it.drain = (do
-      match ← it.step with
+      match (← it.step).inflate with
       | .yield it' _ _ => it'.drain
       | .skip it' _ => it'.drain
       | .done _ => return .unit) := by
@@ -313,7 +314,7 @@ theorem IterM.drain_eq_map_toList {α β : Type w} {m : Type w → Type w'} [Ite
   simp only [map_eq_pure_bind, bind_assoc]
   apply bind_congr
   intro step
-  cases step using PlausibleIterStep.casesOn
+  cases step.inflate using PlausibleIterStep.casesOn
   · rename_i it' out h
     simp [ihy h]
   · rename_i it' h
@@ -348,7 +349,7 @@ theorem IterM.anyM_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iter
     [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
     {it : IterM (α := α) m β} {p : β → m (ULift Bool)} :
     it.anyM p = (do
-      match (← it.step).val with
+      match (← it.step).inflate.val with
       | .yield it' x =>
         if (← p x).down then
           return .up true
@@ -359,7 +360,7 @@ theorem IterM.anyM_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iter
   rw [anyM_eq_forIn, forIn_eq_match_step]
   simp only [monadLift_self, bind_assoc]
   apply bind_congr; intro step
-  split
+  cases step.inflate using PlausibleIterStep.casesOn
   · apply bind_congr; intro px
     split
     · simp
@@ -383,7 +384,7 @@ theorem IterM.any_eq_match_step {α β : Type w} {m : Type w → Type w'} [Itera
     [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
     {it : IterM (α := α) m β} {p : β → Bool} :
     it.any p = (do
-      match (← it.step).val with
+      match (← it.step).inflate.val with
       | .yield it' x =>
         if p x then
           return .up true
@@ -422,7 +423,7 @@ theorem IterM.allM_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iter
     [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
     {it : IterM (α := α) m β} {p : β → m (ULift Bool)} :
     it.allM p = (do
-      match (← it.step).val with
+      match (← it.step).inflate.val with
       | .yield it' x =>
         if (← p x).down then
           it'.allM p
@@ -433,7 +434,7 @@ theorem IterM.allM_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iter
   rw [allM_eq_forIn, forIn_eq_match_step]
   simp only [monadLift_self, bind_assoc]
   apply bind_congr; intro step
-  split
+  cases step.inflate using PlausibleIterStep.casesOn
   · apply bind_congr; intro px
     split
     · simp [allM_eq_forIn]
@@ -457,7 +458,7 @@ theorem IterM.all_eq_match_step {α β : Type w} {m : Type w → Type w'} [Itera
     [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
     {it : IterM (α := α) m β} {p : β → Bool} :
     it.all p = (do
-      match (← it.step).val with
+      match (← it.step).inflate.val with
       | .yield it' x =>
         if p x then
           it'.all p
@@ -489,7 +490,7 @@ theorem IterM.allM_eq_not_anyM_not {α β : Type w} {m : Type w → Type w'} [It
   induction it using IterM.inductSteps with | step it ihy ihs =>
   rw [allM_eq_match_step, anyM_eq_match_step, map_eq_pure_bind, bind_assoc]
   apply bind_congr; intro step
-  cases step using PlausibleIterStep.casesOn
+  cases step.inflate using PlausibleIterStep.casesOn
   · simp only [map_eq_pure_bind, bind_assoc, pure_bind]
     apply bind_congr; intro px
     split
@@ -505,7 +506,7 @@ theorem IterM.all_eq_not_any_not {α β : Type w} {m : Type w → Type w'} [Iter
   induction it using IterM.inductSteps with | step it ihy ihs =>
   rw [all_eq_match_step, any_eq_match_step, map_eq_pure_bind, bind_assoc]
   apply bind_congr; intro step
-  cases step using PlausibleIterStep.casesOn
+  cases step.inflate using PlausibleIterStep.casesOn
   · simp only
     split
     · simp [*, ihy ‹_›]
diff --git a/src/Init/Data/Range/Polymorphic/RangeIterator.lean b/src/Init/Data/Range/Polymorphic/RangeIterator.lean
index 18adffa5f7..0b1ca22fbd 100644
--- a/src/Init/Data/Range/Polymorphic/RangeIterator.lean
+++ b/src/Init/Data/Range/Polymorphic/RangeIterator.lean
@@ -89,7 +89,7 @@ theorem Iterator.step_eq_monadicStep [UpwardEnumerable α] [LE α] [DecidableLE
 instance [UpwardEnumerable α] [LE α] [DecidableLE α] :
     Iterator (Rxc.Iterator α) Id α where
   IsPlausibleStep it step := step = Iterator.Monadic.step it
-  step it := pure ⟨Iterator.Monadic.step it, rfl⟩
+  step it := pure <| .deflate <| ⟨Iterator.Monadic.step it, rfl⟩
 
 theorem Iterator.Monadic.isPlausibleStep_iff [UpwardEnumerable α] [LE α] [DecidableLE α]
     {it : IterM (α := Rxc.Iterator α) Id α} {step} :
@@ -98,7 +98,7 @@ theorem Iterator.Monadic.isPlausibleStep_iff [UpwardEnumerable α] [LE α] [Deci
 
 theorem Iterator.Monadic.step_eq_step [UpwardEnumerable α] [LE α] [DecidableLE α]
     {it : IterM (α := Rxc.Iterator α) Id α} :
-    it.step = pure ⟨Iterator.Monadic.step it, isPlausibleStep_iff.mpr rfl⟩ := by
+    it.step = pure (.deflate ⟨Iterator.Monadic.step it, isPlausibleStep_iff.mpr rfl⟩) := by
   simp [IterM.step, Iterators.Iterator.step]
 
 theorem Iterator.isPlausibleStep_iff [UpwardEnumerable α] [LE α] [DecidableLE α]
@@ -562,7 +562,7 @@ theorem Iterator.instIteratorLoop.loop_eq [UpwardEnumerable α] [LE α] [Decidab
         rw [IterM.DefaultConsumers.forIn']
         simp only [Monadic.step_eq_step, Monadic.step, ↓reduceIte, *,
           Internal.LawfulMonadLiftBindFunction.liftBind_pure]
-        rw [loop_eq (lift := lift)]
+        rw [loop_eq (lift := lift), Shrink.inflate_deflate]
         apply bind_congr
         intro step
         split
@@ -666,7 +666,7 @@ theorem Iterator.step_eq_monadicStep [UpwardEnumerable α] [LT α] [DecidableLT
 instance [UpwardEnumerable α] [LT α] [DecidableLT α] :
     Iterator (Rxo.Iterator α) Id α where
   IsPlausibleStep it step := step = Iterator.Monadic.step it
-  step it := pure ⟨Iterator.Monadic.step it, rfl⟩
+  step it := pure (.deflate ⟨Iterator.Monadic.step it, rfl⟩)
 
 theorem Iterator.Monadic.isPlausibleStep_iff [UpwardEnumerable α] [LT α] [DecidableLT α]
     {it : IterM (α := Rxo.Iterator α) Id α} {step} :
@@ -675,7 +675,7 @@ theorem Iterator.Monadic.isPlausibleStep_iff [UpwardEnumerable α] [LT α] [Deci
 
 theorem Iterator.Monadic.step_eq_step [UpwardEnumerable α] [LT α] [DecidableLT α]
     {it : IterM (α := Rxo.Iterator α) Id α} :
-    it.step = pure ⟨Iterator.Monadic.step it, isPlausibleStep_iff.mpr rfl⟩ := by
+    it.step = pure (.deflate ⟨Iterator.Monadic.step it, isPlausibleStep_iff.mpr rfl⟩) := by
   simp [IterM.step, Iterators.Iterator.step]
 
 theorem Iterator.isPlausibleStep_iff [UpwardEnumerable α] [LT α] [DecidableLT α]
@@ -1139,7 +1139,7 @@ theorem Iterator.instIteratorLoop.loop_eq [UpwardEnumerable α] [LT α] [Decidab
         rw [IterM.DefaultConsumers.forIn']
         simp only [Monadic.step_eq_step, Monadic.step, ↓reduceIte, *,
           Internal.LawfulMonadLiftBindFunction.liftBind_pure]
-        rw [loop_eq (lift := lift)]
+        rw [loop_eq (lift := lift), Shrink.inflate_deflate]
         apply bind_congr
         intro step
         split
@@ -1233,7 +1233,7 @@ theorem Iterator.step_eq_monadicStep [UpwardEnumerable α]
 instance [UpwardEnumerable α] :
     Iterator (Rxi.Iterator α) Id α where
   IsPlausibleStep it step := step = Iterator.Monadic.step it
-  step it := pure ⟨Iterator.Monadic.step it, rfl⟩
+  step it := pure (.deflate ⟨Iterator.Monadic.step it, rfl⟩)
 
 theorem Iterator.Monadic.isPlausibleStep_iff [UpwardEnumerable α]
     {it : IterM (α := Rxi.Iterator α) Id α} {step} :
@@ -1242,7 +1242,7 @@ theorem Iterator.Monadic.isPlausibleStep_iff [UpwardEnumerable α]
 
 theorem Iterator.Monadic.step_eq_step [UpwardEnumerable α]
     {it : IterM (α := Rxi.Iterator α) Id α} :
-    it.step = pure ⟨Iterator.Monadic.step it, isPlausibleStep_iff.mpr rfl⟩ := by
+    it.step = pure (.deflate ⟨Iterator.Monadic.step it, isPlausibleStep_iff.mpr rfl⟩) := by
   simp [IterM.step, Iterators.Iterator.step]
 
 theorem Iterator.isPlausibleStep_iff [UpwardEnumerable α]
@@ -1615,7 +1615,7 @@ theorem Iterator.instIteratorLoop.loop_eq [UpwardEnumerable α]
         rw [IterM.DefaultConsumers.forIn']
         simp only [Monadic.step_eq_step, Monadic.step, *,
           Internal.LawfulMonadLiftBindFunction.liftBind_pure]
-        rw [loop_eq (lift := lift)]
+        rw [loop_eq (lift := lift), Shrink.inflate_deflate]
         apply bind_congr
         intro step
         split
@@ -1644,7 +1644,7 @@ instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α]
     simp only [Internal.LawfulMonadLiftBindFunction.liftBind_pure]
     split
     · rename_i it f next upperBound f'
-      rw [instIteratorLoop.loop_eq (lift := lift)]
+      rw [instIteratorLoop.loop_eq (lift := lift), Shrink.inflate_deflate]
       apply bind_congr
       intro step
       split
diff --git a/src/Init/Data/String/Pattern/Char.lean b/src/Init/Data/String/Pattern/Char.lean
index 80ead3e0f2..ed35339fe5 100644
--- a/src/Init/Data/String/Pattern/Char.lean
+++ b/src/Init/Data/String/Pattern/Char.lean
@@ -50,14 +50,14 @@ instance (s : Slice) : Std.Iterators.Iterator (ForwardCharSearcher s) Id (Search
     | .done => it.internalState.currPos = s.endPos
   step := fun ⟨currPos, needle⟩ =>
     if h1 : currPos = s.endPos then
-      pure ⟨.done, by simp [h1]⟩
+      pure (.deflate ⟨.done, by simp [h1]⟩)
     else
       let nextPos := currPos.next h1
       let nextIt := ⟨nextPos, needle⟩
       if h2 : currPos.get h1 = needle then
-        pure ⟨.yield nextIt (.matched currPos nextPos), by simp [h1, h2, nextIt, nextPos]⟩
+        pure (.deflate ⟨.yield nextIt (.matched currPos nextPos), by simp [h1, h2, nextIt, nextPos]⟩)
       else
-        pure ⟨.yield nextIt (.rejected currPos nextPos), by simp [h1, h2, nextIt, nextPos]⟩
+        pure (.deflate ⟨.yield nextIt (.rejected currPos nextPos), by simp [h1, h2, nextIt, nextPos]⟩)
 
 def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharSearcher s) Id where
   rel := InvImage WellFoundedRelation.rel
@@ -119,14 +119,14 @@ instance (s : Slice) : Std.Iterators.Iterator (BackwardCharSearcher s) Id (Searc
     | .done => it.internalState.currPos = s.startPos
   step := fun ⟨currPos, needle⟩ =>
     if h1 : currPos = s.startPos then
-      pure ⟨.done, by simp [h1]⟩
+      pure (.deflate ⟨.done, by simp [h1]⟩)
     else
       let nextPos := currPos.prev h1
       let nextIt := ⟨nextPos, needle⟩
       if h2 : nextPos.get Pos.prev_ne_endPos = needle then
-        pure ⟨.yield nextIt (.matched nextPos currPos), by simp [h1, h2, nextIt, nextPos]⟩
+        pure (.deflate ⟨.yield nextIt (.matched nextPos currPos), by simp [h1, h2, nextIt, nextPos]⟩)
       else
-        pure ⟨.yield nextIt (.rejected nextPos currPos), by simp [h1, h2, nextIt, nextPos]⟩
+        pure (.deflate ⟨.yield nextIt (.rejected nextPos currPos), by simp [h1, h2, nextIt, nextPos]⟩)
 
 def finitenessRelation : Std.Iterators.FinitenessRelation (BackwardCharSearcher s) Id where
   rel := InvImage WellFoundedRelation.rel
diff --git a/src/Init/Data/String/Pattern/Pred.lean b/src/Init/Data/String/Pattern/Pred.lean
index ffef03637a..232e281ae0 100644
--- a/src/Init/Data/String/Pattern/Pred.lean
+++ b/src/Init/Data/String/Pattern/Pred.lean
@@ -51,14 +51,14 @@ instance (s : Slice) : Std.Iterators.Iterator (ForwardCharPredSearcher s) Id (Se
     | .done => it.internalState.currPos = s.endPos
   step := fun ⟨currPos, needle⟩ =>
     if h1 : currPos = s.endPos then
-      pure ⟨.done, by simp [h1]⟩
+      pure (.deflate ⟨.done, by simp [h1]⟩)
     else
       let nextPos := currPos.next h1
       let nextIt := ⟨nextPos, needle⟩
       if h2 : needle <| currPos.get h1 then
-        pure ⟨.yield nextIt (.matched currPos nextPos), by simp [h1, h2, nextPos, nextIt]⟩
+        pure (.deflate ⟨.yield nextIt (.matched currPos nextPos), by simp [h1, h2, nextPos, nextIt]⟩)
       else
-        pure ⟨.yield nextIt (.rejected currPos nextPos), by simp [h1, h2, nextPos, nextIt]⟩
+        pure (.deflate ⟨.yield nextIt (.rejected currPos nextPos), by simp [h1, h2, nextPos, nextIt]⟩)
 
 
 def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharPredSearcher s) Id where
@@ -121,14 +121,14 @@ instance (s : Slice) : Std.Iterators.Iterator (BackwardCharPredSearcher s) Id (S
     | .done => it.internalState.currPos = s.startPos
   step := fun ⟨currPos, needle⟩ =>
     if h1 : currPos = s.startPos then
-      pure ⟨.done, by simp [h1]⟩
+      pure (.deflate ⟨.done, by simp [h1]⟩)
     else
       let nextPos := currPos.prev h1
       let nextIt := ⟨nextPos, needle⟩
       if h2 : needle <| nextPos.get Pos.prev_ne_endPos then
-        pure ⟨.yield nextIt (.matched nextPos currPos), by simp [h1, h2, nextIt, nextPos]⟩
+        pure (.deflate ⟨.yield nextIt (.matched nextPos currPos), by simp [h1, h2, nextIt, nextPos]⟩)
       else
-        pure ⟨.yield nextIt (.rejected nextPos currPos), by simp [h1, h2, nextIt, nextPos]⟩
+        pure (.deflate ⟨.yield nextIt (.rejected nextPos currPos), by simp [h1, h2, nextIt, nextPos]⟩)
 
 def finitenessRelation : Std.Iterators.FinitenessRelation (BackwardCharPredSearcher s) Id where
   rel := InvImage WellFoundedRelation.rel
diff --git a/src/Init/Data/String/Pattern/String.lean b/src/Init/Data/String/Pattern/String.lean
index 13850a5385..9c839985c6 100644
--- a/src/Init/Data/String/Pattern/String.lean
+++ b/src/Init/Data/String/Pattern/String.lean
@@ -88,9 +88,9 @@ instance (s : Slice) : Std.Iterators.Iterator (ForwardSliceSearcher s) Id (Searc
     | .empty pos =>
       let res := .matched pos pos
       if h : pos ≠ s.endPos then
-        pure ⟨.yield ⟨.empty (pos.next h)⟩ res, by simp⟩
+        pure (.deflate ⟨.yield ⟨.empty (pos.next h)⟩ res, by simp⟩)
       else
-        pure ⟨.yield ⟨.atEnd⟩ res, by simp⟩
+        pure (.deflate ⟨.yield ⟨.atEnd⟩ res, by simp⟩)
     | .proper needle table stackPos needlePos =>
       let rec findNext (startPos : String.Pos.Raw)
           (currStackPos : String.Pos.Raw) (needlePos : String.Pos.Raw) (h : stackPos ≤ currStackPos) :=
@@ -112,7 +112,7 @@ instance (s : Slice) : Std.Iterators.Iterator (ForwardSliceSearcher s) Id (Searc
                 omega
               · apply Pos.Raw.IsValidForSlice.le_utf8ByteSize
                 apply Pos.isValidForSlice
-            ⟨.yield ⟨.proper needle table nextStackPos needlePos⟩ res, hiter⟩
+            .deflate ⟨.yield ⟨.proper needle table nextStackPos needlePos⟩ res, hiter⟩
           else
             let needlePos := needlePos.inc
             if needlePos == needle.rawEndPos then
@@ -128,7 +128,7 @@ instance (s : Slice) : Std.Iterators.Iterator (ForwardSliceSearcher s) Id (Searc
                   omega
                 · simp [String.Pos.Raw.le_iff] at h1 ⊢
                   omega
-              ⟨.yield ⟨.proper needle table nextStackPos 0⟩ res, hiter⟩
+              .deflate ⟨.yield ⟨.proper needle table nextStackPos 0⟩ res, hiter⟩
             else
               have hinv := by
                 simp [String.Pos.Raw.le_iff] at h ⊢
@@ -137,16 +137,16 @@ instance (s : Slice) : Std.Iterators.Iterator (ForwardSliceSearcher s) Id (Searc
         else
           if startPos != s.rawEndPos then
             let res := .rejected (s.pos! startPos) (s.pos! currStackPos)
-            ⟨.yield ⟨.atEnd⟩ res, by simp⟩
+            .deflate ⟨.yield ⟨.atEnd⟩ res, by simp⟩
           else
-            ⟨.done, by simp⟩
+            .deflate ⟨.done, by simp⟩
         termination_by s.utf8ByteSize - currStackPos.byteIdx
         decreasing_by
           simp at h1 ⊢
           omega
 
       findNext stackPos stackPos needlePos (by simp)
-    | .atEnd => pure ⟨.done, by simp⟩
+    | .atEnd => pure (.deflate ⟨.done, by simp⟩)
 
 private def toPair : ForwardSliceSearcher s → (Nat × Nat)
   | .empty pos => (1, s.utf8ByteSize - pos.offset.byteIdx)
diff --git a/src/Init/Data/String/Slice.lean b/src/Init/Data/String/Slice.lean
index 9ae61bad10..bacc1bc79c 100644
--- a/src/Init/Data/String/Slice.lean
+++ b/src/Init/Data/String/Slice.lean
@@ -131,11 +131,11 @@ instance [Pure m] : Std.Iterators.Iterator (SplitIterator ρ) m Slice where
       | some (searcher, startPos, endPos) =>
         let slice := s.replaceStartEnd! currPos startPos
         let nextIt := ⟨.operating s endPos searcher⟩
-        pure ⟨.yield nextIt slice, by simp⟩
+        pure (.deflate ⟨.yield nextIt slice, by simp⟩)
       | none =>
         let slice := s.replaceStart currPos
-        pure ⟨.yield ⟨.atEnd⟩ slice, by simp⟩
-    | .atEnd => pure ⟨.done, by simp⟩
+        pure (.deflate ⟨.yield ⟨.atEnd⟩ slice, by simp⟩)
+    | .atEnd => pure (.deflate ⟨.done, by simp⟩)
 
 -- TODO: Finiteness after we have a notion of lawful searcher
 
@@ -190,14 +190,14 @@ instance [Pure m] : Std.Iterators.Iterator (SplitInclusiveIterator ρ) m Slice w
       | some (searcher, _, endPos) =>
         let slice := s.replaceStartEnd! currPos endPos
         let nextIt := ⟨.operating s endPos searcher⟩
-        pure ⟨.yield nextIt slice, by simp⟩
+        pure (.deflate ⟨.yield nextIt slice, by simp⟩)
       | none =>
         if currPos != s.endPos then
           let slice := s.replaceStart currPos
-          pure ⟨.yield ⟨.atEnd⟩ slice, by simp⟩
+          pure (.deflate ⟨.yield ⟨.atEnd⟩ slice, by simp⟩)
         else
-          pure ⟨.done, by simp⟩
-    | .atEnd => pure ⟨.done, by simp⟩
+          pure (.deflate ⟨.done, by simp⟩)
+    | .atEnd => pure (.deflate ⟨.done, by simp⟩)
 
 -- TODO: Finiteness after we have a notion of lawful searcher
 
@@ -464,14 +464,14 @@ instance [Pure m] : Std.Iterators.Iterator (RevSplitIterator ρ) m Slice where
       | some (searcher, startPos, endPos) =>
         let slice := s.replaceStartEnd! endPos currPos
         let nextIt := ⟨.operating s startPos searcher⟩
-        pure ⟨.yield nextIt slice, by simp⟩
+        pure (.deflate ⟨.yield nextIt slice, by simp⟩)
       | none =>
         if currPos ≠ s.startPos then
           let slice := s.replaceEnd currPos
-          pure ⟨.yield ⟨.atEnd⟩ slice, by simp⟩
+          pure (.deflate ⟨.yield ⟨.atEnd⟩ slice, by simp⟩)
         else
-          pure ⟨.done, by simp⟩
-    | .atEnd => pure ⟨.done, by simp⟩
+          pure (.deflate ⟨.done, by simp⟩)
+    | .atEnd => pure (.deflate ⟨.done, by simp⟩)
 
 -- TODO: Finiteness after we have a notion of lawful searcher
 
@@ -733,9 +733,9 @@ instance [Pure m] :
     | .done => it.internalState.currPos = s.endPos
   step := fun ⟨⟨currPos⟩⟩ =>
     if h : currPos = s.endPos then
-      pure ⟨.done, by simp [h]⟩
+      pure (.deflate ⟨.done, by simp [h]⟩)
     else
-      pure ⟨.yield ⟨⟨currPos.next h⟩⟩ ⟨currPos, h⟩, by simp [h]⟩
+      pure (.deflate ⟨.yield ⟨⟨currPos.next h⟩⟩ ⟨currPos, h⟩, by simp [h]⟩)
 
 private def finitenessRelation [Pure m] :
     Std.Iterators.FinitenessRelation (PosIterator s) m where
@@ -819,10 +819,10 @@ instance [Pure m] :
     | .done => it.internalState.currPos = s.startPos
   step := fun ⟨⟨currPos⟩⟩ =>
     if h : currPos = s.startPos then
-      pure ⟨.done, by simp [h]⟩
+      pure (.deflate ⟨.done, by simp [h]⟩)
     else
       let prevPos := currPos.prev h
-      pure ⟨.yield ⟨⟨prevPos⟩⟩ ⟨prevPos, Pos.prev_ne_endPos⟩, by simp [h, prevPos]⟩
+      pure (.deflate ⟨.yield ⟨⟨prevPos⟩⟩ ⟨prevPos, Pos.prev_ne_endPos⟩, by simp [h, prevPos]⟩)
 
 private def finitenessRelation [Pure m] :
     Std.Iterators.FinitenessRelation (RevPosIterator s) m where
@@ -905,9 +905,9 @@ instance [Pure m] : Std.Iterators.Iterator ByteIterator m UInt8 where
     | .done => ¬ it.internalState.offset < it.internalState.s.rawEndPos
   step := fun ⟨s, offset⟩ =>
     if h : offset < s.rawEndPos then
-      pure ⟨.yield ⟨s, offset.inc⟩ (s.getUTF8Byte offset h), by simp [h]⟩
+      pure (.deflate ⟨.yield ⟨s, offset.inc⟩ (s.getUTF8Byte offset h), by simp [h]⟩)
     else
-      pure ⟨.done, by simp [h]⟩
+      pure (.deflate ⟨.done, by simp [h]⟩)
 
 private def finitenessRelation [Pure m] :
     Std.Iterators.FinitenessRelation (ByteIterator) m where
@@ -994,9 +994,9 @@ instance [Pure m] : Std.Iterators.Iterator RevByteIterator m UInt8 where
         simp [String.Pos.Raw.le_iff, nextOffset] at hinv ⊢
         omega
       have hiter := by simp [nextOffset, hbound, h]
-      pure ⟨.yield ⟨s, nextOffset, hinv⟩ (s.getUTF8Byte nextOffset hbound), hiter⟩
+      pure (.deflate ⟨.yield ⟨s, nextOffset, hinv⟩ (s.getUTF8Byte nextOffset hbound), hiter⟩)
     else
-      pure ⟨.done, by simpa using h⟩
+      pure (.deflate ⟨.done, by simpa using h⟩)
 
 private def finitenessRelation [Pure m] :
     Std.Iterators.FinitenessRelation (RevByteIterator) m where
diff --git a/src/Std/Data/Iterators/Combinators/Monadic/Drop.lean b/src/Std/Data/Iterators/Combinators/Monadic/Drop.lean
index 7f312397b5..fdb5a2f000 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/Drop.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic/Drop.lean
@@ -72,15 +72,15 @@ inductive Drop.PlausibleStep [Iterator α m β] (it : IterM (α := Drop α m β)
 instance Drop.instIterator [Monad m] [Iterator α m β] : Iterator (Drop α m β) m β where
   IsPlausibleStep := Drop.PlausibleStep
   step it := do
-    match ← it.internalState.inner.step with
+    match (← it.internalState.inner.step).inflate with
     | .yield it' out h =>
       match h' : it.internalState.remaining with
-      | 0 => pure <| .yield (it'.drop 0) out (.yield h h')
-      | k + 1 => pure <| .skip (it'.drop k) (.drop h h')
+      | 0 => pure <| .deflate <| .yield (it'.drop 0) out (.yield h h')
+      | k + 1 => pure <| .deflate <| .skip (it'.drop k) (.drop h h')
     | .skip it' h =>
-      pure <| .skip (it'.drop it.internalState.remaining) (.skip h)
+      pure <| .deflate <| .skip (it'.drop it.internalState.remaining) (.skip h)
     | .done h =>
-      pure <| .done (.done h)
+      pure <| .deflate <| .done (.done h)
 
 private def Drop.FiniteRel (m : Type w → Type w') [Iterator α m β] [Finite α m] :
     IterM (α := Drop α m β) m β → IterM (α := Drop α m β) m β → Prop :=
diff --git a/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean b/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean
index 594cf157cb..14b4583b5e 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean
@@ -227,21 +227,21 @@ instance DropWhile.instIterator [Monad m] [Iterator α m β] {P} :
     Iterator (DropWhile α m β P) m β where
   IsPlausibleStep := DropWhile.PlausibleStep
   step it := do
-    match ← it.internalState.inner.step with
+    match (← it.internalState.inner.step).inflate with
     | .yield it' out h =>
       if h' : it.internalState.dropping = true then
         match ← (P out).operation with
         | ⟨.up true, h''⟩ =>
-          return .skip (IterM.Intermediate.dropWhileWithPostcondition P true it') (.dropped h h' h'')
+          return .deflate <| .skip (IterM.Intermediate.dropWhileWithPostcondition P true it') (.dropped h h' h'')
         | ⟨.up false, h''⟩ =>
-          return .yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out (.start h h' h'')
+          return .deflate <| .yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out (.start h h' h'')
       else
-        return .yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out
+        return .deflate <| .yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out
             (.yield h (Bool.not_eq_true _ ▸ h'))
     | .skip it' h =>
-      return .skip (IterM.Intermediate.dropWhileWithPostcondition P it.internalState.dropping it') (.skip h)
+      return .deflate <| .skip (IterM.Intermediate.dropWhileWithPostcondition P it.internalState.dropping it') (.skip h)
     | .done h =>
-      return .done (.done h)
+      return .deflate <| .done (.done h)
 
 private def DropWhile.instFinitenessRelation [Monad m] [Iterator α m β]
     [Finite α m] {P} :
diff --git a/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean b/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean
index e75c2bfe39..9d715029ea 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean
@@ -33,7 +33,7 @@ instance [Iterator α m β] [IteratorAccess α m] [Monad m] :
         (step.mapIterator (Types.StepSizeIterator.inner ∘ IterM.internalState)) ∧
       ∀ it' out, step = .yield it' out →
         it'.internalState.n = it.internalState.n ∧ it'.internalState.nextIdx = it.internalState.n
-  step it := (fun s => ⟨s.1.mapIterator (⟨⟨it.internalState.n, it.internalState.n, ·⟩⟩), by
+  step it := (fun s => .deflate ⟨s.1.mapIterator (⟨⟨it.internalState.n, it.internalState.n, ·⟩⟩), by
       simp only [IterStep.mapIterator_mapIterator]
       refine cast ?_ s.property
       rw (occs := [1]) [← IterStep.mapIterator_id (step := s.val)]
diff --git a/src/Std/Data/Iterators/Combinators/Monadic/Take.lean b/src/Std/Data/Iterators/Combinators/Monadic/Take.lean
index fa19838f29..76fc6bc436 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/Take.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic/Take.lean
@@ -80,12 +80,12 @@ instance Take.instIterator [Monad m] [Iterator α m β] : Iterator (Take α m β
   IsPlausibleStep := Take.PlausibleStep
   step it :=
     match h : it.internalState.remaining with
-    | 0 => pure <| .done (.depleted h)
+    | 0 => pure <| .deflate <| .done (.depleted h)
     | k + 1 => do
-      match ← it.internalState.inner.step with
-      | .yield it' out h' => pure <| .yield (it'.take k) out (.yield h' h)
-      | .skip it' h' => pure <| .skip (it'.take (k + 1)) (.skip h' h)
-      | .done h' => pure <| .done (.done h')
+      match (← it.internalState.inner.step).inflate with
+      | .yield it' out h' => pure <| .deflate <| .yield (it'.take k) out (.yield h' h)
+      | .skip it' h' => pure <| .deflate <| .skip (it'.take (k + 1)) (.skip h' h)
+      | .done h' => pure <| .deflate <| .done (.done h')
 
 def Take.Rel (m : Type w → Type w') [Monad m] [Iterator α m β] [Productive α m] :
     IterM (α := Take α m β) m β → IterM (α := Take α m β) m β → Prop :=
diff --git a/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean b/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean
index 1f5fbf4fb5..74f7be6618 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean
@@ -181,12 +181,12 @@ instance TakeWhile.instIterator [Monad m] [Iterator α m β] {P} :
     Iterator (TakeWhile α m β P) m β where
   IsPlausibleStep := TakeWhile.PlausibleStep
   step it := do
-    match ← it.internalState.inner.step with
+    match (← it.internalState.inner.step).inflate with
     | .yield it' out h => match ← (P out).operation with
-      | ⟨.up true, h'⟩ => pure <| .yield (it'.takeWhileWithPostcondition P) out (.yield h h')
-      | ⟨.up false, h'⟩ => pure <| .done (.rejected h h')
-    | .skip it' h => pure <| .skip (it'.takeWhileWithPostcondition P) (.skip h)
-    | .done h => pure <| .done (.done h)
+      | ⟨.up true, h'⟩ => pure <| .deflate <| .yield (it'.takeWhileWithPostcondition P) out (.yield h h')
+      | ⟨.up false, h'⟩ => pure <| .deflate <| .done (.rejected h h')
+    | .skip it' h => pure <| .deflate <| .skip (it'.takeWhileWithPostcondition P) (.skip h)
+    | .done h => pure <| .deflate <| .done (.done h)
 
 private def TakeWhile.instFinitenessRelation [Monad m] [Iterator α m β]
     [Finite α m] {P} :
diff --git a/src/Std/Data/Iterators/Combinators/Monadic/Zip.lean b/src/Std/Data/Iterators/Combinators/Monadic/Zip.lean
index 9402ff379f..f57b6a2bb8 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/Zip.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic/Zip.lean
@@ -70,21 +70,21 @@ instance Zip.instIterator [Monad m] :
   step it :=
     match hm : it.internalState.memoizedLeft with
     | none => do
-      match ← it.internalState.left.step with
+      match (← it.internalState.left.step).inflate with
       | .yield it₁' out hp =>
-          pure <| .skip ⟨⟨it₁', (some ⟨out, _, _, hp⟩), it.internalState.right⟩⟩ (.yieldLeft hm hp)
+          pure <| .deflate <| .skip ⟨⟨it₁', (some ⟨out, _, _, hp⟩), it.internalState.right⟩⟩ (.yieldLeft hm hp)
       | .skip it₁' hp =>
-          pure <| .skip ⟨⟨it₁', none, it.internalState.right⟩⟩ (.skipLeft hm hp)
+          pure <| .deflate <| .skip ⟨⟨it₁', none, it.internalState.right⟩⟩ (.skipLeft hm hp)
       | .done hp =>
-          pure <| .done (.doneLeft hm hp)
+          pure <| .deflate <| .done (.doneLeft hm hp)
     | some out₁ => do
-      match ← it.internalState.right.step with
+      match (← it.internalState.right.step).inflate with
       | .yield it₂' out₂ hp =>
-          pure <| .yield ⟨⟨it.internalState.left, none, it₂'⟩⟩ (out₁, out₂) (.yieldRight hm hp)
+          pure <| .deflate <| .yield ⟨⟨it.internalState.left, none, it₂'⟩⟩ (out₁, out₂) (.yieldRight hm hp)
       | .skip it₂' hp =>
-          pure <| .skip ⟨⟨it.internalState.left, (some out₁), it₂'⟩⟩ (.skipRight hm hp)
+          pure <| .deflate <| .skip ⟨⟨it.internalState.left, (some out₁), it₂'⟩⟩ (.skipRight hm hp)
       | .done hp =>
-          pure <| .done (.doneRight hm hp)
+          pure <| .deflate <| .done (.doneRight hm hp)
 
 /--
 Given two iterators `left` and `right`, `left.zip right` is an iterator that yields pairs of
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean
index d7f5400f9a..bc020a78fe 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean
@@ -31,8 +31,7 @@ theorem Iter.step_drop {α β} [Iterator α Id β] {n : Nat}
     | .done h => .done (.done h)) := by
   simp only [drop_eq, step, toIterM_toIter, IterM.step_drop, Id.run_bind]
   generalize it.toIterM.step.run = step
-  obtain ⟨step, h⟩ := step
-  cases step <;> cases n <;>
+  cases step.inflate using PlausibleIterStep.casesOn <;> cases n <;>
     simp [PlausibleIterStep.yield, PlausibleIterStep.skip, PlausibleIterStep.done]
 
 theorem Iter.atIdxSlow?_drop {α β}
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean b/src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean
index d17493d212..fdcdbd5a0b 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean
@@ -48,19 +48,19 @@ theorem Iter.step_intermediateDropWhile {α β} [Iterator α Id β]
       | .done h =>
         .done (.done h)) := by
   simp [Intermediate.dropWhile_eq_dropWhile_toIterM, Iter.step, IterM.step_intermediateDropWhile]
-  cases it.toIterM.step.run using PlausibleIterStep.casesOn
+  cases it.toIterM.step.run.inflate using PlausibleIterStep.casesOn
   · simp only [IterM.Step.toPure_yield, PlausibleIterStep.yield, toIter_toIterM, toIterM_toIter]
     split
     · split
       · split
-        · rfl
+        · simp
         · exfalso; simp_all
       · split
         · exfalso; simp_all
-        · rfl
-    · rfl
-  · rfl
-  · rfl
+        · simp
+    · simp
+  · simp
+  · simp
 
 theorem Iter.step_dropWhile {α β} [Iterator α Id β] {P}
     {it : Iter (α := α) β} :
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/Drop.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/Drop.lean
index 577c275c32..fe333ab83e 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/Drop.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/Drop.lean
@@ -16,18 +16,17 @@ namespace Std.Iterators
 theorem IterM.step_drop {α m β} [Monad m] [Iterator α m β] {n : Nat}
     {it : IterM (α := α) m β} :
     (it.drop n).step = (do
-      match ← it.step with
+      match (← it.step).inflate with
       | .yield it' out h =>
         match n with
-        | 0 => pure <| .yield (it'.drop 0) out (.yield h rfl)
-        | k + 1 => pure <| .skip (it'.drop k) (.drop h rfl)
-      | .skip it' h => pure <| .skip (it'.drop n) (.skip h)
-      | .done h => pure <| .done (.done h)) := by
+        | 0 => pure <| .deflate <| .yield (it'.drop 0) out (.yield h rfl)
+        | k + 1 => pure <| .deflate <| .skip (it'.drop k) (.drop h rfl)
+      | .skip it' h => pure <| .deflate <| .skip (it'.drop n) (.skip h)
+      | .done h => pure <| .deflate <| .done (.done h)) := by
   simp only [drop, step, Iterator.step, internalState_toIterM, Nat.succ_eq_add_one]
   apply bind_congr
   intro step
-  obtain ⟨step, h⟩ := step
-  cases step
+  cases step.inflate using PlausibleIterStep.casesOn
   · cases n <;> rfl
   · rfl
   · rfl
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/DropWhile.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/DropWhile.lean
index a06e030a2d..cc10974536 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/DropWhile.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/DropWhile.lean
@@ -43,64 +43,64 @@ theorem IterM.dropWhile_eq_intermediateDropWhile {α m β} [Monad m]
 theorem IterM.step_intermediateDropWhileWithPostcondition {α m β} [Monad m] [Iterator α m β]
     {it : IterM (α := α) m β} {P} {dropping} :
     (IterM.Intermediate.dropWhileWithPostcondition P dropping it).step = (do
-    match ← it.step with
+    match (← it.step).inflate with
     | .yield it' out h =>
       if h' : dropping = true then
         match ← (P out).operation with
         | ⟨.up true, h''⟩ =>
-          return .skip (IterM.Intermediate.dropWhileWithPostcondition P true it') (.dropped h h' h'')
+          return .deflate <| .skip (IterM.Intermediate.dropWhileWithPostcondition P true it') (.dropped h h' h'')
         | ⟨.up false, h''⟩ =>
-          return .yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out (.start h h' h'')
+          return .deflate <| .yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out (.start h h' h'')
       else
-        return .yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out
+        return .deflate <| .yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out
             (.yield h (Bool.not_eq_true _ ▸ h'))
     | .skip it' h =>
-      return .skip (IterM.Intermediate.dropWhileWithPostcondition P dropping it') (.skip h)
+      return .deflate <| .skip (IterM.Intermediate.dropWhileWithPostcondition P dropping it') (.skip h)
     | .done h =>
-      return .done (.done h)) := by
+      return .deflate <| .done (.done h)) := by
   simp only [step, Iterator.step]
   apply bind_congr
   intro step
-  cases step using PlausibleIterStep.casesOn <;> rfl
+  cases step.inflate using PlausibleIterStep.casesOn <;> rfl
 
 theorem IterM.step_dropWhileWithPostcondition {α m β} [Monad m] [Iterator α m β]
     {it : IterM (α := α) m β} {P} :
     (it.dropWhileWithPostcondition P).step = (do
-    match ← it.step with
+    match (← it.step).inflate with
     | .yield it' out h =>
         match ← (P out).operation with
         | ⟨.up true, h''⟩ =>
-          return .skip (IterM.Intermediate.dropWhileWithPostcondition P true it') (.dropped h rfl h'')
+          return .deflate <| .skip (IterM.Intermediate.dropWhileWithPostcondition P true it') (.dropped h rfl h'')
         | ⟨.up false, h''⟩ =>
-          return .yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out (.start h rfl h'')
+          return .deflate <| .yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out (.start h rfl h'')
     | .skip it' h =>
-      return .skip (IterM.Intermediate.dropWhileWithPostcondition P true it') (.skip h)
+      return .deflate <| .skip (IterM.Intermediate.dropWhileWithPostcondition P true it') (.skip h)
     | .done h =>
-      return .done (.done h)) := by
+      return .deflate <| .done (.done h)) := by
   simp [dropWhileWithPostcondition_eq_intermediateDropWhileWithPostcondition, step_intermediateDropWhileWithPostcondition]
 
 theorem IterM.step_intermediateDropWhileM {α m β} [Monad m] [LawfulMonad m] [Iterator α m β]
     {it : IterM (α := α) m β} {P} {dropping} :
     (IterM.Intermediate.dropWhileM P dropping it).step = (do
-    match ← it.step with
+    match (← it.step).inflate with
     | .yield it' out h =>
       if h' : dropping = true then
         match ← P out with
         | .up true =>
-          return .skip (IterM.Intermediate.dropWhileM P true it') (.dropped h h' True.intro)
+          return .deflate <| .skip (IterM.Intermediate.dropWhileM P true it') (.dropped h h' True.intro)
         | .up false =>
-          return .yield (IterM.Intermediate.dropWhileM P false it') out (.start h h' True.intro)
+          return .deflate <| .yield (IterM.Intermediate.dropWhileM P false it') out (.start h h' True.intro)
       else
-        return .yield (IterM.Intermediate.dropWhileM P false it') out
+        return .deflate <| .yield (IterM.Intermediate.dropWhileM P false it') out
             (.yield h (Bool.not_eq_true _ ▸ h'))
     | .skip it' h =>
-      return .skip (IterM.Intermediate.dropWhileM P dropping it') (.skip h)
+      return .deflate <| .skip (IterM.Intermediate.dropWhileM P dropping it') (.skip h)
     | .done h =>
-      return .done (.done h)) := by
+      return .deflate <| .done (.done h)) := by
   simp only [Intermediate.dropWhileM_eq_dropWhileWithPostcondition, step_intermediateDropWhileWithPostcondition]
   apply bind_congr
   intro step
-  cases step using PlausibleIterStep.casesOn
+  cases step.inflate using PlausibleIterStep.casesOn
   · simp only [Function.comp_apply, PostconditionT.operation_lift, PlausibleIterStep.skip,
     PlausibleIterStep.yield, bind_map_left]
     split
@@ -114,41 +114,41 @@ theorem IterM.step_intermediateDropWhileM {α m β} [Monad m] [LawfulMonad m] [I
 theorem IterM.step_dropWhileM {α m β} [Monad m] [LawfulMonad m] [Iterator α m β]
     {it : IterM (α := α) m β} {P} :
     (it.dropWhileM P).step = (do
-    match ← it.step with
+    match (← it.step).inflate with
     | .yield it' out h =>
       match ← P out with
       | .up true =>
-        return .skip (IterM.Intermediate.dropWhileM P true it') (.dropped h rfl True.intro)
+        return .deflate <| .skip (IterM.Intermediate.dropWhileM P true it') (.dropped h rfl True.intro)
       | .up false =>
-        return .yield (IterM.Intermediate.dropWhileM P false it') out (.start h rfl True.intro)
+        return .deflate <| .yield (IterM.Intermediate.dropWhileM P false it') out (.start h rfl True.intro)
     | .skip it' h =>
-      return .skip (IterM.Intermediate.dropWhileM P true it') (.skip h)
+      return .deflate <| .skip (IterM.Intermediate.dropWhileM P true it') (.skip h)
     | .done h =>
-      return .done (.done h)) := by
+      return .deflate <| .done (.done h)) := by
   simp [dropWhileM_eq_intermediateDropWhileM, step_intermediateDropWhileM]
 
 theorem IterM.step_intermediateDropWhile {α m β} [Monad m] [LawfulMonad m] [Iterator α m β]
     {it : IterM (α := α) m β} {P} {dropping} :
     (IterM.Intermediate.dropWhile P dropping it).step = (do
-    match ← it.step with
+    match (← it.step).inflate with
     | .yield it' out h =>
       if h' : dropping = true then
         match P out with
         | true =>
-          return .skip (IterM.Intermediate.dropWhile P true it') (.dropped h h' True.intro)
+          return .deflate <| .skip (IterM.Intermediate.dropWhile P true it') (.dropped h h' True.intro)
         | false =>
-          return .yield (IterM.Intermediate.dropWhile P false it') out (.start h h' True.intro)
+          return .deflate <| .yield (IterM.Intermediate.dropWhile P false it') out (.start h h' True.intro)
       else
-        return .yield (IterM.Intermediate.dropWhile P false it') out
+        return .deflate <| .yield (IterM.Intermediate.dropWhile P false it') out
             (.yield h (Bool.not_eq_true _ ▸ h'))
     | .skip it' h =>
-      return .skip (IterM.Intermediate.dropWhile P dropping it') (.skip h)
+      return .deflate <| .skip (IterM.Intermediate.dropWhile P dropping it') (.skip h)
     | .done h =>
-      return .done (.done h)) := by
+      return .deflate <| .done (.done h)) := by
   simp only [Intermediate.dropWhile_eq_dropWhileM, step_intermediateDropWhileM]
   apply bind_congr
   intro step
-  cases step using PlausibleIterStep.casesOn
+  cases step.inflate using PlausibleIterStep.casesOn
   · simp only [Function.comp_apply, PlausibleIterStep.skip,
     PlausibleIterStep.yield]
     split
@@ -160,17 +160,17 @@ theorem IterM.step_intermediateDropWhile {α m β} [Monad m] [LawfulMonad m] [It
 theorem IterM.step_dropWhile {α m β} [Monad m] [LawfulMonad m] [Iterator α m β]
     {it : IterM (α := α) m β} {P} :
     (it.dropWhile P).step = (do
-    match ← it.step with
+    match (← it.step).inflate with
     | .yield it' out h =>
         match P out with
         | true =>
-          return .skip (IterM.Intermediate.dropWhile P true it') (.dropped h rfl True.intro)
+          return .deflate <| .skip (IterM.Intermediate.dropWhile P true it') (.dropped h rfl True.intro)
         | false =>
-          return .yield (IterM.Intermediate.dropWhile P false it') out (.start h rfl True.intro)
+          return .deflate <| .yield (IterM.Intermediate.dropWhile P false it') out (.start h rfl True.intro)
     | .skip it' h =>
-      return .skip (IterM.Intermediate.dropWhile P true it') (.skip h)
+      return .deflate <| .skip (IterM.Intermediate.dropWhile P true it') (.skip h)
     | .done h =>
-      return .done (.done h)) := by
+      return .deflate <| .done (.done h)) := by
   simp [dropWhile_eq_intermediateDropWhile, step_intermediateDropWhile]
 
 end Std.Iterators
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
index 5ac60552b3..0bf0b4c923 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
@@ -68,7 +68,7 @@ theorem stepAsHetT_filterMapWithPostcondition [Monad m] [LawfulMonad m] [Monad n
       PlausibleIterStep.yield, PlausibleIterStep.done, bind_assoc]
     apply bind_congr
     intro step
-    cases step using PlausibleIterStep.casesOn
+    cases step.inflate using PlausibleIterStep.casesOn
     · simp only [bind_assoc, bind, HetT.prun_bind, HetT.prun_ofPostconditionT]
       apply bind_congr
       rintro ⟨out, _⟩
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/Take.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/Take.lean
index faf32062a7..a5ba9c0215 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/Take.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/Take.lean
@@ -16,20 +16,19 @@ namespace Std.Iterators
 theorem IterM.step_take {α m β} [Monad m] [Iterator α m β] {n : Nat}
     {it : IterM (α := α) m β} :
     (it.take n).step = (match n with
-      | 0 => pure <| .done (.depleted rfl)
+      | 0 => pure <| .deflate <| .done (.depleted rfl)
       | k + 1 => do
-        match ← it.step with
-        | .yield it' out h => pure <| .yield (it'.take k) out (.yield h rfl)
-        | .skip it' h => pure <| .skip (it'.take (k + 1)) (.skip h rfl)
-        | .done h => pure <| .done (.done h)) := by
+        match (← it.step).inflate with
+        | .yield it' out h => pure <| .deflate <| .yield (it'.take k) out (.yield h rfl)
+        | .skip it' h => pure <| .deflate <| .skip (it'.take (k + 1)) (.skip h rfl)
+        | .done h => pure <| .deflate <| .done (.done h)) := by
   simp only [take, step, Iterator.step, internalState_toIterM, Nat.succ_eq_add_one]
   cases n
   case zero => rfl
   case succ k =>
     apply bind_congr
     intro step
-    obtain ⟨step, h⟩ := step
-    cases step <;> rfl
+    cases step.inflate using PlausibleIterStep.casesOn <;> rfl
 
 theorem IterM.toList_take_zero {α m β} [Monad m] [LawfulMonad m] [Iterator α m β]
     [Finite (Take α m β) m]
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/TakeWhile.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/TakeWhile.lean
index 702e27531a..acf03656a6 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/TakeWhile.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/TakeWhile.lean
@@ -16,30 +16,30 @@ namespace Std.Iterators
 theorem IterM.step_takeWhileWithPostcondition {α m β} [Monad m] [Iterator α m β]
     {it : IterM (α := α) m β} {P} :
     (it.takeWhileWithPostcondition P).step = (do
-      match ← it.step with
+      match (← it.step).inflate with
       | .yield it' out h => match ← (P out).operation with
-        | ⟨.up true, h'⟩ => pure <| .yield (it'.takeWhileWithPostcondition P) out (.yield h h')
-        | ⟨.up false, h'⟩ => pure <| .done (.rejected h h')
-      | .skip it' h => pure <| .skip (it'.takeWhileWithPostcondition P) (.skip h)
-      | .done h => pure <| .done (.done h)) := by
+        | ⟨.up true, h'⟩ => pure <| .deflate <| .yield (it'.takeWhileWithPostcondition P) out (.yield h h')
+        | ⟨.up false, h'⟩ => pure <| .deflate <| .done (.rejected h h')
+      | .skip it' h => pure <| .deflate <| .skip (it'.takeWhileWithPostcondition P) (.skip h)
+      | .done h => pure <| .deflate <| .done (.done h)) := by
   simp only [takeWhileWithPostcondition, step, Iterator.step, internalState_toIterM]
   apply bind_congr
   intro step
-  cases step using PlausibleIterStep.casesOn <;> rfl
+  cases step.inflate using PlausibleIterStep.casesOn <;> rfl
 
 theorem IterM.step_takeWhileM {α m β} [Monad m] [LawfulMonad m] [Iterator α m β]
     {it : IterM (α := α) m β} {P} :
     (it.takeWhileM P).step = (do
-      match ← it.step with
+      match (← it.step).inflate with
       | .yield it' out h => match ← P out with
-        | .up true => pure <| .yield (it'.takeWhileM P) out (.yield h True.intro)
-        | .up false => pure <| .done (.rejected h True.intro)
-      | .skip it' h => pure <| .skip (it'.takeWhileM P) (.skip h)
-      | .done h => pure <| .done (.done h)) := by
+        | .up true => pure <| .deflate <| .yield (it'.takeWhileM P) out (.yield h True.intro)
+        | .up false => pure <| .deflate <| .done (.rejected h True.intro)
+      | .skip it' h => pure <| .deflate <| .skip (it'.takeWhileM P) (.skip h)
+      | .done h => pure <| .deflate <| .done (.done h)) := by
   simp only [takeWhileM, step_takeWhileWithPostcondition]
   apply bind_congr
   intro step
-  cases step using PlausibleIterStep.casesOn
+  cases step.inflate using PlausibleIterStep.casesOn
   · simp only [Function.comp_apply, PostconditionT.operation_lift, PlausibleIterStep.yield,
     PlausibleIterStep.done, bind_map_left]
     apply bind_congr
@@ -51,16 +51,16 @@ theorem IterM.step_takeWhileM {α m β} [Monad m] [LawfulMonad m] [Iterator α m
 theorem IterM.step_takeWhile {α m β} [Monad m] [LawfulMonad m] [Iterator α m β]
     {it : IterM (α := α) m β} {P} :
     (it.takeWhile P).step = (do
-      match ← it.step with
+      match (← it.step).inflate with
       | .yield it' out h => match P out with
-        | true => pure <| .yield (it'.takeWhile P) out (.yield h True.intro)
-        | false => pure <| .done (.rejected h True.intro)
-      | .skip it' h => pure <| .skip (it'.takeWhile P) (.skip h)
-      | .done h => pure <| .done (.done h)) := by
+        | true => pure <| .deflate <| .yield (it'.takeWhile P) out (.yield h True.intro)
+        | false => pure <| .deflate <| .done (.rejected h True.intro)
+      | .skip it' h => pure <| .deflate <| .skip (it'.takeWhile P) (.skip h)
+      | .done h => pure <| .deflate <| .done (.done h)) := by
   simp only [takeWhile, step_takeWhileM]
   apply bind_congr
   intro step
-  cases step using PlausibleIterStep.casesOn
+  cases step.inflate using PlausibleIterStep.casesOn
   · simp only [Function.comp_apply, PlausibleIterStep.yield, PlausibleIterStep.done, pure_bind]
     cases P _ <;> rfl
   · simp
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/Zip.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/Zip.lean
index f27a47c2fc..d947246563 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/Zip.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/Zip.lean
@@ -42,51 +42,49 @@ theorem IterM.step_intermediateZip [Monad m] [Iterator α₁ m β₁] [Iterator
     (Intermediate.zip it₁ memo it₂).step = (do
       match memo with
       | none =>
-        match ← it₁.step with
+        match (← it₁.step).inflate with
         | .yield it₁' out hp =>
-          pure <| .skip (Intermediate.zip it₁' (some ⟨out, _, _, hp⟩) it₂)
+          pure <| .deflate <| .skip (Intermediate.zip it₁' (some ⟨out, _, _, hp⟩) it₂)
             (.yieldLeft rfl hp)
         | .skip it₁' hp =>
-          pure <| .skip (Intermediate.zip it₁' none it₂)
+          pure <| .deflate <| .skip (Intermediate.zip it₁' none it₂)
             (.skipLeft rfl hp)
         | .done hp =>
-          pure <| .done (.doneLeft rfl hp)
+          pure <| .deflate <| .done (.doneLeft rfl hp)
       | some out₁ =>
-        match ← it₂.step with
+        match (← it₂.step).inflate with
         | .yield it₂' out₂ hp =>
-          pure <| .yield (Intermediate.zip it₁ none it₂') (out₁, out₂)
+          pure <| .deflate <| .yield (Intermediate.zip it₁ none it₂') (out₁, out₂)
             (.yieldRight rfl hp)
         | .skip it₂' hp =>
-          pure <| .skip (Intermediate.zip it₁ (some out₁) it₂')
+          pure <| .deflate <| .skip (Intermediate.zip it₁ (some out₁) it₂')
             (.skipRight rfl hp)
         | .done hp =>
-          pure <| .done (.doneRight rfl hp)) := by
+          pure <| .deflate <| .done (.doneRight rfl hp)) := by
   simp only [Intermediate.zip, step, Iterator.step]
   split
   · apply bind_congr
     intro step
-    obtain ⟨step, h⟩ := step
-    cases step <;> rfl
+    cases step.inflate using PlausibleIterStep.casesOn <;> rfl
   · rename_i heq
     cases heq
     apply bind_congr
     intro step
-    obtain ⟨step, h⟩ := step
-    cases step <;> rfl
+    cases step.inflate using PlausibleIterStep.casesOn <;> rfl
 
 theorem IterM.step_zip [Monad m] [Iterator α₁ m β₁] [Iterator α₂ m β₂]
     {it₁ : IterM (α := α₁) m β₁}
     {it₂ : IterM (α := α₂) m β₂} :
     (it₁.zip it₂).step = (do
-      match ← it₁.step with
+      match (← it₁.step).inflate with
       | .yield it₁' out hp =>
-        pure <| .skip (Intermediate.zip it₁' (some ⟨out, _, _, hp⟩) it₂)
+        pure <| .deflate <| .skip (Intermediate.zip it₁' (some ⟨out, _, _, hp⟩) it₂)
           (.yieldLeft rfl hp)
       | .skip it₁' hp =>
-        pure <| .skip (Intermediate.zip it₁' none it₂)
+        pure <| .deflate <| .skip (Intermediate.zip it₁' none it₂)
           (.skipLeft rfl hp)
       | .done hp =>
-        pure <| .done (.doneLeft rfl hp)) := by
+        pure <| .deflate <| .done (.doneLeft rfl hp)) := by
   simp [zip_eq_intermediateZip, step_intermediateZip]
 
 end Std.Iterators
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Take.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Take.lean
index 2c1f1e052c..eb856bbdd0 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/Take.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/Take.lean
@@ -35,7 +35,7 @@ theorem Iter.step_take {α β} [Iterator α Id β] {n : Nat}
   case succ k =>
     simp only [Id.run_bind]
     generalize it.toIterM.step.run = step
-    cases step using PlausibleIterStep.casesOn <;>
+    cases step.inflate using PlausibleIterStep.casesOn <;>
       simp [PlausibleIterStep.yield, PlausibleIterStep.skip, PlausibleIterStep.done]
 
 theorem Iter.atIdxSlow?_take {α β}
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean b/src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean
index 62172f1a00..11b3457103 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean
@@ -29,9 +29,9 @@ theorem Iter.step_takeWhile {α β} [Iterator α Id β] {P}
       | .done h => .done (.done h)) := by
   simp [Iter.takeWhile_eq, Iter.step, toIterM_toIter, IterM.step_takeWhile]
   generalize it.toIterM.step.run = step
-  cases step using PlausibleIterStep.casesOn
+  cases step.inflate using PlausibleIterStep.casesOn
   · simp only [IterM.Step.toPure_yield, PlausibleIterStep.yield, toIter_toIterM, toIterM_toIter]
-    cases P _ <;> rfl
+    cases P _ <;> simp
   · simp
   · simp
 
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean
index 80eabc5990..cb4c6998fa 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean
@@ -99,13 +99,11 @@ theorem Iter.step_intermediateZip
   case none =>
     simp only [Option.map_eq_map, Option.map_none, PlausibleIterStep.skip, PlausibleIterStep.done,
       Id.run_bind, Option.map_some]
-    obtain ⟨step, h⟩ := it₁.toIterM.step.run
-    cases step <;> simp
+    cases it₁.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp
   case some out₁ =>
     simp only [Option.map_eq_map, Option.map_some, PlausibleIterStep.yield, PlausibleIterStep.skip,
       PlausibleIterStep.done, Id.run_bind, Option.map_none]
-    obtain ⟨step, h⟩ := it₂.toIterM.step.run
-    cases step <;> simp
+    cases it₂.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp
 
 theorem Iter.toList_intermediateZip_of_finite [Iterator α₁ Id β₁] [Iterator α₂ Id β₂]
     {it₁ : Iter (α := α₁) β₁} {memo} {it₂ : Iter (α := α₂) β₂}
diff --git a/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean b/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean
index 79c94a2d8a..dc6d108dca 100644
--- a/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean
+++ b/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean
@@ -25,14 +25,15 @@ theorem IterM.Equiv.toListRev_eq [Monad m] [LawfulMonad m]
   apply h.lift_step_bind_congr
   intro s₁ s₂ h
   simp only [IterStep.bundledQuotient] at h
-  cases s₁ using PlausibleIterStep.casesOn <;> cases s₂ using PlausibleIterStep.casesOn
+  cases h₁ : s₁.inflate using PlausibleIterStep.casesOn <;>
+    cases h₂ : s₂.inflate using PlausibleIterStep.casesOn
   all_goals try exfalso; simp_all; done
-  · simp only [IterStep.mapIterator_yield, Function.comp_apply, IterStep.yield.injEq] at h
+  · simp only [h₁, h₂, IterStep.mapIterator_yield, Function.comp_apply, IterStep.yield.injEq] at h
     simp_all only [bind_pure_comp, List.append_cancel_right_eq, implies_true,
       map_inj_right_of_nonempty]
     apply ihy ‹_›
     exact BundledIterM.Equiv.exact _ _ h.1
-  · simp only [IterStep.mapIterator_skip, Function.comp_apply, IterStep.skip.injEq] at ⊢ h
+  · simp only [h₁, h₂, IterStep.mapIterator_skip, Function.comp_apply, IterStep.skip.injEq] at ⊢ h
     apply ihs ‹_›
     exact BundledIterM.Equiv.exact _ _ h
   · simp
diff --git a/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean b/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
index 78e12e2b40..258647af8f 100644
--- a/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
+++ b/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
@@ -34,9 +34,10 @@ theorem IterM.Equiv.forIn_eq {α₁ α₂ β γ : Type w} {m : Type w → Type w
   apply h.lift_step_bind_congr
   intro sa sb hs
   simp only [IterStep.bundledQuotient, IterStep.mapIterator_comp, Function.comp_apply] at hs
-  cases sa using PlausibleIterStep.casesOn <;> cases sb using PlausibleIterStep.casesOn
+  cases ha : sa.inflate using PlausibleIterStep.casesOn <;>
+    cases hb : sb.inflate using PlausibleIterStep.casesOn
   all_goals try exfalso; simp_all; done
-  · simp only [IterStep.mapIterator_yield, IterStep.yield.injEq,
+  · simp only [ha, hb, IterStep.mapIterator_yield, IterStep.yield.injEq,
       BundledIterM.Equiv.quotMk_eq_iff] at hs
     rcases hs with ⟨hs, rfl⟩
     apply bind_congr
@@ -44,8 +45,8 @@ theorem IterM.Equiv.forIn_eq {α₁ α₂ β γ : Type w} {m : Type w → Type w
     cases forInStep
     · rfl
     · exact ihy ‹_› hs
-  · simp only [IterStep.mapIterator_skip, IterStep.skip.injEq,
-    BundledIterM.Equiv.quotMk_eq_iff] at hs
+  · simp only [ha, hb, IterStep.mapIterator_skip, IterStep.skip.injEq,
+      BundledIterM.Equiv.quotMk_eq_iff] at hs
     exact ihs ‹_› hs
   · rfl
 
diff --git a/src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean b/src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean
index 22c8ceacd0..9148c6091e 100644
--- a/src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean
+++ b/src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean
@@ -64,7 +64,7 @@ namely `IterM.Equiv` and `Iter.Equiv`.
 -/
 noncomputable def IterM.stepAsHetT [Iterator α m β] [Monad m] (it : IterM (α := α) m β) :
     HetT m (IterStep (IterM (α := α) m β) β) :=
-    ⟨it.IsPlausibleStep, inferInstance, (fun step => .deflate step) <$> it.step⟩
+    ⟨it.IsPlausibleStep, inferInstance, (fun step => .deflate step.inflate) <$> it.step⟩
 
 /-
 Makes a step with a bundled iterator in the `HetT` monad.
@@ -99,7 +99,7 @@ theorem Equivalence.prun_liftInner_step [Iterator α m β] [Monad m] [Monad n]
     [MonadLiftT m n] [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n]
     {it : IterM (α := α) m β} {f : (step : _) → _ → n γ} :
     ((IterM.stepAsHetT it).liftInner n).prun f =
-      (it.step : n _) >>= (fun step => f step.1 step.2) := by
+      (it.step : n _) >>= (fun step => f step.inflate.1 step.inflate.2) := by
   simp [IterM.stepAsHetT, HetT.liftInner, HetT.prun, PlausibleIterStep]
 
 @[simp]
@@ -110,7 +110,7 @@ theorem Equivalence.property_step [Iterator α m β] [Monad m] [LawfulMonad m]
 @[simp]
 theorem Equivalence.prun_step [Iterator α m β] [Monad m] [LawfulMonad m]
     {it : IterM (α := α) m β} {f : (step : _) → _ → m γ} :
-    (IterM.stepAsHetT it).prun f = it.step >>= (fun step => f step.1 step.2) := by
+    (IterM.stepAsHetT it).prun f = it.step >>= (fun step => f step.inflate.1 step.inflate.2) := by
   simp [IterM.stepAsHetT, HetT.prun, PlausibleIterStep]
 
 /--
diff --git a/src/Std/Data/Iterators/Lemmas/Equivalence/StepCongr.lean b/src/Std/Data/Iterators/Lemmas/Equivalence/StepCongr.lean
index e8713be1d7..7d9cd027bb 100644
--- a/src/Std/Data/Iterators/Lemmas/Equivalence/StepCongr.lean
+++ b/src/Std/Data/Iterators/Lemmas/Equivalence/StepCongr.lean
@@ -129,8 +129,9 @@ cancellation property does not hold for all monads.
 theorem IterM.Equiv.step_eq {α₁ α₂ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
     [Iterator α₁ m β] [Iterator α₂ m β] {ita : IterM (α := α₁) m β} {itb : IterM (α := α₂) m β}
     (h : IterM.Equiv ita itb) :
-    (Quot.mk _ : _ → ita.QuotStep) <$> ita.step =
-      IterM.QuotStep.transportAlongEquiv h.symm <$> (Quot.mk _ : _ → itb.QuotStep) <$> itb.step := by
+    (fun s => Shrink.deflate (Quot.mk _ s.inflate : ita.QuotStep)) <$> ita.step =
+      (fun s => Shrink.deflate (QuotStep.transportAlongEquiv h.symm s.inflate)) <$>
+        (fun s => Shrink.deflate (Quot.mk _ s.inflate : itb.QuotStep)) <$> itb.step := by
   have he := h
   simp only [IterM.Equiv, BundledIterM.ofIterM, BundledIterM.Equiv, BundledIterM.step,
     ] at h
@@ -148,11 +149,12 @@ theorem IterM.Equiv.step_eq {α₁ α₂ : Type w} {m : Type w → Type w'} [Mon
   replace h' := congrArg (·.map IterM.QuotStep.restrict) h'
   simp only [HetT.map_pmap, IterStep.restrict_bundle (α₂ := α₂),
     IterStep.restrict_bundle (α₂ := α₁)] at h'
-  replace h' := congrArg (HetT.prun · (fun x _ => pure x)) h'
+  replace h' := congrArg (HetT.prun · (fun x _ => pure (Shrink.deflate x))) h'
   simp only [Equivalence.property_step, HetT.prun_pmap, Equivalence.prun_step, bind_pure_comp] at h'
-  simp only [QuotStep.transportAlongEquiv, Functor.map_map, ← h']
+  simp only [QuotStep.transportAlongEquiv, Functor.map_map, Shrink.inflate_deflate, ← h']
   congr
   ext step
+  rw [Shrink.deflate_inj]
   apply Quot.sound
   change _ = IterStep.bundledQuotient (Subtype.val (Exists.choose ?hex))
   let hex := ?hex
@@ -163,31 +165,37 @@ theorem IterM.Equiv.lift_step_bind_congr {α₁ α₂ : Type w} [Monad m] [Lawfu
     [Iterator α₁ m β] [Iterator α₂ m β]
     {ita : IterM (α := α₁) m β} {itb : IterM (α := α₂) m β} (h : IterM.Equiv ita itb)
     {f : _ → n γ} {g : _ → n γ}
-    (hfg : ∀ s₁ s₂, s₁.1.bundledQuotient = s₂.1.bundledQuotient → f s₁ = g s₂) :
-    ((ita.step : n _) >>= f) = ((itb.step : n _) >>= g) := by
-  let flift : ita.QuotStep → n γ := by
+    (hfg : ∀ s₁ s₂, s₁.inflate.1.bundledQuotient = s₂.inflate.1.bundledQuotient → f s₁ = g s₂) :
+    ((ita.step : n _) >>= f) = ((itb.step : n _) >>= g) := by -- .deflate this
+  let flift : Shrink ita.QuotStep → n γ := by
+    refine ?_ ∘ Shrink.inflate
     refine Quot.lift ?_ ?_
-    · exact f
+    · exact f ∘ Shrink.deflate
     · intro s s' h''
       have hs := (IterM.Equiv.exists_step_of_step h s)
-      rw [hfg s hs.choose hs.choose_spec, hfg s' hs.choose (h'' ▸ hs.choose_spec)]
-  have hf : f = flift ∘ Quot.mk _ := rfl
-  let glift : itb.QuotStep → n γ := by
+      simp only [Function.comp_apply]
+      rw [hfg (.deflate s) (.deflate hs.choose) (by simpa using hs.choose_spec),
+        hfg (.deflate s') (.deflate hs.choose) (by simpa [h''] using hs.choose_spec)]
+  have hf : f = flift ∘ Shrink.deflate ∘ Quot.mk _ ∘ Shrink.inflate := by simp [Function.comp_def, flift]
+  let glift : Shrink itb.QuotStep → n γ := by
+    refine ?_ ∘ Shrink.inflate
     refine Quot.lift ?_ ?_
-    · exact g
+    · exact g ∘ Shrink.deflate
     · intro s s' h''
       have hs := (IterM.Equiv.exists_step_of_step h.symm s)
-      rw [← hfg hs.choose s hs.choose_spec.symm, ← hfg hs.choose s' (h'' ▸ hs.choose_spec.symm)]
-  have hg : g = glift ∘ Quot.mk _ := rfl
-  rw [hf, hg, bind_comp_eq_map_bind, bind_comp_eq_map_bind]
+      simp only [Function.comp_apply]
+      rw [← hfg (.deflate hs.choose) (.deflate s) (by simpa using hs.choose_spec.symm),
+        ← hfg (.deflate hs.choose) (.deflate s') (by simpa [h''] using hs.choose_spec.symm)]
+  have hg : g = glift ∘ Shrink.deflate ∘ Quot.mk _ ∘ Shrink.inflate := by simp [Function.comp_def, glift]
+  rw [hf, bind_comp_eq_map_bind (g := flift), hg, bind_comp_eq_map_bind (g := glift)]
   have := congrArg (fun x => liftM (n := n) x) (step_eq h)
-  simp only [liftM_map, Functor.map_map] at this
-  simp only [this, map_eq_pure_bind, bind_assoc]
-  apply bind_congr
-  intro step
+  simp only [liftM_map] at this
+  simp only [Function.comp_def, this, Functor.map_map, Shrink.inflate_deflate]
+  simp only [map_eq_pure_bind, bind_assoc]
+  apply bind_congr; intro step
   simp only [QuotStep.transportAlongEquiv, pure_bind, flift, glift]
-  have hex := exists_step_of_step h.symm step
-  exact hfg hex.choose step hex.choose_spec.symm
+  have hex := exists_step_of_step h.symm step.inflate
+  simp [hfg (.deflate hex.choose) step (by simpa using hex.choose_spec.symm)]
 
 theorem IterM.Equiv.liftInner_stepAsHetT_pbind_congr [Monad m] [LawfulMonad m]
     [Monad n] [LawfulMonad n]
@@ -211,7 +219,7 @@ theorem IterM.Equiv.liftInner_stepAsHetT_pbind_congr [Monad m] [LawfulMonad m]
   · intro γ l
     apply lift_step_bind_congr h
     intro s₁ s₂ h
-    simp only [hfg s₁.1 s₁.2 s₂.1 s₂.2 h]
+    simp only [hfg s₁.inflate.1 s₁.inflate.2 s₂.inflate.1 s₂.inflate.2 h]
 
 theorem IterM.Equiv.liftInner_stepAsHetT_bind_congr [Monad m] [LawfulMonad m]
     [Monad n] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α₁ m β]
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Array.lean b/src/Std/Data/Iterators/Lemmas/Producers/Array.lean
index 0650881926..4e9b3e5ddc 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers/Array.lean
+++ b/src/Std/Data/Iterators/Lemmas/Producers/Array.lean
@@ -45,7 +45,7 @@ theorem _root_.Array.step_iterFromIdx {array : Array β} {pos : Nat} :
       else
         .done (Nat.not_lt.mp h) := by
   simp only [Array.iterFromIdx_eq_toIter_iterFromIdxM, Iter.step, Iter.toIterM_toIter,
-    Array.step_iterFromIdxM, Id.run_pure]
+    Array.step_iterFromIdxM, Id.run_pure, Shrink.inflate_deflate]
   split <;> rfl
 
 theorem _root_.Array.step_iter {array : Array β} :
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/List.lean b/src/Std/Data/Iterators/Lemmas/Producers/List.lean
index 133535e82a..b09f071b9d 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers/List.lean
+++ b/src/Std/Data/Iterators/Lemmas/Producers/List.lean
@@ -27,12 +27,13 @@ variable {β : Type w}
 @[simp]
 theorem _root_.List.step_iter_nil :
     (([] : List β).iter).step = ⟨.done, rfl⟩ := by
-  simp only [Iter.step, IterM.step, Iterator.step]; rfl
+  simp [Iter.step, IterM.step, Iterator.step, List.iter, List.iterM, toIterM]
 
 @[simp]
 theorem _root_.List.step_iter_cons {x : β} {xs : List β} :
     ((x :: xs).iter).step = ⟨.yield xs.iter x, rfl⟩ := by
-  simp only [List.iter, List.iterM]; rfl
+  simp [List.iter, List.iterM, toIterM, IterM.toIter, Iter.step, Iter.toIterM, IterM.step,
+    Iterator.step]
 
 @[simp]
 theorem _root_.List.toArray_iter {l : List β} :
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean
index 41a5f25c3c..629f73ab4e 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean
+++ b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean
@@ -31,7 +31,7 @@ theorem _root_.Array.iterM_eq_iterFromIdxM {array : Array β} :
   rfl
 
 theorem _root_.Array.step_iterFromIdxM {array : Array β} {pos : Nat} :
-    (array.iterFromIdxM m pos).step = (pure <| if h : pos < array.size then
+    (array.iterFromIdxM m pos).step = (pure <| .deflate <| if h : pos < array.size then
         .yield
           (array.iterFromIdxM m (pos + 1))
           array[pos]
@@ -41,7 +41,7 @@ theorem _root_.Array.step_iterFromIdxM {array : Array β} {pos : Nat} :
   rfl
 
 theorem _root_.Array.step_iterM {array : Array β} :
-    (array.iterM m).step = (pure <| if h : 0 < array.size then
+    (array.iterM m).step = (pure <| .deflate <| if h : 0 < array.size then
         .yield
           (array.iterFromIdxM m 1)
           array[0]
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Empty.lean b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Empty.lean
index e3cb6a2cad..24293887f5 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Empty.lean
+++ b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Empty.lean
@@ -16,7 +16,7 @@ namespace Std.Iterators
 
 @[simp]
 theorem IterM.step_empty {m β} [Monad m] :
-    (IterM.empty m β).step = pure ⟨.done, rfl⟩ :=
+    (IterM.empty m β).step = pure (.deflate ⟨.done, rfl⟩) :=
   rfl
 
 @[simp]
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean
index 3f266717df..55db4a6b63 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean
+++ b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean
@@ -28,18 +28,18 @@ variable {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] {β : Type
 
 @[simp]
 theorem _root_.List.step_iterM_nil :
-    (([] : List β).iterM m).step = pure ⟨.done, rfl⟩ := by
+    (([] : List β).iterM m).step = pure (.deflate ⟨.done, rfl⟩) := by
   simp only [IterM.step, Iterator.step]; rfl
 
 @[simp]
 theorem _root_.List.step_iterM_cons {x : β} {xs : List β} :
-    ((x :: xs).iterM m).step = pure ⟨.yield (xs.iterM m) x, rfl⟩ := by
+    ((x :: xs).iterM m).step = pure (.deflate ⟨.yield (xs.iterM m) x, rfl⟩) := by
   simp only [List.iterM, IterM.step, Iterator.step]; rfl
 
 theorem _root_.List.step_iterM {l : List β} :
     (l.iterM m).step = match l with
-      | [] => pure ⟨.done, rfl⟩
-      | x :: xs => pure ⟨.yield (xs.iterM m) x, rfl⟩ := by
+      | [] => pure (.deflate ⟨.done, rfl⟩)
+      | x :: xs => pure (.deflate ⟨.yield (xs.iterM m) x, rfl⟩) := by
   cases l <;> simp [List.step_iterM_cons, List.step_iterM_nil]
 
 theorem ListIterator.toArrayMapped_iterM [Monad n] [LawfulMonad n]
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Repeat.lean b/src/Std/Data/Iterators/Lemmas/Producers/Repeat.lean
index dcc7425e65..663bff499b 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers/Repeat.lean
+++ b/src/Std/Data/Iterators/Lemmas/Producers/Repeat.lean
@@ -21,7 +21,7 @@ variable {α : Type w} {f : α → α} {init : α}
 
 theorem Iter.step_repeat :
     (Iter.repeat f init).step = .yield (Iter.repeat f (f init)) init ⟨rfl, rfl⟩ := by
-  rfl
+  simp [«repeat», Iter.step, Iter.toIterM, IterM.step, Iterator.step, IterM.toIter]
 
 theorem Iter.atIdxSlow?_zero_repeat :
     (Iter.repeat f init).atIdxSlow? 0 = some init := by
diff --git a/src/Std/Data/Iterators/Producers/Monadic/Array.lean b/src/Std/Data/Iterators/Producers/Monadic/Array.lean
index d903e2391d..85860d9f35 100644
--- a/src/Std/Data/Iterators/Producers/Monadic/Array.lean
+++ b/src/Std/Data/Iterators/Producers/Monadic/Array.lean
@@ -85,7 +85,7 @@ instance {α : Type w} [Pure m] : Iterator (ArrayIterator α) m α where
       it.internalState.array[it.internalState.pos] = out
     | .skip _ => False
     | .done => it.internalState.pos ≥ it.internalState.array.size
-  step it := pure <| if h : it.internalState.pos < it.internalState.array.size then
+  step it := pure <| .deflate <| if h : it.internalState.pos < it.internalState.array.size then
         .yield
           ⟨⟨it.internalState.array, it.internalState.pos + 1⟩⟩
           it.internalState.array[it.internalState.pos]
diff --git a/src/Std/Data/Iterators/Producers/Monadic/Empty.lean b/src/Std/Data/Iterators/Producers/Monadic/Empty.lean
index a0af0a78aa..5c45d1c6ad 100644
--- a/src/Std/Data/Iterators/Producers/Monadic/Empty.lean
+++ b/src/Std/Data/Iterators/Producers/Monadic/Empty.lean
@@ -44,7 +44,7 @@ def Empty.PlausibleStep (_ : IterM (α := Empty m β) m β)
 
 instance Empty.instIterator [Monad m] : Iterator (Empty m β) m β where
   IsPlausibleStep := Empty.PlausibleStep
-  step _ := return .done rfl
+  step _ := return .deflate (.done rfl)
 
 private def Empty.instFinitenessRelation [Monad m] :
     FinitenessRelation (Empty m β) m where
diff --git a/src/Std/Data/Iterators/Producers/Monadic/List.lean b/src/Std/Data/Iterators/Producers/Monadic/List.lean
index e3f3dff3f7..c2d1733249 100644
--- a/src/Std/Data/Iterators/Producers/Monadic/List.lean
+++ b/src/Std/Data/Iterators/Producers/Monadic/List.lean
@@ -47,8 +47,8 @@ instance {α : Type w} [Pure m] : Iterator (ListIterator α) m α where
     | .skip _ => False
     | .done => it.internalState.list = []
   step it := pure (match it with
-        | ⟨⟨[]⟩⟩ => ⟨.done, rfl⟩
-        | ⟨⟨x :: xs⟩⟩ => ⟨.yield (toIterM ⟨xs⟩ m α) x, rfl⟩)
+        | ⟨⟨[]⟩⟩ => .deflate ⟨.done, rfl⟩
+        | ⟨⟨x :: xs⟩⟩ => .deflate ⟨.yield (toIterM ⟨xs⟩ m α) x, rfl⟩)
 
 private def ListIterator.finitenessRelation [Pure m] :
     FinitenessRelation (ListIterator α) m where
diff --git a/src/Std/Data/Iterators/Producers/Repeat.lean b/src/Std/Data/Iterators/Producers/Repeat.lean
index b874ff401a..913a0ee7d1 100644
--- a/src/Std/Data/Iterators/Producers/Repeat.lean
+++ b/src/Std/Data/Iterators/Producers/Repeat.lean
@@ -38,7 +38,7 @@ instance : Iterator (RepeatIterator α f) Id α where
     | .yield it' out => out = it.internalState.next ∧ it' = ⟨⟨f it.internalState.next⟩⟩
     | .skip _ => False
     | .done => False
-  step it := pure <| .yield ⟨⟨f it.internalState.next⟩⟩ it.internalState.next (by simp)
+  step it := pure <| .deflate <| .yield ⟨⟨f it.internalState.next⟩⟩ it.internalState.next (by simp)
 
 /--
 Creates an infinite iterator from an initial value `init` and a function `f : α → α`.
diff --git a/tests/bench/hashmap.lean b/tests/bench/hashmap.lean
index 21065f5546..60a7e8cb75 100644
--- a/tests/bench/hashmap.lean
+++ b/tests/bench/hashmap.lean
@@ -29,7 +29,7 @@ instance [Pure m] : Std.Iterators.Iterator RandomIterator m UInt64 where
     | .skip _ => False
     | .done => False
   step := fun ⟨it⟩ =>
-    pure ⟨.yield (iterRandM <| (it.state + (1 : UInt64)) * (3_787_392_781 : UInt64)) it.state, by trivial⟩
+    pure (.deflate ⟨.yield (iterRandM <| (it.state + (1 : UInt64)) * (3_787_392_781 : UInt64)) it.state, by trivial⟩)
 
 instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RandomIterator) m n :=
   .defaultImplementation
diff --git a/tests/bench/phashmap.lean b/tests/bench/phashmap.lean
index e08d29b940..62c7c5696a 100644
--- a/tests/bench/phashmap.lean
+++ b/tests/bench/phashmap.lean
@@ -29,7 +29,7 @@ instance [Pure m] : Std.Iterators.Iterator RandomIterator m UInt64 where
     | .skip _ => False
     | .done => False
   step := fun ⟨it⟩ =>
-    pure ⟨.yield (iterRandM <| (it.state + (1 : UInt64)) * (3_787_392_781 : UInt64)) it.state, by trivial⟩
+    pure (.deflate ⟨.yield (iterRandM <| (it.state + (1 : UInt64)) * (3_787_392_781 : UInt64)) it.state, by trivial⟩)
 
 instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RandomIterator) m n :=
   .defaultImplementation
diff --git a/tests/bench/treemap.lean b/tests/bench/treemap.lean
index 9ff6f1e98d..cc29bbc71d 100644
--- a/tests/bench/treemap.lean
+++ b/tests/bench/treemap.lean
@@ -26,7 +26,7 @@ instance [Pure m] : Std.Iterators.Iterator RandomIterator m UInt64 where
     | .skip _ => False
     | .done => False
   step := fun ⟨it⟩ =>
-    pure ⟨.yield (iterRandM <| (it.state + (1 : UInt64)) * (3_787_392_781 : UInt64)) it.state, by trivial⟩
+    pure (.deflate ⟨.yield (iterRandM <| (it.state + (1 : UInt64)) * (3_787_392_781 : UInt64)) it.state, by trivial⟩)
 
 instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RandomIterator) m n :=
   .defaultImplementation