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
⊢ darts (bypass nil) ⊆ darts 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 : darts (bypass p✝) ⊆ darts p✝
⊢ darts (if hs : u✝ ∈ support (bypass p✝) then dropUntil (bypass p✝) u✝ hs else cons h✝ (bypass p✝)) ⊆
    { toProd := (u✝, v✝), is_adj := h✝ } :: darts 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 : darts (bypass p✝) ⊆ darts p✝
⊢ darts (bypass (cons h✝ p✝)) ⊆ darts (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 : darts (bypass p✝) ⊆ darts p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ darts (dropUntil (bypass p✝) u✝ h✝) ⊆ { toProd := (u✝, v✝), is_adj := h✝¹ } :: darts 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 : darts (bypass p✝) ⊆ darts p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ darts (cons h✝¹ (bypass p✝)) ⊆ { toProd := (u✝, v✝), is_adj := h✝¹ } :: darts 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 : darts (bypass p✝) ⊆ darts p✝
⊢ darts (if hs : u✝ ∈ support (bypass p✝) then dropUntil (bypass p✝) u✝ hs else cons h✝ (bypass p✝)) ⊆
    { toProd := (u✝, v✝), is_adj := h✝ } :: darts 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 : darts (bypass p✝) ⊆ darts p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ darts (bypass p✝) ⊆ { toProd := (u✝, v✝), is_adj := h✝¹ } :: darts 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 : darts (bypass p✝) ⊆ darts p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ darts (dropUntil (bypass p✝) u✝ h✝) ⊆ { toProd := (u✝, v✝), is_adj := h✝¹ } :: darts p✝
apply List.Subset.trans (darts_dropUntil_subset _ _)
no goals
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 : darts (bypass p✝) ⊆ darts p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ darts (bypass p✝) ⊆ { toProd := (u✝, v✝), is_adj := h✝¹ } :: darts p✝
apply List.subset_cons_of_subset _ ih
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 : darts (bypass p✝) ⊆ darts p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ { toProd := (u✝, v✝), is_adj := h✝¹ } :: darts (bypass p✝) ⊆ { toProd := (u✝, v✝), is_adj := h✝¹ } :: darts 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 : darts (bypass p✝) ⊆ darts p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ darts (cons h✝¹ (bypass p✝)) ⊆ { toProd := (u✝, v✝), is_adj := h✝¹ } :: darts p✝
rw [darts_cons]
no goals
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 : darts (bypass p✝) ⊆ darts p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ { toProd := (u✝, v✝), is_adj := h✝¹ } :: darts (bypass p✝) ⊆ { toProd := (u✝, v✝), is_adj := h✝¹ } :: darts p✝
exact List.cons_subset_cons _ ih