Theorem: Digraph.Walk.edges_subset_edgeSet (GraphProjects/DigraphConnectivity.lean)

State before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v✝ : V
h' : G.Adj u v✝
p' : Walk G v✝ v
e : V × V
h : e ∈ edges (cons h' p')
⊢ e ∈ edgeSet G
Tactic:
cases h
State after:
case head
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v✝ : V
h' : G.Adj u v✝
p' : Walk G v✝ v
⊢ (u, v✝) ∈ edgeSet G

case tail
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v✝ : V
h' : G.Adj u v✝
p' : Walk G v✝ v
e : V × V
a✝ : List.Mem e (edges p')
⊢ e ∈ edgeSet G

State before:
case tail
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v✝ : V
h' : G.Adj u v✝
p' : Walk G v✝ v
e : V × V
a✝ : List.Mem e (edges p')
⊢ e ∈ edgeSet G
Tactic:
next h' => exact edges_subset_edgeSet p' h'
State after:
no goals

State before:
case head
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v✝ : V
h' : G.Adj u v✝
p' : Walk G v✝ v
⊢ (u, v✝) ∈ edgeSet G
Tactic:
exact h'
State after:
no goals

State before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v✝ : V
h'✝ : G.Adj u v✝
p' : Walk G v✝ v
e : V × V
h' : List.Mem e (edges p')
⊢ e ∈ edgeSet G
Tactic:
exact edges_subset_edgeSet p' h'
State after:
no goals