case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
u✝ : V
uS : u✝ ∈ S
vS : ¬u✝ ∈ S
⊢ ∃ d, d ∈ darts nil ∧ d.fst ∈ S ∧ ¬d.snd ∈ S

case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : Adj G x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ d, d ∈ darts p' ∧ d.fst ∈ S ∧ ¬d.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
⊢ ∃ d, d ∈ darts (cons a p') ∧ d.fst ∈ S ∧ ¬d.snd ∈ S
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
p : Walk G u v
S : Set V
uS : u ∈ S
vS : ¬v ∈ S
⊢ ∃ d, d ∈ darts p ∧ d.fst ∈ S ∧ ¬d.snd ∈ S
induction' p with _ x y w a p' ih
no goals
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
u✝ : V
uS : u✝ ∈ S
vS : ¬u✝ ∈ S
⊢ ∃ d, d ∈ darts nil ∧ d.fst ∈ S ∧ ¬d.snd ∈ S
cases vS uS
case pos
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : Adj G x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ d, d ∈ darts p' ∧ d.fst ∈ S ∧ ¬d.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
h : y ∈ S
⊢ ∃ d, d ∈ darts (cons a p') ∧ d.fst ∈ S ∧ ¬d.snd ∈ S

case neg
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : Adj G x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ d, d ∈ darts p' ∧ d.fst ∈ S ∧ ¬d.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
h : ¬y ∈ S
⊢ ∃ d, d ∈ darts (cons a p') ∧ d.fst ∈ S ∧ ¬d.snd ∈ S
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : Adj G x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ d, d ∈ darts p' ∧ d.fst ∈ S ∧ ¬d.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
⊢ ∃ d, d ∈ darts (cons a p') ∧ d.fst ∈ S ∧ ¬d.snd ∈ S
by_cases h : y ∈ S
case pos.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : Adj G x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ d, d ∈ darts p' ∧ d.fst ∈ S ∧ ¬d.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
h : y ∈ S
d : Dart G
hd : d ∈ darts p'
hcd : d.fst ∈ S ∧ ¬d.snd ∈ S
⊢ ∃ d, d ∈ darts (cons a p') ∧ d.fst ∈ S ∧ ¬d.snd ∈ S
case pos
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : Adj G x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ d, d ∈ darts p' ∧ d.fst ∈ S ∧ ¬d.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
h : y ∈ S
⊢ ∃ d, d ∈ darts (cons a p') ∧ d.fst ∈ S ∧ ¬d.snd ∈ S
obtain ⟨d, hd, hcd⟩ := ih h vS
no goals
case pos.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : Adj G x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ d, d ∈ darts p' ∧ d.fst ∈ S ∧ ¬d.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
h : y ∈ S
d : Dart G
hd : d ∈ darts p'
hcd : d.fst ∈ S ∧ ¬d.snd ∈ S
⊢ ∃ d, d ∈ darts (cons a p') ∧ d.fst ∈ S ∧ ¬d.snd ∈ S
exact ⟨d, List.Mem.tail _ hd, hcd⟩
no goals
case neg
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : Adj G x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ d, d ∈ darts p' ∧ d.fst ∈ S ∧ ¬d.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
h : ¬y ∈ S
⊢ ∃ d, d ∈ darts (cons a p') ∧ d.fst ∈ S ∧ ¬d.snd ∈ S
exact ⟨⟨(x, y), a⟩, List.Mem.head _, uS, h⟩