Theorem: List.bind_map_binary_eq_map_bind_map (Algdata/Data/List/Basic.lean)

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

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

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

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