simp only [mem_edgeSet, Sym2.exists, Relation.Map, and_or_left, exists_or, map_adj,
  Set.mem_image, Sym2.map_pair_eq, Sym2.eq, Sym2.rel_iff]
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 : β
⊢ s(a, b) ∈ (Subgraph.map f G').edgeSet ↔ s(a, b) ∈ Sym2.map ⇑f '' G'.edgeSet
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 : β
⊢ (∃ a_1 b_1, G'.Adj a_1 b_1 ∧ f a_1 = a ∧ f b_1 = b) ↔
    (∃ a_1 b_1, G'.Adj a_1 b_1 ∧ f a_1 = a ∧ f b_1 = b) ∨ ∃ x x_1, G'.Adj x x_1 ∧ f x = b ∧ f x_1 = a