case h2
α : Type u_1
inst✝ : Infinite α
s : Finset α
⊢ (#↑↑s) < (#α)
α : Type u_1
inst✝ : Infinite α
s : Finset α
⊢ (#↑(↑sᶜ)) = (#α)
apply mk_compl_of_infinite
no goals
case h2
α : Type u_1
inst✝ : Infinite α
s : Finset α
⊢ (#↑↑s) < (#α)
exact (finset_card_lt_aleph0 s).trans_le (aleph0_le_mk α)