Theorem: Digraph.Walk.exists_cons_eq_concat (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 w : V
h : G.Adj u v
p : Walk G v w
⊢ ∃ x q h', cons h p = concat q h'
Tactic:
induction p generalizing u with
| nil => exact ⟨_, nil, h, rfl⟩
| cons h' p ih =>
  obtain ⟨y, q, h'', hc⟩ := ih h'
  refine' ⟨y, cons h q, h'', _⟩
  rw [concat_cons, hc]
State after:
no goals

State before:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v w u✝ u : V
h : G.Adj u u✝
⊢ ∃ x q h', cons h nil = concat q h'
Tactic:
exact ⟨_, nil, h, rfl⟩
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''
v w u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p : Walk G v✝ w✝
ih : ∀ {u : V} (h : G.Adj u v✝), ∃ x q h', cons h p = concat q h'
u : V
h : G.Adj u u✝
⊢ ∃ x q h'_1, cons h (cons h' p) = concat q h'_1
Tactic:
obtain ⟨y, q, h'', hc⟩ := ih h'
State after:
case cons.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v w u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p : Walk G v✝ w✝
ih : ∀ {u : V} (h : G.Adj u v✝), ∃ x q h', cons h p = concat q h'
u : V
h : G.Adj u u✝
y : V
q : Walk G u✝ y
h'' : G.Adj y w✝
hc : cons h' p = concat q h''
⊢ ∃ x q h'_1, cons h (cons h' p) = concat q h'_1

State before:
case cons.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v w u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p : Walk G v✝ w✝
ih : ∀ {u : V} (h : G.Adj u v✝), ∃ x q h', cons h p = concat q h'
u : V
h : G.Adj u u✝
y : V
q : Walk G u✝ y
h'' : G.Adj y w✝
hc : cons h' p = concat q h''
⊢ ∃ x q h'_1, cons h (cons h' p) = concat q h'_1
Tactic:
refine' ⟨y, cons h q, h'', _⟩
State after:
case cons.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v w u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p : Walk G v✝ w✝
ih : ∀ {u : V} (h : G.Adj u v✝), ∃ x q h', cons h p = concat q h'
u : V
h : G.Adj u u✝
y : V
q : Walk G u✝ y
h'' : G.Adj y w✝
hc : cons h' p = concat q h''
⊢ cons h (cons h' p) = concat (cons h q) h''

State before:
case cons.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v w u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p : Walk G v✝ w✝
ih : ∀ {u : V} (h : G.Adj u v✝), ∃ x q h', cons h p = concat q h'
u : V
h : G.Adj u u✝
y : V
q : Walk G u✝ y
h'' : G.Adj y w✝
hc : cons h' p = concat q h''
⊢ cons h (cons h' p) = concat (cons h q) h''
Tactic:
rw [concat_cons, hc]
State after:
no goals