diff --git a/src/data/finset/basic.lean b/src/data/finset/basic.lean
index 3e423d20e74f0..dd237068d0a01 100644
--- a/src/data/finset/basic.lean
+++ b/src/data/finset/basic.lean
@@ -1436,15 +1436,32 @@ lemma subtype_map_of_mem {p : α → Prop} [decidable_pred p] (h : ∀ x ∈ s,
   (s.subtype p).map (function.embedding.subtype _) = s :=
 by rw [subtype_map, filter_true_of_mem h]
 
+/-- If a `finset` of a subtype is converted to the main type with
+`embedding.subtype`, all elements of the result have the property of
+the subtype. -/
+lemma property_of_mem_map_subtype {p : α → Prop} (s : finset {x // p x}) {a : α}
+    (h : a ∈ s.map (function.embedding.subtype _)) : p a :=
+begin
+  rcases mem_map.1 h with ⟨x, hx, rfl⟩,
+  exact x.2
+end
+
 /-- If a `finset` of a subtype is converted to the main type with
 `embedding.subtype`, the result does not contain any value that does
 not satisfy the property of the subtype. -/
 lemma not_mem_map_subtype_of_not_property {p : α → Prop} (s : finset {x // p x})
     {a : α} (h : ¬ p a) : a ∉ (s.map (function.embedding.subtype _)) :=
+mt s.property_of_mem_map_subtype h
+
+/-- If a `finset` of a subtype is converted to the main type with
+`embedding.subtype`, the result is a subset of the set giving the
+subtype. -/
+lemma map_subtype_subset {t : set α} (s : finset t) :
+    ↑(s.map (function.embedding.subtype _)) ⊆ t :=
 begin
-  rw mem_map,
-  push_neg,
-  exact λ x, λ hxs hx, h (hx ▸ x.property)
+  intros a ha,
+  rw mem_coe at ha,
+  convert property_of_mem_map_subtype s ha
 end
 
 lemma subset_image_iff {f : α → β}