Getting witness from existentially quantified statement

Stream: new members

[George Tsoukalas]

Hi all,

I have a theorem which states the existence of an element satisfying a property, quantified over all elements:

theorem ex
(S : Type*)
(P : S → S → Prop)
: ∀ x, ∃ y, P x y
:= sorry

-- How to make function S → S which takes in x and "outputs" the y which satisfies P x y?

I would like to define a function which maps (x : S) to the y that exists (afforded by theorem ex). How can I go about this? How close is what I am looking for to definitional equivalence of the statement of ex?

[Eric Rodriguez]

docs#Exists.choose

[George Tsoukalas]

Of course! Thank you!

[Sébastien Gouëzel]

Or the choose tactic if you're in the middle of a proof.