convert encard_iUnion (fun i : t ↦ s i) ?_
α : Type u_1
β : Type u_2
s✝ t✝ : Set α
n : ℕ
ι : Type u_3
s : ι → Set α
t : Finset ι
ht : (↑t).PairwiseDisjoint s
⊢ (⋃ i ∈ t, s i).encard = ∑ i ∈ t, (s i).encard
case h.e'_2.h.e'_2
α : Type u_1
β : Type u_2
s✝ t✝ : Set α
n : ℕ
ι : Type u_3
s : ι → Set α
t : Finset ι
ht : (↑t).PairwiseDisjoint s
⊢ ⋃ i ∈ t, s i = ⋃ i, s ↑i

case h.e'_3
α : Type u_1
β : Type u_2
s✝ t✝ : Set α
n : ℕ
ι : Type u_3
s : ι → Set α
t : Finset ι
ht : (↑t).PairwiseDisjoint s
⊢ ∑ i ∈ t, (s i).encard = ∑ i : { x // x ∈ t }, (s ↑i).encard

α : Type u_1
β : Type u_2
s✝ t✝ : Set α
n : ℕ
ι : Type u_3
s : ι → Set α
t : Finset ι
ht : (↑t).PairwiseDisjoint s
⊢ univ.PairwiseDisjoint fun i => s ↑i