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