Theorem: Digraph.Hom.map_mem_edgeSet (GraphProjects/Digraph.lean)

State before:
ι : 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'
e : V × V
h : e ∈ edgeSet G
⊢ Prod.map (↑f) (↑f) e ∈ edgeSet G'
Tactic:
cases e
State after:
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'

State before:
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'
Tactic:
exact f.map_rel' h
State after:
no goals