-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem concat_inj {u v v' w : V} {p : G.Walk u v} {h : G.Adj v w} {p' : G.Walk u v'}
    {h' : G.Adj v' w} (he : p.concat h = p'.concat h') : ∃ hv : v = v', p.copy rfl hv = p'

Proof state:
case cons.cons
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : G.Walk v✝¹ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : G.Walk v✝¹ v'}, p✝¹.concat h = p'.concat h' → ∃ (hv : w✝ = v'), p✝¹.copy ⋯ hv = p'
h : G.Adj w✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ v'
he : v✝¹ = v✝ ∧ HEq (p✝¹.concat h) (p✝.concat h')
⊢ ∃ (hv : w✝ = v'), (cons h✝¹ p✝¹).copy ⋯ hv = cons h✝ p✝

Tactic:
obtain ⟨rfl, he⟩ := he

Result:
case cons.cons.intro
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝¹ : G.Walk v✝ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : G.Walk v✝ v'}, p✝¹.concat h = p'.concat h' → ∃ (hv : w✝ = v'), p✝¹.copy ⋯ hv = p'
h : G.Adj w✝ w
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ v'
he : HEq (p✝¹.concat h) (p✝.concat h')
⊢ ∃ (hv : w✝ = v'), (cons h✝¹ p✝¹).copy ⋯ hv = cons h✝ p✝

Proof state:
case nil.cons
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ : V
h : G.Adj u✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ v'
he : nil.concat h = (cons h✝ p✝).concat h'
⊢ ∃ (hv : u✝ = v'), nil.copy ⋯ hv = cons h✝ p✝

Tactic:
exfalso

Result:
case nil.cons
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ : V
h : G.Adj u✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ v'
he : nil.concat h = (cons h✝ p✝).concat h'
⊢ False

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ : V
h : G.Adj u✝ w
p' : G.Walk u✝ v'
he : nil.concat h = p'.concat h'
⊢ ∃ (hv : u✝ = v'), nil.copy ⋯ hv = p'

Tactic:
cases p'

Result:
case nil.nil
V : Type u
G : SimpleGraph V
u v v' w : V
h' h : G.Adj v' w
he : nil.concat h = nil.concat h'
⊢ ∃ (hv : v' = v'), nil.copy ⋯ hv = nil

case nil.cons
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ : V
h : G.Adj u✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ v'
he : nil.concat h = (cons h✝ p✝).concat h'
⊢ ∃ (hv : u✝ = v'), nil.copy ⋯ hv = cons h✝ p✝

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : G.Walk v✝ v'}, p✝.concat h = p'.concat h' → ∃ (hv : w✝ = v'), p✝.copy ⋯ hv = p'
h : G.Adj w✝ w
p' : G.Walk u✝ v'
he : cons h✝ (p✝.concat h) = p'.concat h'
⊢ ∃ (hv : w✝ = v'), (cons h✝ p✝).copy ⋯ hv = p'

Tactic:
cases p'

Result:
case cons.nil
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
v✝ w✝ : V
p✝ : G.Walk v✝ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : G.Walk v✝ v'}, p✝.concat h = p'.concat h' → ∃ (hv : w✝ = v'), p✝.copy ⋯ hv = p'
h : G.Adj w✝ w
h✝ : G.Adj v' v✝
he : cons h✝ (p✝.concat h) = nil.concat h'
⊢ ∃ (hv : w✝ = v'), (cons h✝ p✝).copy ⋯ hv = nil

case cons.cons
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : G.Walk v✝¹ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : G.Walk v✝¹ v'}, p✝¹.concat h = p'.concat h' → ∃ (hv : w✝ = v'), p✝¹.copy ⋯ hv = p'
h : G.Adj w✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ v'
he : cons h✝¹ (p✝¹.concat h) = (cons h✝ p✝).concat h'
⊢ ∃ (hv : w✝ = v'), (cons h✝¹ p✝¹).copy ⋯ hv = cons h✝ p✝

Proof state:
case cons.cons.intro
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝¹ : G.Walk v✝ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : G.Walk v✝ v'}, p✝¹.concat h = p'.concat h' → ∃ (hv : w✝ = v'), p✝¹.copy ⋯ hv = p'
h : G.Adj w✝ w
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ v'
he : p✝¹.concat h = p✝.concat h'
⊢ ∃ (hv : w✝ = v'), (cons h✝¹ p✝¹).copy ⋯ hv = cons h✝ p✝

Tactic:
obtain ⟨rfl, rfl⟩ := ih he

Result:
case cons.cons.intro.intro
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
h : G.Adj w✝ w
h✝ : G.Adj u✝ v✝
h' : G.Adj w✝ w
ih : ∀ {h : G.Adj w✝ w} {p' : G.Walk v✝ w✝}, p✝.concat h = p'.concat h' → ∃ (hv : w✝ = w✝), p✝.copy ⋯ hv = p'
he : p✝.concat h = (p✝.copy ⋯ ⋯).concat h'
⊢ ∃ (hv : w✝ = w✝), (cons h✝¹ p✝).copy ⋯ hv = cons h✝ (p✝.copy ⋯ ⋯)