cases e
ι : Sort ?u.263245
𝕜 : Type ?u.263248
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'
e : V × V
⊢ Prod.map (↑f) (↑f) e ∈ edgeSet G' ↔ e ∈ edgeSet G
case mk
ι : Sort ?u.263245
𝕜 : Type ?u.263248
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