diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
index 91d5a1a7c7a3f..79e1cf73919c8 100644
--- a/src/data/set/basic.lean
+++ b/src/data/set/basic.lean
@@ -315,6 +315,9 @@ nonempty_subtype.2 h
 
 @[simp] lemma nonempty_insert (a : α) (s : set α) : (insert a s).nonempty := ⟨a, or.inl rfl⟩
 
+@[simp] lemma nonempty_of_nonempty_subtype [nonempty s] : s.nonempty :=
+nonempty_subtype.mp ‹_›
+
 /-! ### Lemmas about the empty set -/
 
 theorem empty_def : (∅ : set α) = {x | false} := rfl