theorem Std.Iterators.Iter.forIn'_eq {α β : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w''} [Monad m] [IteratorLoop α Id m] [hl : LawfulIteratorLoop α Id m] {γ : Type w} {it : Iter β} {init : γ} {f : (b : β) → it.IsPlausibleIndirectOutput b → γ → m (ForInStep γ)} : forIn' it init f = IterM.DefaultConsumers.forIn' (fun (x : Type w) (c : Id x) => pure c.run) γ (fun (x : β) (x : γ) (x : ForInStep γ) => True) ⋯ it.toIterM init it.toIterM.IsPlausibleIndirectOutput ⋯ fun (out : β) (h : it.toIterM.IsPlausibleIndirectOutput out) (acc : γ) => (fun (x : ForInStep γ) => ⟨x, True.intro⟩) <$> f out ⋯ acc

theorem Std.Iterators.Iter.forIn_eq {α β : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w''} [Monad m] [IteratorLoop α Id m] [hl : LawfulIteratorLoop α Id m] {γ : Type w} {it : Iter β} {init : γ} {f : β → γ → m (ForInStep γ)} : forIn it init f = IterM.DefaultConsumers.forIn' (fun (x : Type w) (c : Id x) => pure c.run) γ (fun (x : β) (x : γ) (x : ForInStep γ) => True) ⋯ it.toIterM init it.toIterM.IsPlausibleIndirectOutput ⋯ fun (out : β) (x : it.toIterM.IsPlausibleIndirectOutput out) (acc : γ) => (fun (x : ForInStep γ) => ⟨x, True.intro⟩) <$> f out acc

theorem Std.Iterators.Iter.forIn'_eq_forIn'_toIterM {α β : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] {γ : Type w} {it : Iter β} {init : γ} {f : (out : β) → out ∈ it → γ → m (ForInStep γ)} : forIn' it init f = forIn' it.toIterM init fun (out : β) (h : out ∈ it.toIterM) (acc : γ) => f out ⋯ acc

theorem Std.Iterators.Iter.forIn_eq_forIn_toIterM {α β : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] {γ : Type w} {it : Iter β} {init : γ} {f : β → γ → m (ForInStep γ)} : forIn it init f = forIn it.toIterM init f

theorem Std.Iterators.Iter.forIn'_eq_match_step {α β : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] {γ : Type w} {it : Iter β} {init : γ} {f : (out : β) → out ∈ it → γ → m (ForInStep γ)} : forIn' it init f = match it.step with | ⟨IterStep.yield it' out, h⟩ => do let __do_lift ← f out ⋯ init match __do_lift with | ForInStep.yield c => forIn' it' c fun (out_1 : β) (h'' : out_1 ∈ it') (acc : γ) => f out_1 ⋯ acc | ForInStep.done c => pure c | ⟨IterStep.skip it', h⟩ => forIn' it' init fun (out : β) (h' : out ∈ it') (acc : γ) => f out ⋯ acc | ⟨IterStep.done, property⟩ => pure init

theorem Std.Iterators.Iter.forIn_eq_match_step {α β : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] {γ : Type w} {it : Iter β} {init : γ} {f : β → γ → m (ForInStep γ)} : forIn it init f = match it.step with | ⟨IterStep.yield it' out, property⟩ => do let __do_lift ← f out init match __do_lift with | ForInStep.yield c => forIn it' c f | ForInStep.done c => pure c | ⟨IterStep.skip it', property⟩ => forIn it' init f | ⟨IterStep.done, property⟩ => pure init

theorem Std.Iterators.Iter.isPlausibleStep_iff_step_eq {α β : Type u_1} [Iterator α Id β] [IteratorCollect α Id Id] [Finite α Id] [LawfulIteratorCollect α Id Id] [LawfulDeterministicIterator α Id] {it : Iter β} {step : IterStep (Iter β) β} : it.IsPlausibleStep step ↔ it.step.val = step

theorem Std.Iterators.Iter.mem_toList_iff_isPlausibleIndirectOutput {α β : Type u_1} [Iterator α Id β] [IteratorCollect α Id Id] [Finite α Id] [LawfulIteratorCollect α Id Id] [LawfulDeterministicIterator α Id] {it : Iter β} {out : β} : out ∈ it.toList ↔ it.IsPlausibleIndirectOutput out

theorem Std.Iterators.Iter.forIn'_toList {α β : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] [LawfulDeterministicIterator α Id] {γ : Type w} {it : Iter β} {init : γ} {f : (out : β) → out ∈ it.toList → γ → m (ForInStep γ)} : forIn' it.toList init f = forIn' it init fun (out : β) (h : out ∈ it) (acc : γ) => f out ⋯ acc

theorem Std.Iterators.Iter.forIn'_eq_forIn'_toList {α β : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] [LawfulDeterministicIterator α Id] {γ : Type w} {it : Iter β} {init : γ} {f : (out : β) → out ∈ it → γ → m (ForInStep γ)} : forIn' it init f = forIn' it.toList init fun (out : β) (h : out ∈ it.toList) (acc : γ) => f out ⋯ acc

theorem Std.Iterators.Iter.forIn_toList {α β : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {γ : Type w} {it : Iter β} {init : γ} {f : β → γ → m (ForInStep γ)} : forIn it.toList init f = forIn it init f

theorem Std.Iterators.Iter.foldM_eq_forIn {α β γ : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w'} [Monad m] [IteratorLoop α Id m] {f : γ → β → m γ} {init : γ} {it : Iter β} : foldM f init it = forIn it init fun (x : β) (acc : γ) => ForInStep.yield <$> f acc x

theorem Std.Iterators.Iter.foldM_eq_foldM_toIterM {α β : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] {γ : Type w} {it : Iter β} {init : γ} {f : γ → β → m γ} : foldM f init it = IterM.foldM f init it.toIterM

theorem Std.Iterators.Iter.forIn_yield_eq_foldM {α β γ δ : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] {f : β → γ → m δ} {g : β → γ → δ → γ} {init : γ} {it : Iter β} : (forIn it init fun (c : β) (b : γ) => (fun (d : δ) => ForInStep.yield (g c b d)) <$> f c b) = foldM (fun (b : γ) (c : β) => g c b <$> f c b) init it

theorem Std.Iterators.Iter.foldM_eq_match_step {α β γ : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] {f : γ → β → m γ} {init : γ} {it : Iter β} : foldM f init it = match it.step with | ⟨IterStep.yield it' out, property⟩ => do let __do_lift ← f init out foldM f __do_lift it' | ⟨IterStep.skip it', property⟩ => foldM f init it' | ⟨IterStep.done, property⟩ => pure init

theorem Std.Iterators.Iter.foldlM_toList {α β γ : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {f : γ → β → m γ} {init : γ} {it : Iter β} : List.foldlM f init it.toList = foldM f init it

theorem Std.Iterators.IterM.forIn_eq_foldM {α β : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {γ : Type w} {it : Iter β} {init : γ} {f : β → γ → m (ForInStep γ)} : forIn it init f = ForInStep.value <$> Iter.foldM (fun (c : ForInStep γ) (b : β) => match c with | ForInStep.yield c => f b c | ForInStep.done c => pure (ForInStep.done c)) (ForInStep.yield init) it

theorem Std.Iterators.Iter.fold_eq_forIn {α β γ : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] {f : γ → β → γ} {init : γ} {it : Iter β} : fold f init it = (forIn it init fun (x : β) (acc : γ) => pure (ForInStep.yield (f acc x))).run

theorem Std.Iterators.Iter.fold_eq_foldM {α β γ : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] {f : γ → β → γ} {init : γ} {it : Iter β} : fold f init it = (foldM (fun (x1 : γ) (x2 : β) => pure (f x1 x2)) init it).run

@[simp]

theorem Std.Iterators.Iter.forIn_pure_yield_eq_fold {α β γ : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {f : β → γ → γ} {init : γ} {it : Iter β} : (forIn it init fun (c : β) (b : γ) => pure (ForInStep.yield (f c b))) = pure (fold (fun (b : γ) (c : β) => f c b) init it)

theorem Std.Iterators.Iter.fold_eq_match_step {α β γ : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {f : γ → β → γ} {init : γ} {it : Iter β} : fold f init it = match it.step with | ⟨IterStep.yield it' out, property⟩ => fold f (f init out) it' | ⟨IterStep.skip it', property⟩ => fold f init it' | ⟨IterStep.done, property⟩ => init

@[simp]

theorem Std.Iterators.Iter.foldl_toList {α β γ : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {f : γ → β → γ} {init : γ} {it : Iter β} : List.foldl f init it.toList = fold f init it

@[simp]

theorem Std.Iterators.Iter.size_toArray_eq_size {α β : Type w} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] [IteratorSize α Id] [LawfulIteratorSize α] {it : Iter β} : it.toArray.size = it.size

@[simp]

theorem Std.Iterators.Iter.length_toList_eq_size {α β : Type w} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] [IteratorSize α Id] [LawfulIteratorSize α] {it : Iter β} : it.toList.length = it.size

@[simp]

theorem Std.Iterators.Iter.length_toListRev_eq_size {α β : Type w} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] [IteratorSize α Id] [LawfulIteratorSize α] {it : Iter β} : it.toListRev.length = it.size