Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Mario Carneiro
-/
import Std.Control.ForInStep.Basic

/-! # Additional theorems on `ForInStep` -/

@[simp] theorem ForInStep.bind_done: ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (a : α) (f : α → m (ForInStep α)),
ForInStep.bind (done a) f = pure (done a)ForInStep.bind_done [Monad: (Type ?u.18 → Type ?u.17) → Type (max(?u.18+1)?u.17)Monad m: ?m.5m] (a: αa : α: ?m.14α) (f: α → m (ForInStep α)f : α: ?m.14α → m: ?m.5m (ForInStep: Type ?u.26 → Type ?u.26ForInStep α: ?m.14α)) :
(ForInStep.done: {α : Type ?u.30} → α → ForInStep αForInStep.done a: αa).bind: {m : Type ?u.33 → Type ?u.32} →
{α : Type ?u.33} → [inst : Monad m] → ForInStep α → (α → m (ForInStep α)) → m (ForInStep α)bind (m := m: ?m.5m) f: α → m (ForInStep α)f = pure: {f : Type ?u.55 → Type ?u.54} → [self : Pure f] → {α : Type ?u.55} → α → f αpure (.done: {α : Type ?u.96} → α → ForInStep α.done a: αa) := rfl: ∀ {α : Sort ?u.130} {a : α}, a = arfl
@[simp] theorem ForInStep.bind_yield: ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (a : α) (f : α → m (ForInStep α)),
ForInStep.bind (yield a) f = f aForInStep.bind_yield [Monad: (Type ?u.179 → Type ?u.178) → Type (max(?u.179+1)?u.178)Monad m: ?m.175m] (a: αa : α: ?m.184α) (f: α → m (ForInStep α)f : α: ?m.184α → m: ?m.175m (ForInStep: Type ?u.196 → Type ?u.196ForInStep α: ?m.184α)) :
(ForInStep.yield: {α : Type ?u.200} → α → ForInStep αForInStep.yield a: αa).bind: {m : Type ?u.203 → Type ?u.202} →
{α : Type ?u.203} → [inst : Monad m] → ForInStep α → (α → m (ForInStep α)) → m (ForInStep α)bind (m := m: ?m.175m) f: α → m (ForInStep α)f = f: α → m (ForInStep α)f a: αa := rfl: ∀ {α : Sort ?u.231} {a : α}, a = arfl

attribute [simp] ForInStep.bindM: {m : Type u_1 → Type u_2} →
{α : Type u_1} → [inst : Monad m] → m (ForInStep α) → (α → m (ForInStep α)) → m (ForInStep α)ForInStep.bindM

@[simp] theorem ForInStep.run_done: ∀ {α : Type u_1} {a : α}, run (done a) = aForInStep.run_done : (ForInStep.done: {α : Type ?u.288} → α → ForInStep αForInStep.done a: ?m.284a).run: {α : Type ?u.290} → ForInStep α → αrun = a: ?m.284a := rfl: ∀ {α : Sort ?u.302} {a : α}, a = arfl
@[simp] theorem ForInStep.run_yield: ∀ {α : Type u_1} {a : α}, run (yield a) = aForInStep.run_yield : (ForInStep.yield: {α : Type ?u.336} → α → ForInStep αForInStep.yield a: ?m.332a).run: {α : Type ?u.338} → ForInStep α → αrun = a: ?m.332a := rfl: ∀ {α : Sort ?u.350} {a : α}, a = arfl

@[simp] theorem ForInStep.bindList_nil: ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → β → m (ForInStep β))
(s : ForInStep β), bindList f [] s = pure sForInStep.bindList_nil [Monad: (Type ?u.393 → Type ?u.392) → Type (max(?u.393+1)?u.392)Monad m: ?m.379m] (f: α → β → m (ForInStep β)f : α: ?m.389α → β: ?m.401β → m: ?m.379m (ForInStep: Type ?u.413 → Type ?u.413ForInStep β: ?m.401β))
(s: ForInStep βs : ForInStep: Type ?u.416 → Type ?u.416ForInStep β: ?m.401β) : s: ForInStep βs.bindList: {m : Type ?u.422 → Type ?u.421} →
{α : Type ?u.420} →
{β : Type ?u.422} → [inst : Monad m] → (α → β → m (ForInStep β)) → List α → ForInStep β → m (ForInStep β)bindList f: α → β → m (ForInStep β)f []: List ?m.443[] = pure: {f : Type ?u.451 → Type ?u.450} → [self : Pure f] → {α : Type ?u.451} → α → f αpure s: ForInStep βs := rfl: ∀ {α : Sort ?u.524} {a : α}, a = arfl

@[simp] theorem ForInStep.bindList_cons: ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → β → m (ForInStep β))
(s : ForInStep β) (a : α) (l : List α),
bindList f (a :: l) s =     ForInStep.bind s fun b => do
let x ← f a b
bindList f l xForInStep.bindList_cons [Monad: (Type ?u.603 → Type ?u.602) → Type (max(?u.603+1)?u.602)Monad m: ?m.577m]
(f: α → β → m (ForInStep β)f : α: ?m.587α → β: ?m.599β → m: ?m.577m (ForInStep: Type ?u.611 → Type ?u.611ForInStep β: ?m.599β)) (s: ForInStep βs : ForInStep: Type ?u.614 → Type ?u.614ForInStep β: ?m.599β) (a: αa l: List αl) :
s: ForInStep βs.bindList: {m : Type ?u.626 → Type ?u.625} →
{α : Type ?u.624} →
{β : Type ?u.626} → [inst : Monad m] → (α → β → m (ForInStep β)) → List α → ForInStep β → m (ForInStep β)bindList f: α → β → m (ForInStep β)f (a: ?m.617a::l: ?m.620l) = s: ForInStep βs.bind: {m : Type ?u.655 → Type ?u.654} →
{α : Type ?u.655} → [inst : Monad m] → ForInStep α → (α → m (ForInStep α)) → m (ForInStep α)bind fun b: ?m.665b => f: α → β → m (ForInStep β)f a: ?m.617a b: ?m.665b >>= (·.bindList: {m : Type ?u.708 → Type ?u.707} →
{α : Type ?u.706} →
{β : Type ?u.708} → [inst : Monad m] → (α → β → m (ForInStep β)) → List α → ForInStep β → m (ForInStep β)bindList f: α → β → m (ForInStep β)f l: ?m.620l) := rfl: ∀ {α : Sort ?u.775} {a : α}, a = arfl

@[simp] theorem ForInStep.done_bindList: ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → β → m (ForInStep β)) (a : β)
(l : List α), bindList f l (done a) = pure (done a)ForInStep.done_bindList [Monad: (Type ?u.875 → Type ?u.874) → Type (max(?u.875+1)?u.874)Monad m: ?m.849m]
(f: α → β → m (ForInStep β)f : α: ?m.859α → β: ?m.871β → m: ?m.849m (ForInStep: Type ?u.883 → Type ?u.883ForInStep β: ?m.871β)) (a: βa l: List αl) :
(ForInStep.done: {α : Type ?u.893} → α → ForInStep αForInStep.done a: ?m.886a).bindList: {m : Type ?u.897 → Type ?u.896} →
{α : Type ?u.895} →

@[simp] theorem ForInStep.bind_yield_bindList: ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → β → m (ForInStep β))
(s : ForInStep β) (l : List α), (ForInStep.bind s fun a => bindList f l (yield a)) = bindList f l sForInStep.bind_yield_bindList [Monad: (Type ?u.1433 → Type ?u.1432) → Type (max(?u.1433+1)?u.1432)Monad m: ?m.1419m]
(f: α → β → m (ForInStep β)f : α: ?m.1429α → β: ?m.1441β → m: ?m.1419m (ForInStep: Type ?u.1453 → Type ?u.1453ForInStep β: ?m.1441β)) (s: ForInStep βs : ForInStep: Type ?u.1456 → Type ?u.1456ForInStep β: ?m.1441β) (l: ?m.1459l) :
(s: ForInStep βs.bind: {m : Type ?u.1464 → Type ?u.1463} →
{α : Type ?u.1464} → [inst : Monad m] → ForInStep α → (α → m (ForInStep α)) → m (ForInStep α)bind fun a: ?m.1475a => (yield: {α : Type ?u.1477} → α → ForInStep αyield a: ?m.1475a).bindList: {m : Type ?u.1481 → Type ?u.1480} →
{α : Type ?u.1479} →
{β : Type ?u.1481} → [inst : Monad m] → (α → β → m (ForInStep β)) → List α → ForInStep β → m (ForInStep β)bindList f: α → β → m (ForInStep β)f l: ?m.1459l) = s: ForInStep βs.bindList: {m : Type ?u.1533 → Type ?u.1532} →
{α : Type ?u.1531} →
{β : Type ?u.1533} → [inst : Monad m] → (α → β → m (ForInStep β)) → List α → ForInStep β → m (ForInStep β)bindList f: α → β → m (ForInStep β)f l: ?m.1459l := byGoals accomplished! 🐙 m: Type u_1 → Type u_2α: Type u_3β: Type u_1inst✝: Monad mf: α → β → m (ForInStep β)s: ForInStep βl: List α(ForInStep.bind s fun a => bindList f l (yield a)) = bindList f l scases s: ForInStep βsm: Type u_1 → Type u_2α: Type u_3β: Type u_1inst✝: Monad mf: α → β → m (ForInStep β)l: List αa✝: βdone(ForInStep.bind (done a✝) fun a => bindList f l (yield a)) = bindList f l (done a✝)m: Type u_1 → Type u_2α: Type u_3β: Type u_1inst✝: Monad mf: α → β → m (ForInStep β)l: List αa✝: βyield(ForInStep.bind (yield a✝) fun a => bindList f l (yield a)) = bindList f l (yield a✝) m: Type u_1 → Type u_2α: Type u_3β: Type u_1inst✝: Monad mf: α → β → m (ForInStep β)s: ForInStep βl: List α(ForInStep.bind s fun a => bindList f l (yield a)) = bindList f l s<;>m: Type u_1 → Type u_2α: Type u_3β: Type u_1inst✝: Monad mf: α → β → m (ForInStep β)l: List αa✝: βdone(ForInStep.bind (done a✝) fun a => bindList f l (yield a)) = bindList f l (done a✝)m: Type u_1 → Type u_2α: Type u_3β: Type u_1inst✝: Monad mf: α → β → m (ForInStep β)l: List αa✝: βyield(ForInStep.bind (yield a✝) fun a => bindList f l (yield a)) = bindList f l (yield a✝) m: Type u_1 → Type u_2α: Type u_3β: Type u_1inst✝: Monad mf: α → β → m (ForInStep β)s: ForInStep βl: List α(ForInStep.bind s fun a => bindList f l (yield a)) = bindList f l ssimpGoals accomplished! 🐙

@[simp] theorem ForInStep.bind_bindList_assoc: ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] [inst_1 : LawfulMonad m]
(f : β → m (ForInStep β)) (g : α → β → m (ForInStep β)) (s : ForInStep β) (l : List α),
(do
let x ← ForInStep.bind s f
bindList g l x) =     ForInStep.bind s fun b => do
let x ← f b
bindList g l xForInStep.bind_bindList_assoc [Monad: (Type ?u.1929 → Type ?u.1928) → Type (max(?u.1929+1)?u.1928)Monad m: ?m.1878m] [LawfulMonad: (m : Type ?u.1887 → Type ?u.1886) → [inst : Monad m] → PropLawfulMonad m: ?m.1878m]
(f: β → m (ForInStep β)f : β: ?m.1899β → m: ?m.1878m (ForInStep: Type ?u.1946 → Type ?u.1946ForInStep β: ?m.1899β)) (g: α → β → m (ForInStep β)g : α: ?m.1925α → β: ?m.1899β → m: ?m.1878m (ForInStep: Type ?u.1953 → Type ?u.1953ForInStep β: ?m.1899β)) (s: ForInStep βs : ForInStep: Type ?u.1956 → Type ?u.1956ForInStep β: ?m.1899β) (l: List αl) :
s: ForInStep βs.bind: {m : Type ?u.1970 → Type ?u.1969} →
{α : Type ?u.1970} → [inst : Monad m] → ForInStep α → (α → m (ForInStep α)) → m (ForInStep α)bind f: β → m (ForInStep β)f >>= (·.bindList: {m : Type ?u.2016 → Type ?u.2015} →
{α : Type ?u.2014} →
{β : Type ?u.2016} → [inst : Monad m] → (α → β → m (ForInStep β)) → List α → ForInStep β → m (ForInStep β)bindList g: α → β → m (ForInStep β)g l: ?m.1959l) = s: ForInStep βs.bind: {m : Type ?u.2078 → Type ?u.2077} →
{α : Type ?u.2078} → [inst : Monad m] → ForInStep α → (α → m (ForInStep α)) → m (ForInStep α)bind fun b: ?m.2088b => f: β → m (ForInStep β)f b: ?m.2088b >>= (·.bindList: {m : Type ?u.2131 → Type ?u.2130} →
{α : Type ?u.2129} →
{β : Type ?u.2131} → [inst : Monad m] → (α → β → m (ForInStep β)) → List α → ForInStep β → m (ForInStep β)bindList g: α → β → m (ForInStep β)g l: ?m.1959l)  := byGoals accomplished! 🐙
m: Type u_1 → Type u_2β: Type u_1α: Type u_3inst✝¹: Monad minst✝: LawfulMonad mf: β → m (ForInStep β)g: α → β → m (ForInStep β)s: ForInStep βl: List α(do
let x ← ForInStep.bind s f
bindList g l x) =   ForInStep.bind s fun b => do
let x ← f b
bindList g l xcases s: ForInStep βsm: Type u_1 → Type u_2β: Type u_1α: Type u_3inst✝¹: Monad minst✝: LawfulMonad mf: β → m (ForInStep β)g: α → β → m (ForInStep β)l: List αa✝: βdone(do
let x ← ForInStep.bind (done a✝) f
bindList g l x) =   ForInStep.bind (done a✝) fun b => do
let x ← f b
bindList g l xm: Type u_1 → Type u_2β: Type u_1α: Type u_3inst✝¹: Monad minst✝: LawfulMonad mf: β → m (ForInStep β)g: α → β → m (ForInStep β)l: List αa✝: βyield(do
let x ← ForInStep.bind (yield a✝) f
bindList g l x) =   ForInStep.bind (yield a✝) fun b => do
let x ← f b
bindList g l x m: Type u_1 → Type u_2β: Type u_1α: Type u_3inst✝¹: Monad minst✝: LawfulMonad mf: β → m (ForInStep β)g: α → β → m (ForInStep β)s: ForInStep βl: List α(do
let x ← ForInStep.bind s f
bindList g l x) =   ForInStep.bind s fun b => do
let x ← f b
bindList g l x<;>m: Type u_1 → Type u_2β: Type u_1α: Type u_3inst✝¹: Monad minst✝: LawfulMonad mf: β → m (ForInStep β)g: α → β → m (ForInStep β)l: List αa✝: βdone(do
let x ← ForInStep.bind (done a✝) f
bindList g l x) =   ForInStep.bind (done a✝) fun b => do
let x ← f b
bindList g l xm: Type u_1 → Type u_2β: Type u_1α: Type u_3inst✝¹: Monad minst✝: LawfulMonad mf: β → m (ForInStep β)g: α → β → m (ForInStep β)l: List αa✝: βyield(do
let x ← ForInStep.bind (yield a✝) f
bindList g l x) =   ForInStep.bind (yield a✝) fun b => do
let x ← f b
bindList g l x m: Type u_1 → Type u_2β: Type u_1α: Type u_3inst✝¹: Monad minst✝: LawfulMonad mf: β → m (ForInStep β)g: α → β → m (ForInStep β)s: ForInStep βl: List α(do
let x ← ForInStep.bind s f
bindList g l x) =   ForInStep.bind s fun b => do
let x ← f b
bindList g l xsimpGoals accomplished! 🐙

theorem ForInStep.bindList_cons': ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [inst_1 : LawfulMonad m]
(f : α → β → m (ForInStep β)) (s : ForInStep β) (a : α) (l : List α),
bindList f (a :: l) s = do
let x ← ForInStep.bind s (f a)
bindList f l xForInStep.bindList_cons' [Monad: (Type ?u.2852 → Type ?u.2851) → Type (max(?u.2852+1)?u.2851)Monad m: ?m.2827m] [LawfulMonad: (m : Type ?u.2880 → Type ?u.2879) → [inst : Monad m] → PropLawfulMonad m: ?m.2827m]
(f: α → β → m (ForInStep β)f : α: ?m.2848α → β: ?m.2871β → m: ?m.2827m (ForInStep: Type ?u.2894 → Type ?u.2894ForInStep β: ?m.2871β)) (s: ForInStep βs : ForInStep: Type ?u.2897 → Type ?u.2897ForInStep β: ?m.2871β) (a: ?m.2900a l: List αl) :
s: ForInStep βs.bindList: {m : Type ?u.2909 → Type ?u.2908} →
{α : Type ?u.2907} →
{β : Type ?u.2909} → [inst : Monad m] → (α → β → m (ForInStep β)) → List α → ForInStep β → m (ForInStep β)bindList f: α → β → m (ForInStep β)f (a: ?m.2900a::l: ?m.2903l) = s: ForInStep βs.bind: {m : Type ?u.2944 → Type ?u.2943} →
{α : Type ?u.2944} → [inst : Monad m] → ForInStep α → (α → m (ForInStep α)) → m (ForInStep α)bind (f: α → β → m (ForInStep β)f a: ?m.2900a) >>= (·.bindList: {m : Type ?u.2985 → Type ?u.2984} →
{α : Type ?u.2983} →
{β : Type ?u.2985} → [inst : Monad m] → (α → β → m (ForInStep β)) → List α → ForInStep β → m (ForInStep β)bindList f: α → β → m (ForInStep β)f l: ?m.2903l) := byGoals accomplished! 🐙 m: Type u_1 → Type u_2α: Type u_3β: Type u_1inst✝¹: Monad minst✝: LawfulMonad mf: α → β → m (ForInStep β)s: ForInStep βa: αl: List αbindList f (a :: l) s = do
let x ← ForInStep.bind s (f a)
bindList f l xsimpGoals accomplished! 🐙

@[simp] theorem ForInStep.bindList_append: ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [inst_1 : LawfulMonad m]
(f : α → β → m (ForInStep β)) (s : ForInStep β) (l₁ l₂ : List α),
bindList f (l₁ ++ l₂) s = do
let x ← bindList f l₁ s
bindList f l₂ xForInStep.bindList_append [Monad: (Type ?u.3374 → Type ?u.3373) → Type (max(?u.3374+1)?u.3373)Monad m: ?m.3370m] [LawfulMonad: (m : Type ?u.3379 → Type ?u.3378) → [inst : Monad m] → PropLawfulMonad m: ?m.3370m]
(f: α → β → m (ForInStep β)f : α: ?m.3391α → β: ?m.3414β → m: ?m.3370m (ForInStep: Type ?u.3437 → Type ?u.3437ForInStep β: ?m.3414β)) (s: ForInStep βs : ForInStep: Type ?u.3440 → Type ?u.3440ForInStep β: ?m.3414β) (l₁: ?m.3443l₁ l₂: ?m.3446l₂) :
s: ForInStep βs.bindList: {m : Type ?u.3452 → Type ?u.3451} →
{α : Type ?u.3450} →
{β : Type ?u.3452} → [inst : Monad m] → (α → β → m (ForInStep β)) → List α → ForInStep β → m (ForInStep β)bindList f: α → β → m (ForInStep β)f (l₁: ?m.3443l₁ ++ l₂: ?m.3446l₂) = s: ForInStep βs.bindList: {m : Type ?u.3525 → Type ?u.3524} →
{α : Type ?u.3523} →
{β : Type ?u.3525} → [inst : Monad m] → (α → β → m (ForInStep β)) → List α → ForInStep β → m (ForInStep β)bindList f: α → β → m (ForInStep β)f l₁: ?m.3443l₁ >>= (·.bindList: {m : Type ?u.3570 → Type ?u.3569} →
{α : Type ?u.3568} →
{β : Type ?u.3570} → [inst : Monad m] → (α → β → m (ForInStep β)) → List α → ForInStep β → m (ForInStep β)bindList f: α → β → m (ForInStep β)f l₂: ?m.3446l₂) := byGoals accomplished! 🐙
m: Type u_1 → Type u_2α: Type u_3β: Type u_1inst✝¹: Monad minst✝: LawfulMonad mf: α → β → m (ForInStep β)s: ForInStep βl₁, l₂: List αbindList f (l₁ ++ l₂) s = do
let x ← bindList f l₁ s
bindList f l₂ xinduction l₁: List αl₁ generalizing s: ForInStep βsm: Type u_1 → Type u_2α: Type u_3β: Type u_1inst✝¹: Monad minst✝: LawfulMonad mf: α → β → m (ForInStep β)l₂: List αs: ForInStep βnilbindList f ([] ++ l₂) s = do
let x ← bindList f [] s
bindList f l₂ xm: Type u_1 → Type u_2α: Type u_3β: Type u_1inst✝¹: Monad minst✝: LawfulMonad mf: α → β → m (ForInStep β)l₂: List αhead✝: αtail✝: List αtail_ih✝: ∀ (s : ForInStep β),
bindList f (tail✝ ++ l₂) s = do
let x ← bindList f tail✝ s
bindList f l₂ xs: ForInStep βconsbindList f (head✝ :: tail✝ ++ l₂) s = do
let x ← bindList f (head✝ :: tail✝) s
bindList f l₂ x m: Type u_1 → Type u_2α: Type u_3β: Type u_1inst✝¹: Monad minst✝: LawfulMonad mf: α → β → m (ForInStep β)s: ForInStep βl₁, l₂: List αbindList f (l₁ ++ l₂) s = do
let x ← bindList f l₁ s
bindList f l₂ x<;>m: Type u_1 → Type u_2α: Type u_3β: Type u_1inst✝¹: Monad minst✝: LawfulMonad mf: α → β → m (ForInStep β)l₂: List αs: ForInStep βnilbindList f ([] ++ l₂) s = do
let x ← bindList f [] s
bindList f l₂ xm: Type u_1 → Type u_2α: Type u_3β: Type u_1inst✝¹: Monad minst✝: LawfulMonad mf: α → β → m (ForInStep β)l₂: List αhead✝: αtail✝: List αtail_ih✝: ∀ (s : ForInStep β),
bindList f (tail✝ ++ l₂) s = do
let x ← bindList f tail✝ s
bindList f l₂ xs: ForInStep βconsbindList f (head✝ :: tail✝ ++ l₂) s = do
let x ← bindList f (head✝ :: tail✝) s
bindList f l₂ x m: Type u_1 → Type u_2α: Type u_3β: Type u_1inst✝¹: Monad minst✝: LawfulMonad mf: α → β → m (ForInStep β)s: ForInStep βl₁, l₂: List αbindList f (l₁ ++ l₂) s = do
let x ← bindList f l₁ s
bindList f l₂ xsimp [*]Goals accomplished! 🐙
```