no goals
α✝ : Type ?u.42445
l✝ : List α✝
inst✝¹ : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
l : List α
f : α → List β
x : β
⊢ count x (List.bind l f) = sum (map (count x ∘ f) l)
rw [List.bind, count_join, map_map]