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
V : Type u_1
G : SimpleGraph V
u v : V
h : Reachable G u v
⊢ dist G u v ≤ dist G v u
obtain ⟨p, hp⟩ := h.symm.exists_walk_of_dist
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)
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
rw [← hp, ← Walk.length_reverse]
no goals
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)
apply dist_le