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

Proof state:
case pos.a
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.support ⊆ p✝.support
h✝ : u✝ ∈ p✝.bypass.support
⊢ p✝.bypass.support ⊆ p✝.support

Tactic:
assumption

Result:
no goals

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.support ⊆ p✝.support
⊢ (cons h✝ p✝).bypass.support ⊆ (cons h✝ p✝).support

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.support ⊆ p✝.support
⊢ (if hs : u✝ ∈ p✝.bypass.support then p✝.bypass.dropUntil u✝ hs else cons h✝ p✝.bypass).support ⊆ u✝ :: p✝.support

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.support ⊆ p✝.support
h✝ : u✝ ∈ p✝.bypass.support
⊢ p✝.bypass.support ⊆ u✝ :: p✝.support

Tactic:
apply List.subset_cons_of_subset

Result:
case pos.a
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.support ⊆ p✝.support
h✝ : u✝ ∈ p✝.bypass.support
⊢ p✝.bypass.support ⊆ p✝.support

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.support ⊆ p✝.support
h✝ : u✝ ∉ p✝.bypass.support
⊢ u✝ :: p✝.bypass.support ⊆ u✝ :: p✝.support

Tactic:
apply List.cons_subset_cons

Result:
case neg.s
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.support ⊆ p✝.support
h✝ : u✝ ∉ p✝.bypass.support
⊢ p✝.bypass.support ⊆ p✝.support

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.support ⊆ p✝.support
⊢ (if hs : u✝ ∈ p✝.bypass.support then p✝.bypass.dropUntil u✝ hs else cons h✝ p✝.bypass).support ⊆ u✝ :: p✝.support

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.support ⊆ p✝.support
h✝ : u✝ ∈ p✝.bypass.support
⊢ (p✝.bypass.dropUntil u✝ h✝).support ⊆ u✝ :: p✝.support

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.support ⊆ p✝.support
h✝ : u✝ ∉ p✝.bypass.support
⊢ (cons h✝¹ p✝.bypass).support ⊆ u✝ :: p✝.support

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.support ⊆ p✝.support
h✝ : u✝ ∉ p✝.bypass.support
⊢ (cons h✝¹ p✝.bypass).support ⊆ u✝ :: p✝.support

Tactic:
rw [support_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.support ⊆ p✝.support
h✝ : u✝ ∉ p✝.bypass.support
⊢ u✝ :: p✝.bypass.support ⊆ u✝ :: p✝.support

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.support ⊆ p✝.support
h✝ : u✝ ∈ p✝.bypass.support
⊢ (p✝.bypass.dropUntil u✝ h✝).support ⊆ u✝ :: p✝.support

Tactic:
apply List.Subset.trans (support_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.support ⊆ p✝.support
h✝ : u✝ ∈ p✝.bypass.support
⊢ p✝.bypass.support ⊆ u✝ :: p✝.support

Proof state:
case neg.s
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.support ⊆ p✝.support
h✝ : u✝ ∉ p✝.bypass.support
⊢ p✝.bypass.support ⊆ p✝.support

Tactic:
assumption

Result:
no goals

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

Tactic:
simp!

Result:
no goals