obtain (⟨i, hi⟩ | h) := em <| ∃ i, (s i).Infinite
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
⊢ (⋃ i, s i).encard = ∑ i : ι, (s i).encard
case inl.intro
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
i : ι
hi : (s i).Infinite
⊢ (⋃ i, s i).encard = ∑ i : ι, (s i).encard

case inr
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ¬∃ i, (s i).Infinite
⊢ (⋃ i, s i).encard = ∑ i : ι, (s i).encard