rintro ⟨⟨x, ha, hx⟩, ⟨x', hb, hx'⟩⟩
case h.mpr
G : Type u_1
inst✝ : Group G
A B : Set G
g y : G
⊢ y ∈ {x | ∃ x_1 ∈ A, g * x_1 = x} ∩ {x | ∃ x_1 ∈ B, g * x_1 = x} → ∃ x ∈ A ∩ B, g * x = y
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
x' : G
hb : x' ∈ B
hx' : g * x' = y
⊢ ∃ x ∈ A ∩ B, g * x = y