α✝ β : Type u
α : Type u_1
l : List α
h : ∀ (z : α), z ∈ l
⊢ (#α) ≤ ↑(List.length l)
α✝ β : Type u
α : Type u_1
l : List α
h : ↑(List.length l) < (#α)
⊢ ∃ z, ¬z ∈ l
contrapose! h
no goals
α✝ β : Type u
α : Type u_1
l : List α
h : ∀ (z : α), z ∈ l
⊢ (#α) ≤ ↑(List.length l)
calc
  (#α) = (#(Set.univ : Set α)) := mk_univ.symm
  _ ≤ (#l.toFinset) := mk_le_mk_of_subset fun x _ => List.mem_toFinset.mpr (h x)
  _ = l.toFinset.card := Cardinal.mk_coe_finset
  _ ≤ l.length := Cardinal.natCast_le.mpr (List.toFinset_card_le l)