Existence elimination in Lean 3

Question

Lean 3 is a theorem prover that implements the calculus of inductive constructions. Differently than Coq, Lean 3s kernel works proof irrelevant. This means that in the kernel of Lean all proofs of the same theorem are judgmentally (definitionally) equal and can be substituted for each other.

Does that mean that if I have A : Type, P : A -> Prop, and p : (∃ x : A, P x), then there is no way to extract an actual w : A from p which satisfies P w?

I thought being able to extract witnesses from existence proofs is one of the main arguments for Martin-Löf style type theories.

Answer 1

Indeed, in general there is no way how to extract an actual witness w for p w out of a proof ∃ x : A, p x. And the correct reference was given by Ali in the comments. In the documentation the result

noncomputable theorem indefinite_description
{α : Sort*} (p : α → Prop) : (∃ x, p x) → {x // p x}

uses the choice axiom

axiom choice {α : Sort*} : nonempty α → α

in its derivation, and it is also mentioned that propext, funext, and choice taken together imply the law of excluded middle. But this is, as mentioned at the start, in general. There are types A for which we can extract witnesses (i.e. we can prove an instance of indefinite_description), and the most prominent example is for decidable predicates on nat. But more generally, it holds for encodable types and decidable predicates. This can be found in the Lean standard library under the name encodable.choose_x