exact (hfin i).diff _
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hfin : ∀ (i : ι), (s i).Finite
i✝ : ι
x✝² : i✝ ∈ univ
j : ι
x✝¹ : j ∈ univ
hij : i✝ ≠ j
x : α
hsum : ∑ x_1 : ι, (s x_1 \ {x}).encard + ∑ x_1 : ι, (s x_1 ∩ {x}).encard = (⋃ i, s i \ {x}).encard + 1
hxi : x ∈ s i✝
hxj : x ∈ s j
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
hlb : 1 + 1 ≤ ∑ x_1 : ι, (s x_1 ∩ {x}).encard
hcon : ∑ x_1 : ι, (s x_1 \ {x}).encard + 1 ≤ ∑ i : ι, (s i \ {x}).encard
i : ι
x✝ : i ∈ Finset.univ
⊢ (s i \ {x}).Finite
no goals