Get proof from a definition

Stream: lean4

[Nir Paz]

Is there a way to get a proof that is an argument to a choose statement in the goal, without explicitly writing the definition in code? For example:

import Mathlib

noncomputable section
open Classical

variable (α : Type*) (P : α → α → Prop)

-- random nonsense
variable (h : ∀ a : α, 0 = 0 → ℕ = ℕ → 0 < 1 → 1 = Nat.succ 0 → (∃ b, P a b))

-- chooses a witness from h
def foo : α → α := fun a ↦ by
  have h1 : 0 = 0 := rfl
  have h2 : ℕ = ℕ := rfl
  have h3 : 0 < 1 := zero_lt_one
  have h4 : 1 = Nat.succ 0 := rfl

  exact choose (h a h1 h2 h3 h4)

example (a : α) : P a (foo α P h a) := by
  dsimp [foo]
  exact choose_spec (h a foo.proof_1 (Eq.refl ℕ) foo.proof_2 foo.proof_3) -- stupid

The definition of foo can be very complicated and almost impossible to write in code in nontrivial examples. Is there a better way to do this in general, or even just to set a variable equal to the inside of the choose statement in the goal without defining it?

[Adam Topaz]

What about this?

example (a : α) : P a (foo α P h a) := by
  dsimp [foo]
  generalize_proofs f
  exact f.choose_spec

[Nir Paz]

Thanks that's great!