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

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

State before:
α β : Type u
γ : Type w
f : α → β
a : α
as : List α
⊢ ([f a] ++ List.bind as fun a => [f a]) = f a :: map f as
Tactic:
rw [cons_append, nil_append]
State after:
α β : Type u
γ : Type w
f : α → β
a : α
as : List α
⊢ (f a :: List.bind as fun a => [f a]) = f a :: map f as

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