no goals
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ : V
⊢ support (bypass nil) ⊆ support nil
simp!
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
⊢ support (if hs : u✝ ∈ support (bypass p✝) then dropUntil (bypass p✝) u✝ hs else cons h✝ (bypass p✝)) ⊆
    u✝ :: support p✝
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
⊢ support (bypass (cons h✝ p✝)) ⊆ support (cons h✝ p✝)
simp! only
case cons.inl
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ support (dropUntil (bypass p✝) u✝ h✝) ⊆ u✝ :: support p✝

case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ support (cons h✝¹ (bypass p✝)) ⊆ u✝ :: support p✝
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
⊢ support (if hs : u✝ ∈ support (bypass p✝) then dropUntil (bypass p✝) u✝ hs else cons h✝ (bypass p✝)) ⊆
    u✝ :: support p✝
split_ifs
case cons.inl
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ support (bypass p✝) ⊆ u✝ :: support p✝
case cons.inl
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ support (dropUntil (bypass p✝) u✝ h✝) ⊆ u✝ :: support p✝
apply List.Subset.trans (support_dropUntil_subset _ _)
case cons.inl.a
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ support (bypass p✝) ⊆ support p✝
case cons.inl
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ support (bypass p✝) ⊆ u✝ :: support p✝
apply List.subset_cons_of_subset
no goals
case cons.inl.a
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ support (bypass p✝) ⊆ support p✝
assumption
case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ u✝ :: support (bypass p✝) ⊆ u✝ :: support p✝
case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ support (cons h✝¹ (bypass p✝)) ⊆ u✝ :: support p✝
rw [support_cons]
case cons.inr.s
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ support (bypass p✝) ⊆ support p✝
case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ u✝ :: support (bypass p✝) ⊆ u✝ :: support p✝
apply List.cons_subset_cons
no goals
case cons.inr.s
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : support (bypass p✝) ⊆ support p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ support (bypass p✝) ⊆ support p✝
assumption