simp_rw [Finset.sum_pair hij] at hlb
α : 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 : ∑ x_1 ∈ {i, j}, (fun i => (s i ∩ {x}).encard) x_1 ≤ ∑ x_1 : ι, (fun i => (s i ∩ {x}).encard) x_1
⊢ False
α : 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 : (s i ∩ {x}).encard + (s j ∩ {x}).encard ≤ ∑ x_1 : ι, (s x_1 ∩ {x}).encard
⊢ False