rintro rfl
α : Sort u_1
p : α → Prop
r : α → α → Prop
h : ∀ (x : α), p x → ∃! y, r x y
default x y : α
hpx : p x
⊢ y = extendedChoose! h default x → r x y
α : Sort u_1
p : α → Prop
r : α → α → Prop
h : ∀ (x : α), p x → ∃! y, r x y
default x : α
hpx : p x
⊢ r x (extendedChoose! h default x)