α✝ β α : Type u
n : ℕ
H : ∀ (s : Finset α), Finset.card s ≤ n
hn : (#α) ≥ succ ↑n
⊢ False
α✝ β α : Type u
n : ℕ
H : ∀ (s : Finset α), Finset.card s ≤ n
⊢ (#α) ≤ ↑n
refine' le_of_lt_succ (lt_of_not_ge fun hn => _)
α✝ β α : Type u
n : ℕ
H : ∀ (s : Finset α), Finset.card s ≤ n
hn : (#α) ≥ lift (#Fin (Nat.succ n))
⊢ False
α✝ β α : Type u
n : ℕ
H : ∀ (s : Finset α), Finset.card s ≤ n
hn : (#α) ≥ succ ↑n
⊢ False
rw [← Cardinal.nat_succ, ← lift_mk_fin n.succ] at hn
case intro
α✝ β α : Type u
n : ℕ
H : ∀ (s : Finset α), Finset.card s ≤ n
f : ULift (Fin (Nat.succ n)) ↪ α
⊢ False
α✝ β α : Type u
n : ℕ
H : ∀ (s : Finset α), Finset.card s ≤ n
hn : (#α) ≥ lift (#Fin (Nat.succ n))
⊢ False
cases' hn with f
case intro
α✝ β α : Type u
n : ℕ
H : ∀ (s : Finset α), Finset.card s ≤ n
f : ULift (Fin (Nat.succ n)) ↪ α
⊢ n < Finset.card (Finset.map f Finset.univ)
case intro
α✝ β α : Type u
n : ℕ
H : ∀ (s : Finset α), Finset.card s ≤ n
f : ULift (Fin (Nat.succ n)) ↪ α
⊢ False
refine' (H <| Finset.univ.map f).not_lt _
case intro
α✝ β α : Type u
n : ℕ
H : ∀ (s : Finset α), Finset.card s ≤ n
f : ULift (Fin (Nat.succ n)) ↪ α
⊢ n < Nat.succ n
case intro
α✝ β α : Type u
n : ℕ
H : ∀ (s : Finset α), Finset.card s ≤ n
f : ULift (Fin (Nat.succ n)) ↪ α
⊢ n < Finset.card (Finset.map f Finset.univ)
rw [Finset.card_map, ← Fintype.card, Fintype.card_ulift, Fintype.card_fin]
no goals
case intro
α✝ β α : Type u
n : ℕ
H : ∀ (s : Finset α), Finset.card s ≤ n
f : ULift (Fin (Nat.succ n)) ↪ α
⊢ n < Nat.succ n
exact n.lt_succ_self