no goals
α : Type u_2
β : Type u_1
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : BoundedSMul α β
s : α
x y : β
⊢ dist (s • x) (s • y) = ‖s‖ * dist x y
simp_rw [dist_eq_norm, (norm_smul s (x - y)).symm, smul_sub]