-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem edges_injective {u v : V} : Function.Injective (Walk.edges : G.Walk u v → List (Sym2 V))
  | .nil, .nil, _ => rfl
  | .nil, .cons _ _, h => by simp at h
  | .cons _ _, .nil, h => by simp at h
  | .cons' u v c h₁ w₁, .cons' _ v' _ h₂ w₂, h => by
    have h₃ : u ≠ v'

Proof state:
case intro
V : Type u
G : SimpleGraph V
u✝ v✝ u c v : V
h₁ : G.Adj u v
w₁ : G.Walk v c
h₂ : G.Adj u v
h₃✝ : u ≠ v
h : (cons' u v c h₁ w₁).edges = (cons' u v c h₂ w₁).edges
h₃ : w₁.edges = w₁.edges
⊢ cons' u v c h₁ w₁ = cons' u v c h₂ w₁

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u✝ v✝ u c v : V
h₁ : G.Adj u v
w₁ : G.Walk v c
v' : V
h₂ : G.Adj u v'
w₂ : G.Walk v' c
h : (cons' u v c h₁ w₁).edges = (cons' u v' c h₂ w₂).edges
⊢ cons' u v c h₁ w₁ = cons' u v' c h₂ w₂

Tactic:
have h₃ : u ≠ v' := by rintro rfl; exact G.loopless _ h₂

Result:
V : Type u
G : SimpleGraph V
u✝ v✝ u c v : V
h₁ : G.Adj u v
w₁ : G.Walk v c
v' : V
h₂ : G.Adj u v'
w₂ : G.Walk v' c
h : (cons' u v c h₁ w₁).edges = (cons' u v' c h₂ w₂).edges
h₃ : u ≠ v'
⊢ cons' u v c h₁ w₁ = cons' u v' c h₂ w₂

Proof state:
V : Type u
G : SimpleGraph V
u✝ v✝ u c v : V
h₁ : G.Adj u v
w₁ : G.Walk v c
h₂ : G.Adj u u
w₂ : G.Walk u c
h : (cons' u v c h₁ w₁).edges = (cons' u u c h₂ w₂).edges
⊢ False

Tactic:
exact G.loopless _ h₂

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u✝ v✝ u c v : V
h₁ : G.Adj u v
w₁ : G.Walk v c
v' : V
h₂ : G.Adj u v'
w₂ : G.Walk v' c
h : (cons' u v c h₁ w₁).edges = (cons' u v' c h₂ w₂).edges
⊢ u ≠ v'

Tactic:
rintro rfl

Result:
V : Type u
G : SimpleGraph V
u✝ v✝ u c v : V
h₁ : G.Adj u v
w₁ : G.Walk v c
h₂ : G.Adj u u
w₂ : G.Walk u c
h : (cons' u v c h₁ w₁).edges = (cons' u u c h₂ w₂).edges
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
u✝ v u v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ u
h : nil.edges = (cons h✝ p✝).edges
⊢ nil = cons h✝ p✝

Tactic:
simp at h

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u✝ v✝ u c v : V
h₁ : G.Adj u v
w₁ : G.Walk v c
v' : V
h₂ : G.Adj u v'
w₂ : G.Walk v' c
h : (cons' u v c h₁ w₁).edges = (cons' u v' c h₂ w₂).edges
h₃ : u ≠ v'
⊢ cons' u v c h₁ w₁ = cons' u v' c h₂ w₂

Tactic:
obtain ⟨rfl, h₃⟩ : v = v' ∧ w₁.edges = w₂.edges := by simpa [h₁, h₃] using h

Result:
case intro
V : Type u
G : SimpleGraph V
u✝ v✝ u c v : V
h₁ : G.Adj u v
w₁ : G.Walk v c
h₂ : G.Adj u v
w₂ : G.Walk v c
h : (cons' u v c h₁ w₁).edges = (cons' u v c h₂ w₂).edges
h₃✝ : u ≠ v
h₃ : w₁.edges = w₂.edges
⊢ cons' u v c h₁ w₁ = cons' u v c h₂ w₂

Proof state:
case intro
V : Type u
G : SimpleGraph V
u✝ v✝ u c v : V
h₁ : G.Adj u v
w₁ : G.Walk v c
h₂ : G.Adj u v
w₂ : G.Walk v c
h : (cons' u v c h₁ w₁).edges = (cons' u v c h₂ w₂).edges
h₃✝ : u ≠ v
h₃ : w₁.edges = w₂.edges
⊢ cons' u v c h₁ w₁ = cons' u v c h₂ w₂

Tactic:
obtain rfl := Walk.edges_injective h₃

Result:
case intro
V : Type u
G : SimpleGraph V
u✝ v✝ u c v : V
h₁ : G.Adj u v
w₁ : G.Walk v c
h₂ : G.Adj u v
h₃✝ : u ≠ v
h : (cons' u v c h₁ w₁).edges = (cons' u v c h₂ w₁).edges
h₃ : w₁.edges = w₁.edges
⊢ cons' u v c h₁ w₁ = cons' u v c h₂ w₁

Proof state:
V : Type u
G : SimpleGraph V
u✝ v u v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ u
h : (cons h✝ p✝).edges = nil.edges
⊢ cons h✝ p✝ = nil

Tactic:
simp at h

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u✝ v✝ u c v : V
h₁ : G.Adj u v
w₁ : G.Walk v c
v' : V
h₂ : G.Adj u v'
w₂ : G.Walk v' c
h : (cons' u v c h₁ w₁).edges = (cons' u v' c h₂ w₂).edges
h₃ : u ≠ v'
⊢ v = v' ∧ w₁.edges = w₂.edges

Tactic:
simpa [h₁, h₃] using h

Result:
no goals