α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Fintype.card { x // x ∈ toEnumFinset m } = ↑card m
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Fintype.card (ToType m) = ↑card m
rw [Fintype.card_congr m.coeEquiv]
no goals
α : Type u_1
inst✝ : DecidableEq α
m✝ m : Multiset α
⊢ Fintype.card { x // x ∈ toEnumFinset m } = ↑card m
simp only [Fintype.card_coe, card_toEnumFinset]