Lean proof that the cardinality of the k-subsets of n is n choose k.

choose_subsets.lean

import data.finset data.nat.choose

variables {α : Type*} [decidable_eq α]

namespace finset

/-
`insert_empty_eq_singleton` in the library should be replaced by this.
-/
theorem insert_empty_eq_singleton' (a : α) : insert a ∅ = finset.singleton a := rfl

theorem filter_insert (p : α → Prop) [decidable_pred p] (s : finset α) (a : α) :
  filter p (insert a s) = if p a then insert a (filter p s) else filter p s :=
by ext x; split_ifs; by_cases x = a; simp [finset.mem_filter, *]

theorem filter_singleton (p : α → Prop) [decidable_pred p] (a : α) :
  filter p (finset.singleton a) = if p a then finset.singleton a else ∅ :=
by rw [←insert_empty_eq_singleton', filter_insert, filter_empty]

@[simp] theorem powerset_empty : powerset (∅ : finset α) = {∅} :=
by ext x; simp [subset_empty]

theorem powerset_insert (a : α) (s : finset α) :
  powerset (insert a s) = powerset s ∪ (powerset s).image (insert a) :=
begin
  ext t; simp, split,
  { by_cases has : a ∈ s,
    { simp [has], {exact λ h, or.inl h} },
    intro h,
    by_cases ts : a ∈ t,
    { right, exact ⟨erase t a, subset_insert_iff.mp h, insert_erase ts⟩ },
    left, intros x xt, apply mem_of_mem_insert_of_ne (h xt),
    intro xeq, rw xeq at xt, contradiction },
  intro h, rcases h with xsubs | ⟨u, usubs, hu⟩,
  { exact subset.trans xsubs (subset_insert _ _) },
  rw [←hu, insert_subset],
  exact ⟨mem_insert_self a s, subset.trans usubs (subset_insert _ _)⟩
end

end finset

open finset

-- better name?

theorem card_subsets_eq_choose (s : finset α) :
  ∀ k, card ((powerset s).filter (λ t, card t = k)) = choose (card s) k :=
finset.induction_on s
begin
  intro k, induction k,
  { simp [filter_empty, filter_singleton] },
  simp [filter_singleton], split_ifs; simp, contradiction
end
begin
  intros a s anins ih k,
  induction k with k ih',
  { have : card (finset.singleton (∅ : finset α)) = 1, by simp,
    convert this; simp,
    ext x, split; simp; intro h; simp [h] },
  simp [anins, powerset_insert, filter_union],
  let s₁ := filter (λ t, card t = nat.succ k) (powerset s),
  let s₂ := filter (λ t, card t = nat.succ k) (image (insert a) (powerset s)),
  have : disjoint s₁ s₂,
  { rw disjoint_iff_inter_eq_empty, ext t, simp,
    intros tsubs _ u usubs teq _,
    have : a ∈ t, by rw [←teq]; apply mem_insert_self,
    show false, from anins (subset_iff.mp tsubs this) },
  rw [card_disjoint_union this],
  have : s₂ = image (insert a) (filter (λ (t : finset α), card t = k) (powerset s)),
  { ext u, rw [mem_filter, mem_image, mem_image], split,
    { rintros ⟨⟨t, tmem, ueq⟩, cardu⟩,
      have : a ∉ t, from λ h, anins (subset_iff.mp (mem_powerset.mp tmem) h),
      have : card t = k,
      { rw [←ueq, card_insert_of_not_mem this] at cardu, exact nat.succ.inj cardu },
      refine ⟨t, _, ueq⟩, rw mem_filter, exact ⟨tmem, this⟩ },
    rintros ⟨t, tmem, ht⟩, rw mem_filter at tmem,
    refine ⟨⟨t, tmem.left, ht⟩, _⟩,
    have : a ∉ t, from λ h, anins (subset_iff.mp (mem_powerset.mp tmem.left) h),
    rw [←ht, card_insert_of_not_mem this, tmem.right] },
  rw [this, card_image_of_inj_on, ih, ih, choose_succ_succ, add_comm],
  intros x xmem y ymem e,
  have : x ⊆ s, from mem_powerset.mp (filter_subset _ xmem),
  have aninx : a ∉ x, from λ h, anins (mem_of_subset this h),
  have : y ⊆ s, from mem_powerset.mp (filter_subset _ ymem),
  have aniny : a ∉ y, from λ h, anins (mem_of_subset this h),
  rw [←erase_insert aninx, ←erase_insert aniny, e]
end