rw [biUnion_eq_iUnion, ← ENat.tsum_encard_eq_encard_iUnion]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
ι : Type u_4
s : ι → Set α
t : Set ι
hI : t.PairwiseDisjoint s
⊢ ∑' (i : ↑t), (s ↑i).encard = (⋃ i ∈ t, s i).encard
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
ι : Type u_4
s : ι → Set α
t : Set ι
hI : t.PairwiseDisjoint s
⊢ univ.PairwiseDisjoint fun x => s ↑x