α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ ↑card (map Prod.fst (toEnumFinset m).val) = ↑card m
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Finset.card (toEnumFinset m) = ↑card m
rw [Finset.card, ←Multiset.card_map Prod.fst m.toEnumFinset.val]
case h.e_6.h
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ map Prod.fst (toEnumFinset m).val = m
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ ↑card (map Prod.fst (toEnumFinset m).val) = ↑card m
congr
no goals
case h.e_6.h
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ map Prod.fst (toEnumFinset m).val = m
exact m.map_toEnumFinset_fst