Theorem: Digraph.Embedding.map_mem_edgeSet_iff (GraphProjects/Digraph.lean)

State before:
ι : 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
Tactic:
cases e
State after:
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

State before:
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
Tactic:
simp [f.map_adj_iff]
State after:
no goals