[GOAL]
V : Type u_1
G : SimpleGraph V
u v : V
⊢ dist G u v = 0 ↔ u = v ∨ ¬Reachable G u v
[PROOFSTEP]
simp [dist, Nat.sInf_eq_zero, Reachable]
[GOAL]
V : Type u_1
G : SimpleGraph V
v : V
⊢ dist G v v = 0
[PROOFSTEP]
simp
[GOAL]
V : Type u_1
G : SimpleGraph V
u v : V
hr : Reachable G u v
⊢ dist G u v = 0 ↔ u = v
[PROOFSTEP]
simp [hr]
[GOAL]
V : Type u_1
G : SimpleGraph V
u v : V
h : Reachable G u v
hne : u ≠ v
⊢ dist G u v ≠ 0
[PROOFSTEP]
simp [h, hne]
[GOAL]
V : Type u_1
G : SimpleGraph V
hconn : Connected G
u v : V
⊢ dist G u v = 0 ↔ u = v
[PROOFSTEP]
simp [hconn u v]
[GOAL]
V : Type u_1
G : SimpleGraph V
u v : V
hconn : Connected G
hne : u ≠ v
⊢ dist G u v ≠ 0
[PROOFSTEP]
intro h
[GOAL]
V : Type u_1
G : SimpleGraph V
u v : V
hconn : Connected G
hne : u ≠ v
h : dist G u v = 0
⊢ False
[PROOFSTEP]
exact False.elim (hne (hconn.dist_eq_zero_iff.mp h))
[GOAL]
V : Type u_1
G : SimpleGraph V
u v : V
h : ¬Reachable G u v
⊢ dist G u v = 0
[PROOFSTEP]
simp [h]
[GOAL]
V : Type u_1
G : SimpleGraph V
u v : V
h : 0 < dist G u v
⊢ Set.Nonempty Set.univ
[PROOFSTEP]
simpa [Set.range_nonempty_iff_nonempty, Set.nonempty_iff_univ_nonempty] using Nat.nonempty_of_pos_sInf h
[GOAL]
V : Type u_1
G : SimpleGraph V
hconn : Connected G
u v w : V
⊢ dist G u w ≤ dist G u v + dist G v w
[PROOFSTEP]
obtain ⟨p, hp⟩ := hconn.exists_walk_of_dist u v
[GOAL]
case intro
V : Type u_1
G : SimpleGraph V
hconn : Connected G
u v w : V
p : Walk G u v
hp : Walk.length p = dist G u v
⊢ dist G u w ≤ dist G u v + dist G v w
[PROOFSTEP]
obtain ⟨q, hq⟩ := hconn.exists_walk_of_dist v w
[GOAL]
case intro.intro
V : Type u_1
G : SimpleGraph V
hconn : Connected G
u v w : V
p : Walk G u v
hp : Walk.length p = dist G u v
q : Walk G v w
hq : Walk.length q = dist G v w
⊢ dist G u w ≤ dist G u v + dist G v w
[PROOFSTEP]
rw [← hp, ← hq, ← Walk.length_append]
[GOAL]
case intro.intro
V : Type u_1
G : SimpleGraph V
hconn : Connected G
u v w : V
p : Walk G u v
hp : Walk.length p = dist G u v
q : Walk G v w
hq : Walk.length q = dist G v w
⊢ dist G u w ≤ Walk.length (Walk.append p q)
[PROOFSTEP]
apply dist_le
[GOAL]
V : Type u_1
G : SimpleGraph V
u v : V
h : Reachable G u v
⊢ dist G u v ≤ dist G v u
[PROOFSTEP]
obtain ⟨p, hp⟩ := h.symm.exists_walk_of_dist
[GOAL]
case intro
V : Type u_1
G : SimpleGraph V
u v : V
h : Reachable G u v
p : Walk G v u
hp : Walk.length p = dist G v u
⊢ dist G u v ≤ dist G v u
[PROOFSTEP]
rw [← hp, ← Walk.length_reverse]
[GOAL]
case intro
V : Type u_1
G : SimpleGraph V
u v : V
h : Reachable G u v
p : Walk G v u
hp : Walk.length p = dist G v u
⊢ dist G u v ≤ Walk.length (Walk.reverse p)
[PROOFSTEP]
apply dist_le
[GOAL]
V : Type u_1
G : SimpleGraph V
u v : V
⊢ dist G u v = dist G v u
[PROOFSTEP]
by_cases h : G.Reachable u v
[GOAL]
case pos
V : Type u_1
G : SimpleGraph V
u v : V
h : Reachable G u v
⊢ dist G u v = dist G v u
[PROOFSTEP]
apply le_antisymm (dist_comm_aux h) (dist_comm_aux h.symm)
[GOAL]
case neg
V : Type u_1
G : SimpleGraph V
u v : V
h : ¬Reachable G u v
⊢ dist G u v = dist G v u
[PROOFSTEP]
have h' : ¬G.Reachable v u := fun h' => absurd h'.symm h
[GOAL]
case neg
V : Type u_1
G : SimpleGraph V
u v : V
h : ¬Reachable G u v
h' : ¬Reachable G v u
⊢ dist G u v = dist G v u
[PROOFSTEP]
simp [h, h', dist_eq_zero_of_not_reachable]
