case intro.intro
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
d : Dart G
hd : d ∈ darts p
he : Dart.edge d = Quotient.mk (Sym2.Rel.setoid V) (t, u)
⊢ t ∈ 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
⊢ t ∈ support p
obtain ⟨d, hd, he⟩ := List.mem_map.mp he
case intro.intro
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
d : Dart G
hd : d ∈ darts p
he : d.fst = t ∧ d.snd = u ∨ d.fst = u ∧ d.snd = t
⊢ t ∈ support p
case intro.intro
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
d : Dart G
hd : d ∈ darts p
he : Dart.edge d = Quotient.mk (Sym2.Rel.setoid V) (t, u)
⊢ t ∈ support p
rw [dart_edge_eq_mk'_iff'] at he
case intro.intro.inl.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
p : Walk G v w
d : Dart G
hd : d ∈ darts p
he : Quotient.mk (Sym2.Rel.setoid V) (d.fst, d.snd) ∈ edges p
⊢ d.fst ∈ support p

case intro.intro.inr.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
p : Walk G v w
d : Dart G
hd : d ∈ darts p
he : Quotient.mk (Sym2.Rel.setoid V) (d.snd, d.fst) ∈ edges p
⊢ d.snd ∈ support p
case intro.intro
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
d : Dart G
hd : d ∈ darts p
he : d.fst = t ∧ d.snd = u ∨ d.fst = u ∧ d.snd = t
⊢ t ∈ support p
rcases he with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
no goals
case intro.intro.inl.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
p : Walk G v w
d : Dart G
hd : d ∈ darts p
he : Quotient.mk (Sym2.Rel.setoid V) (d.fst, d.snd) ∈ edges p
⊢ d.fst ∈ support p
exact dart_fst_mem_support_of_mem_darts _ hd
no goals
case intro.intro.inr.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
p : Walk G v w
d : Dart G
hd : d ∈ darts p
he : Quotient.mk (Sym2.Rel.setoid V) (d.snd, d.fst) ∈ edges p
⊢ d.snd ∈ support p
exact dart_snd_mem_support_of_mem_darts _ hd