-- Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
theorem isTree_iff_existsUnique_path :
    G.IsTree ↔ Nonempty V ∧ ∀ v w : V, ∃! p : G.Walk v w, p.IsPath

Proof state:
case mpr.intro.refine_2
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
⊢ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q

Tactic:
rintro v w ⟨p, hp⟩ ⟨q, hq⟩

Result:
case mpr.intro.refine_2.mk.mk
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
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 h
V : Type u
G : SimpleGraph V
hc : G.Connected
hu : ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
v w : V
q : G.Path v w := (Nonempty.some ⋯).toPath
p : G.Walk v w
hp : p.IsPath
⊢ p = ↑q

Tactic:
specialize hu ⟨p, hp⟩ q

Result:
case h
V : Type u
G : SimpleGraph V
hc : G.Connected
v w : V
q : G.Path v w := (Nonempty.some ⋯).toPath
p : G.Walk v w
hp : p.IsPath
hu : ⟨p, hp⟩ = q
⊢ p = ↑q

Proof state:
case h
V : Type u
G : SimpleGraph V
hc : G.Connected
v w : V
q : G.Path v w := (Nonempty.some ⋯).toPath
p : G.Walk v w
hp : p.IsPath
hu : ⟨p, hp⟩ = q
⊢ p = ↑q

Tactic:
exact Subtype.ext_iff.mp hu

Result:
no goals

Proof state:
case mpr.intro.refine_2.mk.mk
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
v w : V
p : G.Walk v w
hp : p.IsPath
q : G.Walk v w
hq : q.IsPath
⊢ ⟨p, hp⟩ = ⟨q, hq⟩

Tactic:
simp only [ExistsUnique.unique (h v w) hp hq]

Result:
no goals

Proof state:
case mpr.intro.refine_1
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
v w : V
⊢ G.Reachable v w

Tactic:
obtain ⟨p, _⟩ := h v w

Result:
case mpr.intro.refine_1.intro
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
v w : V
p : G.Walk v w
h✝ : (fun p => p.IsPath) p ∧ ∀ (y : G.Walk v w), (fun p => p.IsPath) y → y = p
⊢ G.Reachable v w

Proof state:
case mpr.intro.refine_1
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
⊢ G.Preconnected

Tactic:
intro v w

Result:
case mpr.intro.refine_1
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
v w : V
⊢ G.Reachable v w

Proof state:
case mpr.intro.refine_1.intro
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
v w : V
p : G.Walk v w
h✝ : (fun p => p.IsPath) p ∧ ∀ (y : G.Walk v w), (fun p => p.IsPath) y → y = p
⊢ G.Reachable v w

Tactic:
exact p.reachable

Result:
no goals

Proof state:
case mp.intro
V : Type u
G : SimpleGraph V
hc : G.Connected
hu : ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
v w : V
q : G.Path v w := (Nonempty.some ⋯).toPath
⊢ ∃! p, p.IsPath

Tactic:
use q

Result:
case h
V : Type u
G : SimpleGraph V
hc : G.Connected
hu : ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
v w : V
q : G.Path v w := (Nonempty.some ⋯).toPath
⊢ (fun p => p.IsPath) ↑q ∧ ∀ (y : G.Walk v w), (fun p => p.IsPath) y → y = ↑q

Proof state:
case h
V : Type u
G : SimpleGraph V
hc : G.Connected
hu : ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
v w : V
q : G.Path v w := (Nonempty.some ⋯).toPath
⊢ ∀ (y : G.Walk v w), y.IsPath → y = ↑q

Tactic:
intro p hp

Result:
case h
V : Type u
G : SimpleGraph V
hc : G.Connected
hu : ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
v w : V
q : G.Path v w := (Nonempty.some ⋯).toPath
p : G.Walk v w
hp : p.IsPath
⊢ p = ↑q

Proof state:
case mp.intro
V : Type u
G : SimpleGraph V
hc : G.Connected
hu : ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
⊢ Nonempty V ∧ ∀ (v w : V), ∃! p, p.IsPath

Tactic:
refine ⟨hc.nonempty, ?_⟩

Result:
case mp.intro
V : Type u
G : SimpleGraph V
hc : G.Connected
hu : ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
⊢ ∀ (v w : V), ∃! p, p.IsPath

Proof state:
case mp.intro
V : Type u
G : SimpleGraph V
hc : G.Connected
hu : ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
⊢ ∀ (v w : V), ∃! p, p.IsPath

Tactic:
intro v w

Result:
case mp.intro
V : Type u
G : SimpleGraph V
hc : G.Connected
hu : ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
v w : V
⊢ ∃! p, p.IsPath

Proof state:
case mp
V : Type u
G : SimpleGraph V
⊢ (G.Connected ∧ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q) → Nonempty V ∧ ∀ (v w : V), ∃! p, p.IsPath

Tactic:
rintro ⟨hc, hu⟩

Result:
case mp.intro
V : Type u
G : SimpleGraph V
hc : G.Connected
hu : ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
⊢ Nonempty V ∧ ∀ (v w : V), ∃! p, p.IsPath

Proof state:
case mpr.intro
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
⊢ G.Connected ∧ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q

Tactic:
refine ⟨Connected.mk ?_, ?_⟩

Result:
case mpr.intro.refine_1
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
⊢ G.Preconnected

case mpr.intro.refine_2
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
⊢ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q

Proof state:
case h
V : Type u
G : SimpleGraph V
hc : G.Connected
hu : ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
v w : V
q : G.Path v w := (Nonempty.some ⋯).toPath
⊢ (fun p => p.IsPath) ↑q ∧ ∀ (y : G.Walk v w), (fun p => p.IsPath) y → y = ↑q

Tactic:
simp only [true_and, Path.isPath]

Result:
case h
V : Type u
G : SimpleGraph V
hc : G.Connected
hu : ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
v w : V
q : G.Path v w := (Nonempty.some ⋯).toPath
⊢ ∀ (y : G.Walk v w), y.IsPath → y = ↑q

Proof state:
case mpr
V : Type u
G : SimpleGraph V
⊢ (Nonempty V ∧ ∀ (v w : V), ∃! p, p.IsPath) → G.Connected ∧ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q

Tactic:
rintro ⟨hV, h⟩

Result:
case mpr.intro
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
⊢ G.Connected ∧ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q

Proof state:
V : Type u
G : SimpleGraph V
⊢ G.IsTree ↔ Nonempty V ∧ ∀ (v w : V), ∃! p, p.IsPath

Tactic:
rw [isTree_iff, isAcyclic_iff_path_unique]

Result:
V : Type u
G : SimpleGraph V
⊢ (G.Connected ∧ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q) ↔ Nonempty V ∧ ∀ (v w : V), ∃! p, p.IsPath

Proof state:
V : Type u
G : SimpleGraph V
⊢ (G.Connected ∧ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q) ↔ Nonempty V ∧ ∀ (v w : V), ∃! p, p.IsPath

Tactic:
constructor

Result:
case mp
V : Type u
G : SimpleGraph V
⊢ (G.Connected ∧ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q) → Nonempty V ∧ ∀ (v w : V), ∃! p, p.IsPath

case mpr
V : Type u
G : SimpleGraph V
⊢ (Nonempty V ∧ ∀ (v w : V), ∃! p, p.IsPath) → G.Connected ∧ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q

Proof state:
case mp.intro
V : Type u
G : SimpleGraph V
hc : G.Connected
hu : ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
v w : V
⊢ ∃! p, p.IsPath

Tactic:
let q := (hc v w).some.toPath

Result:
case mp.intro
V : Type u
G : SimpleGraph V
hc : G.Connected
hu : ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
v w : V
q : G.Path v w := (Nonempty.some ⋯).toPath
⊢ ∃! p, p.IsPath