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

State before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
p : Walk G u v
S : Set V
uS : u ∈ S
vS : ¬v ∈ S
⊢ ∃ e, e ∈ edges p ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
Tactic:
induction' p with _ x y w a p' ih
State after:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
u✝ : V
uS : u✝ ∈ S
vS : ¬u✝ ∈ S
⊢ ∃ e, e ∈ edges nil ∧ e.fst ∈ S ∧ ¬e.snd ∈ S

case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : G.Adj x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ e, e ∈ edges p' ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
⊢ ∃ e, e ∈ edges (cons a p') ∧ e.fst ∈ S ∧ ¬e.snd ∈ S

State before:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
u✝ : V
uS : u✝ ∈ S
vS : ¬u✝ ∈ S
⊢ ∃ e, e ∈ edges nil ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
Tactic:
cases vS uS
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''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : G.Adj x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ e, e ∈ edges p' ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
⊢ ∃ e, e ∈ edges (cons a p') ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
Tactic:
by_cases h : y ∈ S
State after:
case pos
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : G.Adj x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ e, e ∈ edges p' ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
h : y ∈ S
⊢ ∃ e, e ∈ edges (cons a p') ∧ e.fst ∈ S ∧ ¬e.snd ∈ S

case neg
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : G.Adj x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ e, e ∈ edges p' ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
h : ¬y ∈ S
⊢ ∃ e, e ∈ edges (cons a p') ∧ e.fst ∈ S ∧ ¬e.snd ∈ S

State before:
case pos
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : G.Adj x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ e, e ∈ edges p' ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
h : y ∈ S
⊢ ∃ e, e ∈ edges (cons a p') ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
Tactic:
obtain ⟨d, hd, hcd⟩ := ih h vS
State after:
case pos.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : G.Adj x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ e, e ∈ edges p' ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
h : y ∈ S
d : V × V
hd : d ∈ edges p'
hcd : d.fst ∈ S ∧ ¬d.snd ∈ S
⊢ ∃ e, e ∈ edges (cons a p') ∧ e.fst ∈ S ∧ ¬e.snd ∈ S

State before:
case pos.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : G.Adj x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ e, e ∈ edges p' ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
h : y ∈ S
d : V × V
hd : d ∈ edges p'
hcd : d.fst ∈ S ∧ ¬d.snd ∈ S
⊢ ∃ e, e ∈ edges (cons a p') ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
Tactic:
exact ⟨d, List.Mem.tail _ hd, hcd⟩
State after:
no goals

State before:
case neg
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : G.Adj x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ e, e ∈ edges p' ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
h : ¬y ∈ S
⊢ ∃ e, e ∈ edges (cons a p') ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
Tactic:
exact ⟨(x, y), List.Mem.head _, uS, h⟩
State after:
no goals