no goals
α : Type u_2
β : Type u_1
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : BoundedSMul α β
s : α
x y : β
⊢ edist (s • x) (s • y) = ‖s‖₊ • edist x y
simp only [edist_nndist, nndist_smul₀, ENNReal.coe_mul, ENNReal.smul_def, smul_eq_mul]