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

State before:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ Set.Nonempty (sᶜ ∩ tᶜ)
Tactic:
apply Set.ncard_pigeonhole
State after:
case h
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ Fintype.card α < ncard sᶜ + ncard tᶜ

State before:
case h
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ Fintype.card α < ncard sᶜ + ncard tᶜ
Tactic:
apply Nat.lt_of_add_lt_add_left
State after:
case h.a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ?h.n + Fintype.card α < ?h.n + (ncard sᶜ + ncard tᶜ)

case h.n
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ℕ

State before:
case h.a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ?h.n + Fintype.card α < ?h.n + (ncard sᶜ + ncard tᶜ)

case h.n
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ℕ
Tactic:
rw [← add_assoc, Set.ncard_add_ncard_compl]
State after:
case h.a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ncard s + Fintype.card α < Nat.card α + ncard tᶜ

State before:
case h.a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ncard s + Fintype.card α < Nat.card α + ncard tᶜ
Tactic:
simp only [Nat.card_eq_fintype_card, add_comm, add_lt_add_iff_left]
State after:
case h.a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ncard s < ncard tᶜ

State before:
case h.a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ncard s < ncard tᶜ
Tactic:
apply Nat.lt_of_add_lt_add_left
State after:
case h.a.a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ?h.a.n + ncard s < ?h.a.n + ncard tᶜ

case h.a.n
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ℕ

State before:
case h.a.a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ?h.a.n + ncard s < ?h.a.n + ncard tᶜ

case h.a.n
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ℕ
Tactic:
rw [Set.ncard_add_ncard_compl, Nat.card_eq_fintype_card, add_comm]
State after:
case h.a.a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ncard s + ncard t < Fintype.card α

State before:
case h.a.a
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
⊢ ncard s + ncard t < Fintype.card α
Tactic:
exact h
State after:
no goals