feat: append iterator combinator (#12844)

This PR provides the iterator combinator `append` that permits the
concatenation of two iterators.

src/Init/Data/Iterators/Combinators.lean

@@ -6,6 +6,7 @@ Authors: Paul Reichert
 module
 
 prelude
+public import Init.Data.Iterators.Combinators.Append
 public import Init.Data.Iterators.Combinators.Monadic
 public import Init.Data.Iterators.Combinators.FilterMap
 public import Init.Data.Iterators.Combinators.FlatMap

src/Init/Data/Iterators/Combinators/Append.lean

@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.Iterators.Combinators.Monadic.Append
+
+public section
+
+namespace Std
+open Std.Iterators Std.Iterators.Types
+
+/--
+Given two iterators `it₁` and `it₂`, `it₁.append it₂` is an iterator that first outputs all values
+of `it₁` in order and then all values of `it₂` in order.
+
+**Marble diagram:**
+
+```text
+it₁                 ---a----b---c--⊥
+it₂                                 --d--e--⊥
+it₁.append it₂      ---a----b---c-----d--e--⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: only if `it₁` and `it₂` are finite
+* `Productive` instance: only if `it₁` and `it₂` are productive
+
+Note: If `it₁` is not finite, then `it₁.append it₂` can be productive while `it₂` is not.
+The standard library does not provide a `Productive` instance for this case.
+
+**Performance:**
+
+This combinator incurs an additional O(1) cost with each output of `it₁` and `it₂`.
+-/
+@[inline, expose]
+def Iter.append {α₁ : Type w} {α₂ : Type w} {β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β]
+    (it₁ : Iter (α := α₁) β) (it₂ : Iter (α := α₂) β) :
+    Iter (α := Append α₁ α₂ Id β) β :=
+  (it₁.toIterM.append it₂.toIterM).toIter
+
+/--
+This combinator is only useful for advanced use cases.
+
+Given an iterator `it₂`, returns an iterator that behaves exactly like `it₂` but is of the same
+type as `it₁.append it₂` (after `it₁` has been exhausted).
+This is useful for constructing intermediate states of the append iterator.
+
+**Marble diagram:**
+
+```text
+it₂                        --a--b--⊥
+Iter.appendSnd α₁ it₂      --a--b--⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: only if `it₂` and iterators of type `α₁` are finite
+* `Productive` instance: only if `it₂` and iterators of type `α₁` are productive
+
+Note: If iterators of type `α₁` are not finite, then `append α₁ it₂` can be productive while `it₂` is not.
+The standard library does not provide a `Productive` instance for this case.
+
+**Performance:**
+
+This combinator incurs an additional O(1) cost with each output of `it₂`.
+-/
+@[inline, expose]
+def Iter.Intermediate.appendSnd {α₂ : Type w} {β : Type w}
+    [Iterator α₂ Id β] (α₁ : Type w) (it₂ : Iter (α := α₂) β) :
+    Iter (α := Append α₁ α₂ Id β) β :=
+  (IterM.Intermediate.appendSnd α₁ it₂.toIterM).toIter
+
+end Std

src/Init/Data/Iterators/Combinators/Monadic.lean

@@ -6,6 +6,7 @@ Authors: Paul Reichert
 module
 
 prelude
+public import Init.Data.Iterators.Combinators.Monadic.Append
 public import Init.Data.Iterators.Combinators.Monadic.FilterMap
 public import Init.Data.Iterators.Combinators.Monadic.FlatMap
 public import Init.Data.Iterators.Combinators.Monadic.Take

src/Init/Data/Iterators/Combinators/Monadic/Append.lean

@@ -0,0 +1,261 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.Iterators.Consumers.Monadic.Loop
+public import Init.Classical
+import Init.Data.Option.Lemmas
+import Init.ByCases
+import Init.Omega
+
+public section
+
+/-!
+This module provides the iterator combinator `IterM.append`.
+-/
+
+namespace Std
+
+variable {α : Type w} {m : Type w → Type w'} {β : Type w}
+
+/--
+The internal state of the `IterM.append` iterator combinator.
+-/
+inductive Iterators.Types.Append (α₁ α₂ : Type w) (m : Type w → Type w') (β : Type w) where
+  | fst : IterM (α := α₁) m β → IterM (α := α₂) m β → Append α₁ α₂ m β
+  | snd : IterM (α := α₂) m β → Append α₁ α₂ m β
+
+open Std.Iterators Std.Iterators.Types
+
+/--
+Given two iterators `it₁` and `it₂`, `it₁.append it₂` is an iterator that first outputs all values
+of `it₁` in order and then all values of `it₂` in order.
+
+**Marble diagram:**
+
+```text
+it₁                 ---a----b---c--⊥
+it₂                                 --d--e--⊥
+it₁.append it₂      ---a----b---c-----d--e--⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: only if `it₁` and `it₂` are finite
+* `Productive` instance: only if `it₁` and `it₂` are productive
+
+Note: If `it₁` is not finite, then `it₁.append it₂` can be productive while `it₂` is not.
+The standard library does not provide a `Productive` instance for this case.
+
+**Performance:**
+
+This combinator incurs an additional O(1) cost with each output of `it₁` and `it₂`.
+-/
+@[inline, expose]
+def IterM.append [Iterator α₁ m β] [Iterator α₂ m β]
+    (it₁ : IterM (α := α₁) m β) (it₂ : IterM (α := α₂) m β) :=
+  (⟨Iterators.Types.Append.fst it₁ it₂⟩ : IterM m β)
+
+/--
+This combinator is only useful for advanced use cases.
+
+Given an iterator `it₂`, `IterM.Intermediate.appendSnd α₁ it₂` returns an iterator that behaves
+exactly like `it₂` but has the same type as `it₁.append it₂` (after `it₁` has been exhausted).
+This is useful for constructing intermediate states of the append iterator.
+
+**Marble diagram:**
+
+```text
+it₂                                  --a--b--⊥
+IterM.Intermediate.appendSnd α₁ it₂  --a--b--⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: only if `it₂` and iterators of type `α₁` are finite
+* `Productive` instance: only if `it₂` and iterators of type `α₁` are productive
+
+Note: If iterators of type `α₁` are not finite, then `appendSnd α₁ it₂` can be productive
+while `it₂` is not. The standard library does not provide a `Productive` instance for this case.
+
+**Performance:**
+
+This combinator incurs an additional O(1) cost with each output of `it₂`.
+-/
+@[inline, expose]
+def IterM.Intermediate.appendSnd [Iterator α₂ m β] (α₁ : Type w) (it₂ : IterM (α := α₂) m β) :=
+  (⟨Iterators.Types.Append.snd (α₁ := α₁) it₂⟩ : IterM m β)
+
+namespace Iterators.Types
+
+inductive Append.PlausibleStep [Iterator α₁ m β] [Iterator α₂ m β] :
+    IterM (α := Append α₁ α₂ m β) m β → IterStep (IterM (α := Append α₁ α₂ m β) m β) β → Prop where
+  | fstYield {it₁ : IterM (α := α₁) m β}  {it₂ : IterM (α := α₂) m β} :
+    it₁.IsPlausibleStep (.yield it₁' out) → PlausibleStep (it₁.append it₂) (.yield (it₁'.append it₂) out)
+  | fstSkip {it₁ : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β} :
+    it₁.IsPlausibleStep (.skip it₁') → PlausibleStep (it₁.append it₂) (.skip (it₁'.append it₂))
+  | fstDone {it₁ : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β} :
+    it₁.IsPlausibleStep .done → PlausibleStep (it₁.append it₂) (.skip (IterM.Intermediate.appendSnd α₁ it₂))
+  | sndYield {it₂ : IterM (α := α₂) m β} :
+    it₂.IsPlausibleStep (.yield it₂' out) →
+      PlausibleStep (IterM.Intermediate.appendSnd α₁ it₂) (.yield (IterM.Intermediate.appendSnd α₁ it₂') out)
+  | sndSkip {it₂ : IterM (α := α₂) m β} :
+    it₂.IsPlausibleStep (.skip it₂') →
+      PlausibleStep (IterM.Intermediate.appendSnd α₁ it₂) (.skip (IterM.Intermediate.appendSnd α₁ it₂'))
+  | sndDone {it₂ : IterM (α := α₂) m β} :
+    it₂.IsPlausibleStep .done → PlausibleStep (IterM.Intermediate.appendSnd α₁ it₂) .done
+
+@[inline]
+instance Append.instIterator [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] :
+    Iterator (Append α₁ α₂ m β) m β where
+  IsPlausibleStep := Append.PlausibleStep
+  step
+    | ⟨.fst it₁ it₂⟩ => do
+      match (← it₁.step).inflate with
+      | .yield it₁' out h => return .deflate <| .yield (it₁'.append it₂) out (.fstYield h)
+      | .skip it₁' h => return .deflate <| .skip (it₁'.append it₂) (.fstSkip h)
+      | .done h => return .deflate <| .skip (IterM.Intermediate.appendSnd α₁ it₂) (.fstDone h)
+    | ⟨.snd it₂⟩ => do
+      match (← it₂.step).inflate with
+      | .yield it₂' out h => return .deflate <| .yield (IterM.Intermediate.appendSnd α₁ it₂') out (.sndYield h)
+      | .skip it₂' h => return .deflate <| .skip (IterM.Intermediate.appendSnd α₁ it₂') (.sndSkip h)
+      | .done h => return .deflate <| .done (.sndDone h)
+
+instance Append.instIteratorLoop {n : Type x → Type x'} [Monad m] [Monad n]
+    [Iterator α₁ m β] [Iterator α₂ m β] :
+    IteratorLoop (Append α₁ α₂ m β) m n :=
+  .defaultImplementation
+
+section Finite
+
+variable {α₁ : Type w} {α₂ : Type w} {m : Type w → Type w'} {β : Type w}
+
+variable (α₁ α₂ m β) in
+def Append.Rel [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m] :
+    IterM (α := Append α₁ α₂ m β) m β → IterM (α := Append α₁ α₂ m β) m β → Prop :=
+  InvImage
+    (Prod.Lex
+      (Option.lt (InvImage IterM.TerminationMeasures.Finite.Rel IterM.finitelyManySteps))
+      (InvImage IterM.TerminationMeasures.Finite.Rel IterM.finitelyManySteps))
+    (fun it => match it.internalState with
+      | .fst it₁ it₂ => (some it₁, it₂)
+      | .snd it₂ => (none, it₂))
+
+theorem Append.rel_of_fst [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    [Finite α₁ m] [Finite α₂ m] {it₁ it₁' : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β}
+    (h : it₁'.finitelyManySteps.Rel it₁.finitelyManySteps) :
+    Append.Rel α₁ α₂ m β (it₁'.append it₂) (it₁.append it₂) := by
+  exact Prod.Lex.left _ _ h
+
+theorem Append.rel_fstDone [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    [Finite α₁ m] [Finite α₂ m] {it₁ : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β} :
+    Append.Rel α₁ α₂ m β (IterM.Intermediate.appendSnd α₁ it₂) (it₁.append it₂) := by
+  exact Prod.Lex.left _ _ trivial
+
+theorem Append.rel_of_snd [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    [Finite α₁ m] [Finite α₂ m] {it₂ it₂' : IterM (α := α₂) m β}
+    (h : it₂'.finitelyManySteps.Rel it₂.finitelyManySteps) :
+    Append.Rel α₁ α₂ m β (IterM.Intermediate.appendSnd α₁ it₂') (IterM.Intermediate.appendSnd α₁ it₂) := by
+  exact Prod.Lex.right _ h
+
+def Append.instFinitenessRelation [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    [Finite α₁ m] [Finite α₂ m] :
+    FinitenessRelation (Append α₁ α₂ m β) m where
+  Rel := Append.Rel α₁ α₂ m β
+  wf := by
+    apply InvImage.wf
+    refine ⟨fun (a, b) => Prod.lexAccessible (WellFounded.apply ?_ a) (WellFounded.apply ?_) b⟩
+    · exact Option.wellFounded_lt <| InvImage.wf _ WellFoundedRelation.wf
+    · exact InvImage.wf _ WellFoundedRelation.wf
+  subrelation {it it'} h := by
+    obtain ⟨step, h, h'⟩ := h
+    cases h' <;> cases h
+    case fstYield =>
+      apply Append.rel_of_fst
+      exact IterM.TerminationMeasures.Finite.rel_of_yield ‹_›
+    case fstSkip =>
+      apply Append.rel_of_fst
+      exact IterM.TerminationMeasures.Finite.rel_of_skip ‹_›
+    case fstDone =>
+      exact Append.rel_fstDone
+    case sndYield =>
+      apply Append.rel_of_snd
+      exact IterM.TerminationMeasures.Finite.rel_of_yield ‹_›
+    case sndSkip =>
+      apply Append.rel_of_snd
+      exact IterM.TerminationMeasures.Finite.rel_of_skip ‹_›
+
+@[no_expose]
+public instance Append.instFinite [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    [Finite α₁ m] [Finite α₂ m] : Finite (Append α₁ α₂ m β) m :=
+  .of_finitenessRelation instFinitenessRelation
+
+end Finite
+
+section Productive
+
+variable {α₁ : Type w} {α₂ : Type w} {m : Type w → Type w'} {β : Type w}
+
+variable (α₁ α₂ m β) in
+def Append.ProductiveRel [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    [Productive α₁ m] [Productive α₂ m] :
+    IterM (α := Append α₁ α₂ m β) m β → IterM (α := Append α₁ α₂ m β) m β → Prop :=
+  InvImage
+    (Prod.Lex
+      (Option.lt (InvImage IterM.TerminationMeasures.Productive.Rel IterM.finitelyManySkips))
+      (InvImage IterM.TerminationMeasures.Productive.Rel IterM.finitelyManySkips))
+    (fun it => match it.internalState with
+      | .fst it₁ it₂ => (some it₁, it₂)
+      | .snd it₂ => (none, it₂))
+
+theorem Append.productiveRel_of_fst [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    [Productive α₁ m] [Productive α₂ m] {it₁ it₁' : IterM (α := α₁) m β}
+    {it₂ : IterM (α := α₂) m β}
+    (h : it₁'.finitelyManySkips.Rel it₁.finitelyManySkips) :
+    Append.ProductiveRel α₁ α₂ m β (it₁'.append it₂) (it₁.append it₂) := by
+  exact Prod.Lex.left _ _ h
+
+theorem Append.productiveRel_fstDone [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    [Productive α₁ m] [Productive α₂ m] {it₁ : IterM (α := α₁) m β}
+    {it₂ : IterM (α := α₂) m β} :
+    Append.ProductiveRel α₁ α₂ m β (IterM.Intermediate.appendSnd α₁ it₂) (it₁.append it₂) := by
+  exact Prod.Lex.left _ _ trivial
+
+theorem Append.productiveRel_of_snd [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    [Productive α₁ m] [Productive α₂ m] {it₂ it₂' : IterM (α := α₂) m β}
+    (h : it₂'.finitelyManySkips.Rel it₂.finitelyManySkips) :
+    Append.ProductiveRel α₁ α₂ m β
+      (IterM.Intermediate.appendSnd α₁ it₂') (IterM.Intermediate.appendSnd α₁ it₂) := by
+  exact Prod.Lex.right _ h
+
+private def Append.instProductivenessRelation [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    [Productive α₁ m] [Productive α₂ m] :
+    ProductivenessRelation (Append α₁ α₂ m β) m where
+  Rel := Append.ProductiveRel α₁ α₂ m β
+  wf := by
+    apply InvImage.wf
+    refine ⟨fun (a, b) => Prod.lexAccessible (WellFounded.apply ?_ a) (WellFounded.apply ?_) b⟩
+    · exact Option.wellFounded_lt <| InvImage.wf _ WellFoundedRelation.wf
+    · exact InvImage.wf _ WellFoundedRelation.wf
+  subrelation {it it'} h := by
+    cases h
+    case fstSkip =>
+      apply Append.productiveRel_of_fst
+      exact IterM.TerminationMeasures.Productive.rel_of_skip ‹_›
+    case fstDone =>
+      exact Append.productiveRel_fstDone
+    case sndSkip =>
+      apply Append.productiveRel_of_snd
+      exact IterM.TerminationMeasures.Productive.rel_of_skip ‹_›
+
+instance Append.instProductive [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    [Productive α₁ m] [Productive α₂ m] : Productive (Append α₁ α₂ m β) m :=
+  .of_productivenessRelation instProductivenessRelation
+
+end Productive
+
+end Std.Iterators.Types

src/Init/Data/Iterators/Lemmas/Combinators.lean

@@ -6,6 +6,7 @@ Authors: Paul Reichert
 module
 
 prelude
+public import Init.Data.Iterators.Lemmas.Combinators.Append
 public import Init.Data.Iterators.Lemmas.Combinators.Attach
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic
 public import Init.Data.Iterators.Lemmas.Combinators.FilterMap

src/Init/Data/Iterators/Lemmas/Combinators/Append.lean

@@ -0,0 +1,193 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.Iterators.Combinators.Append
+public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
+public import Init.Data.Iterators.Consumers.Collect
+public import Init.Data.Iterators.Consumers.Access
+import Init.Data.Iterators.Lemmas.Consumers.Collect
+import Init.Data.Iterators.Lemmas.Consumers.Access
+import Init.Data.Iterators.Lemmas.Basic
+import Init.Omega
+
+public section
+
+namespace Std
+open Std.Iterators Std.Iterators.Types
+
+theorem Iter.append_eq_toIter_append_toIterM {α₁ α₂ β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β]
+    {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} :
+    it₁.append it₂ = (it₁.toIterM.append it₂.toIterM).toIter :=
+  rfl
+
+theorem Iter.Intermediate.appendSnd_eq_toIter_appendSnd_toIterM {α₁ α₂ β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β]
+    {it₂ : Iter (α := α₂) β} :
+    Iter.Intermediate.appendSnd α₁ it₂ = (IterM.Intermediate.appendSnd α₁ it₂.toIterM).toIter :=
+  rfl
+
+theorem Iter.step_append {α₁ α₂ β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β]
+    {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} :
+    (it₁.append it₂).step =
+      match it₁.step with
+      | .yield it₁' out h => .yield (it₁'.append it₂) out (.fstYield h)
+      | .skip it₁' h => .skip (it₁'.append it₂) (.fstSkip h)
+      | .done h => .skip (Iter.Intermediate.appendSnd α₁ it₂) (.fstDone h) := by
+  simp only [Iter.step, append_eq_toIter_append_toIterM, toIterM_toIter, IterM.step_append,
+    Id.run_bind]
+  cases it₁.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;>
+    simp [Intermediate.appendSnd_eq_toIter_appendSnd_toIterM]
+
+theorem Iter.Intermediate.step_appendSnd {α₁ α₂ β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β]
+    {it₂ : Iter (α := α₂) β} :
+    (Iter.Intermediate.appendSnd α₁ it₂).step =
+      match it₂.step with
+      | .yield it₂' out h => .yield (Iter.Intermediate.appendSnd α₁ it₂') out (.sndYield h)
+      | .skip it₂' h => .skip (Iter.Intermediate.appendSnd α₁ it₂') (.sndSkip h)
+      | .done h => .done (.sndDone h) := by
+  simp only [Iter.step, appendSnd, toIterM_toIter, IterM.Intermediate.step_appendSnd, Id.run_bind]
+  cases it₂.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp
+
+@[simp]
+theorem Iter.toList_append {α₁ α₂ β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β] [Finite α₁ Id] [Finite α₂ Id]
+    {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} :
+    (it₁.append it₂).toList = it₁.toList ++ it₂.toList := by
+  simp [append_eq_toIter_append_toIterM, toList_eq_toList_toIterM]
+
+@[simp]
+theorem Iter.toListRev_append {α₁ α₂ β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β] [Finite α₁ Id] [Finite α₂ Id]
+    {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} :
+    (it₁.append it₂).toListRev = it₂.toListRev ++ it₁.toListRev := by
+  simp [append_eq_toIter_append_toIterM, toListRev_eq_toListRev_toIterM]
+
+@[simp]
+theorem Iter.toArray_append {α₁ α₂ β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β] [Finite α₁ Id] [Finite α₂ Id]
+    {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} :
+    (it₁.append it₂).toArray = it₁.toArray ++ it₂.toArray := by
+  simp [append_eq_toIter_append_toIterM, toArray_eq_toArray_toIterM]
+
+@[simp]
+theorem Iter.atIdxSlow?_appendSnd {α₁ α₂ β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β] [Productive α₁ Id] [Productive α₂ Id]
+    {it₂ : Iter (α := α₂) β} {n : Nat} :
+    (Iter.Intermediate.appendSnd α₁ it₂).atIdxSlow? n = it₂.atIdxSlow? n := by
+  induction n, it₂ using Iter.atIdxSlow?.induct_unfolding with
+  | yield_zero it it' out h h' =>
+    simp only [atIdxSlow?_eq_match (it := Iter.Intermediate.appendSnd α₁ it),
+      Intermediate.step_appendSnd, h']
+  | yield_succ it it' out h h' n ih =>
+    simp only [atIdxSlow?_eq_match (it := Iter.Intermediate.appendSnd α₁ it),
+      Intermediate.step_appendSnd, h', ih]
+  | skip_case n it it' h h' ih =>
+    simp only [atIdxSlow?_eq_match (it := Iter.Intermediate.appendSnd α₁ it),
+      Intermediate.step_appendSnd, h', ih]
+  | done_case n it h h' =>
+    simp only [atIdxSlow?_eq_match (it := Iter.Intermediate.appendSnd α₁ it),
+      Intermediate.step_appendSnd, h']
+
+theorem Iter.atIdxSlow?_append_of_eq_some {α₁ α₂ β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β] [Productive α₁ Id] [Productive α₂ Id]
+    {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} {n : Nat} {b : β}
+    (h : it₁.atIdxSlow? n = some b) :
+    (it₁.append it₂).atIdxSlow? n = some b := by
+  induction n, it₁ using Iter.atIdxSlow?.induct_unfolding generalizing it₂ with
+  | yield_zero it it' out hp h' =>
+    rw [atIdxSlow?_eq_match (it := it.append it₂)]
+    cases h
+    simp [step_append, h']
+  | yield_succ it it' out hp h' n ih =>
+    rw [atIdxSlow?_eq_match (it := it.append it₂)]
+    simp [step_append, h', ih h]
+  | skip_case n it it' hp h' ih =>
+    rw [atIdxSlow?_eq_match (it := it.append it₂)]
+    simp [step_append, h', ih h]
+  | done_case n it hp h' =>
+    cases h
+
+theorem Iter.atIdxSlow?_append {α₁ α₂ β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β] [Finite α₁ Id] [Productive α₂ Id]
+    {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} {n : Nat} :
+    (it₁.append it₂).atIdxSlow? n =
+      if n < it₁.toList.length then it₁.atIdxSlow? n
+      else it₂.atIdxSlow? (n - it₁.toList.length) := by
+  induction n, it₁ using Iter.atIdxSlow?.induct_unfolding generalizing it₂ with
+  | yield_zero it it' out h h' =>
+    simp only [atIdxSlow?_eq_match (it := it.append it₂), step_append, h']
+    rw [toList_eq_match_step (it := it)]
+    simp [h']
+  | yield_succ it it' out h h' n ih =>
+    simp only [atIdxSlow?_eq_match (it := it.append it₂), step_append, h', ih]
+    rw [toList_eq_match_step (it := it)]
+    simp [h', Nat.succ_lt_succ_iff, Nat.succ_sub_succ]
+  | skip_case n it it' h h' ih =>
+    simp only [atIdxSlow?_eq_match (it := it.append it₂), step_append, h', ih]
+    rw [toList_eq_match_step (it := it)]
+    simp [h']
+  | done_case n it h h' =>
+    simp [atIdxSlow?_eq_match (it := it.append it₂), step_append, h',
+      atIdxSlow?_appendSnd, toList_eq_match_step]
+
+theorem Iter.atIdxSlow?_append_of_productive {α₁ α₂ β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β] [Productive α₁ Id] [Productive α₂ Id]
+    {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} {n k : Nat}
+    (hk : it₁.atIdxSlow? k = none)
+    (hmin : ∀ j, j < k → (it₁.atIdxSlow? j).isSome)
+    (hle : k ≤ n) :
+    (it₁.append it₂).atIdxSlow? n = it₂.atIdxSlow? (n - k) := by
+  induction n, it₁ using Iter.atIdxSlow?.induct_unfolding generalizing k it₂ with
+  | yield_zero it it' out hp h' =>
+    exfalso
+    have : k = 0 := by omega
+    subst this
+    rw [atIdxSlow?_eq_match (it := it)] at hk
+    simp [h'] at hk
+  | yield_succ it it' out hp h' n ih =>
+    rw [atIdxSlow?_eq_match (it := it.append it₂)]
+    simp only [step_append, h']
+    match k with
+    | 0 =>
+      rw [atIdxSlow?_eq_match (it := it)] at hk
+      simp [h'] at hk
+    | k + 1 =>
+      rw [atIdxSlow?_eq_match (it := it)] at hk
+      simp [h'] at hk
+      have hmin' : ∀ j, j < k → (it'.atIdxSlow? j).isSome := by
+        intro j hj
+        have h := hmin (j + 1) (by omega)
+        rw [atIdxSlow?_eq_match (it := it)] at h
+        simpa [h'] using h
+      rw [ih hk hmin' (by omega)]
+      congr 1
+      omega
+  | skip_case n it it' hp h' ih =>
+    rw [atIdxSlow?_eq_match (it := it.append it₂)]
+    simp only [step_append, h']
+    rw [atIdxSlow?_eq_match (it := it)] at hk; simp [h'] at hk
+    have hmin' : ∀ j, j < k → (it'.atIdxSlow? j).isSome := by
+      intro j hj
+      have h := hmin j hj
+      rw [atIdxSlow?_eq_match (it := it)] at h
+      simpa [h'] using h
+    exact ih hk hmin' hle
+  | done_case n it hp h' =>
+    rw [atIdxSlow?_eq_match (it := it.append it₂)]
+    simp only [step_append, h', atIdxSlow?_appendSnd]
+    have hk0 : k = 0 := by
+      false_or_by_contra
+      have h := hmin 0 (by omega)
+      rw [atIdxSlow?_eq_match (it := it)] at h
+      simp [h'] at h
+    simp [hk0]
+
+end Std

src/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean

@@ -6,6 +6,7 @@ Authors: Paul Reichert
 module
 
 prelude
+public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap

src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Append.lean

@@ -0,0 +1,107 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.Iterators.Combinators.Monadic.Append
+public import Init.Data.Iterators.Consumers.Monadic.Collect
+import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
+import Init.Data.Iterators.Lemmas.Monadic.Basic
+import Init.Data.List.Lemmas
+import Init.Data.List.ToArray
+
+public section
+
+namespace Std
+open Std.Iterators Std.Iterators.Types
+
+variable {α₁ α₂ β : Type w} {m : Type w → Type w'}
+
+theorem IterM.step_append [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    {it₁ : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β} :
+    (it₁.append it₂).step = (do
+      match (← it₁.step).inflate with
+      | .yield it₁' out h =>
+        pure <| .deflate <| .yield (it₁'.append it₂) out (.fstYield h)
+      | .skip it₁' h =>
+        pure <| .deflate <| .skip (it₁'.append it₂) (.fstSkip h)
+      | .done h =>
+        pure <| .deflate <| .skip (IterM.Intermediate.appendSnd α₁ it₂) (.fstDone h)) := by
+  simp only [append, Intermediate.appendSnd, step, Iterator.step]
+  apply bind_congr; intro step
+  cases step.inflate using PlausibleIterStep.casesOn <;> rfl
+
+theorem IterM.Intermediate.step_appendSnd [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    {it₂ : IterM (α := α₂) m β} :
+    (IterM.Intermediate.appendSnd α₁ it₂).step = (do
+      match (← it₂.step).inflate with
+      | .yield it₂' out h =>
+        pure <| .deflate <| .yield (IterM.Intermediate.appendSnd α₁ it₂') out (.sndYield h)
+      | .skip it₂' h =>
+        pure <| .deflate <| .skip (IterM.Intermediate.appendSnd α₁ it₂') (.sndSkip h)
+      | .done h =>
+        pure <| .deflate <| .done (.sndDone h)) := by
+  simp only [Intermediate.appendSnd, step, Iterator.step]
+  apply bind_congr; intro step
+  cases step.inflate using PlausibleIterStep.casesOn <;> rfl
+
+@[simp]
+theorem IterM.toList_appendSnd [Monad m] [LawfulMonad m]
+    [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m]
+    {it₂ : IterM (α := α₂) m β} :
+    (IterM.Intermediate.appendSnd α₁ it₂).toList = it₂.toList := by
+  induction it₂ using IterM.inductSteps with | step it₂ ihy ihs
+  rw [toList_eq_match_step (it := IterM.Intermediate.appendSnd α₁ it₂),
+      toList_eq_match_step (it := it₂)]
+  simp only [Intermediate.step_appendSnd, bind_assoc]
+  apply bind_congr; intro step
+  cases step.inflate using PlausibleIterStep.casesOn
+  · simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
+@[simp]
+theorem IterM.toList_append [Monad m] [LawfulMonad m]
+    [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m]
+    {it₁ : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β} :
+    (it₁.append it₂).toList = (do
+      let l₁ ← it₁.toList
+      let l₂ ← it₂.toList
+      pure (l₁ ++ l₂)) := by
+  induction it₁ using IterM.inductSteps with | step it₁ ihy ihs
+  rw [toList_eq_match_step (it := it₁.append it₂), toList_eq_match_step (it := it₁)]
+  simp only [step_append, bind_assoc]
+  apply bind_congr; intro step
+  cases step.inflate using PlausibleIterStep.casesOn
+  · simp [ihy ‹_›, - bind_pure_comp]
+  · simp [ihs ‹_›]
+  · simp [toList_appendSnd, - bind_pure_comp]
+
+@[simp]
+theorem IterM.toListRev_append [Monad m] [LawfulMonad m]
+    [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m]
+    {it₁ : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β} :
+    (it₁.append it₂).toListRev = (do
+      let l₁ ← it₁.toListRev
+      let l₂ ← it₂.toListRev
+      pure (l₂ ++ l₁)) := by
+  rw [toListRev_eq (it := it₁.append it₂), toList_append,
+      toListRev_eq (it := it₁), toListRev_eq (it := it₂)]
+  simp [map_bind, bind_pure_comp, List.reverse_append]
+
+@[simp]
+theorem IterM.toArray_append [Monad m] [LawfulMonad m]
+    [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m]
+    {it₁ : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β} :
+    (it₁.append it₂).toArray = (do
+      let a₁ ← it₁.toArray
+      let a₂ ← it₂.toArray
+      pure (a₁ ++ a₂)) := by
+  rw [← toArray_toList (it := it₁.append it₂), toList_append,
+      ← toArray_toList (it := it₁), ← toArray_toList (it := it₂)]
+  simp [map_bind, - bind_pure_comp, ← List.toArray_appendList, - toArray_toList]
+
+end Std