no goals
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyOrderedAddMonoid α
inst✝ : LocallyFiniteOrder α
f : ι →₀ α
⊢ card (Iic f) = ∏ i in f.support, card (Iic (↑f i))
classical simp_rw [Iic_eq_Icc, card_Icc, Finsupp.bot_eq_zero, support_zero, empty_union,
    zero_apply, bot_eq_zero]
no goals
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyOrderedAddMonoid α
inst✝ : LocallyFiniteOrder α
f : ι →₀ α
⊢ card (Iic f) = ∏ i in f.support, card (Iic (↑f i))
simp_rw [Iic_eq_Icc, card_Icc, Finsupp.bot_eq_zero, support_zero, empty_union,
zero_apply, bot_eq_zero]