theorem Std.Iter.forIn'_eq {α β : Type w} [Iterator α Id β] [Iterators.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_1 : γ) (x_2 : ForInStep γ) => True) it.toIterM init it.toIterM.IsPlausibleIndirectOutput ⋯ fun (out : β) (h : it.toIterM.IsPlausibleIndirectOutput out) (acc : γ) => do let __do_lift ← f out ⋯ acc pure ⟨__do_lift, trivial⟩

theorem Std.Iter.forIn_eq {α β : Type w} [Iterator α Id β] [Iterators.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_1 : γ) (x_2 : ForInStep γ) => True) it.toIterM init it.toIterM.IsPlausibleIndirectOutput ⋯ fun (out : β) (x : it.toIterM.IsPlausibleIndirectOutput out) (acc : γ) => do let __do_lift ← f out acc pure ⟨__do_lift, trivial⟩

theorem Std.Iter.forIn'_congr {γ α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id m] {ita itb : Iter β} (w : ita = itb) {b b' : γ} (hb : b = b') {f : (a' : β) → a' ∈ ita → γ → m (ForInStep γ)} {g : (a' : β) → a' ∈ itb → γ → m (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.Iter.forIn_congr {γ α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id m] {ita itb : Iter β} (w : ita = itb) {b b' : γ} (hb : b = b') {f g : β → γ → m (ForInStep γ)} (h : ∀ (a : β) (b : γ), f a b = g a b) : forIn ita b f = forIn itb b' g

theorem Std.Iter.forIn'_eq_forIn'_toIterM {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] [IteratorLoop α 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.Iter.forIn_eq_forIn_toIterM {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] {γ : Type w} {it : Iter β} {init : γ} {f : β → γ → m (ForInStep γ)} : forIn it init f = forIn it.toIterM init f

theorem Std.Iter.forIn'_eq_match_step {α β : Type w} [Iterator α Id β] [Iterators.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.Iter.forIn_eq_match_step {α β : Type w} [Iterator α Id β] [Iterators.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.Iter.isPlausibleStep_iff_step_eq {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] [LawfulDeterministicIterator α Id] {it : Iter β} {step : IterStep (Iter β) β} : it.IsPlausibleStep step ↔ it.step.val = step

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

theorem Std.Iter.mem_toArray_iff_isPlausibleIndirectOutput {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] [LawfulDeterministicIterator α Id] {it : Iter β} {out : β} : out ∈ it.toArray ↔ it.IsPlausibleIndirectOutput out

theorem Std.Iter.forIn'_toList {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] [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.Iter.forIn'_toArray {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] [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.Iter.forIn'_eq_forIn'_toList {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] [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.Iter.forIn'_eq_forIn'_toArray {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] [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.Iter.forIn_toList {α β : Type w} [Iterator α Id β] [Iterators.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.toList init f = forIn it init f

theorem Std.Iter.forIn_toArray {α β : Type w} [Iterator α Id β] [Iterators.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.toArray init f = forIn it init f

theorem Std.Iter.foldM_eq_forIn {α β : Type w} {γ : Type x} [Iterator α Id β] [Iterators.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.Iter.foldM_eq_foldM_toIterM {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] {γ : Type w} {it : Iter β} {init : γ} {f : γ → β → m γ} : foldM f init it = IterM.foldM f init it.toIterM

theorem Std.Iter.forIn_yield_eq_foldM {α β : Type w} {γ δ : Type x} [Iterator α Id β] [Iterators.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.Iter.foldM_eq_match_step {α β : Type w} {γ : Type x} [Iterator α Id β] [Iterators.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.Iter.foldlM_toList {α β : Type w} {γ : Type x} [Iterator α Id β] [Iterators.Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] {f : γ → β → m γ} {init : γ} {it : Iter β} : List.foldlM f init it.toList = foldM f init it

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

theorem Std.IterM.forIn_eq_foldM {α β : Type w} [Iterator α Id β] [Iterators.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 = 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.Iter.fold_eq_forIn {α β : Type w} {γ : Type x} [Iterator α Id β] [Iterators.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.Iter.fold_eq_foldM {α β : Type w} {γ : Type x} [Iterator α Id β] [Iterators.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.Iter.fold_eq_fold_toIterM {α β γ : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] {f : γ → β → γ} {init : γ} {it : Iter β} : fold f init it = (IterM.fold f init it.toIterM).run

@[simp]

theorem Std.Iter.forIn_pure_yield_eq_fold {α β : Type w} {γ : Type x} [Iterator α Id β] [Iterators.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.Iter.fold_eq_match_step {α β : Type w} {γ : Type x} [Iterator α Id β] [Iterators.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.Iter.fold_hom {α β : Type u_1} {γ₁ : Type x₁} {γ₂ : Type x₂} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id 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.Iter.toList_eq_fold {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} : it.toList = fold (fun (l : List β) (out : β) => l ++ [out]) [] it

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

@[simp]

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

@[simp]

theorem Std.Iter.foldl_toArray {α β : Type w} {γ : Type x} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {f : γ → β → γ} {init : γ} {it : Iter β} : Array.foldl f init it.toArray = fold f init it

theorem Std.Iter.length_eq_length_toIterM {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] {it : Iter β} : it.length = it.toIterM.length.run.down

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

def Std.Iter.count_eq_count_toIterM {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] {it : Iter β} : it.length = it.toIterM.length.run.down

Equations

• @Std.Iter.count_eq_count_toIterM = @Std.Iter.length_eq_length_toIterM

theorem Std.Iter.length_eq_fold {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} : it.length = fold (fun (acc : Nat) (x : β) => acc + 1) 0 it

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

def Std.Iter.count_eq_fold {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} : it.length = fold (fun (acc : Nat) (x : β) => acc + 1) 0 it

Equations

• @Std.Iter.count_eq_fold = @Std.Iter.length_eq_fold

theorem Std.Iter.length_eq_forIn {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} : it.length = (forIn it 0 fun (x : β) (acc : Nat) => pure (ForInStep.yield (acc + 1))).run

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

def Std.Iter.count_eq_forIn {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} : it.length = (forIn it 0 fun (x : β) (acc : Nat) => pure (ForInStep.yield (acc + 1))).run

Equations

• @Std.Iter.count_eq_forIn = @Std.Iter.length_eq_forIn

theorem Std.Iter.length_eq_match_step {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} : it.length = match it.step.val with | IterStep.yield it' out => it'.length + 1 | IterStep.skip it' => it'.length | IterStep.done => 0

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

def Std.Iter.count_eq_match_step {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} : it.length = match it.step.val with | IterStep.yield it' out => it'.length + 1 | IterStep.skip it' => it'.length | IterStep.done => 0

Equations

• @Std.Iter.count_eq_match_step = @Std.Iter.length_eq_match_step

@[simp]

theorem Std.Iter.size_toArray_eq_length {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} : it.toArray.size = it.length

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

def Std.Iter.size_toArray_eq_count {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} : it.toArray.size = it.length

Equations

• @Std.Iter.size_toArray_eq_count = @Std.Iter.size_toArray_eq_length

@[simp]

theorem Std.Iter.length_toList_eq_length {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} : it.toList.length = it.length

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

def Std.Iter.length_toList_eq_count {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} : it.toList.length = it.length

Equations

• @Std.Iter.length_toList_eq_count = @Std.Iter.length_toList_eq_length

@[simp]

theorem Std.Iter.length_toListRev_eq_length {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} : it.toListRev.length = it.length

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

def Std.Iter.length_toListRev_eq_count {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} : it.toListRev.length = it.length

Equations

• @Std.Iter.length_toListRev_eq_count = @Std.Iter.length_toListRev_eq_length

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

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

theorem Std.Iter.anyM_toList {α β : Type w} {m : Type → Type w'} [Iterator α Id β] [Iterators.Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] {it : Iter β} {p : β → m Bool} : List.anyM p it.toList = anyM p it

theorem Std.Iter.anyM_toArray {α β : Type w} {m : Type → Type w'} [Iterator α Id β] [Iterators.Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] {it : Iter β} {p : β → m Bool} : Array.anyM p it.toArray = anyM p it

theorem Std.Iter.any_eq_anyM {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} {p : β → Bool} : any p it = (anyM (fun (x : β) => pure (p x)) it).run

theorem Std.Iter.anyM_pure {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} {p : β → Bool} : anyM (fun (x : β) => pure (p x)) it = pure (any (fun (x : β) => p x) it)

theorem Std.Iter.any_eq_match_step {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} {p : β → Bool} : any p it = match it.step.val with | IterStep.yield it' x => if p x = true then true else any p it' | IterStep.skip it' => any p it' | IterStep.done => false

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

theorem Std.Iter.any_toList {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} {p : β → Bool} : it.toList.any p = any p it

theorem Std.Iter.any_toArray {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} {p : β → Bool} : it.toArray.any p = any p it

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

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

theorem Std.Iter.all_eq_allM {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} {p : β → Bool} : all p it = (allM (fun (x : β) => pure (p x)) it).run

theorem Std.Iter.allM_pure {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} {p : β → Bool} : allM (fun (x : β) => pure (p x)) it = pure (all (fun (x : β) => p x) it)

theorem Std.Iter.all_eq_match_step {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} {p : β → Bool} : all p it = match it.step.val with | IterStep.yield it' x => if p x = true then all p it' else false | IterStep.skip it' => all p it' | IterStep.done => true

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

theorem Std.Iter.all_toList {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} {p : β → Bool} : it.toList.all p = all p it

theorem Std.Iter.all_toArray {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} {p : β → Bool} : it.toArray.all p = all p it

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

theorem Std.Iter.all_eq_not_any_not {m : Type u_1 → Type u_2} {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} {p : β → Bool} : all p it = !any (fun (x : β) => !p x) it

theorem Std.Iter.findSomeM?_eq_match_step {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Monad m] [Iterator α Id β] [IteratorLoop α Id m] [LawfulMonad m] [Iterators.Finite α Id] [LawfulIteratorLoop α Id m] {it : Iter β} {f : β → m (Option γ)} : it.findSomeM? f = match it.step.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.Iter.findSomeM?_toList {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Monad m] [Iterator α Id β] [IteratorLoop α Id m] [LawfulMonad m] [Iterators.Finite α Id] [LawfulIteratorLoop α Id m] {it : Iter β} {f : β → m (Option γ)} : List.findSomeM? f it.toList = it.findSomeM? f

theorem Std.Iter.findSome?_eq_findSomeM? {α β : Type w} {γ : Type x} [Iterator α Id β] [IteratorLoop α Id Id] [Iterators.Finite α Id] {it : Iter β} {f : β → Option γ} : it.findSome? f = (it.findSomeM? fun (x : β) => pure (f x)).run

theorem Std.Iter.findSome?_eq_findSome?_toIterM {α β γ : Type w} [Iterator α Id β] [IteratorLoop α Id Id] [Iterators.Finite α Id] {it : Iter β} {f : β → Option γ} : it.findSome? f = (it.toIterM.findSome? f).run

theorem Std.Iter.findSome?_eq_match_step {α β : Type w} {γ : Type x} [Iterator α Id β] [IteratorLoop α Id Id] [Iterators.Finite α Id] [LawfulIteratorLoop α Id Id] {it : Iter β} {f : β → Option γ} : it.findSome? f = match it.step.val with | IterStep.yield it' out => match f out with | none => it'.findSome? f | some fx => some fx | IterStep.skip it' => it'.findSome? f | IterStep.done => none

theorem Std.Iter.findSome?_toList {α β : Type w} {γ : Type x} [Iterator α Id β] [IteratorLoop α Id Id] [Iterators.Finite α Id] [LawfulIteratorLoop α Id Id] {it : Iter β} {f : β → Option γ} : List.findSome? f it.toList = it.findSome? f

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

theorem Std.Iter.findM?_eq_findSomeM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β] [IteratorLoop α Id m] [Iterators.Finite α Id] {it : Iter β} {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.Iter.findM?_eq_match_step {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β] [IteratorLoop α Id m] [LawfulMonad m] [Iterators.Finite α Id] [LawfulIteratorLoop α Id m] {it : Iter β} {f : β → m (ULift Bool)} : it.findM? f = match it.step.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.Iter.findM?_toList {α β : Type} {m : Type → Type w'} [Monad m] [Iterator α Id β] [IteratorLoop α Id m] [LawfulMonad m] [Iterators.Finite α Id] [LawfulIteratorLoop α Id m] {it : Iter β} {f : β → m Bool} : List.findM? f it.toList = it.findM? fun (x : β) => ULift.up <$> f x

theorem Std.Iter.findM?_eq_findM?_toList {α β : Type} {m : Type → Type w'} [Monad m] [Iterator α Id β] [IteratorLoop α Id m] [LawfulMonad m] [Iterators.Finite α Id] [LawfulIteratorLoop α Id m] {it : Iter β} {f : β → m (ULift Bool)} : it.findM? f = List.findM? (fun (x : β) => ULift.down <$> f x) it.toList

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

theorem Std.Iter.find?_eq_find?_toIterM {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id] [Iterators.Finite α Id] {it : Iter β} {f : β → Bool} : it.find? f = (it.toIterM.find? f).run

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

theorem Std.Iter.find?_eq_match_step {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id] [Iterators.Finite α Id] [LawfulIteratorLoop α Id Id] {it : Iter β} {f : β → Bool} : it.find? f = match it.step.val with | IterStep.yield it' out => if f out = true then some out else it'.find? f | IterStep.skip it' => it'.find? f | IterStep.done => none

theorem Std.Iter.find?_toList {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id] [Iterators.Finite α Id] [LawfulIteratorLoop α Id Id] {it : Iter β} {f : β → Bool} : List.find? f it.toList = it.find? f

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

theorem Std.Iter.first?_eq_first?_toIterM {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id] {it : Iter β} : it.first? = it.toIterM.first?.run

theorem Std.Iter.first?_eq_match_step {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id] [Iterators.Productive α Id] [LawfulIteratorLoop α Id Id] {it : Iter β} : it.first? = match it.step.val with | IterStep.yield it out => some out | IterStep.skip it' => it'.first? | IterStep.done => none

@[simp]

theorem Std.Iter.head?_toList {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id] [Iterators.Finite α Id] [LawfulIteratorLoop α Id Id] {it : Iter β} : it.toList.head? = it.first?

theorem Std.Iter.isEmpty_eq_isEmpty_toIterM {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id] {it : Iter β} : it.isEmpty = it.toIterM.isEmpty.run.down

theorem Std.Iter.isEmpty_eq_match_step {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id] [Iterators.Productive α Id] [LawfulIteratorLoop α Id Id] {it : Iter β} : it.isEmpty = match it.step.val with | IterStep.yield it out => false | IterStep.skip it' => it'.isEmpty | IterStep.done => true

@[simp]

theorem Std.Iter.isEmpty_toList {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id] [Iterators.Finite α Id] [LawfulIteratorLoop α Id Id] {it : Iter β} : it.toList.isEmpty = it.isEmpty