α : Type u_2
inst✝ : DecidableEq α
m✝ : Multiset α
β : Type u_1
m : Multiset α
f : α → β
⊢ map f (map (fun x => x.fst) Finset.univ.val) = map f m
α : Type u_2
inst✝ : DecidableEq α
m✝ : Multiset α
β : Type u_1
m : Multiset α
f : α → β
⊢ map (fun x => f x.fst) Finset.univ.val = map f m
erw [← Multiset.map_map]
no goals
α : Type u_2
inst✝ : DecidableEq α
m✝ : Multiset α
β : Type u_1
m : Multiset α
f : α → β
⊢ map f (map (fun x => x.fst) Finset.univ.val) = map f m
rw [Multiset.map_univ_coe]