ι : Type ?u.22232
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ map f l = List.bind l fun x => map f [x]
ι : Type ?u.22232
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ map f l = List.bind l fun x => [f x]
simp_rw [←map_singleton]
no goals
ι : Type ?u.22232
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ map f l = List.bind l fun x => map f [x]
rw [← bind_singleton' l, bind_map, bind_singleton']