theorem Std.IterM.DefaultConsumers.forIn_eq {γ : Type x} {α β : Type w} {m : Type w → Type w'} {n : Type x → Type x'} [Monad n] [Iterator α m β] {lift : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ} {plausible_forInStep : β → γ → ForInStep γ → Prop} {it : IterM m β} {init : γ} {f : (b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (plausible_forInStep b c))} : IteratorLoop.forIn lift γ plausible_forInStep it init f = forIn' lift γ plausible_forInStep it init it.IsPlausibleIndirectOutput ⋯ f

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

theorem Std.IterM.DefaultConsumers.forIn'_eq_wf {m : Type w → Type w'} {α β : Type w} [Iterator α m β] {n : Type x → Type x'} [Monad n] [LawfulMonad n] {lift : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ} {γ : Type x} (Pl : β → γ → ForInStep γ → Prop) (wf : IteratorLoop.WellFounded α m Pl) {it : IterM m β} {init : γ} {P : β → Prop} {hP : ∀ (b : β), it.IsPlausibleIndirectOutput b → P b} (f : (b : β) → P b → (c : γ) → n (Subtype (Pl b c))) : forIn' lift γ Pl it init P hP f = forIn'.wf lift γ Pl wf it init P hP f

theorem Std.IterM.DefaultConsumers.forIn'_eq_wf_of_finite {m : Type w → Type w'} {α β : Type w} [Iterator α m β] [Iterators.Finite α m] {n : Type x → Type x'} [Monad n] [LawfulMonad n] {lift : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ} {γ : Type x} {it : IterM m β} {init : γ} {P : β → Prop} {hP : ∀ (b : β), it.IsPlausibleIndirectOutput b → P b} (f : (b : β) → P b → γ → n { x : ForInStep γ // True }) : forIn' lift γ (fun (x : β) (x_1 : γ) (x_2 : ForInStep γ) => True) it init P hP f = forIn'.wf lift γ (fun (x : β) (x_1 : γ) (x_2 : ForInStep γ) => True) ⋯ it init P hP f

theorem Std.IterM.forIn'_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] [hl : LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {γ : Type w} {it : IterM m β} {init : γ} {f : (b : β) → it.IsPlausibleIndirectOutput b → γ → n (ForInStep γ)} : forIn' it init f = DefaultConsumers.forIn' (fun (x x_1 : Type w) (f : x → n x_1) (x_2 : m x) => monadLift x_2 >>= f) γ (fun (x : β) (x_1 : γ) (x_2 : ForInStep γ) => True) it init it.IsPlausibleIndirectOutput ⋯ fun (x1 : β) (x2 : it.IsPlausibleIndirectOutput x1) (x3 : γ) => do let __do_lift ← f x1 x2 x3 pure ⟨__do_lift, trivial⟩

theorem Std.IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] [hl : LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {γ : Type w} {it : IterM m β} {init : γ} {f : β → γ → n (ForInStep γ)} : forIn it init f = DefaultConsumers.forIn' (fun (x x_1 : Type w) (f : x → n x_1) (x_2 : m x) => monadLift x_2 >>= f) γ (fun (x : β) (x_1 : γ) (x_2 : ForInStep γ) => True) it init it.IsPlausibleIndirectOutput ⋯ fun (out : β) (x : it.IsPlausibleIndirectOutput out) (acc : γ) => do let __do_lift ← f out acc pure ⟨__do_lift, trivial⟩

theorem Std.IterM.forIn'_congr {γ α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Monad m] [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] {ita itb : IterM m β} (w : ita = itb) {b b' : γ} (hb : b = b') {f : (a' : β) → a' ∈ ita → γ → n (ForInStep γ)} {g : (a' : β) → a' ∈ itb → γ → n (ForInStep γ)} (h : ∀ (a : β) (m_1 : a ∈ itb) (b : γ), f a ⋯ b = g a m_1 b) : forIn' ita b f = forIn' itb b' g

theorem Std.IterM.forIn_congr {γ α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Monad m] [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] {ita itb : IterM m β} (w : ita = itb) {b b' : γ} (hb : b = b') {f g : β → γ → n (ForInStep γ)} (h : ∀ (a : β) (b : γ), f a b = g a b) : forIn ita b f = forIn itb b' g

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

theorem Std.IterM.forIn'_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT 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.inflate 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.IterM.forIn_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT 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.inflate 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.IterM.forIn_toList {m : Type w → Type u_1} {γ α β : Type w} [Monad m] [LawfulMonad m] [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] {it : IterM Id β} {f : β → γ → m (ForInStep γ)} {init : γ} : forIn it.toList.run init f = forIn it init f

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

theorem Std.IterM.forM_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] {n : Type w → Type w''} [Monad m] [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.IterM.forM_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {it : IterM m β} {f : β → n PUnit} : forM it f = do let __do_lift ← liftM it.step match __do_lift.inflate 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.IterM.foldM_eq_forIn {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.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.IterM.forIn_yield_eq_foldM {α β γ δ : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] {n : Type w → Type w''} [Monad m] [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.IterM.foldM_eq_match_step {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : γ → β → n γ} {init : γ} {it : IterM m β} : foldM f init it = do let __do_lift ← liftM it.step match __do_lift.inflate 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.IterM.fold_eq_forIn {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.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.IterM.fold_eq_foldM {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.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.IterM.forIn_pure_yield_eq_fold {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.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.IterM.fold_eq_match_step {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.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.inflate 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.IterM.fold_hom {α β γ₁ γ₂ : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} (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.IterM.toList_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} : it.toList = fold (fun (l : List β) (out : β) => l ++ [out]) [] it

theorem Std.IterM.toArray_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} : it.toArray = fold (fun (xs : Array β) (out : β) => xs.push out) #[] it

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

theorem Std.IterM.foldlM_toArray {m : Type w → Type u_1} {γ α β : Type w} [Monad m] [LawfulMonad m] [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] {it : IterM Id β} {f : γ → β → m γ} {init : γ} : Array.foldlM f init it.toArray.run = foldM f init it

theorem Std.IterM.foldl_toList {m : Type w → Type u_1} {γ α β : Type w} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {f : γ → β → γ} {init : γ} : (fun (x : List β) => List.foldl f init x) <$> it.toList = fold f init it

theorem Std.IterM.foldl_toArray {m : Type w → Type u_1} {γ α β : Type w} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {f : γ → β → γ} {init : γ} : (fun (x : Array β) => Array.foldl f init x) <$> it.toArray = fold f init it

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

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

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

theorem Std.IterM.drain_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.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.inflate with | ⟨IterStep.yield it' out, property⟩ => it'.drain | ⟨IterStep.skip it', property⟩ => it'.drain | ⟨IterStep.done, property⟩ => pure PUnit.unit

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

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

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

theorem Std.IterM.length_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] {it : IterM m β} : it.length = fold (fun (acc : ULift Nat) (x : β) => { down := acc.down + 1 }) { down := 0 } it

@[deprecated Std.IterM.length_eq_fold (since := "2026-01-28")]

def Std.IterM.count_eq_fold {α β : Type u_1} {m : Type u_1 → Type u_2} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] {it : IterM m β} : it.length = fold (fun (acc : ULift Nat) (x : β) => { down := acc.down + 1 }) { down := 0 } it

Equations

• @Std.IterM.count_eq_fold = @Std.IterM.length_eq_fold

theorem Std.IterM.length_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] {it : IterM m β} : it.length = forIn it { down := 0 } fun (x : β) (acc : ULift Nat) => pure (ForInStep.yield { down := acc.down + 1 })

@[deprecated Std.IterM.length_eq_forIn (since := "2026-01-28")]

def Std.IterM.count_eq_forIn {α β : Type u_1} {m : Type u_1 → Type u_2} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] {it : IterM m β} : it.length = forIn it { down := 0 } fun (x : β) (acc : ULift Nat) => pure (ForInStep.yield { down := acc.down + 1 })

Equations

• @Std.IterM.count_eq_forIn = @Std.IterM.length_eq_forIn

theorem Std.IterM.length_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} : it.length = do let __do_lift ← it.step match __do_lift.inflate.val with | IterStep.yield it' out => do let __do_lift ← it'.length pure { down := __do_lift.down + 1 } | IterStep.skip it' => do let __do_lift ← it'.length pure { down := __do_lift.down } | IterStep.done => pure { down := 0 }

@[deprecated Std.IterM.length_eq_match_step (since := "2026-01-28")]

def Std.IterM.count_eq_match_step {α β : Type u_1} {m : Type u_1 → Type u_2} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} : it.length = do let __do_lift ← it.step match __do_lift.inflate.val with | IterStep.yield it' out => do let __do_lift ← it'.length pure { down := __do_lift.down + 1 } | IterStep.skip it' => do let __do_lift ← it'.length pure { down := __do_lift.down } | IterStep.done => pure { down := 0 }

Equations

• @Std.IterM.count_eq_match_step = @Std.IterM.length_eq_match_step

@[simp]

theorem Std.IterM.up_size_toArray_eq_length {m : Type w → Type u_1} {α β : Type w} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} : (fun (x : Array β) => { down := x.size }) <$> it.toArray = it.length

@[deprecated Std.IterM.up_size_toArray_eq_length (since := "2026-01-28")]

def Std.IterM.up_size_toArray_eq_count {m : Type u_1 → Type u_2} {α β : Type u_1} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} : (fun (x : Array β) => { down := x.size }) <$> it.toArray = it.length

Equations

• @Std.IterM.up_size_toArray_eq_count = @Std.IterM.up_size_toArray_eq_length

@[simp]

theorem Std.IterM.up_length_toList_eq_length {m : Type w → Type u_1} {α β : Type w} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} : (fun (x : List β) => { down := x.length }) <$> it.toList = it.length

@[deprecated Std.IterM.up_length_toList_eq_length (since := "2026-01-28")]

def Std.IterM.up_length_toList_eq_count {m : Type u_1 → Type u_2} {α β : Type u_1} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} : (fun (x : List β) => { down := x.length }) <$> it.toList = it.length

Equations

• @Std.IterM.up_length_toList_eq_count = @Std.IterM.up_length_toList_eq_length

@[simp]

theorem Std.IterM.up_length_toListRev_eq_length {m : Type w → Type u_1} {α β : Type w} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} : (fun (x : List β) => { down := x.length }) <$> it.toListRev = it.length

@[deprecated Std.IterM.up_length_toListRev_eq_length (since := "2026-01-28")]

def Std.IterM.up_length_toListRev_eq_count {m : Type u_1 → Type u_2} {α β : Type u_1} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} : (fun (x : List β) => { down := x.length }) <$> it.toListRev = it.length

Equations

• @Std.IterM.up_length_toListRev_eq_count = @Std.IterM.up_length_toListRev_eq_length

theorem Std.IterM.anyM_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → m (ULift Bool)} : anyM p it = forIn it { down := false } fun (x : β) (x_1 : ULift Bool) => do let __do_lift ← p x if __do_lift.down = true then pure (ForInStep.done { down := true }) else pure (ForInStep.yield { down := false })

theorem Std.IterM.anyM_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → m (ULift Bool)} : anyM p it = do let __do_lift ← it.step match __do_lift.inflate.val with | IterStep.yield it' x => do let __do_lift ← p x if __do_lift.down = true then pure { down := true } else anyM p it' | IterStep.skip it' => anyM p it' | IterStep.done => pure { down := false }

theorem Std.IterM.any_eq_anyM {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → Bool} : any p it = anyM (fun (x : β) => pure { down := p x }) it

theorem Std.IterM.anyM_pure {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → ULift Bool} : anyM (fun (x : β) => pure (p x)) it = any (fun (x : β) => (p x).down) it

theorem Std.IterM.any_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → Bool} : any p it = do let __do_lift ← it.step match __do_lift.inflate.val with | IterStep.yield it' x => if p x = true then pure { down := true } else any p it' | IterStep.skip it' => any p it' | IterStep.done => pure { down := false }

theorem Std.IterM.any_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → Bool} : any p it = forIn it { down := false } fun (x : β) (x_1 : ULift Bool) => if p x = true then pure (ForInStep.done { down := true }) else pure (ForInStep.yield { down := false })

theorem Std.IterM.allM_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → m (ULift Bool)} : allM p it = forIn it { down := true } fun (x : β) (x_1 : ULift Bool) => do let __do_lift ← p x if __do_lift.down = true then pure (ForInStep.yield { down := true }) else pure (ForInStep.done { down := false })

theorem Std.IterM.allM_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → m (ULift Bool)} : allM p it = do let __do_lift ← it.step match __do_lift.inflate.val with | IterStep.yield it' x => do let __do_lift ← p x if __do_lift.down = true then allM p it' else pure { down := false } | IterStep.skip it' => allM p it' | IterStep.done => pure { down := true }

theorem Std.IterM.all_eq_allM {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → Bool} : all p it = allM (fun (x : β) => pure { down := p x }) it

theorem Std.IterM.allM_pure {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → ULift Bool} : allM (fun (x : β) => pure (p x)) it = all (fun (x : β) => (p x).down) it

theorem Std.IterM.all_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → Bool} : all p it = do let __do_lift ← it.step match __do_lift.inflate.val with | IterStep.yield it' x => if p x = true then all p it' else pure { down := false } | IterStep.skip it' => all p it' | IterStep.done => pure { down := true }

theorem Std.IterM.all_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → Bool} : all p it = forIn it { down := true } fun (x : β) (x_1 : ULift Bool) => if p x = true then pure (ForInStep.yield { down := true }) else pure (ForInStep.done { down := false })

theorem Std.IterM.allM_eq_not_anyM_not {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → m (ULift Bool)} : allM p it = (fun (x : ULift Bool) => { down := !x.down }) <$> anyM (fun (x : β) => (fun (x : ULift Bool) => { down := !x.down }) <$> p x) it

theorem Std.IterM.all_eq_not_any_not {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → Bool} : all p it = (fun (x : ULift Bool) => { down := !x.down }) <$> any (fun (x : β) => !p x) it

theorem Std.IterM.findSomeM?_eq_match_step {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] [LawfulMonad m] [Iterators.Finite α m] [LawfulIteratorLoop α m m] {it : IterM m β} {f : β → m (Option γ)} : it.findSomeM? f = do let __do_lift ← it.step match __do_lift.inflate.val with | IterStep.yield it' out => do let __do_lift ← f out match __do_lift with | none => it'.findSomeM? f | some fx => pure (some fx) | IterStep.skip it' => it'.findSomeM? f | IterStep.done => pure none

theorem Std.IterM.findSome?_eq_findSomeM? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] {it : IterM m β} {f : β → Option γ} : it.findSome? f = it.findSomeM? fun (x : β) => pure (f x)

theorem Std.IterM.findSome?_eq_match_step {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] [LawfulMonad m] [Iterators.Finite α m] [LawfulIteratorLoop α m m] {it : IterM m β} {f : β → Option γ} : it.findSome? f = do let __do_lift ← it.step match __do_lift.inflate.val with | IterStep.yield it' out => match f out with | none => it'.findSome? f | some fx => pure (some fx) | IterStep.skip it' => it'.findSome? f | IterStep.done => pure none

theorem Std.IterM.findSomeM?_pure {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] [LawfulMonad m] [Iterators.Finite α m] [LawfulIteratorLoop α m m] {it : IterM m β} {f : β → Option γ} : (it.findSomeM? fun (x : β) => pure (f x)) = it.findSome? f

theorem Std.IterM.findM?_eq_findSomeM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] [Iterators.Finite α m] {it : IterM m β} {f : β → m (ULift Bool)} : it.findM? f = it.findSomeM? fun (x : β) => do let __do_lift ← f x pure (if __do_lift.down = true then some x else none)

theorem Std.IterM.findM?_eq_match_step {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] [LawfulMonad m] [Iterators.Finite α m] [LawfulIteratorLoop α m m] {it : IterM m β} {f : β → m (ULift Bool)} : it.findM? f = do let __do_lift ← it.step match __do_lift.inflate.val with | IterStep.yield it' out => do let __do_lift ← f out if __do_lift.down = true then pure (some out) else it'.findM? f | IterStep.skip it' => it'.findM? f | IterStep.done => pure none

theorem Std.IterM.find?_eq_findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] [Iterators.Finite α m] {it : IterM m β} {f : β → Bool} : it.find? f = it.findM? fun (x : β) => pure { down := f x }

theorem Std.IterM.find?_eq_findSome? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] [LawfulMonad m] [Iterators.Finite α m] {it : IterM m β} {f : β → Bool} : it.find? f = it.findSome? fun (x : β) => if f x = true then some x else none

theorem Std.IterM.find?_eq_match_step {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] [LawfulMonad m] [Iterators.Finite α m] [LawfulIteratorLoop α m m] {it : IterM m β} {f : β → Bool} : it.find? f = do let __do_lift ← it.step match __do_lift.inflate.val with | IterStep.yield it' out => if f out = true then pure (some out) else it'.find? f | IterStep.skip it' => it'.find? f | IterStep.done => pure none

theorem Std.IterM.findM?_pure {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] [LawfulMonad m] [Iterators.Finite α m] [LawfulIteratorLoop α m m] {it : IterM m β} {f : β → ULift Bool} : (it.findM? fun (x : β) => pure (f x)) = it.find? fun (x : β) => (f x).down

theorem Std.IterM.first?_eq_match_step {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] [LawfulMonad m] [Iterators.Productive α m] [LawfulIteratorLoop α m m] {it : IterM m β} : it.first? = do let __do_lift ← it.step match __do_lift.inflate.val with | IterStep.yield it out => pure (some out) | IterStep.skip it' => it'.first? | IterStep.done => pure none

theorem Std.IterM.isEmpty_eq_match_step {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] [LawfulMonad m] [Iterators.Productive α m] [LawfulIteratorLoop α m m] {it : IterM m β} : it.isEmpty = do let __do_lift ← it.step match __do_lift.inflate.val with | IterStep.yield it out => pure { down := false } | IterStep.skip it' => it'.isEmpty | IterStep.done => pure { down := true }