no goals
α : Type ?u.8057
V : Type u_2
P : Type u_1
W : Type ?u.8066
Q : Type ?u.8069
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
v₁ v₂ : V
x : P
⊢ dist (v₁ +ᵥ x) (v₂ +ᵥ x) = dist v₁ v₂
rw [dist_eq_norm_vsub V, dist_eq_norm, vadd_vsub_vadd_cancel_right]