Binomial coefficients

Stream: Is there code for X?

[Vincent Beffara]

Does mathlib know that the number of subsets of fin n that have k elements is given by a binomial coefficient? I am especially looking for a special case:

example {n : ℕ} :
  (finset.univ : finset {s : finset (fin (1 + n)) // s.card = n}).card = 1 + n :=
sorry

[Junyan Xu]

docs#finset.card_powerset_len

[Junyan Xu]

docs#finset.powerset_len_eq_filter