-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem map_linearMap_volume_pi_eq_smul_volume_pi {f : (ι → ℝ) →ₗ[ℝ] ι → ℝ}
    (hf : LinearMap.det f ≠ 0) : Measure.map f volume =
      ENNReal.ofReal (abs (LinearMap.det f)⁻¹) • volume

Proof state:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
⊢ Measure.map (⇑f) volume = ofReal |(LinearMap.det f)⁻¹| • volume

Tactic:
let M := LinearMap.toMatrix' f

Result:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
M : Matrix ι ι ℝ := LinearMap.toMatrix' f
⊢ Measure.map (⇑f) volume = ofReal |(LinearMap.det f)⁻¹| • volume

Proof state:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
⊢ Measure.map (⇑f) volume = ofReal |(LinearMap.det f)⁻¹| • volume

Tactic:
classical
  let M := LinearMap.toMatrix' f
  have A : LinearMap.det f = det M := by simp only [M, LinearMap.det_toMatrix']
  have B : f = toLin' M := by simp only [M, toLin'_toMatrix']
  rw [A, B]
  apply map_matrix_volume_pi_eq_smul_volume_pi
  rwa [A] at hf

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
M : Matrix ι ι ℝ := LinearMap.toMatrix' f
⊢ Measure.map (⇑f) volume = ofReal |(LinearMap.det f)⁻¹| • volume

Tactic:
have A : LinearMap.det f = det M := by simp only [M, LinearMap.det_toMatrix']

Result:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
M : Matrix ι ι ℝ := LinearMap.toMatrix' f
A : LinearMap.det f = M.det
⊢ Measure.map (⇑f) volume = ofReal |(LinearMap.det f)⁻¹| • volume

Proof state:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
M : Matrix ι ι ℝ := LinearMap.toMatrix' f
A : LinearMap.det f = M.det
B : f = toLin' M
⊢ Measure.map (⇑(toLin' M)) volume = ofReal |M.det⁻¹| • volume

Tactic:
apply map_matrix_volume_pi_eq_smul_volume_pi

Result:
case hM
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
M : Matrix ι ι ℝ := LinearMap.toMatrix' f
A : LinearMap.det f = M.det
B : f = toLin' M
⊢ M.det ≠ 0

Proof state:
case hM
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
M : Matrix ι ι ℝ := LinearMap.toMatrix' f
A : LinearMap.det f = M.det
B : f = toLin' M
⊢ M.det ≠ 0

Tactic:
rwa [A] at hf

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
M : Matrix ι ι ℝ := LinearMap.toMatrix' f
A : LinearMap.det f = M.det
⊢ f = toLin' M

Tactic:
simp only [M, toLin'_toMatrix']

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
M : Matrix ι ι ℝ := LinearMap.toMatrix' f
⊢ LinearMap.det f = M.det

Tactic:
simp only [M, LinearMap.det_toMatrix']

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
M : Matrix ι ι ℝ := LinearMap.toMatrix' f
A : LinearMap.det f = M.det
B : f = toLin' M
⊢ Measure.map (⇑f) volume = ofReal |(LinearMap.det f)⁻¹| • volume

Tactic:
rw [A, B]

Result:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
M : Matrix ι ι ℝ := LinearMap.toMatrix' f
A : LinearMap.det f = M.det
B : f = toLin' M
⊢ Measure.map (⇑(toLin' M)) volume = ofReal |M.det⁻¹| • volume

Proof state:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
M : Matrix ι ι ℝ := LinearMap.toMatrix' f
A : LinearMap.det f = M.det
⊢ Measure.map (⇑f) volume = ofReal |(LinearMap.det f)⁻¹| • volume

Tactic:
have B : f = toLin' M := by simp only [M, toLin'_toMatrix']

Result:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
M : Matrix ι ι ℝ := LinearMap.toMatrix' f
A : LinearMap.det f = M.det
B : f = toLin' M
⊢ Measure.map (⇑f) volume = ofReal |(LinearMap.det f)⁻¹| • volume