-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem darts_bypass_subset {u v : V} (p : G.Walk u v) : p.bypass.darts ⊆ p.darts

Proof state:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.darts ⊆ p✝.darts
h✝ : u✝ ∈ p✝.bypass.support
⊢ (p✝.bypass.dropUntil u✝ h✝).darts ⊆ { toProd := (u✝, v✝), adj := h✝¹ } :: p✝.darts

Tactic:
apply List.Subset.trans (darts_dropUntil_subset _ _)

Result:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.darts ⊆ p✝.darts
h✝ : u✝ ∈ p✝.bypass.support
⊢ p✝.bypass.darts ⊆ { toProd := (u✝, v✝), adj := h✝¹ } :: p✝.darts

Proof state:
case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.darts ⊆ p✝.darts
⊢ (cons h✝ p✝).bypass.darts ⊆ (cons h✝ p✝).darts

Tactic:
simp! only

Result:
case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.darts ⊆ p✝.darts
⊢ (if hs : u✝ ∈ p✝.bypass.support then p✝.bypass.dropUntil u✝ hs else cons h✝ p✝.bypass).darts ⊆
    { toProd := (u✝, v✝), adj := h✝ } :: p✝.darts

Proof state:
case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.darts ⊆ p✝.darts
⊢ (if hs : u✝ ∈ p✝.bypass.support then p✝.bypass.dropUntil u✝ hs else cons h✝ p✝.bypass).darts ⊆
    { toProd := (u✝, v✝), adj := h✝ } :: p✝.darts

Tactic:
split_ifs

Result:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.darts ⊆ p✝.darts
h✝ : u✝ ∈ p✝.bypass.support
⊢ (p✝.bypass.dropUntil u✝ h✝).darts ⊆ { toProd := (u✝, v✝), adj := h✝¹ } :: p✝.darts

case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.darts ⊆ p✝.darts
h✝ : u✝ ∉ p✝.bypass.support
⊢ (cons h✝¹ p✝.bypass).darts ⊆ { toProd := (u✝, v✝), adj := h✝¹ } :: p✝.darts

Proof state:
case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.darts ⊆ p✝.darts
h✝ : u✝ ∉ p✝.bypass.support
⊢ (cons h✝¹ p✝.bypass).darts ⊆ { toProd := (u✝, v✝), adj := h✝¹ } :: p✝.darts

Tactic:
rw [darts_cons]

Result:
case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.darts ⊆ p✝.darts
h✝ : u✝ ∉ p✝.bypass.support
⊢ { toProd := (u✝, v✝), adj := h✝¹ } :: p✝.bypass.darts ⊆ { toProd := (u✝, v✝), adj := h✝¹ } :: p✝.darts

Proof state:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.darts ⊆ p✝.darts
h✝ : u✝ ∈ p✝.bypass.support
⊢ p✝.bypass.darts ⊆ { toProd := (u✝, v✝), adj := h✝¹ } :: p✝.darts

Tactic:
apply List.subset_cons_of_subset _ ih

Result:
no goals

Proof state:
case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.darts ⊆ p✝.darts
h✝ : u✝ ∉ p✝.bypass.support
⊢ { toProd := (u✝, v✝), adj := h✝¹ } :: p✝.bypass.darts ⊆ { toProd := (u✝, v✝), adj := h✝¹ } :: p✝.darts

Tactic:
exact List.cons_subset_cons _ ih

Result:
no goals

Proof state:
case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ : V
⊢ nil.bypass.darts ⊆ nil.darts

Tactic:
simp!

Result:
no goals