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

State before:
α β : Type u
γ : Type w
a : α
f : α → List β
⊢ List.bind [a] f = f a
Tactic:
rw [List.bind, map, map, join, join]
State after:
α β : Type u
γ : Type w
a : α
f : α → List β
⊢ f a ++ [] = f a

State before:
α β : Type u
γ : Type w
a : α
f : α → List β
⊢ f a ++ [] = f a
Tactic:
simp
State after:
no goals