-- 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 nil.cons.intro
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ : V
h h✝ : G.Adj u✝ w
p✝ : G.Walk w v'
he : nil = p✝.concat h'
⊢ False

Tactic:
exact concat_ne_nil _ _ he.symm

Result:
no goals

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'
⊢ False

Tactic:
simp only [concat_nil, concat_cons, cons.injEq] at he

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 : w = v✝ ∧ HEq nil (p✝.concat h')
⊢ False

Proof state:
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

Tactic:
exfalso

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'
⊢ False

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 : HEq (p✝¹.concat h) (p✝.concat h')
⊢ ∃ (hv : w✝ = v'), (cons h✝¹ p✝¹).copy ⋯ hv = cons h✝ p✝

Tactic:
rw [heq_iff_eq] at 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 : p✝¹.concat h = p✝.concat h'
⊢ ∃ (hv : w✝ = v'), (cons h✝¹ p✝¹).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:
rw [concat_cons] at he

Result:
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'

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

Tactic:
simp only [heq_iff_eq] at he

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

Proof state:
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

Tactic:
exact ⟨rfl, rfl⟩

Result:
no goals

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

Tactic:
exact concat_ne_nil _ _ he

Result:
no goals

Proof state:
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 ⋯ ⋯)

Tactic:
exact ⟨rfl, rfl⟩

Result:
no goals

Proof state:
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 : v✝ = w ∧ HEq (p✝.concat h) nil
⊢ False

Tactic:
obtain ⟨rfl, he⟩ := he

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

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 : cons h✝¹ (p✝¹.concat h) = (cons h✝ p✝).concat h'
⊢ ∃ (hv : w✝ = v'), (cons h✝¹ p✝¹).copy ⋯ hv = cons h✝ p✝

Tactic:
rw [concat_cons, cons.injEq] at he

Result:
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✝

Proof state:
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'
⊢ False

Tactic:
simp only [concat_nil, cons.injEq] at he

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 : v✝ = w ∧ HEq (p✝.concat h) nil
⊢ False

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

Tactic:
rw [heq_iff_eq] at he

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

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 : w = v✝ ∧ HEq nil (p✝.concat h')
⊢ False

Tactic:
obtain ⟨rfl, he⟩ := he

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