theorem Std.Iterators.Iter.forIn'_eq {α β : Type w} [Iterator α Id β] [Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [hl : LawfulIteratorLoop α Id m] {γ : Type x} {it : Iter β} {init : γ} {f : (b : β) → it.IsPlausibleIndirectOutput b → γ → m (ForInStep γ)} : forIn' it init f = IterM.DefaultConsumers.forIn' (fun (x : Type w) (x_1 : Type x) (f : x → m x_1) (x_2 : Id x) => f x_2.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 x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [hl : LawfulIteratorLoop α Id m] {γ : Type x} {it : Iter β} {init : γ} {f : β → γ → m (ForInStep γ)} : forIn it init f = IterM.DefaultConsumers.forIn' (fun (x : Type w) (x_1 : Type x) (f : x → m x_1) (c : Id x) => f 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'_congr {γ : Type u_1} {α β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] {ita itb : Iter β} (w : ita = itb) {b b' : γ} (hb : b = b') {f : (a' : β) → a' ∈ ita → γ → Id (ForInStep γ)} {g : (a' : β) → a' ∈ itb → γ → Id (ForInStep γ)} (h : ∀ (a : β) (m : a ∈ itb) (b : γ), f a ⋯ b = g a m b) : forIn' ita b f = forIn' itb b' g

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 x → Type x''} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] {γ : Type x} {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 x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] {γ : Type x} {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.mem_toArray_iff_isPlausibleIndirectOutput {α β : Type u_1} [Iterator α Id β] [IteratorCollect α Id Id] [Finite α Id] [LawfulIteratorCollect α Id Id] [LawfulDeterministicIterator α Id] {it : Iter β} {out : β} : out ∈ it.toArray ↔ it.IsPlausibleIndirectOutput out

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

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

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

theorem Std.Iterators.Iter.foldM_eq_forIn {α β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id] {m : Type x → Type x'} [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} {γ δ : Type x} [Iterator α Id β] [Finite α Id] {m : Type x → Type x'} [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} {γ : Type x} [Iterator α Id β] [Finite α Id] {m : Type x → Type x'} [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} {γ : Type x} [Iterator α Id β] [Finite α Id] {m : Type x → Type x'} [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.Iter.foldlM_toArray {α β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {f : γ → β → m γ} {init : γ} {it : Iter β} : Array.foldlM f init it.toArray = foldM f init it

theorem Std.Iterators.IterM.forIn_eq_foldM {α β : Type w} [Iterator α Id β] [Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {γ : Type x} {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} {γ : Type x} [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} {γ : Type x} [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

theorem Std.Iterators.Iter.fold_eq_fold_toIterM {α β γ : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {f : γ → β → γ} {init : γ} {it : Iter β} : fold f init it = (IterM.fold f init it.toIterM).run

@[simp]

theorem Std.Iterators.Iter.forIn_pure_yield_eq_fold {α β : Type w} {γ : Type x} [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} {γ : Type x} [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

theorem Std.Iterators.Iter.fold_hom {α β : Type u_1} {γ₁ γ₂ : Type u_2} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} (f : γ₁ → γ₂) {g₁ : γ₁ → β → γ₁} {g₂ : γ₂ → β → γ₂} {init : γ₁} (H : ∀ (x : γ₁) (y : β), g₂ (f x) y = f (g₁ x y)) : fold g₂ (f init) it = f (fold g₁ init it)

theorem Std.Iterators.Iter.toList_eq_fold {α β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} : it.toList = fold (fun (l : List β) (out : β) => l ++ [out]) [] it

theorem Std.Iterators.Iter.toArray_eq_fold {α β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} : it.toArray = fold (fun (xs : Array β) (out : β) => xs.push out) #[] it

@[simp]

theorem Std.Iterators.Iter.foldl_toList {α β : Type w} {γ : Type x} [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.foldl_toArray {α β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {f : γ → β → γ} {init : γ} {it : Iter β} : Array.foldl f init it.toArray = 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