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

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
V : Type u_1
G : SimpleGraph V
u v : V
⊢ dist G u v = dist G v u
by_cases h : G.Reachable u v
no goals
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
apply le_antisymm (dist_comm_aux h) (dist_comm_aux h.symm)
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
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
have h' : ¬G.Reachable v u := fun h' => absurd h'.symm h
no goals
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
simp [h, h', dist_eq_zero_of_not_reachable]