case mp
V✝ : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V✝
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V✝
V : Type u
G : SimpleGraph V
u v w : V
p : Walk G u v
⊢ w ∈ support p → ∃ q r, p = append q r

case mpr
V✝ : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V✝
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V✝
V : Type u
G : SimpleGraph V
u v w : V
p : Walk G u v
⊢ (∃ q r, p = append q r) → w ∈ support p
V✝ : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V✝
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V✝
V : Type u
G : SimpleGraph V
u v w : V
p : Walk G u v
⊢ w ∈ support p ↔ ∃ q r, p = append q r
constructor
no goals
case mp
V✝ : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V✝
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V✝
V : Type u
G : SimpleGraph V
u v w : V
p : Walk G u v
⊢ w ∈ support p → ∃ q r, p = append q r
exact fun h => ⟨_, _, (p.take_spec h).symm⟩
case mpr.intro.intro
V✝ : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V✝
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V✝
V : Type u
G : SimpleGraph V
u v w : V
q : Walk G u w
r : Walk G w v
⊢ w ∈ support (append q r)
case mpr
V✝ : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V✝
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V✝
V : Type u
G : SimpleGraph V
u v w : V
p : Walk G u v
⊢ (∃ q r, p = append q r) → w ∈ support p
rintro ⟨q, r, rfl⟩
no goals
case mpr.intro.intro
V✝ : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V✝
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V✝
V : Type u
G : SimpleGraph V
u v w : V
q : Walk G u w
r : Walk G w v
⊢ w ∈ support (append q r)
simp only [mem_support_append_iff, end_mem_support, start_mem_support, or_self_iff]