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
d : Dart G
hd : d = { toProd := (u, v✝), is_adj := h } ∨ d ∈ darts p'
⊢ d.fst = u ∨ d.fst ∈ support p'
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
d : Dart G
hd : d ∈ darts (cons h p')
⊢ d.fst ∈ support (cons h p')
simp only [support_cons, darts_cons, List.mem_cons] at hd ⊢
case inl
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
⊢ { toProd := (u, v✝), is_adj := h }.toProd.fst = u ∨ { toProd := (u, v✝), is_adj := h }.toProd.fst ∈ support p'

case inr
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
d : Dart G
hd : d ∈ darts p'
⊢ d.fst = u ∨ d.fst ∈ support p'
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
d : Dart G
hd : d = { toProd := (u, v✝), is_adj := h } ∨ d ∈ darts p'
⊢ d.fst = u ∨ d.fst ∈ support p'
rcases hd with (rfl | hd)
no goals
case inl
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
⊢ { toProd := (u, v✝), is_adj := h }.toProd.fst = u ∨ { toProd := (u, v✝), is_adj := h }.toProd.fst ∈ support p'
exact Or.inl rfl
no goals
case inr
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
d : Dart G
hd : d ∈ darts p'
⊢ d.fst = u ∨ d.fst ∈ support p'
exact Or.inr (dart_fst_mem_support_of_mem_darts _ hd)