α : Type u_1
β : Type u_2
γ : Type ?u.9950
δ : Type ?u.9953
a : α
s t : Multiset α
f✝ g : α → Multiset β
l : List α
f : α → List β
⊢ (bind ↑l fun a => ↑(f a)) = join ↑(List.map (ofList ∘ f) l)
α : Type u_1
β : Type u_2
γ : Type ?u.9950
δ : Type ?u.9953
a : α
s t : Multiset α
f✝ g : α → Multiset β
l : List α
f : α → List β
⊢ (bind ↑l fun a => ↑(f a)) = ↑(List.bind l f)
rw [List.bind, ← coe_join, List.map_map]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.9950
δ : Type ?u.9953
a : α
s t : Multiset α
f✝ g : α → Multiset β
l : List α
f : α → List β
⊢ (bind ↑l fun a => ↑(f a)) = join ↑(List.map (ofList ∘ f) l)
rfl