Theorem: SimpleGraph.head_or_exists_tail₀ (Untitled/Graphs/Walk.lean)

State before:
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
⊢ P a ∨ ¬P a ∧ ∃ v ∈ Walk.tail₀ p, P v
Tactic:
by_cases h1 : P a
State after:
case pos
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : P a
⊢ P a ∨ ¬P a ∧ ∃ v ∈ Walk.tail₀ p, P v

case neg
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : ¬P a
⊢ P a ∨ ¬P a ∧ ∃ v ∈ Walk.tail₀ p, P v

State before:
case pos
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : P a
⊢ P a ∨ ¬P a ∧ ∃ v ∈ Walk.tail₀ p, P v
Tactic:
left
State after:
case pos.h
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : P a
⊢ P a

State before:
case pos.h
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : P a
⊢ P a
Tactic:
assumption
State after:
no goals

State before:
case neg
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : ¬P a
⊢ P a ∨ ¬P a ∧ ∃ v ∈ Walk.tail₀ p, P v
Tactic:
right
State after:
case neg.h
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : ¬P a
⊢ ¬P a ∧ ∃ v ∈ Walk.tail₀ p, P v

State before:
case neg.h
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : ¬P a
⊢ ¬P a ∧ ∃ v ∈ Walk.tail₀ p, P v
Tactic:
simp [h1]
State after:
case neg.h
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : ¬P a
⊢ ∃ v ∈ Walk.tail₀ p, P v

State before:
case neg.h
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : ¬P a
⊢ ∃ v ∈ Walk.tail₀ p, P v
Tactic:
by_cases h2 : p.Nil
State after:
case pos
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : ¬P a
h2 : Walk.Nil p
⊢ ∃ v ∈ Walk.tail₀ p, P v

case neg
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : ¬P a
h2 : ¬Walk.Nil p
⊢ ∃ v ∈ Walk.tail₀ p, P v

State before:
case pos
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : ¬P a
h2 : Walk.Nil p
⊢ ∃ v ∈ Walk.tail₀ p, P v
Tactic:
cases h2
State after:
case pos.nil
V : Type u_1
V' : Type u_2
a c d : V
G G' : SimpleGraph V
f : V → V'
P : V → Prop
h1 : ¬P a
h : ∃ v ∈ Walk.support Walk.nil, P v
⊢ ∃ v ∈ Walk.tail₀ Walk.nil, P v

State before:
case pos.nil
V : Type u_1
V' : Type u_2
a c d : V
G G' : SimpleGraph V
f : V → V'
P : V → Prop
h1 : ¬P a
h : ∃ v ∈ Walk.support Walk.nil, P v
⊢ ∃ v ∈ Walk.tail₀ Walk.nil, P v
Tactic:
simp at h
State after:
case pos.nil
V : Type u_1
V' : Type u_2
a c d : V
G G' : SimpleGraph V
f : V → V'
P : V → Prop
h1 : ¬P a
h : P a
⊢ ∃ v ∈ Walk.tail₀ Walk.nil, P v

State before:
case pos.nil
V : Type u_1
V' : Type u_2
a c d : V
G G' : SimpleGraph V
f : V → V'
P : V → Prop
h1 : ¬P a
h : P a
⊢ ∃ v ∈ Walk.tail₀ Walk.nil, P v
Tactic:
contradiction
State after:
no goals

State before:
case neg
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
P : V → Prop
h : ∃ v ∈ Walk.support p, P v
h1 : ¬P a
h2 : ¬Walk.Nil p
⊢ ∃ v ∈ Walk.tail₀ p, P v
Tactic:
cases p
State after:
case neg.nil
V : Type u_1
V' : Type u_2
a c d : V
G G' : SimpleGraph V
f : V → V'
P : V → Prop
h1 : ¬P a
h : ∃ v ∈ Walk.support Walk.nil, P v
h2 : ¬Walk.Nil Walk.nil
⊢ ∃ v ∈ Walk.tail₀ Walk.nil, P v

case neg.cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
P : V → Prop
h1 : ¬P a
v✝ : V
h✝ : Adj G a v✝
p✝ : Walk G v✝ b
h : ∃ v ∈ Walk.support (Walk.cons h✝ p✝), P v
h2 : ¬Walk.Nil (Walk.cons h✝ p✝)
⊢ ∃ v ∈ Walk.tail₀ (Walk.cons h✝ p✝), P v

State before:
case neg.nil
V : Type u_1
V' : Type u_2
a c d : V
G G' : SimpleGraph V
f : V → V'
P : V → Prop
h1 : ¬P a
h : ∃ v ∈ Walk.support Walk.nil, P v
h2 : ¬Walk.Nil Walk.nil
⊢ ∃ v ∈ Walk.tail₀ Walk.nil, P v
Tactic:
cases h2 Walk.nil_nil
State after:
no goals

State before:
case neg.cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
P : V → Prop
h1 : ¬P a
v✝ : V
h✝ : Adj G a v✝
p✝ : Walk G v✝ b
h : ∃ v ∈ Walk.support (Walk.cons h✝ p✝), P v
h2 : ¬Walk.Nil (Walk.cons h✝ p✝)
⊢ ∃ v ∈ Walk.tail₀ (Walk.cons h✝ p✝), P v
Tactic:
simpa [h1] using h
State after:
no goals