V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
t u v w : V
p : Walk G v w
he : Quotient.mk (Sym2.Rel.setoid V) (u, t) ∈ edges p
⊢ u ∈ support p
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
t u v w : V
p : Walk G v w
he : Quotient.mk (Sym2.Rel.setoid V) (t, u) ∈ edges p
⊢ u ∈ support p
rw [Sym2.eq_swap] at he
no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
t u v w : V
p : Walk G v w
he : Quotient.mk (Sym2.Rel.setoid V) (u, t) ∈ edges p
⊢ u ∈ support p
exact p.fst_mem_support_of_mem_edges he