rintro ⟨a, b, hab, rfl, rfl⟩
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
a b : β
⊢ (∃ x x_1, G'.Adj x x_1 ∧ f x = b ∧ f x_1 = a) → ∃ a_2 b_1, G'.Adj a_2 b_1 ∧ f a_2 = a ∧ f b_1 = b
case h.h.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
f : G →g H
G' : G.Subgraph
a b : α
hab : G'.Adj a b
⊢ ∃ a_1 b_1, G'.Adj a_1 b_1 ∧ f a_1 = f b ∧ f b_1 = f a