Eliminating a set into an element

Stream: new members

[Yakov Pechersky]

I have a function f : x \to option y that is injective over all the some y values in the codomain. I'm trying to define a function that retrieves the x that has f x = y, if I also know that f is surjective. I can say that {x | f x = y} for some fixed y is a subsingleton, due to the injectivity, and is nonempty, due to the surjectivity.

Is there some definition that lets me eliminate a singleton set back into the element it's made from? That is, I can (I think) show that a set that is a singleton from subsingleton and nonempty. Is there some better way of expressing this? I couldn't find a mathlib way of expressing "partially injective".

[Johan Commelin]

classical.some (h : s.nonempty) will give you an element of s.

[Yakov Pechersky]

But in a noncomputable way, correct?

[Yury G. Kudryashov]

There is no computable way to invert a function.

[Eric Wieser]

Does lean mathlib have the computable brute-force def for doing so given [fintype x]?

[Yakov Pechersky]

Eric's on the same thought as me

[Reid Barton]

You mean, "Does mathlib have ..."

[Bryan Gin-ge Chen]

You might need encodable as well.

[Yury G. Kudryashov]

Let me try docs#finset.choose

[Bryan Gin-ge Chen]

Oh, maybe docs#fintype.bij_inv

[Adam Topaz]

docs#fintype.choose I assume?