ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ↑↑(ofReal (abs (det (Matrix.diagonal D))) • Measure.map (↑(↑toLin' (Matrix.diagonal D))) volume) (Set.pi univ s) =
    ∏ i : ι, ↑↑volume (s i)
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
⊢ ofReal (abs (det (Matrix.diagonal D))) • Measure.map (↑(↑toLin' (Matrix.diagonal D))) volume = volume
refine' (Measure.pi_eq fun s hs => _).symm
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ofReal (abs (∏ i : ι, D i)) * ↑↑(Measure.map (↑(↑toLin' (Matrix.diagonal D))) volume) (Set.pi univ s) =
    ∏ x : ι, ↑↑volume (s x)
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ↑↑(ofReal (abs (det (Matrix.diagonal D))) • Measure.map (↑(↑toLin' (Matrix.diagonal D))) volume) (Set.pi univ s) =
    ∏ i : ι, ↑↑volume (s i)
simp only [det_diagonal, Measure.coe_smul, Algebra.id.smul_eq_mul, Pi.smul_apply]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ofReal (abs (∏ i : ι, D i)) * ↑↑volume (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) =
    ∏ x : ι, ↑↑volume (s x)

ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Measurable ↑(↑toLin' (Matrix.diagonal D))
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ofReal (abs (∏ i : ι, D i)) * ↑↑(Measure.map (↑(↑toLin' (Matrix.diagonal D))) volume) (Set.pi univ s) =
    ∏ x : ι, ↑↑volume (s x)
rw [Measure.map_apply _ (MeasurableSet.univ_pi hs)]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Measurable ↑(↑toLin' (Matrix.diagonal D))

ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ofReal (abs (∏ i : ι, D i)) * ↑↑volume (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) =
    ∏ x : ι, ↑↑volume (s x)
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ofReal (abs (∏ i : ι, D i)) * ↑↑volume (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) =
    ∏ x : ι, ↑↑volume (s x)

ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Measurable ↑(↑toLin' (Matrix.diagonal D))
swap
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) = Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
B : ∀ (i : ι), ofReal (abs (D i)) * ↑↑volume ((fun x => D i * x) ⁻¹' s i) = ↑↑volume (s i)
⊢ ∏ x : ι, ofReal (abs (D x)) * ↑↑volume ((fun x_1 => D x * x_1) ⁻¹' s x) = ∏ x : ι, ↑↑volume (s x)
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) = Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
B : ∀ (i : ι), ofReal (abs (D i)) * ↑↑volume ((fun x => D i * x) ⁻¹' s i) = ↑↑volume (s i)
⊢ ofReal (abs (∏ i : ι, D i)) * ↑↑volume (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) =
    ∏ x : ι, ↑↑volume (s x)
rw [this, volume_pi_pi, Finset.abs_prod,
  ENNReal.ofReal_prod_of_nonneg fun i _ => abs_nonneg (D i), ← Finset.prod_mul_distrib]
no goals
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) = Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
B : ∀ (i : ι), ofReal (abs (D i)) * ↑↑volume ((fun x => D i * x) ⁻¹' s i) = ↑↑volume (s i)
⊢ ∏ x : ι, ofReal (abs (D x)) * ↑↑volume ((fun x_1 => D x * x_1) ⁻¹' s x) = ∏ x : ι, ↑↑volume (s x)
simp only [B]
no goals
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Measurable ↑(↑toLin' (Matrix.diagonal D))
exact Continuous.measurable (LinearMap.continuous_on_pi _)
case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
f : ι → ℝ
⊢ (f ∈ ↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) ↔
    f ∈ Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) = Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
ext f
no goals
case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
f : ι → ℝ
⊢ (f ∈ ↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) ↔
    f ∈ Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
simp only [LinearMap.coe_proj, Algebra.id.smul_eq_mul, LinearMap.smul_apply, mem_univ_pi,
  mem_preimage, LinearMap.pi_apply, diagonal_toLin']
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) = Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
i : ι
⊢ ofReal (abs (D i)) * ↑↑volume ((fun x => D i * x) ⁻¹' s i) = ↑↑volume (s i)
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) = Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
⊢ ∀ (i : ι), ofReal (abs (D i)) * ↑↑volume ((fun x => D i * x) ⁻¹' s i) = ↑↑volume (s i)
intro i
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) = Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
i : ι
A : D i ≠ 0
⊢ ofReal (abs (D i)) * ↑↑volume ((fun x => D i * x) ⁻¹' s i) = ↑↑volume (s i)
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) = Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
i : ι
⊢ ofReal (abs (D i)) * ↑↑volume ((fun x => D i * x) ⁻¹' s i) = ↑↑volume (s i)
have A : D i ≠ 0 := by
  simp only [det_diagonal, Ne.def] at h
  exact Finset.prod_ne_zero_iff.1 h i (Finset.mem_univ i)
no goals
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) = Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
i : ι
A : D i ≠ 0
⊢ ofReal (abs (D i)) * ↑↑volume ((fun x => D i * x) ⁻¹' s i) = ↑↑volume (s i)
rw [volume_preimage_mul_left A, ← mul_assoc, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul,
  mul_inv_cancel A, abs_one, ENNReal.ofReal_one, one_mul]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) = Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
i : ι
h : ¬∏ i : ι, D i = 0
⊢ D i ≠ 0
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : det (Matrix.diagonal D) ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) = Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
i : ι
⊢ D i ≠ 0
simp only [det_diagonal, Ne.def] at h
no goals
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (↑(↑toLin' (Matrix.diagonal D)) ⁻¹' Set.pi univ fun i => s i) = Set.pi univ fun i => (fun x => D i * x) ⁻¹' s i
i : ι
h : ¬∏ i : ι, D i = 0
⊢ D i ≠ 0
exact Finset.prod_ne_zero_iff.1 h i (Finset.mem_univ i)