case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w u✝ : V
⊢ w ∈ (Walk.toSubgraph nil).verts ↔ w ∈ support nil

case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w x y z : V
h : Adj G x y
p' : Walk G y z
ih : w ∈ (Walk.toSubgraph p').verts ↔ w ∈ support p'
⊢ w ∈ (Walk.toSubgraph (cons h p')).verts ↔ w ∈ support (cons h p')
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w : V
p : Walk G u v
⊢ w ∈ (Walk.toSubgraph p).verts ↔ w ∈ support p
induction' p with _ x y z h p' ih
no goals
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w u✝ : V
⊢ w ∈ (Walk.toSubgraph nil).verts ↔ w ∈ support nil
simp
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w x y z : V
h : Adj G x y
p' : Walk G y z
ih : w ∈ (Walk.toSubgraph p').verts ↔ w ∈ support p'
this : w = y ∨ w ∈ support p' ↔ w ∈ support p'
⊢ w ∈ (Walk.toSubgraph (cons h p')).verts ↔ w ∈ support (cons h p')
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w x y z : V
h : Adj G x y
p' : Walk G y z
ih : w ∈ (Walk.toSubgraph p').verts ↔ w ∈ support p'
⊢ w ∈ (Walk.toSubgraph (cons h p')).verts ↔ w ∈ support (cons h p')
have : w = y ∨ w ∈ p'.support ↔ w ∈ p'.support :=
  ⟨by rintro (rfl | h) <;> simp [*], by simp (config := { contextual := true })⟩
no goals
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w x y z : V
h : Adj G x y
p' : Walk G y z
ih : w ∈ (Walk.toSubgraph p').verts ↔ w ∈ support p'
this : w = y ∨ w ∈ support p' ↔ w ∈ support p'
⊢ w ∈ (Walk.toSubgraph (cons h p')).verts ↔ w ∈ support (cons h p')
simp [ih, or_assoc, this]
no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w x y z : V
h : Adj G x y
p' : Walk G y z
ih : w ∈ (Walk.toSubgraph p').verts ↔ w ∈ support p'
⊢ w = y ∨ w ∈ support p' → w ∈ support p'
rintro (rfl | h) <;> simp [*]
no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w x y z : V
h : Adj G x y
p' : Walk G y z
ih : w ∈ (Walk.toSubgraph p').verts ↔ w ∈ support p'
⊢ w ∈ support p' → w = y ∨ w ∈ support p'
simp (config := { contextual := true })