Theorem: List.bind_assoc (Extra/List.lean)

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

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

State before:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → List β
g : β → List γ
a : α
as : List α
H : (as.bind f).bind g = as.bind fun a => (f a).bind g
⊢ ((a :: as).bind f).bind g = (a :: as).bind fun a => (f a).bind g
Tactic:
rw [cons_bind, cons_bind, append_bind, H]
State after:
no goals