no goals
α : Type u_1
β : α → Type ?u.45300
inst✝ : DecidableEq α
f g : Multiset α
⊢ Finset.card (Finset.Ico f g) = ∏ i in toFinset f ∪ toFinset g, (count i g + 1 - count i f) - 1
rw [card_Ico_eq_card_Icc_sub_one, card_Icc]