-- Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
theorem isAcyclic_of_path_unique (h : ∀ (v w : V) (p q : G.Path v w), p = q) : G.IsAcyclic

Proof state:
case cons
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : G.Path v w), p = q
v v✝ : V
ha : G.Adj v v✝
c' : G.Walk v✝ v
hc : (cons ha c').IsTrail ∧ ¬cons ha c' = nil ∧ (cons ha c').support.tail.Nodup
⊢ False

Tactic:
simp only [Walk.cons_isTrail_iff, Walk.support_cons, List.tail_cons] at hc

Result:
case cons
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : G.Path v w), p = q
v v✝ : V
ha : G.Adj v v✝
c' : G.Walk v✝ v
hc : (c'.IsTrail ∧ s(v, v✝) ∉ c'.edges) ∧ ¬cons ha c' = nil ∧ c'.support.Nodup
⊢ False

Proof state:
case cons
V : Type u
G : SimpleGraph V
v v✝ : V
ha : G.Adj v v✝
c' : G.Walk v✝ v
hc : (c'.IsTrail ∧ s(v, v✝) ∉ c'.edges) ∧ ¬cons ha c' = nil ∧ c'.support.Nodup
h : ⟨c', ⋯⟩ = Path.singleton ⋯
⊢ False

Tactic:
rw [Path.singleton, Subtype.mk.injEq] at h

Result:
case cons
V : Type u
G : SimpleGraph V
v v✝ : V
ha : G.Adj v v✝
c' : G.Walk v✝ v
hc : (c'.IsTrail ∧ s(v, v✝) ∉ c'.edges) ∧ ¬cons ha c' = nil ∧ c'.support.Nodup
h : c' = cons ⋯ nil
⊢ False

Proof state:
case nil
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : G.Path v w), p = q
v : V
hc : nil.IsTrail ∧ ¬nil = nil ∧ nil.support.tail.Nodup
⊢ False

Tactic:
cases hc.2.1 rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : G.Path v w), p = q
v : V
c : G.Walk v v
hc : c.IsTrail ∧ ¬c = nil ∧ c.support.tail.Nodup
⊢ False

Tactic:
cases c with
| nil => cases hc.2.1 rfl
| cons ha c' =>
  simp only [Walk.cons_isTrail_iff, Walk.support_cons, List.tail_cons] at hc
  specialize h _ _ ⟨c', by simp only [Walk.isPath_def, hc.2]⟩ (Path.singleton ha.symm)
  rw [Path.singleton, Subtype.mk.injEq] at h
  simp [h] at hc

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : G.Path v w), p = q
v v✝ : V
ha : G.Adj v v✝
c' : G.Walk v✝ v
hc : (c'.IsTrail ∧ s(v, v✝) ∉ c'.edges) ∧ ¬cons ha c' = nil ∧ c'.support.Nodup
⊢ c'.IsPath

Tactic:
simp only [Walk.isPath_def, hc.2]

Result:
no goals

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

Tactic:
intro v c hc

Result:
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : G.Path v w), p = q
v : V
c : G.Walk v v
hc : c.IsCycle
⊢ False

Proof state:
case cons
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : G.Path v w), p = q
v v✝ : V
ha : G.Adj v v✝
c' : G.Walk v✝ v
hc : (c'.IsTrail ∧ s(v, v✝) ∉ c'.edges) ∧ ¬cons ha c' = nil ∧ c'.support.Nodup
⊢ False

Tactic:
specialize h _ _ ⟨c', by simp only [Walk.isPath_def, hc.2]⟩ (Path.singleton ha.symm)

Result:
case cons
V : Type u
G : SimpleGraph V
v v✝ : V
ha : G.Adj v v✝
c' : G.Walk v✝ v
hc : (c'.IsTrail ∧ s(v, v✝) ∉ c'.edges) ∧ ¬cons ha c' = nil ∧ c'.support.Nodup
h : ⟨c', ⋯⟩ = Path.singleton ⋯
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : G.Path v w), p = q
v : V
c : G.Walk v v
hc : c.IsCycle
⊢ False

Tactic:
simp only [Walk.isCycle_def, Ne] at hc

Result:
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : G.Path v w), p = q
v : V
c : G.Walk v v
hc : c.IsTrail ∧ ¬c = nil ∧ c.support.tail.Nodup
⊢ False

Proof state:
case cons
V : Type u
G : SimpleGraph V
v v✝ : V
ha : G.Adj v v✝
c' : G.Walk v✝ v
hc : (c'.IsTrail ∧ s(v, v✝) ∉ c'.edges) ∧ ¬cons ha c' = nil ∧ c'.support.Nodup
h : c' = cons ⋯ nil
⊢ False

Tactic:
simp [h] at hc

Result:
no goals