feat(data/set/basic): nonempty set of nonempty subtype (#5373)

leanprover-community · Dec 15, 2020 · 75130b3 · 75130b3
1 parent d21d17b
commit 75130b3
Showing 1 changed file with 3 additions and 0 deletions.
diff --git 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