exact ⟨x, ⟨ha, hb⟩, hx⟩
case h.mpr.intro.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
A B : Set G
g y x : G
ha : x ∈ A
hx : g * x = y
hb : x ∈ B
hx' : g * x = y
⊢ ∃ x ∈ A ∩ B, g * x = y
no goals