diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean
index da63e87c5..9c718ea27 100644
--- a/library/data/finset/basic.lean
+++ b/library/data/finset/basic.lean
@@ -553,6 +553,15 @@ subset_of_forall (take x, assume H : x ∈ s, mem_insert_of_mem _ H)
 theorem eq_of_subset_of_subset {s₁ s₂ : finset A} (H₁ : s₁ ⊆ s₂) (H₂ : s₂ ⊆ s₁) : s₁ = s₂ :=
 ext (take x, iff.intro (assume H, mem_of_subset_of_mem H₁ H) (assume H, mem_of_subset_of_mem H₂ H))
 
+section
+variable [decA : decidable_eq A]
+include decA
+
+theorem erase_subset_erase_of_subset {a : A} {s₁ s₂ : finset A} : s₁ ⊆ s₂ → erase a s₁ ⊆ erase a s₂ :=
+λ is_sub, subset_of_forall (λ b bin,
+  mem_erase_of_ne_of_mem (ne_of_mem_erase bin) (mem_of_subset_of_mem is_sub (mem_of_mem_erase bin)))
+end
+
 /- upto -/
 section upto
 definition upto (n : nat) : finset nat :=
diff --git a/library/data/finset/card.lean b/library/data/finset/card.lean
index 7cd2b72c4..4d6238f56 100644
--- a/library/data/finset/card.lean
+++ b/library/data/finset/card.lean
@@ -190,4 +190,24 @@ finset.induction_on s
                 card_union_of_disjoint H8, H6])
 end deceqB
 
+lemma eq_of_card_eq_of_subset {s₁ s₂ : finset A} : card s₁ = card s₂ → s₁ ⊆ s₂ → s₁ = s₂ :=
+have aux : ∀ (n : nat) (s₁ s₂ : finset A), card s₁ = n → card s₂ = n → s₁ ⊆ s₂ → s₁ = s₂,
+  begin
+    clear s₁ s₂,
+    intro n, induction n with n ih,
+      {intro s₁ s₂ e₁ e₂ is_sub, rewrite [empty_of_card_eq_zero e₁, empty_of_card_eq_zero e₂] },
+      {intro s₁ s₂ e₁ e₂ is_sub,
+       have ne : s₁ ≠ ∅, from non_empty_of_card_succ e₁,
+       cases (exists_of_not_empty ne) with a ains₁,
+       have ains₂ : a ∈ s₂,                    from mem_of_subset_of_mem is_sub ains₁,
+       have e₁' : card (erase a s₁) = n,       by rewrite [card_erase_of_mem ains₁, e₁],
+       have e₂' : card (erase a s₂) = n,       by rewrite [card_erase_of_mem ains₂, e₂],
+       have is_sub' : erase a s₁ ⊆ erase a s₂, from erase_subset_erase_of_subset is_sub,
+       have eq₁ : erase a s₁ = erase a s₂,     from ih _ _ e₁' e₂' is_sub',
+       have eq₂ : insert a (erase a s₁) = insert a (erase a s₂), by rewrite eq₁,
+       rewrite [insert_erase ains₁ at eq₂, insert_erase ains₂ at eq₂],
+       exact eq₂}
+  end,
+λ e h, aux (card s₂) s₁ s₂ e rfl h
+
 end finset