ignore proof obligations

Stream: Is there code for X?

[Aaron Liu]

Is there a canonical way to get an element hidden under a proof obligation if it's defined and get an arbitrary thing otherwise? Something like this:

noncomputable example {α : Sort u} [Nonempty α] {P : Prop} (x : P → α) : α :=
  open scoped Classical in
  if h : P then x h else Classical.ofNonempty

[Jakub Nowak]

Part.getOrElse is somewhat similar. It takes the default as an argument though.

[Sébastien Gouëzel]

docs#Classical.epsilon