diff --git a/src/algebra/big_operators.lean b/src/algebra/big_operators.lean
index 689af00eee446..066f144c92fe7 100644
--- a/src/algebra/big_operators.lean
+++ b/src/algebra/big_operators.lean
@@ -713,6 +713,50 @@ begin
     { simp only [mem_image], rintro ⟨⟨_, hm⟩, _, rfl⟩, exact ha hm } }
 end
 
+open_locale classical
+
+/-- The product of `f a + g a` over all of `s` is the sum
+  over the powerset of `s` of the product of `f` over a subset `t` times
+  the product of `g` over the complement of `t`  -/
+lemma prod_add (f g : α → β) (s : finset α) :
+  s.prod (λ a, f a + g a) =
+  s.powerset.sum (λ t : finset α, t.prod f * (s \ t).prod g) :=
+calc s.prod (λ a, f a + g a)
+    = s.prod (λ a, ({false, true} : finset Prop).sum
+      (λ p : Prop, if p then f a else g a)) : by simp
+... = (s.pi (λ _, {false, true})).sum (λ p : Π a ∈ s, Prop,
+      s.attach.prod (λ a : {a // a ∈ s}, if p a.1 a.2 then f a.1 else g a.1)) : prod_sum
+... = s.powerset.sum (λ (t : finset α), t.prod f * (s \ t).prod g) : begin
+  refine eq.symm (sum_bij (λ t _ a _, a ∈ t) _ _ _ _),
+  { simp [subset_iff]; tauto },
+  { intros t ht,
+    erw [prod_ite (λ a : {a // a ∈ s}, f a.1) (λ a : {a // a ∈ s}, g a.1)],
+    refine congr_arg2 _
+      (prod_bij (λ (a : α) (ha : a ∈ t), ⟨a, mem_powerset.1 ht ha⟩)
+         _ _ _
+        (λ b hb, ⟨b, by cases b; finish⟩))
+      (prod_bij (λ (a : α) (ha : a ∈ s \ t), ⟨a, by simp * at *⟩)
+        _ _ _
+        (λ b hb, ⟨b, by cases b; finish⟩));
+    intros; simp * at *; simp * at * },
+  { finish [function.funext_iff, finset.ext, subset_iff] },
+  { assume f hf,
+    exact ⟨s.filter (λ a : α, ∃ h : a ∈ s, f a h),
+      by simp, by funext; intros; simp *⟩ }
+end
+
+/--  Summing `a^s.card * b^(n-s.card)` over all finite subsets `s` of a `finset`
+gives `(a + b)^s.card`.-/
+lemma sum_pow_mul_eq_add_pow
+  {α R : Type*} [comm_semiring R] (a b : R) (s : finset α) :
+  s.powerset.sum (λ t : finset α, a ^ t.card * b ^ (s.card - t.card)) =
+  (a + b) ^ s.card :=
+begin
+  rw [← prod_const, prod_add],
+  refine finset.sum_congr rfl (λ t ht, _),
+  rw [prod_const, prod_const, ← card_sdiff (mem_powerset.1 ht)]
+end
+
 lemma prod_pow_eq_pow_sum {x : β} {f : α → ℕ} :
   ∀ {s : finset α}, s.prod (λ i, x ^ (f i)) = x ^ (s.sum f) :=
 begin
diff --git a/src/data/fin.lean b/src/data/fin.lean
index 2d18d330f754a..c44bf5e453a61 100644
--- a/src/data/fin.lean
+++ b/src/data/fin.lean
@@ -91,12 +91,19 @@ lemma mk_val {m n : ℕ} (h : m < n) : (⟨m, h⟩ : fin n).val = m := rfl
 
 lemma coe_eq_val (a : fin n) : (a : ℕ) = a.val := rfl
 
+attribute [simp] val_zero
 @[simp] lemma val_one  {n : ℕ} : (1 : fin (n+2)).val = 1 := rfl
 @[simp] lemma val_two  {n : ℕ} : (2 : fin (n+3)).val = 2 := rfl
 @[simp] lemma coe_zero {n : ℕ} : ((0 : fin (n+1)) : ℕ) = 0 := rfl
 @[simp] lemma coe_one  {n : ℕ} : ((1 : fin (n+2)) : ℕ) = 1 := rfl
 @[simp] lemma coe_two  {n : ℕ} : ((2 : fin (n+3)) : ℕ) = 2 := rfl
 
+/-- Assume `k = l`. If two functions defined on `fin k` and `fin l` are equal on each element,
+then they coincide (in the heq sense). -/
+protected lemma heq {α : Type*} {k l : ℕ} (h : k = l) {f : fin k → α} {g : fin l → α}
+  (H : ∀ (i : fin k), f i = g ⟨i.val, lt_of_lt_of_le i.2 (le_of_eq h)⟩) : f == g :=
+by { induction h, rw heq_iff_eq, ext i, convert H i, exact (fin.ext_iff _ _).mpr rfl }
+
 instance {n : ℕ} : decidable_linear_order (fin n) :=
 decidable_linear_order.lift fin.val (@fin.eq_of_veq _) (by apply_instance)
 
diff --git a/src/data/finset.lean b/src/data/finset.lean
index d08e68d7b0aa4..e7f51b7a4d76d 100644
--- a/src/data/finset.lean
+++ b/src/data/finset.lean
@@ -2222,6 +2222,13 @@ def mono_of_fin (s : finset α) {k : ℕ} (h : s.card = k) (i : fin k) : α :=
 have A : (i : ℕ) < (s.sort (≤)).length, by simpa [h] using i.2,
 (s.sort (≤)).nth_le i A
 
+lemma mono_of_fin_strict_mono (s : finset α) {k : ℕ} (h : s.card = k) :
+  strict_mono (s.mono_of_fin h) :=
+begin
+  assume i j hij,
+  exact list.pairwise_iff_nth_le.1 s.sort_sorted_lt _ _ _ hij
+end
+
 lemma bij_on_mono_of_fin (s : finset α) {k : ℕ} (h : s.card = k) :
   set.bij_on (s.mono_of_fin h) set.univ ↑s :=
 begin
@@ -2230,8 +2237,7 @@ begin
   { assume i hi,
     simp only [mono_of_fin, set.mem_preimage, mem_coe, list.nth_le, A],
     exact list.nth_le_mem _ _ _ },
-  { refine (strict_mono.injective (λ i j hij, _)).inj_on _,
-    exact list.pairwise_iff_nth_le.1 s.sort_sorted_lt _ _ _ hij },
+  { exact ((mono_of_fin_strict_mono s h).injective).inj_on _ },
   { assume x hx,
     simp only [mem_coe, A] at hx,
     obtain ⟨i, il, hi⟩ : ∃ (i : ℕ) (h : i < (s.sort (≤)).length), (s.sort (≤)).nth_le i h = x :=
@@ -2240,6 +2246,64 @@ begin
     exact ⟨⟨i, il⟩, set.mem_univ _, hi⟩ }
 end
 
+/-- The bijection `mono_of_fin s h` sends `0` to the minimum of `s`. -/
+lemma mono_of_fin_zero {s : finset α} {k : ℕ} (h : s.card = k) (hs : s.nonempty) (hz : 0 < k) :
+  mono_of_fin s h ⟨0, hz⟩ = s.min' hs :=
+begin
+  apply le_antisymm,
+  { have : min' s hs ∈ s := min'_mem s hs,
+    rcases (bij_on_mono_of_fin s h).surj_on this with ⟨a, _, ha⟩,
+    rw ← ha,
+    apply (mono_of_fin_strict_mono s h).monotone,
+    exact zero_le a.val },
+  { have : mono_of_fin s h ⟨0, hz⟩ ∈ s := (bij_on_mono_of_fin s h).maps_to (set.mem_univ _),
+    exact min'_le s hs _ this }
+end
+
+/-- The bijection `mono_of_fin s h` sends `k-1` to the maximum of `s`. -/
+lemma mono_of_fin_last {s : finset α} {k : ℕ} (h : s.card = k) (hs : s.nonempty) (hz : 0 < k) :
+  mono_of_fin s h ⟨k-1, buffer.lt_aux_2 hz⟩ = s.max' hs :=
+begin
+  have h'' : k - 1 < k := buffer.lt_aux_2 hz,
+  apply le_antisymm,
+  { have : mono_of_fin s h ⟨k-1, h''⟩ ∈ s := (bij_on_mono_of_fin s h).maps_to (set.mem_univ _),
+    exact le_max' s hs _ this },
+  { have : max' s hs ∈ s := max'_mem s hs,
+    rcases (bij_on_mono_of_fin s h).surj_on this with ⟨a, _, ha⟩,
+    rw ← ha,
+    apply (mono_of_fin_strict_mono s h).monotone,
+    exact le_pred_of_lt a.2},
+end
+
+/-- Any increasing bijection between `fin k` and a finset of cardinality `k` has to coincide with
+the increasing bijection `mono_of_fin s h`. For a statement assuming only that `f` maps `univ` to
+`s`, see `mono_of_fin_unique'`.-/
+lemma mono_of_fin_unique {s : finset α} {k : ℕ} (h : s.card = k) {f : fin k → α}
+  (hbij : set.bij_on f set.univ ↑s) (hmono : strict_mono f) : f = s.mono_of_fin h :=
+begin
+  ext i,
+  rcases i with ⟨i, hi⟩,
+  induction i using nat.strong_induction_on with i IH,
+  rcases lt_trichotomy (f ⟨i, hi⟩) (mono_of_fin s h ⟨i, hi⟩) with H|H|H,
+  { have A : f ⟨i, hi⟩ ∈ ↑s := hbij.maps_to (set.mem_univ _),
+    rcases (bij_on_mono_of_fin s h).surj_on A with ⟨j, _, hj⟩,
+    rw ← hj at H,
+    have ji : j < ⟨i, hi⟩ := (mono_of_fin_strict_mono s h).lt_iff_lt.1 H,
+    have : f j = mono_of_fin s h j,
+      by { convert IH j.1 ji (lt_trans ji hi), rw fin.ext_iff },
+    rw ← this at hj,
+    exact (ne_of_lt (hmono ji) hj).elim },
+  { exact H },
+  { have A : mono_of_fin s h ⟨i, hi⟩ ∈ ↑s := (bij_on_mono_of_fin s h).maps_to (set.mem_univ _),
+    rcases hbij.surj_on A with ⟨j, _, hj⟩,
+    rw ← hj at H,
+    have ji : j < ⟨i, hi⟩ := hmono.lt_iff_lt.1 H,
+    have : f j = mono_of_fin s h j,
+      by { convert IH j.1 ji (lt_trans ji hi), rw fin.ext_iff },
+    rw this at hj,
+    exact (ne_of_lt (mono_of_fin_strict_mono s h ji) hj).elim }
+end
+
 /-- Given a finset `s` of cardinal `k` in a linear order `α`, the equiv `mono_equiv_of_fin s h`
 is the increasing bijection between `fin k` and `s` as an `s`-valued map. Here, `h` is a proof that
 the cardinality of `s` is `k`. We use this instead of a map `fin s.card → α` to avoid
@@ -2342,6 +2406,10 @@ disjoint_iff_ne.2 $ λ f₁ hf₁ f₂ hf₂ eq₁₂,
   disjoint_iff_ne.1 h (f₁ a ha) (mem_pi.mp hf₁ a ha) (f₂ a ha) (mem_pi.mp hf₂ a ha)
   $ congr_fun (congr_fun eq₁₂ a) ha
 
+lemma disjoint_iff_disjoint_coe {α : Type*} {a b : finset α} [decidable_eq α] :
+  disjoint a b ↔ disjoint (↑a : set α) (↑b : set α) :=
+by { rw [finset.disjoint_left, set.disjoint_left], refl }
+
 end disjoint
 
 instance [has_repr α] : has_repr (finset α) := ⟨λ s, repr s.1⟩
@@ -2527,6 +2595,9 @@ by ext k; by_cases n ≤ k; simp [h, this]
 
 end Ico
 
+lemma range_eq_Ico (n : ℕ) : finset.range n = finset.Ico 0 n :=
+by { ext i, simp }
+
 -- TODO We don't yet attempt to reproduce the entire interface for `Ico` for `Ico_ℤ`.
 
 /-- `Ico_ℤ l u` is the set of integers `l ≤ k < u`. -/
diff --git a/src/data/fintype.lean b/src/data/fintype.lean
index cf918c46a79d5..b736f0b92c71f 100644
--- a/src/data/fintype.lean
+++ b/src/data/fintype.lean
@@ -263,6 +263,21 @@ begin
     exact fin.eq_last_of_not_lt h }
 end
 
+/-- Any increasing map between `fin k` and a finset of cardinality `k` has to coincide with
+the increasing bijection `mono_of_fin s h`. -/
+lemma finset.mono_of_fin_unique' [decidable_linear_order α] {s : finset α} {k : ℕ} (h : s.card = k)
+  {f : fin k → α} (fmap : set.maps_to f set.univ ↑s) (hmono : strict_mono f) :
+  f = s.mono_of_fin h :=
+begin
+  have finj : set.inj_on f set.univ := hmono.injective.inj_on _,
+  apply mono_of_fin_unique h (set.bij_on.mk fmap finj (λ y hy, _)) hmono,
+  simp only [set.image_univ, set.mem_range],
+  rcases surj_on_of_inj_on_of_card_le (λ i (hi : i ∈ finset.univ), f i)
+    (λ i hi, fmap (set.mem_univ i)) (λ i j hi hj hij, finj (set.mem_univ i) (set.mem_univ j) hij)
+    (by simp [h]) y hy with ⟨x, _, hx⟩,
+  exact ⟨x, hx.symm⟩
+end
+
 @[instance, priority 10] def unique.fintype {α : Type*} [unique α] : fintype α :=
 ⟨finset.singleton (default α), λ x, by rw [unique.eq_default x]; simp⟩
 
@@ -432,6 +447,10 @@ have injective (e.symm ∘ f) ↔ surjective (e.symm ∘ f), from fintype.inject
 λ hsurj, by simpa [function.comp] using
   injective_comp e.injective (this.2 (surjective_comp e.symm.surjective hsurj))⟩
 
+lemma fintype.coe_image_univ [fintype α] [decidable_eq β] {f : α → β} :
+  ↑(finset.image f finset.univ) = set.range f :=
+by { ext x, simp }
+
 instance list.subtype.fintype [decidable_eq α] (l : list α) : fintype {x // x ∈ l} :=
 fintype.of_list l.attach l.mem_attach
 
diff --git a/src/data/fintype/card.lean b/src/data/fintype/card.lean
index 0e6de1c6fdd17..295738af1b662 100644
--- a/src/data/fintype/card.lean
+++ b/src/data/fintype/card.lean
@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Mario Carneiro
 -/
 
-import data.fintype
-import algebra.big_operators
+import data.fintype algebra.big_operators data.nat.choose tactic.ring
 
 /-!
 Results about "big operations" over a `fintype`, and consequent
@@ -116,3 +115,18 @@ begin
     ext a ha,
     exact (congr_fun hfg a : _) }
 end
+
+/-- Summing `a^s.card * b^(n-s.card)` over all finite subsets `s` of a fintype of cardinality `n`
+gives `(a + b)^n`. The "good" proof involves expanding along all coordinates using the fact that
+`x^n` is multilinear, but multilinear maps are only available now over rings, so we give instead
+a proof reducing to the usual binomial theorem to have a result over semirings. -/
+lemma fintype.sum_pow_mul_eq_add_pow
+  (α : Type*) [fintype α] {R : Type*} [comm_semiring R] (a b : R) :
+  finset.univ.sum (λ (s : finset α), a ^ s.card * b ^ (fintype.card α - s.card)) =
+  (a + b) ^ (fintype.card α) :=
+finset.sum_pow_mul_eq_add_pow _ _ _
+
+lemma fin.sum_pow_mul_eq_add_pow {n : ℕ} {R : Type*} [comm_semiring R] (a b : R) :
+  finset.univ.sum (λ (s : finset (fin n)), a ^ s.card * b ^ (n - s.card)) =
+  (a + b) ^ n :=
+by simpa using fintype.sum_pow_mul_eq_add_pow (fin n) a b