α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
this : map Prod.fst (toEnumFinset m).val = m
⊢ map (fun x => x.fst) Finset.univ.val = m
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ map (fun x => x.fst) Finset.univ.val = m
have := m.map_toEnumFinset_fst
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
this : map Prod.fst (Finset.map (coeEmbedding m) Finset.univ).val = m
⊢ map (fun x => x.fst) Finset.univ.val = m
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
this : map Prod.fst (toEnumFinset m).val = m
⊢ map (fun x => x.fst) Finset.univ.val = m
rw [← m.map_univ_coeEmbedding] at this
no goals
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
this : map Prod.fst (Finset.map (coeEmbedding m) Finset.univ).val = m
⊢ map (fun x => x.fst) Finset.univ.val = m
simpa only [Finset.map_val, Multiset.coeEmbedding_apply, Multiset.map_map,
  Function.comp_apply] using this