no goals
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
b : (i : ι) → α i
⊢ Finset.card (Iio b) = ∏ i : ι, Finset.card (Iic (b i)) - 1
rw [card_Iio_eq_card_Iic_sub_one, card_Iic]