theorem Std.Iterators.IterM.DefaultConsumers.forIn'_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] {n : Type w → Type w''} [Monad n] {lift : (γ : Type w) → m γ → n γ} {γ : Type w} {plausible_forInStep : β → γ → ForInStep γ → Prop} {wf : IteratorLoop.WellFounded α m plausible_forInStep} {it : IterM m β} {init : γ} {P : β → Prop} {hP : ∀ (b : β), it.IsPlausibleIndirectOutput b → P b} {f : (b : β) → P b → (c : γ) → n (Subtype (plausible_forInStep b c))} : forIn' lift γ plausible_forInStep wf it init P hP f = do let __do_lift ← lift it.Step it.step match __do_lift with | ⟨IterStep.yield it' out, h⟩ => do let __do_lift ← f out ⋯ init match __do_lift with | ⟨ForInStep.yield c, property⟩ => forIn' lift γ plausible_forInStep wf it' c P ⋯ f | ⟨ForInStep.done c, property⟩ => pure c | ⟨IterStep.skip it', h⟩ => forIn' lift γ plausible_forInStep wf it' init P ⋯ f | ⟨IterStep.done, property⟩ => pure init

theorem Std.Iterators.IterM.forIn'_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] {n : Type w → Type w''} [Monad n] [IteratorLoop α m n] [hl : LawfulIteratorLoop α m n] [MonadLiftT m n] {γ : Type w} {it : IterM m β} {init : γ} {f : (b : β) → it.IsPlausibleIndirectOutput b → γ → n (ForInStep γ)} : forIn' it init f = DefaultConsumers.forIn' (fun (x : Type w) => monadLift) γ (fun (x : β) (x : γ) (x : ForInStep γ) => True) ⋯ it init it.IsPlausibleIndirectOutput ⋯ fun (x1 : β) (x2 : it.IsPlausibleIndirectOutput x1) (x3 : γ) => (fun (x : ForInStep γ) => ⟨x, True.intro⟩) <$> f x1 x2 x3

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

@[irreducible]

theorem Std.Iterators.IterM.DefaultConsumers.forIn'_eq_forIn' {m : Type w → Type w'} {α β : Type w} [Iterator α m β] {n : Type w → Type w''} [Monad n] {lift : (γ : Type w) → m γ → n γ} {γ : Type w} {Pl : β → γ → ForInStep γ → Prop} {wf : IteratorLoop.WellFounded α m Pl} {it : IterM m β} {init : γ} {P : β → Prop} {hP : ∀ (b : β), it.IsPlausibleIndirectOutput b → P b} {Q : β → Prop} {hQ : ∀ (b : β), it.IsPlausibleIndirectOutput b → Q b} {f : (b : β) → P b → (c : γ) → n (Subtype (Pl b c))} {g : (b : β) → Q b → (c : γ) → n (Subtype (Pl b c))} (hfg : ∀ (b : β) (c : γ) (hPb : P b) (hQb : Q b), f b hPb c = g b hQb c) : forIn' lift γ Pl wf it init P hP f = forIn' lift γ Pl wf it init Q hQ g

theorem Std.Iterators.IterM.forIn'_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] {n : Type w → Type w''} [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] {γ : Type w} {it : IterM m β} {init : γ} {f : (out : β) → out ∈ it → γ → n (ForInStep γ)} : forIn' it init f = do let __do_lift ← liftM it.step match __do_lift 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.IterM.forIn_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] {n : Type w → Type w''} [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] {γ : Type w} {it : IterM m β} {init : γ} {f : β → γ → n (ForInStep γ)} : forIn it init f = do let __do_lift ← liftM it.step match __do_lift 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.IterM.forM_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] {n : Type w → Type w''} [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] {it : IterM m β} {f : β → n PUnit} : forM it f = forIn it PUnit.unit fun (out : β) (x : PUnit) => do f out pure (ForInStep.yield PUnit.unit)

theorem Std.Iterators.IterM.forM_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] {n : Type w → Type w''} [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] {it : IterM m β} {f : β → n PUnit} : forM it f = do let __do_lift ← liftM it.step match __do_lift with | ⟨IterStep.yield it' out, property⟩ => do f out forM it' f | ⟨IterStep.skip it', property⟩ => forM it' f | ⟨IterStep.done, property⟩ => pure PUnit.unit

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

theorem Std.Iterators.IterM.forIn_yield_eq_foldM {α β γ δ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] {n : Type w → Type w''} [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] {f : β → γ → n δ} {g : β → γ → δ → γ} {init : γ} {it : IterM m β} : (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.IterM.foldM_eq_match_step {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] {n : Type w → Type w''} [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] {f : γ → β → n γ} {init : γ} {it : IterM m β} : foldM f init it = do let __do_lift ← liftM it.step match __do_lift 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.IterM.fold_eq_forIn {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [IteratorLoop α m m] {f : γ → β → γ} {init : γ} {it : IterM m β} : fold f init it = forIn it init fun (x : β) (acc : γ) => pure (ForInStep.yield (f acc x))

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

@[simp]

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

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

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

theorem Std.Iterators.IterM.drain_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [IteratorLoop α m m] {it : IterM m β} : it.drain = fold (fun (x : PUnit) (x : β) => PUnit.unit) PUnit.unit it

theorem Std.Iterators.IterM.drain_eq_foldM {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] {it : IterM m β} : it.drain = foldM (fun (x : PUnit) (x : β) => pure PUnit.unit) PUnit.unit it

theorem Std.Iterators.IterM.drain_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [IteratorLoop α m m] {it : IterM m β} : it.drain = forIn it PUnit.unit fun (x : β) (x : PUnit) => pure (ForInStep.yield PUnit.unit)

theorem Std.Iterators.IterM.drain_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} : it.drain = do let __do_lift ← it.step match __do_lift with | ⟨IterStep.yield it' out, property⟩ => it'.drain | ⟨IterStep.skip it', property⟩ => it'.drain | ⟨IterStep.done, property⟩ => pure PUnit.unit

theorem Std.Iterators.IterM.drain_eq_map_toList {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] [IteratorCollect α m m] [LawfulIteratorCollect α m m] {it : IterM m β} : it.drain = (fun (x : List β) => PUnit.unit) <$> it.toList

theorem Std.Iterators.IterM.drain_eq_map_toListRev {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] [IteratorCollect α m m] [LawfulIteratorCollect α m m] {it : IterM m β} : it.drain = (fun (x : List β) => PUnit.unit) <$> it.toListRev

theorem Std.Iterators.IterM.drain_eq_map_toArray {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] [IteratorCollect α m m] [LawfulIteratorCollect α m m] {it : IterM m β} : it.drain = (fun (x : List β) => PUnit.unit) <$> it.toList