induction' e using Sym2.ind with a b
case 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
e : Sym2 β
⊢ e ∈ (Subgraph.map f G').edgeSet ↔ e ∈ 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 : β
⊢ s(a, b) ∈ (Subgraph.map f G').edgeSet ↔ s(a, b) ∈ Sym2.map ⇑f '' G'.edgeSet