-- Mathlib/Data/Finset/Card.lean
theorem exists_subset_or_subset_of_two_mul_lt_card [DecidableEq α] {X Y : Finset α} {n : ℕ}
    (hXY : 2 * n < #(X ∪ Y)) : ∃ C : Finset α, n < #C ∧ (C ⊆ X ∨ C ⊆ Y)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < #(X ∪ Y)
⊢ ∃ C, n < #C ∧ (C ⊆ X ∨ C ⊆ Y)

Tactic:
have h₁ : #(X ∩ (Y \ X)) = 0 := Finset.card_eq_zero.mpr (Finset.inter_sdiff_self X Y)

Result:
α : Type u_1
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < #(X ∪ Y)
h₁ : #(X ∩ (Y \ X)) = 0
⊢ ∃ C, n < #C ∧ (C ⊆ X ∨ C ⊆ Y)

Proof state:
case inr
α : Type u_1
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : n + n < #X + #(Y \ X)
h₁ : #(X ∩ (Y \ X)) = 0
h₂ : #(X ∪ Y) = #X + #(Y \ X)
h : n < #(Y \ X)
⊢ ∃ C, n < #C ∧ (C ⊆ X ∨ C ⊆ Y)

Tactic:
exact ⟨Y \ X, h, Or.inr sdiff_subset⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < #(X ∪ Y)
h₁ : #(X ∩ (Y \ X)) = 0
⊢ ∃ C, n < #C ∧ (C ⊆ X ∨ C ⊆ Y)

Tactic:
have h₂ : #(X ∪ Y) = #X + #(Y \ X) := by
  rw [← card_union_add_card_inter X (Y \ X), Finset.union_sdiff_self_eq_union, h₁, Nat.add_zero]

Result:
α : Type u_1
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < #(X ∪ Y)
h₁ : #(X ∩ (Y \ X)) = 0
h₂ : #(X ∪ Y) = #X + #(Y \ X)
⊢ ∃ C, n < #C ∧ (C ⊆ X ∨ C ⊆ Y)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
h₁ : #(X ∩ (Y \ X)) = 0
h₂ : #(X ∪ Y) = #X + #(Y \ X)
hXY : #X ≤ n ∧ #(Y \ X) ≤ n
⊢ #X + #(Y \ X) ≤ n + n

Tactic:
omega

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : n + n < #X + #(Y \ X)
h₁ : #(X ∩ (Y \ X)) = 0
h₂ : #(X ∪ Y) = #X + #(Y \ X)
h : n < #X
⊢ ∃ C, n < #C ∧ (C ⊆ X ∨ C ⊆ Y)

Tactic:
exact ⟨X, h, Or.inl (Finset.Subset.refl X)⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < #(X ∪ Y)
h₁ : #(X ∩ (Y \ X)) = 0
⊢ #(X ∪ Y) = #X + #(Y \ X)

Tactic:
rw [← card_union_add_card_inter X (Y \ X), Finset.union_sdiff_self_eq_union, h₁, Nat.add_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : n + n < #X + #(Y \ X)
h₁ : #(X ∩ (Y \ X)) = 0
h₂ : #(X ∪ Y) = #X + #(Y \ X)
⊢ n < #X ∨ n < #(Y \ X)

Tactic:
contrapose! hXY

Result:
α : Type u_1
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
h₁ : #(X ∩ (Y \ X)) = 0
h₂ : #(X ∪ Y) = #X + #(Y \ X)
hXY : #X ≤ n ∧ #(Y \ X) ≤ n
⊢ #X + #(Y \ X) ≤ n + n

Proof state:
α : Type u_1
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : n + n < #X + #(Y \ X)
h₁ : #(X ∩ (Y \ X)) = 0
h₂ : #(X ∪ Y) = #X + #(Y \ X)
⊢ ∃ C, n < #C ∧ (C ⊆ X ∨ C ⊆ Y)

Tactic:
obtain h | h : n < #X ∨ n < #(Y \ X) := by contrapose! hXY; omega

Result:
case inl
α : Type u_1
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : n + n < #X + #(Y \ X)
h₁ : #(X ∩ (Y \ X)) = 0
h₂ : #(X ∪ Y) = #X + #(Y \ X)
h : n < #X
⊢ ∃ C, n < #C ∧ (C ⊆ X ∨ C ⊆ Y)

case inr
α : Type u_1
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : n + n < #X + #(Y \ X)
h₁ : #(X ∩ (Y \ X)) = 0
h₂ : #(X ∪ Y) = #X + #(Y \ X)
h : n < #(Y \ X)
⊢ ∃ C, n < #C ∧ (C ⊆ X ∨ C ⊆ Y)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < #(X ∪ Y)
h₁ : #(X ∩ (Y \ X)) = 0
h₂ : #(X ∪ Y) = #X + #(Y \ X)
⊢ ∃ C, n < #C ∧ (C ⊆ X ∨ C ⊆ Y)

Tactic:
rw [h₂, Nat.two_mul] at hXY

Result:
α : Type u_1
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : n + n < #X + #(Y \ X)
h₁ : #(X ∩ (Y \ X)) = 0
h₂ : #(X ∪ Y) = #X + #(Y \ X)
⊢ ∃ C, n < #C ∧ (C ⊆ X ∨ C ⊆ Y)