Taking element from non-empty set

Stream: Is there code for X?

[sty]

Hi, I'm fairly new to Lean, which could be why I'm failing to find something I'd really expect to exist in mathlib.
Essentially I'd like to have a way to take an element from a set that I know is non-empty. Currently I'm using the following, but there's probably a cleaner alternative:

constant element {γ: Type*} {S: set γ}: S ≠ ∅ -> S

[Eric Wieser]

docs#set.nonempty_iff_ne_empty, so you can implement that with (set.nonempty_iff_ne_empty.mpr h).some

[Eric Wieser]

The explanation is that S ≠ ∅ is not the preferred spelling of saying that a set is not empty, S.nonempty is

[Kevin Buzzard]

As far as lean's concerned, this is the axiom of choice, by the way

[Eric Wieser]

Right, as explained in docs#set.nonempty.some

[Eric Wieser]

Note that if you're in a proof and your step is "pick an arbitrary element from the nonempty set", often you don't need to use choice, and can just use the cases tactic

[sty]

Eric Wieser said:

Note that if you're in a proof and your step is "pick an arbitrary element from the nonempty set", often you don't need to use choice, and can just use the cases tactic

How do I use cases in such a way?

[Eric Wieser]

If you have h : S.nonempty then use cases h with x hx

[Kevin Buzzard]

You've asked for a function which needs a nonconstructive proof, but if actually your goal is a Prop then you don't need to move from the Prop world to the Type world so you can avoid AC/nonconstructivism. The cases tactic won't eliminate into Type but it will work in tactic mode if your goal is a Prop.