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 fun (x1 : β) (x2 : γ) => (fun (x : ForInStep γ) => ⟨x, True.intro⟩) <$> f x1 x2

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 : β → γ → 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.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.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

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