V : Type u
G : SimpleGraph V
⊢ (Connected G ∧ ∀ ⦃v w : V⦄ (p q : Path G v w), p = q) ↔ Nonempty V ∧ ∀ (v w : V), ∃! p, Walk.IsPath p
V : Type u
G : SimpleGraph V
⊢ IsTree G ↔ Nonempty V ∧ ∀ (v w : V), ∃! p, Walk.IsPath p
rw [IsTree_iff, isAcyclic_iff_path_unique]
case mp
V : Type u
G : SimpleGraph V
⊢ (Connected G ∧ ∀ ⦃v w : V⦄ (p q : Path G v w), p = q) → Nonempty V ∧ ∀ (v w : V), ∃! p, Walk.IsPath p

case mpr
V : Type u
G : SimpleGraph V
⊢ (Nonempty V ∧ ∀ (v w : V), ∃! p, Walk.IsPath p) → Connected G ∧ ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
V : Type u
G : SimpleGraph V
⊢ (Connected G ∧ ∀ ⦃v w : V⦄ (p q : Path G v w), p = q) ↔ Nonempty V ∧ ∀ (v w : V), ∃! p, Walk.IsPath p
constructor
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
⊢ Nonempty V ∧ ∀ (v w : V), ∃! p, Walk.IsPath p
case mp
V : Type u
G : SimpleGraph V
⊢ (Connected G ∧ ∀ ⦃v w : V⦄ (p q : Path G v w), p = q) → Nonempty V ∧ ∀ (v w : V), ∃! p, Walk.IsPath p
rintro ⟨hc, hu⟩
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
⊢ ∀ (v w : V), ∃! p, Walk.IsPath p
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
⊢ Nonempty V ∧ ∀ (v w : V), ∃! p, Walk.IsPath p
refine ⟨hc.nonempty, ?_⟩
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
v w : V
⊢ ∃! p, Walk.IsPath p
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
⊢ ∀ (v w : V), ∃! p, Walk.IsPath p
intro v w
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
v w : V
q : Path G v w := Walk.toPath (Nonempty.some (_ : Reachable G v w))
⊢ ∃! p, Walk.IsPath p
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
v w : V
⊢ ∃! p, Walk.IsPath p
let q := (hc v w).some.toPath
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
v w : V
q : Path G v w := Walk.toPath (Nonempty.some (_ : Reachable G v w))
⊢ (fun p => Walk.IsPath p) ↑q ∧ ∀ (y : Walk G v w), (fun p => Walk.IsPath p) y → y = ↑q
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
v w : V
q : Path G v w := Walk.toPath (Nonempty.some (_ : Reachable G v w))
⊢ ∃! p, Walk.IsPath p
use q
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
v w : V
q : Path G v w := Walk.toPath (Nonempty.some (_ : Reachable G v w))
⊢ ∀ (y : Walk G v w), Walk.IsPath y → y = ↑(Walk.toPath (Nonempty.some (_ : Reachable G v w)))
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
v w : V
q : Path G v w := Walk.toPath (Nonempty.some (_ : Reachable G v w))
⊢ (fun p => Walk.IsPath p) ↑q ∧ ∀ (y : Walk G v w), (fun p => Walk.IsPath p) y → y = ↑q
simp only [true_and_iff, Path.isPath]
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
v w : V
q : Path G v w := Walk.toPath (Nonempty.some (_ : Reachable G v w))
p : Walk G v w
hp : Walk.IsPath p
⊢ p = ↑(Walk.toPath (Nonempty.some (_ : Reachable G v w)))
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
v w : V
q : Path G v w := Walk.toPath (Nonempty.some (_ : Reachable G v w))
⊢ ∀ (y : Walk G v w), Walk.IsPath y → y = ↑(Walk.toPath (Nonempty.some (_ : Reachable G v w)))
intro p hp
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
v w : V
q : Path G v w := Walk.toPath (Nonempty.some (_ : Reachable G v w))
p : Walk G v w
hp : Walk.IsPath p
hu : { val := p, property := hp } = q
⊢ p = ↑(Walk.toPath (Nonempty.some (_ : Reachable G v w)))
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
hu : ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
v w : V
q : Path G v w := Walk.toPath (Nonempty.some (_ : Reachable G v w))
p : Walk G v w
hp : Walk.IsPath p
⊢ p = ↑(Walk.toPath (Nonempty.some (_ : Reachable G v w)))
specialize hu ⟨p, hp⟩ q
no goals
case mp.intro
V : Type u
G : SimpleGraph V
hc : Connected G
v w : V
q : Path G v w := Walk.toPath (Nonempty.some (_ : Reachable G v w))
p : Walk G v w
hp : Walk.IsPath p
hu : { val := p, property := hp } = q
⊢ p = ↑(Walk.toPath (Nonempty.some (_ : Reachable G v w)))
exact Subtype.ext_iff.mp hu
case mpr.intro
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, Walk.IsPath p
⊢ Connected G ∧ ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
case mpr
V : Type u
G : SimpleGraph V
⊢ (Nonempty V ∧ ∀ (v w : V), ∃! p, Walk.IsPath p) → Connected G ∧ ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
rintro ⟨hV, h⟩
case mpr.intro.refine_1
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, Walk.IsPath p
⊢ Preconnected G

case mpr.intro.refine_2
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, Walk.IsPath p
⊢ ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
case mpr.intro
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, Walk.IsPath p
⊢ Connected G ∧ ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
refine ⟨Connected.mk ?_, ?_⟩
case mpr.intro.refine_1
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, Walk.IsPath p
v w : V
⊢ Reachable G v w
case mpr.intro.refine_1
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, Walk.IsPath p
⊢ Preconnected G
intro v w
case mpr.intro.refine_1.intro
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, Walk.IsPath p
v w : V
p : Walk G v w
h✝ : (fun p => Walk.IsPath p) p ∧ ∀ (y : Walk G v w), (fun p => Walk.IsPath p) y → y = p
⊢ Reachable G v w
case mpr.intro.refine_1
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, Walk.IsPath p
v w : V
⊢ Reachable G v w
obtain ⟨p, _⟩ := h v w
no goals
case mpr.intro.refine_1.intro
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, Walk.IsPath p
v w : V
p : Walk G v w
h✝ : (fun p => Walk.IsPath p) p ∧ ∀ (y : Walk G v w), (fun p => Walk.IsPath p) y → y = p
⊢ Reachable G v w
exact p.reachable
case mpr.intro.refine_2.mk.mk
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, Walk.IsPath p
v w : V
p : Walk G v w
hp : Walk.IsPath p
q : Walk G v w
hq : Walk.IsPath q
⊢ { val := p, property := hp } = { val := q, property := hq }
case mpr.intro.refine_2
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, Walk.IsPath p
⊢ ∀ ⦃v w : V⦄ (p q : Path G v w), p = q
rintro v w ⟨p, hp⟩ ⟨q, hq⟩
no goals
case mpr.intro.refine_2.mk.mk
V : Type u
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, Walk.IsPath p
v w : V
p : Walk G v w
hp : Walk.IsPath p
q : Walk G v w
hq : Walk.IsPath q
⊢ { val := p, property := hp } = { val := q, property := hq }
simp only [ExistsUnique.unique (h v w) hp hq]