-- 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.cons.inl.inr.intro
V : Type u
G : SimpleGraph V
v w v✝ w✝ : V
p : G.Walk v✝ w✝
ih : p.IsPath → ∀ (q : G.Walk v✝ w✝), q.IsPath → p = q
ph : G.Adj v✝ v✝
hp : p.IsPath ∧ v✝ ∉ p.support
h✝ : G.Adj v✝ v✝
q : G.Walk v✝ w✝
hq : q.IsPath ∧ v✝ ∉ q.support
⊢ cons ph p = cons h✝ q

Tactic:
simp at hq

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 : s(u✝, v✝) ∈ q.edges ∨ s(u✝, v✝) ∈ p.edges
⊢ cons ph p = q

Tactic:
rcases h with h | h

Result:
case mk.mk.cons.inl
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.edges
⊢ cons ph p = q

case mk.mk.cons.inr
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✝) ∈ p.edges
⊢ cons ph p = q

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

Tactic:
rw [Subtype.mk.injEq]

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 = q

Proof state:
V : Type u
G : SimpleGraph V
h : G.IsAcyclic
v w : V
p q : G.Path v w
⊢ p = q

Tactic:
obtain ⟨p, hp⟩ := p

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

Proof state:
case mk.mk.nil.refl
V : Type u
G : SimpleGraph V
h : G.IsAcyclic
v w u✝ : V
hp hq : nil.IsPath
⊢ nil = nil

Tactic:
rfl

Result:
no goals

Proof state:
case mk.mk.cons.inr
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✝) ∈ p.edges
⊢ cons ph p = q

Tactic:
rw [Walk.cons_isPath_iff] at hp

Result:
case mk.mk.cons.inr
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
q : G.Walk u✝ w✝
hq : q.IsPath
h : s(u✝, v✝) ∈ p.edges
⊢ cons ph p = q

Proof state:
case mk.mk.cons.inl.cons.inr
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✝¹) ∈ q.edges
⊢ cons ph p = cons h✝ q

Tactic:
exact absurd (Walk.fst_mem_support_of_mem_edges _ h) hq.2

Result:
no goals

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

Tactic:
rfl

Result:
no goals

Proof state:
case mk.mk.cons
V : Type u
G : SimpleGraph V
h : G.IsAcyclic
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
⊢ cons ph p = q

Tactic:
rw [isAcyclic_iff_forall_adj_isBridge] at h

Result:
case mk.mk.cons
V : Type u
G : SimpleGraph V
h : ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)
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
⊢ cons ph p = q

Proof state:
case mk.mk.cons
V : Type u
G : SimpleGraph V
h : ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)
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
⊢ cons ph p = q

Tactic:
specialize h ph

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.IsBridge s(u✝, v✝)
⊢ cons ph p = q

Proof state:
case mk.mk.nil
V : Type u
G : SimpleGraph V
h : G.IsAcyclic
v w u✝ : V
hp : nil.IsPath
q : G.Walk u✝ u✝
hq : q.IsPath
⊢ nil = q

Tactic:
cases (Walk.isPath_iff_eq_nil _).mp hq

Result:
case mk.mk.nil.refl
V : Type u
G : SimpleGraph V
h : G.IsAcyclic
v w u✝ : V
hp hq : nil.IsPath
⊢ nil = nil

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 : (v✝¹ = v✝ ∨ u✝ = v✝ ∧ v✝¹ = u✝) ∨ s(u✝, v✝¹) ∈ q.edges
⊢ cons ph p = cons h✝ q

Tactic:
rcases h with (⟨h, rfl⟩ | ⟨rfl, rfl⟩) | h

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

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

case mk.mk.cons.inl.cons.inr
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✝¹) ∈ q.edges
⊢ cons ph p = cons h✝ q

Proof state:
case mk.mk.cons.inr
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
q : G.Walk u✝ w✝
hq : q.IsPath
h : s(u✝, v✝) ∈ p.edges
⊢ cons ph p = q

Tactic:
exact absurd (Walk.fst_mem_support_of_mem_edges _ h) hp.2

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 : s(u✝, v✝) ∈ (q.append p.reverse).edges
⊢ cons ph p = q

Tactic:
simp only [Walk.edges_append, Walk.edges_reverse, List.mem_append, List.mem_reverse] 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 : s(u✝, v✝) ∈ q.edges ∨ 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 : (cons ph p).IsPath
v✝ : V
h✝ : G.Adj u✝ v✝
q : G.Walk v✝ w✝
hq : (cons h✝ q).IsPath
h : s(u✝, v✝¹) ∈ (cons h✝ q).edges
⊢ cons ph p = cons h✝ q

Tactic:
rw [Walk.cons_isPath_iff] at hp hq

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 : s(u✝, v✝¹) ∈ (cons h✝ q).edges
⊢ cons ph p = cons h✝ q