From bc0f9e3a0407aa27a26928315ef8b4d013575adf Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 15 May 2023 09:04:34 +0000
Subject: [PATCH 1/4] wip

---
 src/measure_theory/measure/haar_lebesgue.lean | 53 +++++++++----------
 src/measure_theory/measure/lebesgue.lean      | 47 ++++++++--------
 2 files changed, 49 insertions(+), 51 deletions(-)

diff --git a/src/measure_theory/measure/haar_lebesgue.lean b/src/measure_theory/measure/haar_lebesgue.lean
index 965c33384fa36..da06c67ef7865 100644
--- a/src/measure_theory/measure/haar_lebesgue.lean
+++ b/src/measure_theory/measure/haar_lebesgue.lean
@@ -202,7 +202,7 @@ linear equiv maps Haar measure to Haar measure.
 lemma map_linear_map_add_haar_pi_eq_smul_add_haar
   {ι : Type*} [finite ι] {f : (ι → ℝ) →ₗ[ℝ] (ι → ℝ)} (hf : f.det ≠ 0)
   (μ : measure (ι → ℝ)) [is_add_haar_measure μ] :
-  measure.map f μ = ennreal.of_real (abs (f.det)⁻¹) • μ :=
+  measure.map f μ = ‖(f.det)⁻¹‖₊ • μ :=
 begin
   casesI nonempty_fintype ι,
   /- We have already proved the result for the Lebesgue product measure, using matrices.
@@ -218,7 +218,7 @@ variables {E : Type*} [normed_add_comm_group E] [normed_space ℝ E] [measurable
 
 lemma map_linear_map_add_haar_eq_smul_add_haar
   {f : E →ₗ[ℝ] E} (hf : f.det ≠ 0) :
-  measure.map f μ = ennreal.of_real (abs (f.det)⁻¹) • μ :=
+  measure.map f μ = ‖(f.det)⁻¹‖₊ • μ :=
 begin
   -- we reduce to the case of `E = ι → ℝ`, for which we have already proved the result using
   -- matrices in `map_linear_map_add_haar_pi_eq_smul_add_haar`.
@@ -243,7 +243,7 @@ begin
   haveI : is_add_haar_measure (map e μ) := (e : E ≃+ (ι → ℝ)).is_add_haar_measure_map μ Ce Cesymm,
   have ecomp : (e.symm) ∘ e = id,
     by { ext x, simp only [id.def, function.comp_app, linear_equiv.symm_apply_apply] },
-  rw [map_linear_map_add_haar_pi_eq_smul_add_haar hf (map e μ), measure.map_smul,
+  rw [map_linear_map_add_haar_pi_eq_smul_add_haar hf (map e μ), measure.map_smul_nnreal,
     map_map Cesymm.measurable Ce.measurable, ecomp, measure.map_id]
 end
 
@@ -251,25 +251,25 @@ end
 equal to `μ s` times the absolute value of the inverse of the determinant of `f`. -/
 @[simp] lemma add_haar_preimage_linear_map
   {f : E →ₗ[ℝ] E} (hf : f.det ≠ 0) (s : set E) :
-  μ (f ⁻¹' s) = ennreal.of_real (abs (f.det)⁻¹) * μ s :=
+  μ (f ⁻¹' s) = ‖(f.det)⁻¹‖₊ • μ s :=
 calc μ (f ⁻¹' s) = measure.map f μ s :
   ((f.equiv_of_det_ne_zero hf).to_continuous_linear_equiv.to_homeomorph
     .to_measurable_equiv.map_apply s).symm
-... = ennreal.of_real (abs (f.det)⁻¹) * μ s :
+... = ‖(f.det)⁻¹‖₊ * μ s :
   by { rw map_linear_map_add_haar_eq_smul_add_haar μ hf, refl }
 
 /-- The preimage of a set `s` under a continuous linear map `f` with nonzero determinant has measure
 equal to `μ s` times the absolute value of the inverse of the determinant of `f`. -/
 @[simp] lemma add_haar_preimage_continuous_linear_map
   {f : E →L[ℝ] E} (hf : linear_map.det (f : E →ₗ[ℝ] E) ≠ 0) (s : set E) :
-  μ (f ⁻¹' s) = ennreal.of_real (abs (linear_map.det (f : E →ₗ[ℝ] E))⁻¹) * μ s :=
+  μ (f ⁻¹' s) = ‖(linear_map.det (f : E →ₗ[ℝ] E))⁻¹‖₊ • μ s :=
 add_haar_preimage_linear_map μ hf s
 
 /-- The preimage of a set `s` under a linear equiv `f` has measure
 equal to `μ s` times the absolute value of the inverse of the determinant of `f`. -/
 @[simp] lemma add_haar_preimage_linear_equiv
   (f : E ≃ₗ[ℝ] E) (s : set E) :
-  μ (f ⁻¹' s) = ennreal.of_real (abs (f.symm : E →ₗ[ℝ] E).det) * μ s :=
+  μ (f ⁻¹' s) = ‖(f.symm : E →ₗ[ℝ] E).det‖₊ • μ s :=
 begin
   have A : (f : E →ₗ[ℝ] E).det ≠ 0 := (linear_equiv.is_unit_det' f).ne_zero,
   convert add_haar_preimage_linear_map μ A s,
@@ -280,14 +280,14 @@ end
 equal to `μ s` times the absolute value of the inverse of the determinant of `f`. -/
 @[simp] lemma add_haar_preimage_continuous_linear_equiv
   (f : E ≃L[ℝ] E) (s : set E) :
-  μ (f ⁻¹' s) = ennreal.of_real (abs (f.symm : E →ₗ[ℝ] E).det) * μ s :=
+  μ (f ⁻¹' s) = ‖(f.symm : E →ₗ[ℝ] E).det‖₊ • μ s :=
 add_haar_preimage_linear_equiv μ _ s
 
 /-- The image of a set `s` under a linear map `f` has measure
 equal to `μ s` times the absolute value of the determinant of `f`. -/
 @[simp] lemma add_haar_image_linear_map
   (f : E →ₗ[ℝ] E) (s : set E) :
-  μ (f '' s) = ennreal.of_real (abs f.det) * μ s :=
+  μ (f '' s) = ‖f.det‖₊ • μ s :=
 begin
   rcases ne_or_eq f.det 0 with hf|hf,
   { let g := (f.equiv_of_det_ne_zero hf).to_continuous_linear_equiv,
@@ -297,7 +297,7 @@ begin
     ext x,
     simp only [linear_equiv.coe_to_continuous_linear_equiv, linear_equiv.of_is_unit_det_apply,
                linear_equiv.coe_coe, continuous_linear_equiv.symm_symm], },
-  { simp only [hf, zero_mul, ennreal.of_real_zero, abs_zero],
+  { simp only [hf, zero_smul, ennreal.of_real_zero, nnnorm_zero],
     have : μ f.range = 0 :=
       add_haar_submodule μ _ (linear_map.range_lt_top_of_det_eq_zero hf).ne,
     exact le_antisymm (le_trans (measure_mono (image_subset_range _ _)) this.le) (zero_le _) }
@@ -307,14 +307,14 @@ end
 equal to `μ s` times the absolute value of the determinant of `f`. -/
 @[simp] lemma add_haar_image_continuous_linear_map
   (f : E →L[ℝ] E) (s : set E) :
-  μ (f '' s) = ennreal.of_real (abs (f : E →ₗ[ℝ] E).det) * μ s :=
+  μ (f '' s) =‖(f : E →ₗ[ℝ] E).det‖₊ • μ s :=
 add_haar_image_linear_map μ _ s
 
 /-- The image of a set `s` under a continuous linear equiv `f` has measure
 equal to `μ s` times the absolute value of the determinant of `f`. -/
 @[simp] lemma add_haar_image_continuous_linear_equiv
   (f : E ≃L[ℝ] E) (s : set E) :
-  μ (f '' s) = ennreal.of_real (abs (f : E →ₗ[ℝ] E).det) * μ s :=
+  μ (f '' s) = ‖(f : E →ₗ[ℝ] E).det‖₊ • μ s :=
 μ.add_haar_image_linear_map (f : E →ₗ[ℝ] E) s
 
 /-!
@@ -322,7 +322,7 @@ equal to `μ s` times the absolute value of the determinant of `f`. -/
 -/
 
 lemma map_add_haar_smul {r : ℝ} (hr : r ≠ 0) :
-  measure.map ((•) r) μ = ennreal.of_real (abs (r ^ (finrank ℝ E))⁻¹) • μ :=
+  measure.map ((•) r) μ = ‖(r ^ (finrank ℝ E))⁻¹‖₊ • μ :=
 begin
   let f : E →ₗ[ℝ] E := r • 1,
   change measure.map f μ = _,
@@ -335,32 +335,31 @@ begin
 end
 
 @[simp] lemma add_haar_preimage_smul {r : ℝ} (hr : r ≠ 0) (s : set E) :
-  μ (((•) r) ⁻¹' s) = ennreal.of_real (abs (r ^ (finrank ℝ E))⁻¹) * μ s :=
+  μ (((•) r) ⁻¹' s) = ‖(r ^ finrank ℝ E)⁻¹‖₊ • μ s :=
 calc μ (((•) r) ⁻¹' s) = measure.map ((•) r) μ s :
   ((homeomorph.smul (is_unit_iff_ne_zero.2 hr).unit).to_measurable_equiv.map_apply s).symm
-... = ennreal.of_real (abs (r^(finrank ℝ E))⁻¹) * μ s : by { rw map_add_haar_smul μ hr, refl }
+... = ‖(r^finrank ℝ E)⁻¹‖₊ • μ s : by { rw map_add_haar_smul μ hr, refl }
 
 /-- Rescaling a set by a factor `r` multiplies its measure by `abs (r ^ dim)`. -/
 @[simp] lemma add_haar_smul (r : ℝ) (s : set E) :
-  μ (r • s) = ennreal.of_real (abs (r ^ (finrank ℝ E))) * μ s :=
+  μ (r • s) = ‖r ^ finrank ℝ E‖₊ • μ s :=
 begin
   rcases ne_or_eq r 0 with h|rfl,
   { rw [← preimage_smul_inv₀ h, add_haar_preimage_smul μ (inv_ne_zero h), inv_pow, inv_inv] },
   rcases eq_empty_or_nonempty s with rfl|hs,
-  { simp only [measure_empty, mul_zero, smul_set_empty] },
+  { simp only [measure_empty, smul_zero, smul_set_empty] },
   rw [zero_smul_set hs, ← singleton_zero],
   by_cases h : finrank ℝ E = 0,
   { haveI : subsingleton E := finrank_zero_iff.1 h,
-    simp only [h, one_mul, ennreal.of_real_one, abs_one, subsingleton.eq_univ_of_nonempty hs,
+    simp only [h, one_smul, nnnorm_one, subsingleton.eq_univ_of_nonempty hs,
       pow_zero, subsingleton.eq_univ_of_nonempty (singleton_nonempty (0 : E))] },
   { haveI : nontrivial E := nontrivial_of_finrank_pos (bot_lt_iff_ne_bot.2 h),
-    simp only [h, zero_mul, ennreal.of_real_zero, abs_zero, ne.def, not_false_iff, zero_pow',
-      measure_singleton] }
+    simp only [h, zero_smul, nnnorm_zero, ne.def, not_false_iff, zero_pow', measure_singleton] }
 end
 
 lemma add_haar_smul_of_nonneg {r : ℝ} (hr : 0 ≤ r) (s : set E) :
-  μ (r • s) = ennreal.of_real (r ^ finrank ℝ E) * μ s :=
-by rw [add_haar_smul, abs_pow, abs_of_nonneg hr]
+  μ (r • s) = (⟨r, hr⟩ ^ finrank ℝ E : ℝ≥0) • μ s :=
+by rw [add_haar_smul, nnnorm_pow, real.nnnorm_of_nonneg]
 
 variables {μ} {s : set E}
 
@@ -376,16 +375,16 @@ begin
   obtain ⟨t, ht, hst⟩ := hs,
   refine ⟨_, ht.const_smul_of_ne_zero hr, _⟩,
   rw ←measure_symm_diff_eq_zero_iff at ⊢ hst,
-  rw [←smul_set_symm_diff₀ hr, add_haar_smul μ, hst, mul_zero],
+  rw [←smul_set_symm_diff₀ hr, add_haar_smul μ, hst, smul_zero],
 end
 
 variables (μ)
 
 @[simp] lemma add_haar_image_homothety (x : E) (r : ℝ) (s : set E) :
-  μ (affine_map.homothety x r '' s) = ennreal.of_real (abs (r ^ (finrank ℝ E))) * μ s :=
+  μ (affine_map.homothety x r '' s) = ‖r ^ finrank ℝ E‖₊ • μ s :=
 calc μ (affine_map.homothety x r '' s) = μ ((λ y, y + x) '' (r • ((λ y, y + (-x)) '' s))) :
   by { simp only [← image_smul, image_image, ← sub_eq_add_neg], refl }
-... = ennreal.of_real (abs (r ^ (finrank ℝ E))) * μ s :
+... = ‖r ^ finrank ℝ E‖₊ • μ s :
   by simp only [image_add_right, measure_preimage_add_right, add_haar_smul]
 
 /-- The integral of `f (R • x)` with respect to an additive Haar measure is a multiple of the
@@ -457,7 +456,7 @@ begin
 end
 
 lemma add_haar_ball_mul_of_pos (x : E) {r : ℝ} (hr : 0 < r) (s : ℝ) :
-  μ (ball x (r * s)) = ennreal.of_real (r ^ (finrank ℝ E)) * μ (ball 0 s) :=
+  μ (ball x (r * s)) = ennreal.of_real (r ^ (finrank ℝ E)) • μ (ball 0 s) :=
 begin
   have : ball (0 : E) (r * s) = r • ball 0 s,
     by simp only [smul_ball hr.ne' (0 : E) s, real.norm_eq_abs, abs_of_nonneg hr.le, smul_zero],
@@ -465,7 +464,7 @@ begin
 end
 
 lemma add_haar_ball_of_pos (x : E) {r : ℝ} (hr : 0 < r) :
-  μ (ball x r) = ennreal.of_real (r ^ (finrank ℝ E)) * μ (ball 0 1) :=
+  μ (ball x r) = ennreal.of_real (r ^ (finrank ℝ E)) • μ (ball 0 1) :=
 by rw [← add_haar_ball_mul_of_pos μ x hr, mul_one]
 
 lemma add_haar_ball_mul [nontrivial E] (x : E) {r : ℝ} (hr : 0 ≤ r) (s : ℝ) :
diff --git a/src/measure_theory/measure/lebesgue.lean b/src/measure_theory/measure/lebesgue.lean
index c347ccce0c02b..dbeabb2bc674f 100644
--- a/src/measure_theory/measure/lebesgue.lean
+++ b/src/measure_theory/measure/lebesgue.lean
@@ -239,11 +239,14 @@ calc volume s ≤ ∏ i : ι, emetric.diam (function.eval i '' s) : volume_pi_le
 -/
 
 lemma smul_map_volume_mul_left {a : ℝ} (h : a ≠ 0) :
-  ennreal.of_real (|a|) • measure.map ((*) a) volume = volume :=
+  ‖a‖₊ • measure.map ((*) a) volume = volume :=
 begin
   refine (real.measure_ext_Ioo_rat $ λ p q, _).symm,
   cases lt_or_gt_of_ne h with h h,
-  { simp only [real.volume_Ioo, measure.smul_apply, ← ennreal.of_real_mul (le_of_lt $ neg_pos.2 h),
+  { simp_rw [measure.smul_apply,
+      measure.map_apply (measurable_const_mul a) measurable_set_Ioo,
+      preimage_const_mul_Ioo_of_neg _ _ h, real.volume_Ioo],
+    simp only [real.volume_Ioo, measure.smul_apply, ← ennreal.of_real_mul (le_of_lt $ neg_pos.2 h),
       measure.map_apply (measurable_const_mul a) measurable_set_Ioo, neg_sub_neg,
       neg_mul, preimage_const_mul_Ioo_of_neg _ _ h, abs_of_neg h, mul_sub, smul_eq_mul,
       mul_div_cancel' _ (ne_of_lt h)] },
@@ -253,30 +256,28 @@ begin
 end
 
 lemma map_volume_mul_left {a : ℝ} (h : a ≠ 0) :
-  measure.map ((*) a) volume = ennreal.of_real (|a⁻¹|) • volume :=
-by conv_rhs { rw [← real.smul_map_volume_mul_left h, smul_smul,
-  ← ennreal.of_real_mul (abs_nonneg _), ← abs_mul, inv_mul_cancel h, abs_one, ennreal.of_real_one,
-  one_smul] }
+  measure.map ((*) a) volume = ‖a⁻¹‖₊ • volume :=
+by rw [nnnorm_inv, eq_inv_smul_iff₀ (nnnorm_ne_zero_iff.mpr h), smul_map_volume_mul_left h]
 
 @[simp] lemma volume_preimage_mul_left {a : ℝ} (h : a ≠ 0) (s : set ℝ) :
-  volume (((*) a) ⁻¹' s) = ennreal.of_real (abs a⁻¹) * volume s :=
+  volume (((*) a) ⁻¹' s) = ‖a⁻¹‖₊ • volume s :=
 calc volume (((*) a) ⁻¹' s) = measure.map ((*) a) volume s :
   ((homeomorph.mul_left₀ a h).to_measurable_equiv.map_apply s).symm
-... = ennreal.of_real (abs a⁻¹) * volume s : by { rw map_volume_mul_left h, refl }
+... = ‖a⁻¹‖₊ * volume s : by { rw map_volume_mul_left h, refl }
 
 lemma smul_map_volume_mul_right {a : ℝ} (h : a ≠ 0) :
-  ennreal.of_real (|a|) • measure.map (* a) volume = volume :=
+  ‖a‖₊ • measure.map (* a) volume = volume :=
 by simpa only [mul_comm] using real.smul_map_volume_mul_left h
 
 lemma map_volume_mul_right {a : ℝ} (h : a ≠ 0) :
-  measure.map (* a) volume = ennreal.of_real (|a⁻¹|) • volume :=
+  measure.map (* a) volume = ‖a⁻¹‖₊ • volume :=
 by simpa only [mul_comm] using real.map_volume_mul_left h
 
 @[simp] lemma volume_preimage_mul_right {a : ℝ} (h : a ≠ 0) (s : set ℝ) :
-  volume ((* a) ⁻¹' s) = ennreal.of_real (abs a⁻¹) * volume s :=
+  volume ((* a) ⁻¹' s) = ‖a⁻¹‖₊ • volume s :=
 calc volume ((* a) ⁻¹' s) = measure.map (* a) volume s :
   ((homeomorph.mul_right₀ a h).to_measurable_equiv.map_apply s).symm
-... = ennreal.of_real (abs a⁻¹) * volume s : by { rw map_volume_mul_right h, refl }
+... = ‖a⁻¹‖₊ • volume s : by { rw map_volume_mul_right h, refl }
 
 /-!
 ### Images of the Lebesgue measure under translation/linear maps in ℝⁿ
@@ -288,7 +289,7 @@ open matrix
 `real.map_matrix_volume_pi_eq_smul_volume_pi`, that one should use instead (and whose proof
 uses this particular case). -/
 lemma smul_map_diagonal_volume_pi [decidable_eq ι] {D : ι → ℝ} (h : det (diagonal D) ≠ 0) :
-  ennreal.of_real (abs (det (diagonal D))) • measure.map ((diagonal D).to_lin') volume = volume :=
+  ‖det (diagonal D)‖₊ • measure.map ((diagonal D).to_lin') volume = volume :=
 begin
   refine (measure.pi_eq (λ s hs, _)).symm,
   simp only [det_diagonal, measure.coe_smul, algebra.id.smul_eq_mul, pi.smul_apply],
@@ -299,14 +300,13 @@ begin
   { ext f,
     simp only [linear_map.coe_proj, algebra.id.smul_eq_mul, linear_map.smul_apply, mem_univ_pi,
       mem_preimage, linear_map.pi_apply, diagonal_to_lin'] },
-  have B : ∀ i, of_real (abs (D i)) * volume (has_mul.mul (D i) ⁻¹' s i) = volume (s i),
+  have B : ∀ i, ‖D i‖₊ • volume (has_mul.mul (D i) ⁻¹' s i) = volume (s i),
   { assume i,
     have A : D i ≠ 0,
     { simp only [det_diagonal, ne.def] at h,
       exact finset.prod_ne_zero_iff.1 h i (finset.mem_univ i) },
-    rw [volume_preimage_mul_left A, ← mul_assoc, ← ennreal.of_real_mul (abs_nonneg _), ← abs_mul,
-      mul_inv_cancel A, abs_one, ennreal.of_real_one, one_mul] },
-  rw [this, volume_pi_pi, finset.abs_prod,
+    rw [volume_preimage_mul_left A, nnnorm_inv, smul_inv_smul₀ (nnnorm_ne_zero_iff.mpr A)] },
+  rw [this, volume_pi_pi, finset.nnnorm_prod,
     ennreal.of_real_prod_of_nonneg (λ i hi, abs_nonneg (D i)), ← finset.prod_mul_distrib],
   simp only [B]
 end
@@ -356,19 +356,18 @@ end
 /-- Any invertible matrix rescales Lebesgue measure through the absolute value of its
 determinant. -/
 lemma map_matrix_volume_pi_eq_smul_volume_pi [decidable_eq ι] {M : matrix ι ι ℝ} (hM : det M ≠ 0) :
-  measure.map M.to_lin' volume = ennreal.of_real (abs (det M)⁻¹) • volume :=
+  measure.map M.to_lin' volume = ‖(det M)⁻¹‖₊ • volume :=
 begin
   -- This follows from the cases we have already proved, of diagonal matrices and transvections,
   -- as these matrices generate all invertible matrices.
   apply diagonal_transvection_induction_of_det_ne_zero _ M hM (λ D hD, _) (λ t, _)
     (λ A B hA hB IHA IHB, _),
   { conv_rhs { rw [← smul_map_diagonal_volume_pi hD] },
-    rw [smul_smul, ← ennreal.of_real_mul (abs_nonneg _), ← abs_mul, inv_mul_cancel hD, abs_one,
-      ennreal.of_real_one, one_smul] },
+    rw [nnnorm_inv, inv_smul_smul₀ (nnnorm_ne_zero_iff.mpr hD)] },
   { simp only [matrix.transvection_struct.det, ennreal.of_real_one,
-      (volume_preserving_transvection_struct _).map_eq, one_smul, _root_.inv_one, abs_one] },
-  { rw [to_lin'_mul, det_mul, linear_map.coe_comp, ← measure.map_map, IHB, measure.map_smul,
-      IHA, smul_smul, ← ennreal.of_real_mul (abs_nonneg _), ← abs_mul, mul_comm, mul_inv],
+      (volume_preserving_transvection_struct _).map_eq, one_smul, _root_.inv_one, nnnorm_one] },
+  { rw [to_lin'_mul, det_mul, linear_map.coe_comp, ← measure.map_map, IHB, measure.map_smul_nnreal,
+      IHA, smul_smul, ← nnnorm_mul, _root_.mul_inv_rev],
     { apply continuous.measurable,
       apply linear_map.continuous_on_pi },
     { apply continuous.measurable,
@@ -378,7 +377,7 @@ end
 /-- Any invertible linear map rescales Lebesgue measure through the absolute value of its
 determinant. -/
 lemma map_linear_map_volume_pi_eq_smul_volume_pi {f : (ι → ℝ) →ₗ[ℝ] (ι → ℝ)} (hf : f.det ≠ 0) :
-  measure.map f volume = ennreal.of_real (abs (f.det)⁻¹) • volume :=
+  measure.map f volume = ‖f.det⁻¹‖₊ • volume :=
 begin
   -- this is deduced from the matrix case
   classical,

From 78101ac89a49b478b0cad14c7c8b232d3f2340d6 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 15 May 2023 09:43:41 +0000
Subject: [PATCH 2/4] wip

---
 src/data/real/ennreal.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/data/real/ennreal.lean b/src/data/real/ennreal.lean
index fda281f3e2bfe..87a4b0771316c 100644
--- a/src/data/real/ennreal.lean
+++ b/src/data/real/ennreal.lean
@@ -1708,6 +1708,11 @@ lemma of_real_nsmul {x : ℝ} {n : ℕ} :
   ennreal.of_real (n • x) = n • ennreal.of_real x :=
 by simp only [nsmul_eq_mul, ← of_real_coe_nat n, ← of_real_mul n.cast_nonneg]
 
+lemma of_real_nnreal_smul (c : ℝ≥0) (x : ℝ) :
+  ennreal.of_real (c • x) = c • ennreal.of_real x :=
+by simp_rw [nnreal.smul_def, smul_eq_mul, of_real_mul c.coe_nonneg, of_real_coe_nnreal, smul_def,
+  smul_eq_mul]
+
 lemma of_real_inv_of_pos {x : ℝ} (hx : 0 < x) :
   (ennreal.of_real x)⁻¹ = ennreal.of_real x⁻¹ :=
 by rw [ennreal.of_real, ennreal.of_real, ←@coe_inv (real.to_nnreal x) (by simp [hx]), coe_eq_coe,

From 8ef9630aa7559fd754058d1e4e62f9422f6808bb Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 15 May 2023 22:39:38 +0000
Subject: [PATCH 3/4] fix

---
 src/measure_theory/measure/lebesgue.lean | 17 +++++++----------
 1 file changed, 7 insertions(+), 10 deletions(-)

diff --git a/src/measure_theory/measure/lebesgue.lean b/src/measure_theory/measure/lebesgue.lean
index dbeabb2bc674f..f2ef45c49817d 100644
--- a/src/measure_theory/measure/lebesgue.lean
+++ b/src/measure_theory/measure/lebesgue.lean
@@ -242,17 +242,14 @@ lemma smul_map_volume_mul_left {a : ℝ} (h : a ≠ 0) :
   ‖a‖₊ • measure.map ((*) a) volume = volume :=
 begin
   refine (real.measure_ext_Ioo_rat $ λ p q, _).symm,
+  rw [measure.smul_apply, measure.map_apply (measurable_const_mul a) measurable_set_Ioo],
   cases lt_or_gt_of_ne h with h h,
-  { simp_rw [measure.smul_apply,
-      measure.map_apply (measurable_const_mul a) measurable_set_Ioo,
-      preimage_const_mul_Ioo_of_neg _ _ h, real.volume_Ioo],
-    simp only [real.volume_Ioo, measure.smul_apply, ← ennreal.of_real_mul (le_of_lt $ neg_pos.2 h),
-      measure.map_apply (measurable_const_mul a) measurable_set_Ioo, neg_sub_neg,
-      neg_mul, preimage_const_mul_Ioo_of_neg _ _ h, abs_of_neg h, mul_sub, smul_eq_mul,
-      mul_div_cancel' _ (ne_of_lt h)] },
-  { simp only [real.volume_Ioo, measure.smul_apply, ← ennreal.of_real_mul (le_of_lt h),
-      measure.map_apply (measurable_const_mul a) measurable_set_Ioo, preimage_const_mul_Ioo _ _ h,
-      abs_of_pos h, mul_sub, mul_div_cancel' _ (ne_of_gt h), smul_eq_mul] }
+  { simp_rw [preimage_const_mul_Ioo_of_neg _ _ h, real.volume_Ioo, ←ennreal.of_real_nnreal_smul,
+      nnreal.smul_def, coe_nnnorm, smul_eq_mul, norm_eq_abs, abs_of_neg h, mul_sub, neg_mul,
+      neg_sub_neg, mul_div_cancel' _ (ne_of_lt h)] },
+  { simp_rw [preimage_const_mul_Ioo _ _ h, real.volume_Ioo, ←ennreal.of_real_nnreal_smul,
+      nnreal.smul_def, coe_nnnorm, smul_eq_mul, norm_eq_abs, abs_of_pos h, mul_sub,
+      mul_div_cancel' _ (ne_of_gt h)] }
 end
 
 lemma map_volume_mul_left {a : ℝ} (h : a ≠ 0) :

From 2f781bf675e912c1ae482485c598ca99bcc45531 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 15 May 2023 22:44:18 +0000
Subject: [PATCH 4/4] fix

---
 src/measure_theory/measure/lebesgue.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/measure_theory/measure/lebesgue.lean b/src/measure_theory/measure/lebesgue.lean
index f2ef45c49817d..2dc7cbe2bc430 100644
--- a/src/measure_theory/measure/lebesgue.lean
+++ b/src/measure_theory/measure/lebesgue.lean
@@ -303,9 +303,9 @@ begin
     { simp only [det_diagonal, ne.def] at h,
       exact finset.prod_ne_zero_iff.1 h i (finset.mem_univ i) },
     rw [volume_preimage_mul_left A, nnnorm_inv, smul_inv_smul₀ (nnnorm_ne_zero_iff.mpr A)] },
-  rw [this, volume_pi_pi, finset.nnnorm_prod,
-    ennreal.of_real_prod_of_nonneg (λ i hi, abs_nonneg (D i)), ← finset.prod_mul_distrib],
-  simp only [B]
+  simp_rw [this, volume_pi_pi, nnnorm_prod, ennreal.smul_def, smul_eq_mul, ennreal.coe_finset_prod,
+    ← finset.prod_mul_distrib, ←smul_eq_mul, ←ennreal.smul_def],
+  simp only [B],
 end
 
 /-- A transvection preserves Lebesgue measure. -/