Theorem Definition:

        theorem Finset.card_powersetCard {α : Type u_1}  (n : ℕ)  (s : Finset α) : (powersetCard n s).card = s.card.choose n :=