awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ 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₁ : 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)
Tactic: rw [smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, inv_mul_cancel₀ hD, abs_one,
      ENNReal.ofReal_one, one_smul]
-- 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)
⊢ 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₂ : 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)
Tactic: rw [smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, inv_mul_cancel₀ hD, abs_one,
      ENNReal.ofReal_one, one_smul]
-- 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)
⊢ 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₃ : 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)
Tactic: rw [smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, inv_mul_cancel₀ hD, abs_one,
      ENNReal.ofReal_one, one_smul]
-- 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)
⊢ 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₄ : 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)
Tactic: rw [smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, inv_mul_cancel₀ hD, abs_one,
      ENNReal.ofReal_one, one_smul]
-- 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
t : TransvectionStruct ι ℝ
⊢ Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |t.toMatrix.det⁻¹|) volume
have htransvec : Measure.map (α := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
    volume =
  HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |1⁻¹|) volume
Tactic: simp_rw [Matrix.TransvectionStruct.det, _root_.inv_one, abs_one, ENNReal.ofReal_one, one_smul,
      (volume_preserving_transvectionStruct _).map_eq]
-- 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
t : TransvectionStruct ι ℝ
htransvec :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |1⁻¹|) volume
⊢ Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |t.toMatrix.det⁻¹|) volume
have htransvec₁ : Measure.map (α := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
    volume =
  HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |1|) volume
Tactic: simp_rw [Matrix.TransvectionStruct.det, _root_.inv_one, abs_one, ENNReal.ofReal_one, one_smul,
      (volume_preserving_transvectionStruct _).map_eq]
-- 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
t : TransvectionStruct ι ℝ
htransvec :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |1⁻¹|) volume
htransvec₁ :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |1|) volume
⊢ Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |t.toMatrix.det⁻¹|) volume
have htransvec₂ : Measure.map (α := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
    volume =
  HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal 1) volume
Tactic: simp_rw [Matrix.TransvectionStruct.det, _root_.inv_one, abs_one, ENNReal.ofReal_one, one_smul,
      (volume_preserving_transvectionStruct _).map_eq]
-- 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
t : TransvectionStruct ι ℝ
htransvec :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |1⁻¹|) volume
htransvec₁ :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |1|) volume
htransvec₂ :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal 1) volume
⊢ Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |t.toMatrix.det⁻¹|) volume
have htransvec₃ : Measure.map (α := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
    volume =
  HSMul.hSMul (α := ℝ≥0∞) (β := Measure (ι → ℝ)) 1 volume
Tactic: simp_rw [Matrix.TransvectionStruct.det, _root_.inv_one, abs_one, ENNReal.ofReal_one, one_smul,
      (volume_preserving_transvectionStruct _).map_eq]
-- 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
t : TransvectionStruct ι ℝ
htransvec :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |1⁻¹|) volume
htransvec₁ :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |1|) volume
htransvec₂ :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal 1) volume
htransvec₃ :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure (ι → ℝ)) 1 volume
⊢ Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |t.toMatrix.det⁻¹|) volume
have htransvec₄ : Eq (α := Measure (ι → ℝ))
  (Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
      volume :
    Measure (ι → ℝ))
  (volume : Measure (ι → ℝ))
Tactic: simp_rw [Matrix.TransvectionStruct.det, _root_.inv_one, abs_one, ENNReal.ofReal_one, one_smul,
      (volume_preserving_transvectionStruct _).map_eq]
-- 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
A B : Matrix ι ι ℝ
h : A.det ≠ 0
h_1 : B.det ≠ 0
IHA :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) A : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |A.det⁻¹|) volume
IHB :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) B : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |B.det⁻¹|) volume
⊢ Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (A * B) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |(A * B).det⁻¹|) volume
have hmul : Measurable (α := ι → ℝ) (β := ι → ℝ)
  (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) A : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
Tactic: rw [toLin'_mul, det_mul, LinearMap.coe_comp, ← Measure.map_map, IHB, Measure.map_smul, IHA,
      smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, mul_comm, mul_inv]
-- 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
A B : Matrix ι ι ℝ
h : A.det ≠ 0
h_1 : B.det ≠ 0
IHA :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) A : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |A.det⁻¹|) volume
IHB :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) B : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |B.det⁻¹|) volume
hmul :
  Measurable (α := ι → ℝ) (β := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) A : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
⊢ Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (A * B) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |(A * B).det⁻¹|) volume
have hmul₁ : Measurable (α := ι → ℝ) (β := ι → ℝ)
  (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) B : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
Tactic: rw [toLin'_mul, det_mul, LinearMap.coe_comp, ← Measure.map_map, IHB, Measure.map_smul, IHA,
      smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, mul_comm, mul_inv]
-- 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
A B : Matrix ι ι ℝ
h : A.det ≠ 0
h_1 : B.det ≠ 0
IHA :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) A : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |A.det⁻¹|) volume
IHB :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) B : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |B.det⁻¹|) volume
⊢ Measurable (α := ι → ℝ) (β := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) A : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
have hmul : Continuous (X := ι → ℝ) (Y := ι → ℝ)
  (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) A : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
Tactic: apply Continuous.measurable
-- 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
A B : Matrix ι ι ℝ
h : A.det ≠ 0
h_1 : B.det ≠ 0
IHA :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) A : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |A.det⁻¹|) volume
IHB :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) B : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |B.det⁻¹|) volume
⊢ Measurable (α := ι → ℝ) (β := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) B : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
have hmul : Continuous (X := ι → ℝ) (Y := ι → ℝ)
  (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) B : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
Tactic: apply Continuous.measurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f : ℝ) (0 : ℝ)
M : Matrix ι ι ℝ := (LinearMap.toMatrix' : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → Matrix ι ι ℝ) f
⊢ Measure.map (α := ι → ℝ) (⇑f : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹|) volume
have A : (LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f = M.det
Tactic: have A : LinearMap.det f = det M := by simp only [M, LinearMap.det_toMatrix']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f : ℝ) (0 : ℝ)
M : Matrix ι ι ℝ := (LinearMap.toMatrix' : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → Matrix ι ι ℝ) f
A : (LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f = M.det
⊢ Measure.map (α := ι → ℝ) (⇑f : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹|) volume
have B : f = (toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M
Tactic: have B : f = toLin' M := by simp only [M, toLin'_toMatrix']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f : ℝ) (0 : ℝ)
M : Matrix ι ι ℝ := (LinearMap.toMatrix' : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → Matrix ι ι ℝ) f
A : (LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f = M.det
B : f = (toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M
⊢ Measure.map (α := ι → ℝ) (⇑f : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹|) volume
have rw : Measure.map (α := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ) volume =
  HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |M.det⁻¹|) volume
Tactic: rw [A, B]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f : ℝ) (0 : ℝ)
M : Matrix ι ι ℝ := (LinearMap.toMatrix' : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → Matrix ι ι ℝ) f
A : (LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f = M.det
B : f = (toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M
⊢ Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |M.det⁻¹|) volume
have hM : M.det ≠ 0
Tactic: apply map_matrix_volume_pi_eq_smul_volume_pi
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f : ℝ) (0 : ℝ)
M : Matrix ι ι ℝ := (LinearMap.toMatrix' : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → Matrix ι ι ℝ) f
A : (LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f = M.det
B : f = (toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M
⊢ M.det ≠ 0
have hM : ∀ (hf : M.det ≠ 0) (A : (LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f = M.det)
  (B : f = (toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M), M.det ≠ 0
Tactic: rwa [A] at hf
Cleared hypotheses: hf, A, B