no goals
α : Type u_1
β : α → Type ?u.41665
inst✝ : DecidableEq α
f g : Multiset α
⊢ Finset.card (Finset.Icc f g) = ∏ i in toFinset f ∪ toFinset g, (count i g + 1 - count i f)
simp_rw [Icc_eq, Finset.card_map, Dfinsupp.card_Icc, Nat.card_Icc, Multiset.toDfinsupp_apply,
  toDfinsupp_support]