no goals
α : Type ?u.11888
V : Type u_2
P : Type u_1
W : Type ?u.11897
Q : Type ?u.11900
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
v : V
x : P
⊢ dist x (v +ᵥ x) = ‖v‖
rw [dist_comm, dist_vadd_left]