Theorem: Classical.extendedChoose!_eq_iff (Arithmetization/Vorspiel/ExistsUnique.lean)

State before:
α : 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
Tactic:
rintro rfl
State after:
α : 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)

State before:
α : 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)
Tactic:
exact extendedchoose!_spec h default hpx
State after:
no goals