/-
Copyright (c) 2022 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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.5
m] (
a: α
a : 
α: ?m.14
α) (
f: α → m (ForInStep α)
f : 
α: ?m.14
α → 
m: ?m.5
m (
ForInStep: Type ?u.26 → Type ?u.26
ForInStep 
α: ?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.5
m) 
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 = a
rfl
@[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 a
ForInStep.bind_yield [
Monad: (Type ?u.179 → Type ?u.178) → Type (max(?u.179+1)?u.178)
Monad 
m: ?m.175
m] (
a: α
a : 
α: ?m.184
α) (
f: α → m (ForInStep α)
f : 
α: ?m.184
α → 
m: ?m.175
m (
ForInStep: Type ?u.196 → Type ?u.196
ForInStep 
α: ?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.175
m) 
f: α → m (ForInStep α)
f = 
f: α → m (ForInStep α)
f 
a: α
a := 
rfl: ∀ {α : Sort ?u.231} {a : α}, a = a
rfl

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) = a
ForInStep.run_done : (
ForInStep.done: {α : Type ?u.288} → α → ForInStep α
ForInStep.done 
a: ?m.284
a).
run: {α : Type ?u.290} → ForInStep α → α
run = 
a: ?m.284
a := 
rfl: ∀ {α : Sort ?u.302} {a : α}, a = a
rfl
@[simp] theorem 
ForInStep.run_yield: ∀ {α : Type u_1} {a : α}, run (yield a) = a
ForInStep.run_yield : (
ForInStep.yield: {α : Type ?u.336} → α → ForInStep α
ForInStep.yield 
a: ?m.332
a).
run: {α : Type ?u.338} → ForInStep α → α
run = 
a: ?m.332
a := 
rfl: ∀ {α : Sort ?u.350} {a : α}, a = a
rfl

@[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 s
ForInStep.bindList_nil [
Monad: (Type ?u.393 → Type ?u.392) → Type (max(?u.393+1)?u.392)
Monad 
m: ?m.379
m] (
f: α → β → m (ForInStep β)
f : 
α: ?m.389
α → 
β: ?m.401
β → 
m: ?m.379
m (
ForInStep: Type ?u.413 → Type ?u.413
ForInStep 
β: ?m.401
β))
    (
s: ForInStep β
s : 
ForInStep: Type ?u.416 → Type ?u.416
ForInStep 
β: ?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 = a
rfl

@[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 x
ForInStep.bindList_cons [
Monad: (Type ?u.603 → Type ?u.602) → Type (max(?u.603+1)?u.602)
Monad 
m: ?m.577
m]
    (
f: α → β → m (ForInStep β)
f : 
α: ?m.587
α → 
β: ?m.599
β → 
m: ?m.577
m (
ForInStep: Type ?u.611 → Type ?u.611
ForInStep 
β: ?m.599
β)) (
s: ForInStep β
s : 
ForInStep: Type ?u.614 → Type ?u.614
ForInStep 
β: ?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.617
a::
l: ?m.620
l) = 
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.665
b => 
f: α → β → m (ForInStep β)
f 
a: ?m.617
a 
b: ?m.665
b >>= (·.
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.620
l) := 
rfl: ∀ {α : Sort ?u.775} {a : α}, a = a
rfl

@[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.849
m]
    (
f: α → β → m (ForInStep β)
f : 
α: ?m.859
α → 
β: ?m.871
β → 
m: ?m.849
m (
ForInStep: Type ?u.883 → Type ?u.883
ForInStep 
β: ?m.871
β)) (
a: β
a 
l: List α
l) :
    (
ForInStep.done: {α : Type ?u.893} → α → ForInStep α
ForInStep.done 
a: ?m.886
a).
bindList: {m : Type ?u.897 → Type ?u.896} →
  {α : Type ?u.895} →
    {β : Type ?u.897} → [inst : Monad m] → (α → β → m (ForInStep β)) → List α → ForInStep β → m (ForInStep β)
bindList 
f: α → β → m (ForInStep β)
f 
l: ?m.889
l = 
pure: {f : Type ?u.925 → Type ?u.924} → [self : Pure f] → {α : Type ?u.925} → α → f α
pure (
.done: {α : Type ?u.966} → α → ForInStep α
.done 
a: ?m.886
a) := by
Goals accomplished! 🐙 
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)cases 
l: List α
l
m: Type u_1 → Type u_2

α: Type u_3

β: Type u_1

inst✝: Monad m

f: α → β → m (ForInStep β)

a: β

nil
bindList f [] (done a) = pure (done a)
m: Type u_1 → Type u_2

α: Type u_3

β: Type u_1

inst✝: Monad m

f: α → β → m (ForInStep β)

a: β

head✝: α

tail✝: List α

cons
bindList f (head✝ :: tail✝) (done a) = pure (done a) 
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)<;>
m: Type u_1 → Type u_2

α: Type u_3

β: Type u_1

inst✝: Monad m

f: α → β → m (ForInStep β)

a: β

nil
bindList f [] (done a) = pure (done a)
m: Type u_1 → Type u_2

α: Type u_3

β: Type u_1

inst✝: Monad m

f: α → β → m (ForInStep β)

a: β

head✝: α

tail✝: List α

cons
bindList f (head✝ :: tail✝) (done a) = pure (done a) 
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)simp
Goals accomplished! 🐙

@[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 s
ForInStep.bind_yield_bindList [
Monad: (Type ?u.1433 → Type ?u.1432) → Type (max(?u.1433+1)?u.1432)
Monad 
m: ?m.1419
m]
    (
f: α → β → m (ForInStep β)
f : 
α: ?m.1429
α → 
β: ?m.1441
β → 
m: ?m.1419
m (
ForInStep: Type ?u.1453 → Type ?u.1453
ForInStep 
β: ?m.1441
β)) (
s: ForInStep β
s : 
ForInStep: Type ?u.1456 → Type ?u.1456
ForInStep 
β: ?m.1441
β) (
l: ?m.1459
l) :
    (
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.1475
a => (
yield: {α : Type ?u.1477} → α → ForInStep α
yield 
a: ?m.1475
a).
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.1459
l) = 
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.1459
l := by
Goals accomplished! 🐙 
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 scases 
s: ForInStep β
s
m: Type u_1 → Type u_2

α: Type u_3

β: Type u_1

inst✝: Monad m

f: α → β → 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_1

inst✝: Monad m

f: α → β → 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_1

inst✝: Monad m

f: α → β → 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_1

inst✝: Monad m

f: α → β → 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_1

inst✝: Monad m

f: α → β → 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_1

inst✝: Monad m

f: α → β → m (ForInStep β)

s: ForInStep β

l: List α

(ForInStep.bind s fun a => bindList f l (yield a)) = bindList f l ssimp
Goals 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 x
ForInStep.bind_bindList_assoc [
Monad: (Type ?u.1929 → Type ?u.1928) → Type (max(?u.1929+1)?u.1928)
Monad 
m: ?m.1878
m] [
LawfulMonad: (m : Type ?u.1887 → Type ?u.1886) → [inst : Monad m] → Prop
LawfulMonad 
m: ?m.1878
m]
    (
f: β → m (ForInStep β)
f : 
β: ?m.1899
β → 
m: ?m.1878
m (
ForInStep: Type ?u.1946 → Type ?u.1946
ForInStep 
β: ?m.1899
β)) (
g: α → β → m (ForInStep β)
g : 
α: ?m.1925
α → 
β: ?m.1899
β → 
m: ?m.1878
m (
ForInStep: Type ?u.1953 → Type ?u.1953
ForInStep 
β: ?m.1899
β)) (
s: ForInStep β
s : 
ForInStep: Type ?u.1956 → Type ?u.1956
ForInStep 
β: ?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.1959
l) = 
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.2088
b => 
f: β → m (ForInStep β)
f 
b: ?m.2088
b >>= (·.
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.1959
l)  := by
Goals accomplished! 🐙
  
m: Type u_1 → Type u_2

β: Type u_1

α: Type u_3

inst✝¹: Monad m

inst✝: 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 xcases 
s: ForInStep β
s
m: Type u_1 → Type u_2

β: Type u_1

α: Type u_3

inst✝¹: Monad m

inst✝: LawfulMonad m

f: β → 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 x
m: Type u_1 → Type u_2

β: Type u_1

α: Type u_3

inst✝¹: Monad m

inst✝: LawfulMonad m

f: β → 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_3

inst✝¹: Monad m

inst✝: 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 x<;>
m: Type u_1 → Type u_2

β: Type u_1

α: Type u_3

inst✝¹: Monad m

inst✝: LawfulMonad m

f: β → 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 x
m: Type u_1 → Type u_2

β: Type u_1

α: Type u_3

inst✝¹: Monad m

inst✝: LawfulMonad m

f: β → 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_3

inst✝¹: Monad m

inst✝: 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 xsimp
Goals 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 x
ForInStep.bindList_cons' [
Monad: (Type ?u.2852 → Type ?u.2851) → Type (max(?u.2852+1)?u.2851)
Monad 
m: ?m.2827
m] [
LawfulMonad: (m : Type ?u.2880 → Type ?u.2879) → [inst : Monad m] → Prop
LawfulMonad 
m: ?m.2827
m]
    (
f: α → β → m (ForInStep β)
f : 
α: ?m.2848
α → 
β: ?m.2871
β → 
m: ?m.2827
m (
ForInStep: Type ?u.2894 → Type ?u.2894
ForInStep 
β: ?m.2871
β)) (
s: ForInStep β
s : 
ForInStep: Type ?u.2897 → Type ?u.2897
ForInStep 
β: ?m.2871
β) (
a: ?m.2900
a 
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.2900
a::
l: ?m.2903
l) = 
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.2900
a) >>= (·.
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.2903
l) := by
Goals accomplished! 🐙 
m: Type u_1 → Type u_2

α: Type u_3

β: Type u_1

inst✝¹: Monad m

inst✝: 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 xsimp
Goals 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₂ x
ForInStep.bindList_append [
Monad: (Type ?u.3374 → Type ?u.3373) → Type (max(?u.3374+1)?u.3373)
Monad 
m: ?m.3370
m] [
LawfulMonad: (m : Type ?u.3379 → Type ?u.3378) → [inst : Monad m] → Prop
LawfulMonad 
m: ?m.3370
m]
    (
f: α → β → m (ForInStep β)
f : 
α: ?m.3391
α → 
β: ?m.3414
β → 
m: ?m.3370
m (
ForInStep: Type ?u.3437 → Type ?u.3437
ForInStep 
β: ?m.3414
β)) (
s: ForInStep β
s : 
ForInStep: Type ?u.3440 → Type ?u.3440
ForInStep 
β: ?m.3414
β) (
l₁: ?m.3443
l₁ 
l₂: ?m.3446
l₂) :
    
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.3443
l₁ ++ 
l₂: ?m.3446
l₂) = 
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.3443
l₁ >>= (·.
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.3446
l₂) := by
Goals accomplished! 🐙
  
m: Type u_1 → Type u_2

α: Type u_3

β: Type u_1

inst✝¹: Monad m

inst✝: 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₂ xinduction 
l₁: List α
l₁ generalizing 
s: ForInStep β
s
m: Type u_1 → Type u_2

α: Type u_3

β: Type u_1

inst✝¹: Monad m

inst✝: LawfulMonad m

f: α → β → m (ForInStep β)

l₂: List α

s: ForInStep β

nil
bindList f ([] ++ l₂) s = do
  let x ← bindList f [] s
  bindList f l₂ x
m: Type u_1 → Type u_2

α: Type u_3

β: Type u_1

inst✝¹: Monad m

inst✝: LawfulMonad m

f: α → β → 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₂ x

s: ForInStep β

cons
bindList 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_1

inst✝¹: Monad m

inst✝: 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₂ x<;>
m: Type u_1 → Type u_2

α: Type u_3

β: Type u_1

inst✝¹: Monad m

inst✝: LawfulMonad m

f: α → β → m (ForInStep β)

l₂: List α

s: ForInStep β

nil
bindList f ([] ++ l₂) s = do
  let x ← bindList f [] s
  bindList f l₂ x
m: Type u_1 → Type u_2

α: Type u_3

β: Type u_1

inst✝¹: Monad m

inst✝: LawfulMonad m

f: α → β → 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₂ x

s: ForInStep β

cons
bindList 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_1

inst✝¹: Monad m

inst✝: 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₂ xsimp [*]
Goals accomplished! 🐙