∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] (v : E) (s : Set ℝ),
  (MeasureTheory.Measure.hausdorffMeasure 1) ((fun r => r • v) '' s) =
    ‖v‖₊ • (MeasureTheory.Measure.hausdorffMeasure 1) s