Theorem: List.bind_assoc (Algdata/Data/List/Instances.lean)

State before:
α β : Type u
γ : Type w
as : List α
f : α → List β
g : β → List γ
⊢ List.bind (List.bind as f) g = List.bind as fun x => List.bind (f x) g
Tactic:
induction as with
| nil => rfl
| cons a as hi =>
  rw [cons_bind, cons_bind]
  rw [append_bind]
  rw [hi]
State after:
no goals

State before:
case nil
α β : Type u
γ : Type w
f : α → List β
g : β → List γ
⊢ List.bind (List.bind [] f) g = List.bind [] fun x => List.bind (f x) g
Tactic:
rfl
State after:
no goals

State before:
case cons
α β : Type u
γ : Type w
f : α → List β
g : β → List γ
a : α
as : List α
hi : List.bind (List.bind as f) g = List.bind as fun x => List.bind (f x) g
⊢ List.bind (List.bind (a :: as) f) g = List.bind (a :: as) fun x => List.bind (f x) g
Tactic:
rw [cons_bind, cons_bind]
State after:
case cons
α β : Type u
γ : Type w
f : α → List β
g : β → List γ
a : α
as : List α
hi : List.bind (List.bind as f) g = List.bind as fun x => List.bind (f x) g
⊢ List.bind (f a ++ List.bind as f) g = List.bind (f a) g ++ List.bind as fun x => List.bind (f x) g

State before:
case cons
α β : Type u
γ : Type w
f : α → List β
g : β → List γ
a : α
as : List α
hi : List.bind (List.bind as f) g = List.bind as fun x => List.bind (f x) g
⊢ List.bind (f a ++ List.bind as f) g = List.bind (f a) g ++ List.bind as fun x => List.bind (f x) g
Tactic:
rw [append_bind]
State after:
case cons
α β : Type u
γ : Type w
f : α → List β
g : β → List γ
a : α
as : List α
hi : List.bind (List.bind as f) g = List.bind as fun x => List.bind (f x) g
⊢ List.bind (f a) g ++ List.bind (List.bind as f) g = List.bind (f a) g ++ List.bind as fun x => List.bind (f x) g

State before:
case cons
α β : Type u
γ : Type w
f : α → List β
g : β → List γ
a : α
as : List α
hi : List.bind (List.bind as f) g = List.bind as fun x => List.bind (f x) g
⊢ List.bind (f a) g ++ List.bind (List.bind as f) g = List.bind (f a) g ++ List.bind as fun x => List.bind (f x) g
Tactic:
rw [hi]
State after:
no goals