no goals
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ card (Ioc f g) = ∏ i in support f ∪ support g, card (Icc (↑f i) (↑g i)) - 1
rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]