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
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
obtain ⟨p, hp⟩ := hconn.exists_walk_of_dist u v
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
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
obtain ⟨q, hq⟩ := hconn.exists_walk_of_dist v w
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)
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
rw [← hp, ← hq, ← Walk.length_append]
no goals
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)
apply dist_le