exact f.map_rel' h
case mk
ι : Sort ?u.200863
𝕜 : Type ?u.200866
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
h : (fst✝, snd✝) ∈ edgeSet G
⊢ Prod.map ↑f ↑f (fst✝, snd✝) ∈ edgeSet G'
no goals