-- Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
theorem IsAcyclic.path_unique {G : SimpleGraph V} (h : G.IsAcyclic) {v w : V} (p q : G.Path v w) :
    p = q

Proof state:
case mk.mk.cons.inl.nil
V : Type u
G : SimpleGraph V
v w u✝ v✝ : V
ph : G.Adj u✝ v✝
p : G.Walk v✝ u✝
ih : p.IsPath → ∀ (q : G.Walk v✝ u✝), q.IsPath → p = q
hp : (cons ph p).IsPath
hq : nil.IsPath
h : s(u✝, v✝) ∈ nil.edges
⊢ cons ph p = nil

Tactic:
simp [Walk.isPath_def] at hp

Result:
no goals

Proof state:
case mk.mk.cons
V : Type u
G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.IsPath → ∀ (q : G.Walk v✝ w✝), q.IsPath → p = q
hp : (cons ph p).IsPath
q : G.Walk u✝ w✝
hq : q.IsPath
h : G.Adj u✝ v✝ ∧ ∀ (p : G.Walk u✝ v✝), s(u✝, v✝) ∈ p.edges
⊢ cons ph p = q

Tactic:
replace h := h.2 (q.append p.reverse)

Result:
case mk.mk.cons
V : Type u
G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.IsPath → ∀ (q : G.Walk v✝ w✝), q.IsPath → p = q
hp : (cons ph p).IsPath
q : G.Walk u✝ w✝
hq : q.IsPath
h : s(u✝, v✝) ∈ (q.append p.reverse).edges
⊢ cons ph p = q

Proof state:
case mk
V : Type u
G : SimpleGraph V
h : G.IsAcyclic
v w : V
q : G.Path v w
p : G.Walk v w
hp : p.IsPath
⊢ ⟨p, hp⟩ = q

Tactic:
obtain ⟨q, hq⟩ := q

Result:
case mk.mk
V : Type u
G : SimpleGraph V
h : G.IsAcyclic
v w : V
p : G.Walk v w
hp : p.IsPath
q : G.Walk v w
hq : q.IsPath
⊢ ⟨p, hp⟩ = ⟨q, hq⟩

Proof state:
case mk.mk.cons
V : Type u
G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.IsPath → ∀ (q : G.Walk v✝ w✝), q.IsPath → p = q
hp : (cons ph p).IsPath
q : G.Walk u✝ w✝
hq : q.IsPath
h : G.IsBridge s(u✝, v✝)
⊢ cons ph p = q

Tactic:
rw [isBridge_iff_adj_and_forall_walk_mem_edges] at h

Result:
case mk.mk.cons
V : Type u
G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.IsPath → ∀ (q : G.Walk v✝ w✝), q.IsPath → p = q
hp : (cons ph p).IsPath
q : G.Walk u✝ w✝
hq : q.IsPath
h : G.Adj u✝ v✝ ∧ ∀ (p : G.Walk u✝ v✝), s(u✝, v✝) ∈ p.edges
⊢ cons ph p = q

Proof state:
case mk.mk.cons.inl.cons
V : Type u
G : SimpleGraph V
v w u✝ v✝¹ w✝ : V
ph : G.Adj u✝ v✝¹
p : G.Walk v✝¹ w✝
ih : p.IsPath → ∀ (q : G.Walk v✝¹ w✝), q.IsPath → p = q
hp : p.IsPath ∧ u✝ ∉ p.support
v✝ : V
h✝ : G.Adj u✝ v✝
q : G.Walk v✝ w✝
hq : q.IsPath ∧ u✝ ∉ q.support
h : s(u✝, v✝¹) ∈ (cons h✝ q).edges
⊢ cons ph p = cons h✝ q

Tactic:
simp only [Walk.edges_cons, List.mem_cons, Sym2.eq_iff, true_and] at h

Result:
case mk.mk.cons.inl.cons
V : Type u
G : SimpleGraph V
v w u✝ v✝¹ w✝ : V
ph : G.Adj u✝ v✝¹
p : G.Walk v✝¹ w✝
ih : p.IsPath → ∀ (q : G.Walk v✝¹ w✝), q.IsPath → p = q
hp : p.IsPath ∧ u✝ ∉ p.support
v✝ : V
h✝ : G.Adj u✝ v✝
q : G.Walk v✝ w✝
hq : q.IsPath ∧ u✝ ∉ q.support
h : (v✝¹ = v✝ ∨ u✝ = v✝ ∧ v✝¹ = u✝) ∨ s(u✝, v✝¹) ∈ q.edges
⊢ cons ph p = cons h✝ q

Proof state:
case mk.mk.cons.inl.cons.inl.inl.refl
V : Type u
G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.IsPath → ∀ (q : G.Walk v✝ w✝), q.IsPath → p = q
hp : p.IsPath ∧ u✝ ∉ p.support
h✝ : G.Adj u✝ v✝
q : G.Walk v✝ w✝
hq : q.IsPath ∧ u✝ ∉ q.support
⊢ cons ph p = cons h✝ q

Tactic:
cases ih hp.1 q hq.1

Result:
case mk.mk.cons.inl.cons.inl.inl.refl.refl
V : Type u
G : SimpleGraph V
v w u✝ v✝ w✝ : V
ph : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.IsPath → ∀ (q : G.Walk v✝ w✝), q.IsPath → p = q
hp : p.IsPath ∧ u✝ ∉ p.support
h✝ : G.Adj u✝ v✝
hq : p.IsPath ∧ u✝ ∉ p.support
⊢ cons ph p = cons h✝ p