obtain ⟨y, h1e, h1u⟩ := h1 x
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x : α
⊢ Classical.choose ⋯ = x
case intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
⊢ Classical.choose ⋯ = x