-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
D : ι → ℝ
hD : (Matrix.diagonal D).det ≠ 0
hdiag :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
        (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |(Matrix.diagonal D).det⁻¹| * ofReal |(Matrix.diagonal D).det|)
      (Measure.map (α := ι → ℝ)
        (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
          (a : ι → ℝ) → ι → ℝ)
        volume)
hdiag₁ :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
        (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal (|(Matrix.diagonal D).det⁻¹| * |(Matrix.diagonal D).det|))
      (Measure.map (α := ι → ℝ)
        (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
          (a : ι → ℝ) → ι → ℝ)
        volume)
hdiag₂ :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
        (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |(Matrix.diagonal D).det⁻¹ * (Matrix.diagonal D).det|)
      (Measure.map (α := ι → ℝ)
        (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
          (a : ι → ℝ) → ι → ℝ)
        volume)
hdiag₃ :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
        (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |1|)
      (Measure.map (α := ι → ℝ)
        (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
          (a : ι → ℝ) → ι → ℝ)
        volume)
hdiag₄ :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
        (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal 1)
      (Measure.map (α := ι → ℝ)
        (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
          (a : ι → ℝ) → ι → ℝ)
        volume)
hdiag₅ :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
        (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure (ι → ℝ)) 1
      (Measure.map (α := ι → ℝ)
        (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
          (a : ι → ℝ) → ι → ℝ)
        volume)
⊢ Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
        (a : ι → ℝ) → ι → ℝ)
      volume =
    ofReal |(Matrix.diagonal D).det⁻¹| •
      HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |(Matrix.diagonal D).det|)
        (Measure.map (α := ι → ℝ)
          (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
            (a : ι → ℝ) → ι → ℝ)
          volume)
have hdiag₆ : Eq (α := Measure (ι → ℝ))
  (Measure.map (α := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
      (a : ι → ℝ) → ι → ℝ)
    volume)
  (Measure.map (α := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
      (a : ι → ℝ) → ι → ℝ)
    volume)
Tactic: rw [smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, inv_mul_cancel₀ hD, abs_one,
      ENNReal.ofReal_one, one_smul]