convert encard_iUnion_eq_sum_iff_pairwiseDisjoint (ι := u) (s := fun i ↦ s i) (by simpa)
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
u : Finset ι
s : ι → Set α
hs : ∀ i ∈ u, (s i).Finite
⊢ (⋃ x, s ↑x).encard = ∑ i ∈ u, (s i).encard ↔ (↑u).PairwiseDisjoint s
case h.e'_1.h.e'_3
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
u : Finset ι
s : ι → Set α
hs : ∀ i ∈ u, (s i).Finite
⊢ ∑ i ∈ u, (s i).encard = ∑ i : { x // x ∈ u }, (s ↑i).encard

case h.e'_2.a
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
u : Finset ι
s : ι → Set α
hs : ∀ i ∈ u, (s i).Finite
⊢ (↑u).PairwiseDisjoint s ↔ univ.PairwiseDisjoint fun i => s ↑i