simp [f.map_adj_iff]
case mk
ι : Sort ?u.420032
𝕜 : Type ?u.420035
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G ≃g G'
fst✝ snd✝ : V
⊢ Prod.map ↑f ↑f (fst✝, snd✝) ∈ edgeSet G' ↔ (fst✝, snd✝) ∈ edgeSet G
no goals