theorem Std.IterM.step_append {α₁ α₂ β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] {it₁ : IterM m β} {it₂ : IterM m β} : (it₁.append it₂).step = do let __do_lift ← it₁.step match __do_lift.inflate with | ⟨IterStep.yield it₁' out, h⟩ => pure (Shrink.deflate (PlausibleIterStep.yield (it₁'.append it₂) out ⋯)) | ⟨IterStep.skip it₁', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (it₁'.append it₂) ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (Intermediate.appendSnd α₁ it₂) ⋯))

theorem Std.IterM.Intermediate.step_appendSnd {α₁ α₂ β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] {it₂ : IterM m β} : (appendSnd α₁ it₂).step = do let __do_lift ← it₂.step match __do_lift.inflate with | ⟨IterStep.yield it₂' out, h⟩ => pure (Shrink.deflate (PlausibleIterStep.yield (appendSnd α₁ it₂') out ⋯)) | ⟨IterStep.skip it₂', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (appendSnd α₁ it₂') ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))

@[simp]

theorem Std.IterM.toList_appendSnd {α₁ α₂ β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α₁ m β] [Iterator α₂ m β] [Iterators.Finite α₁ m] [Iterators.Finite α₂ m] {it₂ : IterM m β} : (Intermediate.appendSnd α₁ it₂).toList = it₂.toList

@[simp]

theorem Std.IterM.toList_append {α₁ α₂ β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α₁ m β] [Iterator α₂ m β] [Iterators.Finite α₁ m] [Iterators.Finite α₂ m] {it₁ : IterM m β} {it₂ : IterM m β} : (it₁.append it₂).toList = do let l₁ ← it₁.toList let l₂ ← it₂.toList pure (l₁ ++ l₂)

@[simp]

theorem Std.IterM.toListRev_append {α₁ α₂ β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α₁ m β] [Iterator α₂ m β] [Iterators.Finite α₁ m] [Iterators.Finite α₂ m] {it₁ : IterM m β} {it₂ : IterM m β} : (it₁.append it₂).toListRev = do let l₁ ← it₁.toListRev let l₂ ← it₂.toListRev pure (l₂ ++ l₁)

@[simp]

theorem Std.IterM.toArray_append {α₁ α₂ β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α₁ m β] [Iterator α₂ m β] [Iterators.Finite α₁ m] [Iterators.Finite α₂ m] {it₁ : IterM m β} {it₂ : IterM m β} : (it₁.append it₂).toArray = do let a₁ ← it₁.toArray let a₂ ← it₂.toArray pure (a₁ ++ a₂)