α : Type u_1
β : Type ?u.45753
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < card (X ∪ Y)
h₁ : card (X ∩ (Y \ X)) = 0
⊢ ∃ C, n < card C ∧ (C ⊆ X ∨ C ⊆ Y)
α : Type u_1
β : Type ?u.45753
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < card (X ∪ Y)
⊢ ∃ C, n < card C ∧ (C ⊆ X ∨ C ⊆ Y)
have h₁ : (X ∩ (Y \ X)).card = 0 := Finset.card_eq_zero.mpr (Finset.inter_sdiff_self X Y)
α : Type u_1
β : Type ?u.45753
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < card (X ∪ Y)
h₁ : card (X ∩ (Y \ X)) = 0
h₂ : card (X ∪ Y) = card X + card (Y \ X)
⊢ ∃ C, n < card C ∧ (C ⊆ X ∨ C ⊆ Y)
α : Type u_1
β : Type ?u.45753
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < card (X ∪ Y)
h₁ : card (X ∩ (Y \ X)) = 0
⊢ ∃ C, n < card C ∧ (C ⊆ X ∨ C ⊆ Y)
have h₂ : (X ∪ Y).card = X.card + (Y \ X).card := by
  rw [← card_union_add_card_inter X (Y \ X), Finset.union_sdiff_self_eq_union, h₁, add_zero]
α : Type u_1
β : Type ?u.45753
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : n + n < card X + card (Y \ X)
h₁ : card (X ∩ (Y \ X)) = 0
h₂ : card (X ∪ Y) = card X + card (Y \ X)
⊢ ∃ C, n < card C ∧ (C ⊆ X ∨ C ⊆ Y)
α : Type u_1
β : Type ?u.45753
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < card (X ∪ Y)
h₁ : card (X ∩ (Y \ X)) = 0
h₂ : card (X ∪ Y) = card X + card (Y \ X)
⊢ ∃ C, n < card C ∧ (C ⊆ X ∨ C ⊆ Y)
rw [h₂, two_mul] at hXY
case inl
α : Type u_1
β : Type ?u.45753
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : n + n < card X + card (Y \ X)
h₁ : card (X ∩ (Y \ X)) = 0
h₂ : card (X ∪ Y) = card X + card (Y \ X)
h : n < card X
⊢ ∃ C, n < card C ∧ (C ⊆ X ∨ C ⊆ Y)

case inr
α : Type u_1
β : Type ?u.45753
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : n + n < card X + card (Y \ X)
h₁ : card (X ∩ (Y \ X)) = 0
h₂ : card (X ∪ Y) = card X + card (Y \ X)
h : n < card (Y \ X)
⊢ ∃ C, n < card C ∧ (C ⊆ X ∨ C ⊆ Y)
α : Type u_1
β : Type ?u.45753
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : n + n < card X + card (Y \ X)
h₁ : card (X ∩ (Y \ X)) = 0
h₂ : card (X ∪ Y) = card X + card (Y \ X)
⊢ ∃ C, n < card C ∧ (C ⊆ X ∨ C ⊆ Y)
rcases lt_or_lt_of_add_lt_add hXY with (h | h)
no goals
α : Type u_1
β : Type ?u.45753
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < card (X ∪ Y)
h₁ : card (X ∩ (Y \ X)) = 0
⊢ card (X ∪ Y) = card X + card (Y \ X)
rw [← card_union_add_card_inter X (Y \ X), Finset.union_sdiff_self_eq_union, h₁, add_zero]
no goals
case inl
α : Type u_1
β : Type ?u.45753
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : n + n < card X + card (Y \ X)
h₁ : card (X ∩ (Y \ X)) = 0
h₂ : card (X ∪ Y) = card X + card (Y \ X)
h : n < card X
⊢ ∃ C, n < card C ∧ (C ⊆ X ∨ C ⊆ Y)
exact ⟨X, h, Or.inl (Finset.Subset.refl X)⟩
no goals
case inr
α : Type u_1
β : Type ?u.45753
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : n + n < card X + card (Y \ X)
h₁ : card (X ∩ (Y \ X)) = 0
h₂ : card (X ∪ Y) = card X + card (Y \ X)
h : n < card (Y \ X)
⊢ ∃ C, n < card C ∧ (C ⊆ X ∨ C ⊆ Y)
exact ⟨Y \ X, h, Or.inr (Finset.sdiff_subset Y X)⟩