no goals
α : Type u_1
β : α → Type ?u.47784
inst✝ : DecidableEq α
f g : Multiset α
⊢ Finset.card (Finset.Iic f) = ∏ i in toFinset f, (count i f + 1)
simp_rw [Iic_eq_Icc, card_Icc, bot_eq_zero, toFinset_zero, empty_union, count_zero, tsub_zero]