simp [List.pathLength]
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
r : ℝ
hr : 0 ≤ r
h : ∀ (x y : V), x ≠ y → r ≤ dist x y
head✝ : V
x✝ : List.Chain' (fun x x_1 => x ≠ x_1) [head✝]
⊢ ↑[head✝].length * r ≤ [head✝].pathLength + r
no goals