no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w : V
h : Adj G u v
p : Walk G v w
⊢ ∃ x q h', cons h p = concat q h'
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]
no goals
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u✝ u : V
h : Adj G u u✝
⊢ ∃ x q h', cons h nil = concat q h'
exact ⟨_, nil, h, rfl⟩
case cons.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u✝ v✝ w✝ : V
h' : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ {u : V} (h : Adj G u v✝), ∃ x q h', cons h p = concat q h'
u : V
h : Adj G u u✝
y : V
q : Walk G u✝ y
h'' : Adj G y w✝
hc : cons h' p = concat q h''
⊢ ∃ x q h'_1, cons h (cons h' p) = concat q h'_1
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u✝ v✝ w✝ : V
h' : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ {u : V} (h : Adj G u v✝), ∃ x q h', cons h p = concat q h'
u : V
h : Adj G u u✝
⊢ ∃ x q h'_1, cons h (cons h' p) = concat q h'_1
obtain ⟨y, q, h'', hc⟩ := ih h'
case cons.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u✝ v✝ w✝ : V
h' : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ {u : V} (h : Adj G u v✝), ∃ x q h', cons h p = concat q h'
u : V
h : Adj G u u✝
y : V
q : Walk G u✝ y
h'' : Adj G y w✝
hc : cons h' p = concat q h''
⊢ cons h (cons h' p) = concat (cons h q) h''
case cons.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u✝ v✝ w✝ : V
h' : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ {u : V} (h : Adj G u v✝), ∃ x q h', cons h p = concat q h'
u : V
h : Adj G u u✝
y : V
q : Walk G u✝ y
h'' : Adj G y w✝
hc : cons h' p = concat q h''
⊢ ∃ x q h'_1, cons h (cons h' p) = concat q h'_1
refine' ⟨y, cons h q, h'', _⟩
no goals
case cons.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u✝ v✝ w✝ : V
h' : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ {u : V} (h : Adj G u v✝), ∃ x q h', cons h p = concat q h'
u : V
h : Adj G u u✝
y : V
q : Walk G u✝ y
h'' : Adj G y w✝
hc : cons h' p = concat q h''
⊢ cons h (cons h' p) = concat (cons h q) h''
rw [concat_cons, hc]