no goals
ι : Type u_1
α : Type u_2
inst✝¹ : CanonicallyOrderedAddMonoid α
inst✝ : LocallyFiniteOrder α
f : ι →₀ α
⊢ card (Iio f) = ∏ i in f.support, card (Iic (↑f i)) - 1
rw [card_Iio_eq_card_Iic_sub_one, card_Iic]