Theorem: Set.ncard_pigeonhole (Jordan/Jordan.lean)

State before:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
⊢ Set.Nonempty (s ∩ t)
Tactic:
rw [← compl_ne_univ]
State after:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
⊢ (s ∩ t)ᶜ ≠ univ

State before:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
⊢ (s ∩ t)ᶜ ≠ univ
Tactic:
intro h'
State after:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ False

State before:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ False
Tactic:
apply not_le.mpr h
State after:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ ncard s + ncard t ≤ Fintype.card α

State before:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ ncard s + ncard t ≤ Fintype.card α
Tactic:
rw [← Set.ncard_union_add_ncard_inter]
State after:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ ncard (s ∪ t) + ncard (s ∩ t) ≤ Fintype.card α

State before:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ ncard (s ∪ t) + ncard (s ∩ t) ≤ Fintype.card α
Tactic:
apply Nat.le_of_add_le_add_right
State after:
case a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ ncard (s ∪ t) + ncard (s ∩ t) + ?b ≤ Fintype.card α + ?b

case b
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ ℕ

State before:
case a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ ncard (s ∪ t) + ncard (s ∩ t) + ?b ≤ Fintype.card α + ?b

case b
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ ℕ
Tactic:
rw [add_assoc, Set.ncard_add_ncard_compl, h', Set.ncard_univ, ← Nat.card_eq_fintype_card, add_le_add_iff_right, ← Set.ncard_univ]
State after:
case a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ ncard (s ∪ t) ≤ ncard univ

State before:
case a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : Fintype.card α < ncard s + ncard t
h' : (s ∩ t)ᶜ = univ
⊢ ncard (s ∪ t) ≤ ncard univ
Tactic:
apply Set.ncard_le_ncard (subset_univ _)
State after:
no goals