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 α
⊢ s ∪ t ≠ ⊤
Tactic:
intro h'
State after:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
h' : s ∪ t = ⊤
⊢ False

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

State before:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
h' : s ∪ t = ⊤
⊢ Fintype.card α ≤ ncard s + ncard t
Tactic:
rw [← Nat.card_eq_fintype_card, ← Set.ncard_univ, ← top_eq_univ, ← h']
State after:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
h' : s ∪ t = ⊤
⊢ ncard (s ∪ t) ≤ ncard s + ncard t

State before:
α : Type u_1
inst✝ : Fintype α
s t : Set α
h : ncard s + ncard t < Fintype.card α
h' : s ∪ t = ⊤
⊢ ncard (s ∪ t) ≤ ncard s + ncard t
Tactic:
exact ncard_union_le s t
State after:
no goals