NNReal.smul_map_volume_mul_left

theorem NNReal.smul_map_volume_mul_left {a : ℝ≥0} (h : a ≠ 0) :    a • Measure.map (a * ·) volume = volume := by  ext s hs  rw [NNReal.volume_val, ← Real.smul_map_volume_mul_left (a := a) (by simpa)]  simp only [Measure.smul_apply, Measure.nnreal_smul_coe_apply, NNReal.abs_eq, ofReal_coe_nnreal,    val_eq_coe, smul_eq_mul]  congr 1  rw [Measure.map_apply (by fun_prop) hs, Measure.map_apply (by fun_prop), NNReal.volume_val]  rotate_left  · exact (MeasurableEmbedding.subtype_coe measurableSet_Ici).measurableSet_image.mpr hs  congr 1  ext x  simp only [val_eq_coe, mem_image, mem_preimage, Subtype.exists]  simp_rw [← val_eq_coe, exists_and_right, exists_eq_right]  constructor  · rintro ⟨hx, hax⟩    apply Exists.intro    · exact hax    exact mul_nonneg (by simp) hx  · rintro ⟨hx, hax⟩    apply Exists.intro    · exact hax    rwa [mul_nonneg_iff_right_nonneg_of_pos] at hx    simp only [val_eq_coe, coe_pos]    exact h.pos