no goals
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
a : (i : ι) → α i
⊢ Finset.card (Ioi a) = ∏ i : ι, Finset.card (Ici (a i)) - 1
rw [card_Ioi_eq_card_Ici_sub_one, card_Ici]