no goals
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ card (Icc f g) = ∏ i in f.support ∪ g.support, card (Icc (↑f i) (↑g i))
simp_rw [icc_eq, card_finsupp, coe_rangeIcc]