Lean4
/-- Given a decidable predicate `p` and a proof of existence of `a ∈ l` such that `p a`,
choose the first element with this property. This version returns both `a` and proofs
of `a ∈ l` and `p a`. -/
def chooseX : ∀ l : List α, ∀ _ : ∃ a, a ∈ l ∧ p a, { a // a ∈ l ∧ p a }
| [], hp => False.elim (Exists.elim hp fun _ h => not_mem_nil h.left)
| l :: ls, hp =>
if pl : p l then ⟨l, ⟨mem_cons.mpr <| Or.inl rfl, pl⟩⟩
else
-- pattern matching on `hx` too makes this not reducible!
let ⟨a, ha⟩ := chooseX ls (hp.imp fun _ ⟨o, h₂⟩ => ⟨(mem_cons.mp o).resolve_left fun e => pl <| e ▸ h₂, h₂⟩)
⟨a, mem_cons.mpr <| Or.inr ha.1, ha.2⟩
