obtain ⟨w, h1e', h1u'⟩ := h1 y
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
h2' : Classical.choose ⋯ = y
⊢ Classical.choose ⋯ = x
case intro.intro.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
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
⊢ Classical.choose ⋯ = x