Theorem: Digraph.Walk.edges_bypass_subset (GraphProjects/DigraphConnectivity.lean)

State before:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ : V
⊢ edges (bypass nil) ⊆ edges nil
Tactic:
simp!
State after:
no goals

State before:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : edges (bypass p✝) ⊆ edges p✝
⊢ edges (bypass (cons h✝ p✝)) ⊆ edges (cons h✝ p✝)
Tactic:
simp! only
State after:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : edges (bypass p✝) ⊆ edges p✝
⊢ edges (if hs : u✝ ∈ support (bypass p✝) then dropUntil (bypass p✝) u✝ hs else cons h✝ (bypass p✝)) ⊆
    (u✝, v✝) :: edges p✝

State before:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : edges (bypass p✝) ⊆ edges p✝
⊢ edges (if hs : u✝ ∈ support (bypass p✝) then dropUntil (bypass p✝) u✝ hs else cons h✝ (bypass p✝)) ⊆
    (u✝, v✝) :: edges p✝
Tactic:
split_ifs
State after:
case cons.inl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : edges (bypass p✝) ⊆ edges p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ edges (dropUntil (bypass p✝) u✝ h✝) ⊆ (u✝, v✝) :: edges p✝

case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : edges (bypass p✝) ⊆ edges p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ edges (cons h✝¹ (bypass p✝)) ⊆ (u✝, v✝) :: edges p✝

State before:
case cons.inl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : edges (bypass p✝) ⊆ edges p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ edges (dropUntil (bypass p✝) u✝ h✝) ⊆ (u✝, v✝) :: edges p✝
Tactic:
apply List.Subset.trans (edges_dropUntil_subset _ _)
State after:
case cons.inl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : edges (bypass p✝) ⊆ edges p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ edges (bypass p✝) ⊆ (u✝, v✝) :: edges p✝

State before:
case cons.inl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : edges (bypass p✝) ⊆ edges p✝
h✝ : u✝ ∈ support (bypass p✝)
⊢ edges (bypass p✝) ⊆ (u✝, v✝) :: edges p✝
Tactic:
apply List.subset_cons_of_subset _ ih
State after:
no goals

State before:
case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : edges (bypass p✝) ⊆ edges p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ edges (cons h✝¹ (bypass p✝)) ⊆ (u✝, v✝) :: edges p✝
Tactic:
rw [edges_cons]
State after:
case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : edges (bypass p✝) ⊆ edges p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ (u✝, v✝) :: edges (bypass p✝) ⊆ (u✝, v✝) :: edges p✝

State before:
case cons.inr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : edges (bypass p✝) ⊆ edges p✝
h✝ : ¬u✝ ∈ support (bypass p✝)
⊢ (u✝, v✝) :: edges (bypass p✝) ⊆ (u✝, v✝) :: edges p✝
Tactic:
exact List.cons_subset_cons _ ih
State after:
no goals