refine ⟨fun hsum i _ j _ hij ↦ disjoint_iff_forall_ne.2 ?_, fun hdj ↦ encard_iUnion s hdj⟩
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
⊢ (⋃ i, s i).encard = ∑ i : ι, (s i).encard ↔ univ.PairwiseDisjoint s
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
hsum : (⋃ i, s i).encard = ∑ i : ι, (s i).encard
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
hij : i ≠ j
⊢ ∀ ⦃a : α⦄, a ∈ s i → ∀ ⦃b : α⦄, b ∈ s j → a ≠ b