case head
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v v✝ : V
h' : Adj G u v✝
p' : Walk G v✝ v
⊢ Dart.edge { toProd := (u, v✝), is_adj := h' } ∈ edgeSet G

case tail
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v v✝ : V
h' : Adj G u v✝
p' : Walk G v✝ v
e : Sym2 V
a✝ : List.Mem e (List.map Dart.edge (darts p'))
⊢ e ∈ edgeSet G
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v v✝ : V
h' : Adj G u v✝
p' : Walk G v✝ v
e : Sym2 V
h : e ∈ edges (cons h' p')
⊢ e ∈ edgeSet G
cases h
no goals
case tail
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v v✝ : V
h' : Adj G u v✝
p' : Walk G v✝ v
e : Sym2 V
a✝ : List.Mem e (List.map Dart.edge (darts p'))
⊢ e ∈ edgeSet G
next h' => exact edges_subset_edgeSet p' h'
no goals
case head
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v v✝ : V
h' : Adj G u v✝
p' : Walk G v✝ v
⊢ Dart.edge { toProd := (u, v✝), is_adj := h' } ∈ edgeSet G
exact h'
no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v v✝ : V
h'✝ : Adj G u v✝
p' : Walk G v✝ v
e : Sym2 V
h' : List.Mem e (List.map Dart.edge (darts p'))
⊢ e ∈ edgeSet G
exact edges_subset_edgeSet p' h'