Skip to content

Instantly share code, notes, and snippets.

@bryangingechen

bryangingechen/card_subsets_binomial.lean

Created November 13, 2018 18:03
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save bryangingechen/3f8e3fa3664bb4b044e9e607725cab1b to your computer and use it in GitHub Desktop.
Save bryangingechen/3f8e3fa3664bb4b044e9e607725cab1b to your computer and use it in GitHub Desktop.
Download ZIP
Raw
card_subsets_binomial.lean
import data.nat.choose
open finset nat
lemma not_mem_subset_range {n : ℕ} {t : finset ℕ} (H : t ⊆ range n) : n ∉ t :=
λ h, not_mem_range_self (mem_of_subset H h)
lemma card_subsets_of_range_eq_choose (n k : ℕ) :
card ((powerset (range n)).filter (λ t, card t = k)) = choose n k :=
match n, k with
|n, 0 :=
begin
rw choose_zero_right,
have : (powerset (range n)).filter (λ t, card t = 0) = finset.singleton ∅ :=
by { simp only [card_eq_zero],
ext,
simp,
split,
{ intro h₁,
exact h₁.2 },
{ intro h₁,
rw h₁, simp } },
rw this,
exact card_singleton ∅
end
|0, (k + 1) :=
begin
change _ = 0,
rw [card_eq_zero],
ext,
simp,
intro h,
rw [subset_empty] at h,
rw [h, card_empty],
contradiction
end
|(n + 1), (k + 1) :=
begin
change _ = choose n k + choose n (k + 1),
rw [←_match n k, ←_match n (k + 1)],
have : disjoint ((powerset (range n)).filter (λ t, card t = k))
((powerset (range n)).filter (λ t, card t = k + 1)) :=
by { change _ ∩ _ ⊆ ∅,
rw [subset_empty, ←filter_and],
ext t,
rw [mem_filter, mem_powerset],
split,
{ intro h,
have : card t = card t + 1 := (h.2.1).substr h.2.2,
exact not_succ_le_self (card t) (le_of_eq this.symm) },
{ intro h,
exact (not_mem_empty t h).elim } },
rw [←card_disjoint_union this, ←filter_or],
let f : finset ℕ → finset ℕ :=
λ t, if card t = k then insert n t else t,
let s : finset (finset ℕ) := (powerset (range n)).filter (λ t, card t = k ∨ card t = k + 1),
have hinj : ∀ x, x ∈ s → ∀ y, y ∈ s → f x = f y → x = y :=
by { intros x hx y hy h,
simp at hx hy,
by_cases H : card x = card y,
{ cases hy.2 with hk hk',
{ have hx' : card x = k := H.symm ▸ hk,
have Hx : f x = insert n x := if_pos hx',
have Hy : f y = insert n y := if_pos hk,
rw [Hx, Hy] at h,
have : erase (insert n x) n = erase (insert n y) n := congr_arg (λ s, erase s n) h,
have Hyy := erase_insert (not_mem_subset_range hy.1),
have Hxx := erase_insert (not_mem_subset_range hx.1),
rw [Hyy, Hxx] at this,
exact this },
{ have hx' : card x = k + 1 := H.symm ▸ hk',
have hx'' : card x ≠ k :=
by { intro h,
rw [hx'] at h,
revert h,
exact succ_ne_self k },
have hy'' : card y ≠ k :=
by { intro h,
rw [hk'] at h,
revert h,
exact succ_ne_self k },
have Hx : f x = x := if_neg hx'',
have Hy : f y = y := if_neg hy'',
rw [Hx, Hy] at h,
exact h } },
{ exfalso,
cases hy.2 with hk hk',
{ cases hx.2 with Hk Hk',
{ exact H (hk.symm ▸ Hk) },
{ have Hy : f y = insert n y := if_pos hk,
have Hx : f x = x :=
if_neg (by { intro h,
rw [Hk'] at h,
revert h,
exact succ_ne_self k }),
have : insert n y ⊆ range n := (Hy.subst (Hx.subst h.symm).symm).subst hx.1,
have HH : n ∈ insert n y := mem_insert.mpr (or.inl rfl),
exact not_mem_range_self (mem_of_subset this HH) } },
{ cases hx.2 with Hk Hk',
{ have Hx : f x = insert n x := if_pos Hk,
have Hy : f y = y :=
if_neg (by { intro h,
rw [hk'] at h,
revert h,
exact succ_ne_self k }),
have : insert n x ⊆ range n := (Hx.subst (Hy.subst h).symm).subst hy.1,
have HH : n ∈ insert n x := mem_insert.mpr (or.inl rfl),
exact not_mem_range_self (mem_of_subset this HH) },
{ exact H (hk'.symm ▸ Hk') } } } },
have hf : image f s = (powerset (range (n + 1))).filter (λ t, card t = k + 1) :=
by { ext t,
simp,
split,
{ intro h,
cases h with t' ht',
split,
{ by_cases card t' = k,
{ have : t = insert n t' := (if_pos h).subst ht'.2.symm,
rw this,
exact insert_subset_insert n ht'.1.1 },
{ have : t = t' := (if_neg h).subst ht'.2.symm,
rw this,
exact subset.trans ht'.1.1 (subset_insert n _) } },
{ by_cases card t' = k,
{ have : t = insert n t' := (if_pos h).subst ht'.2.symm,
rw this,
have H : n ∉ t' := not_mem_subset_range ht'.1.1,
exact h ▸ (card_insert_of_not_mem H) },
{ have : t = t' := (if_neg h).subst ht'.2.symm,
rw this,
cases ht'.1.2,
{ exact (h h_1).elim },
{ exact h_1 } } } },
{ intro h,
by_cases H : n ∈ t,
{ exact ⟨erase t n,
⟨⟨(by { rw subset_iff,
intros i hi,
have hi' : i ∈ t := mem_of_mem_erase hi,
have hih : i ∈ insert n (range n) := mem_of_subset h.1 hi',
have hie : i ≠ n := (mem_erase.mp hi).1,
have : i = n ∨ i ∈ range n := mem_insert.mp hih,
exact or.elim this (λ hh, (hie hh).elim) id }),
or.inl (by { have : card (erase t n) = pred (card t) := (card_erase_of_mem H),
rw [this, h.2, pred_succ] })⟩,
(by { have : card (erase t n) = k := calc
card (erase t n) = card t - 1 : card_erase_of_mem H
... = (k + 1) - 1 : by rw h.2,
have H' : f (erase t n) = insert n (erase t n) := if_pos this,
rw [H', insert_erase H] })⟩⟩ },
{ exact ⟨t, ⟨⟨(by { rw [subset_iff] at h ⊢,
intros x hx,
have : x ∈ insert n (range n) := h.1 hx,
rw [mem_insert] at this,
cases this,
{ exact (H (this_1 ▸ hx)).elim },
{ exact this_1 } }),
or.inr h.2⟩,
if_neg (by { intro h',
rw h.2 at h',
revert h',
exact succ_ne_self k })⟩⟩ } } },
rw [←hf],
exact card_image_of_inj_on hinj
end
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment