no goals
ι : Type ?u.2204078
inst✝ : Fintype ι
a : ℝ
h : a ≠ 0
⊢ Measure.map (fun x => a * x) volume = ofReal (abs a⁻¹) • volume
conv_rhs =>
  rw [← Real.smul_map_volume_mul_left h, smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ←
    abs_mul, inv_mul_cancel h, abs_one, ENNReal.ofReal_one, one_smul]