Defining witness function without choice

Stream: new members

[Nir Paz]

How can I fill these sorrys

variable {α : Type _} {P : α → α → Prop} (h : ∀ x : α, ∃! y : α, P x y)

def f : α → α := sorry

theorem spec (x : α) : P x (f x) := sorry

so that the definition of f and the theorem don't use the axiom of choice? I'm hoping there's a simple way to just "pick that y," but I can't figure out how.

[Eric Wieser]

I think the closest you can get is docs#Fintype.choose

[Ruben Van de Velde]

You can't

[Kevin Buzzard]

In set theory you wouldn't need AC but in type theory you do because you're moving from Prop (the statement that something exists) to Type (the thing that exists) and in lean's type theory this is impossible to do computably.