exists element in nonempty set

Stream: new members

[Lucas V.]

I feel this is very simple, but library_search is not helping me:

lemma exists_element (a : set α) : ¬(a = ∅) → ∃x, x ∈ a :=
    by library_search

It fails :(
Is there something like this in the library? Or am I missing something?

(side question: does library_search also search in the default libraries?)

[Alex J. Best]

I'm not sure why library search doesn't find this: set.ne_empty_iff_nonempty.mp, maybe because the way the library writes the right hand side is just a.nonempty now.

[Lucas V.]

If I write a.nonempty it actually suggests using nmem_singleton_empty.mp

[Alex J. Best]

Yeah I saw that, library search doesn't always find the perfect answer, if you do by suggest instead the second suggestion is better here.

[Lucas V.]

Uuh, didn't know about suggest, thank you :)

[Kevin Buzzard]

The canonical way of writing $a\not=\emptyset$ in Lean is a.nonempty(maybe set.nonempty(a) looks better for mathematicians?), so the library lemmas will be stated in this form.