rw [← encard_union_eq, diff_union_inter]
α : 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
x : α
hxi : x ∈ s i
hxj : x ∈ s j
t : Set α
⊢ t.encard = (t \ {x}).encard + (t ∩ {x}).encard
α : 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
x : α
hxi : x ∈ s i
hxj : x ∈ s j
t : Set α
⊢ Disjoint (t \ {x}) (t ∩ {x})