Theorem: encard_iUnion_eq_sum_iff_pairwiseDisjoint (Matroid/ForMathlib/Card.lean)

State before:
α : 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
Tactic:
refine ⟨fun hsum i _ j _ hij ↦ disjoint_iff_forall_ne.2 ?_, fun hdj ↦ encard_iUnion s hdj⟩
State after:
α : 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

State before:
α : 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
Tactic:
rintro x hxi _ hxj rfl
State after:
α : 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
⊢ False

State before:
α : 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
⊢ False
Tactic:
have hrw : ∀ t : Set α, encard t = encard (t \ {x}) + encard (t ∩ {x}) := by
  intro t
  rw [← encard_union_eq, diff_union_inter]
  exact disjoint_sdiff_left.mono_right inter_subset_right
State after:
α : 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
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
⊢ False

State before:
α : 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
hrw : ∀ (t : Set α), t.encard = (t \ {x}).encard + (t ∩ {x}).encard
⊢ False
Tactic:
rw [hrw, Finset.sum_congr rfl (fun i _ ↦ hrw (s i)), Finset.sum_add_distrib,
  inter_eq_self_of_subset_right (singleton_subset_iff.2 (mem_iUnion_of_mem i hxi)),
  encard_singleton, eq_comm, iUnion_diff] at hsum
State after:
α : 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
⊢ False

State before:
α : 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
⊢ False
Tactic:
have hlb := Finset.sum_le_sum_of_subset
  (f := fun i ↦ (s i ∩ {x}).encard) (Finset.subset_univ {i,j})
State after:
α : 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

State before:
α : 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
Tactic:
simp_rw [Finset.sum_pair hij] at hlb
State after:
α : 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

State before:
α : 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
Tactic:
rw [inter_eq_self_of_subset_right (by simpa), inter_eq_self_of_subset_right (by simpa),
  encard_singleton] at hlb
State after:
α : 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
⊢ False

State before:
α : 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
⊢ False
Tactic:
have hcon := ((add_le_add_left hlb _).trans hsum.le).trans
  (add_le_add_right (encard_iUnion_le _) 1)
State after:
α : 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 + 1) ≤ ∑ i : ι, (s i \ {x}).encard + 1
⊢ False

State before:
α : 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 + 1) ≤ ∑ i : ι, (s i \ {x}).encard + 1
⊢ False
Tactic:
rw [← add_assoc, WithTop.add_le_add_iff_right (by simp), ENat.add_one_le_iff] at hcon
State after:
α : 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 < ∑ i : ι, (s i \ {x}).encard
⊢ 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 : 1 + 1 ≤ ∑ x_1 : ι, (s x_1 ∩ {x}).encard
hcon : ∑ x_1 : ι, (s x_1 \ {x}).encard + 1 ≤ ∑ i : ι, (s i \ {x}).encard
⊢ ∑ x_1 : ι, (s x_1 \ {x}).encard ≠ ⊤

State before:
α : 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
⊢ ∑ x_1 : ι, (s x_1 \ {x}).encard ≠ ⊤
Tactic:
refine (WithTop.sum_lt_top (fun i _ ↦ ?_)).ne
State after:
α : 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}).encard ≠ ⊤

State before:
α : 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}).encard ≠ ⊤
Tactic:
rw [encard_ne_top_iff]
State after:
α : 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

State before:
α : 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
Tactic:
exact (hfin i).diff _
State after:
no goals

State before:
α : 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
Tactic:
intro t
State after:
α : 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

State before:
α : 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
Tactic:
rw [← encard_union_eq, diff_union_inter]
State after:
α : 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})

State before:
α : 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})
Tactic:
exact disjoint_sdiff_left.mono_right inter_subset_right
State after:
no goals

State before:
α : 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
⊢ {x} ⊆ s i
Tactic:
simpa
State after:
no goals

State before:
α : 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}.encard + (s j ∩ {x}).encard ≤ ∑ x_1 : ι, (s x_1 ∩ {x}).encard
⊢ {x} ⊆ s j
Tactic:
simpa
State after:
no goals

State before:
α : 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 + 1 ≤ ∑ i : ι, (s i \ {x}).encard + 1
⊢ 1 ≠ ⊤
Tactic:
simp
State after:
no goals

State before:
α : 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 < ∑ i : ι, (s i \ {x}).encard
⊢ False
Tactic:
exact hcon.ne rfl
State after:
no goals