awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
D : ι → ℝ
hD : (Matrix.diagonal D).det ≠ 0
rw :
  ofReal |(Matrix.diagonal D).det⁻¹| •
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |(Matrix.diagonal D).det|)
      (Measure.map (α := ι → ℝ)
        (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
          (a : ι → ℝ) → ι → ℝ)
        volume)
| HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |(Matrix.diagonal D).det⁻¹|) volume

Tactic:
rw [← smul_map_diagonal_volume_pi hD]

Premises used: Real.smul_map_diagonal_volume_pi
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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 =
    ofReal |(Matrix.diagonal D).det⁻¹| •
      HSMul.hSMul (β := Measure (ι → ℝ)) (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 =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |(Matrix.diagonal D).det⁻¹|) volume

Tactic:
conv_rhs => rw [← smul_map_diagonal_volume_pi hD]

Premises used: Real.smul_map_diagonal_volume_pi
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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
htransvec₄ :
  Eq (α := Measure (ι → ℝ))
    (Measure.map (α := ι → ℝ)
        (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
        volume :
      Measure (ι → ℝ))
    (volume : Measure (ι → ℝ))
⊢ Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |t.toMatrix.det⁻¹|) volume

Tactic:
simp_rw [Matrix.TransvectionStruct.det, _root_.inv_one, abs_one, ENNReal.ofReal_one, one_smul,
      (volume_preserving_transvectionStruct _).map_eq]

Premises used: inv_one, Matrix.TransvectionStruct.det, MeasureTheory.MeasurePreserving.map_eq, ENNReal.ofReal_one, one_smul, abs_one, Real.volume_preserving_transvectionStruct
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
hmul :
  A.det ≠ 0 →
    B.det ≠ 0 →
      Measure.map (α := ι → ℝ)
            (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) A : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
            volume =
          HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |A.det⁻¹|) volume →
        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
⊢ A.det ≠ 0 →
    B.det ≠ 0 →
      Measure.map (α := ι → ℝ)
            (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) A : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
            volume =
          HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |A.det⁻¹|) volume →
        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

Tactic:
_
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
h : A.det ≠ 0
hmul :
  B.det ≠ 0 →
    Measure.map (α := ι → ℝ)
          (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) A : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
          volume =
        HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |A.det⁻¹|) volume →
      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
⊢ B.det ≠ 0 →
    Measure.map (α := ι → ℝ)
          (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) A : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
          volume =
        HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |A.det⁻¹|) volume →
      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

Tactic:
_
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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 : ι → ℝ) → ι → ℝ)
hmul₁ :
  Measurable (α := ι → ℝ) (β := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) B : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
⊢ Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (A * B) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |(A * B).det⁻¹|) volume

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]

Premises used: mul_inv, ENNReal.ofReal_mul, abs_mul, smul_smul, Matrix.toLin'_mul, Matrix.det_mul, LinearMap.coe_comp, mul_comm, MeasureTheory.Measure.map_smul, MeasureTheory.Measure.map_map, abs_nonneg
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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 :
  Continuous (X := ι → ℝ) (Y := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) A : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
⊢ Measurable (α := ι → ℝ) (β := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) A : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)

Tactic:
apply Continuous.measurable

Premises used: Continuous.measurable
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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
⊢ Continuous (X := ι → ℝ) (Y := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) A : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)

Tactic:
apply LinearMap.continuous_on_pi

Premises used: LinearMap.continuous_on_pi
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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 :
  Continuous (X := ι → ℝ) (Y := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) B : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
⊢ Measurable (α := ι → ℝ) (β := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) B : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)

Tactic:
apply Continuous.measurable

Premises used: Continuous.measurable
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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
⊢ Continuous (X := ι → ℝ) (Y := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) B : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)

Tactic:
apply LinearMap.continuous_on_pi

Premises used: LinearMap.continuous_on_pi
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f : ℝ) (0 : ℝ)
M : Matrix ι ι ℝ := (LinearMap.toMatrix' : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → Matrix ι ι ℝ) f
⊢ (LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f = M.det

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

Premises used: LinearMap.det_toMatrix'
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f : ℝ) (0 : ℝ)
M : Matrix ι ι ℝ := (LinearMap.toMatrix' : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → Matrix ι ι ℝ) f
⊢ (LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f = M.det

Tactic:
have A : LinearMap.det f = det M := by simp only [M, LinearMap.det_toMatrix']
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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
⊢ f = (toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M

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

Premises used: Matrix.toLin'_toMatrix'
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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
⊢ f = (toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M

Tactic:
have B : f = toLin' M := by simp only [M, toLin'_toMatrix']
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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
rw :
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |M.det⁻¹|) volume
⊢ Measure.map (α := ι → ℝ) (⇑f : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹|) volume

Tactic:
rw [A, B]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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
hM : M.det ≠ 0
⊢ Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |M.det⁻¹|) volume

Tactic:
apply map_matrix_volume_pi_eq_smul_volume_pi

Premises used: Real.map_matrix_volume_pi_eq_smul_volume_pi
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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
hM hM₁ hM₂ hM₃ :
  ∀ (hf : M.det ≠ 0) (A : (LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f = M.det)
    (B : f = (toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M), M.det ≠ 0
⊢ M.det ≠ 0

Tactic:
rwa [A] at hf
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f : ℝ) (0 : ℝ)
this this₁ this₂ :
  Measure.map (α := ι → ℝ) (⇑f : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹|) volume
this₃ :
  let 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
this₄ :
  let 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
this₅ :
  let 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
hM :
  let M : Matrix ι ι ℝ := (LinearMap.toMatrix' : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → Matrix ι ι ℝ) f;
  ∀ (A : (LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f = M.det)
    (B : f = (toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M), M.det ≠ 0
⊢ Measure.map (α := ι → ℝ) (⇑f : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹|) volume

Tactic:
classical
    -- this is deduced from the matrix case
    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

Premises used: Real.map_matrix_volume_pi_eq_smul_volume_pi
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
f g : α → ℝ
s : Set α
⊢ regionBetween f g s ⊆ SProd.sprod (β := Set ℝ) s univ

Tactic:
simpa only [prod_univ, regionBetween, Set.preimage, setOf_subset_setOf] using fun a => And.left

Premises used: regionBetween, Set.prod_univ, Set.preimage, And.left, Set.setOf_subset_setOf
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
dsimp :
  MeasurableSet.{u_1} (α := α × ℝ)
    ({a : α × ℝ | a.1 ∈ s} ∩
      {a : α × ℝ | Membership.mem (γ := Set ℝ) ({a_1 : ℝ | f a.1 < a_1} ∩ {a_1 : ℝ | a_1 < g a.1}) a.2})
⊢ MeasurableSet (regionBetween f g s)

Tactic:
dsimp only [regionBetween, Ioo, mem_setOf_eq, setOf_and]

Premises used: Set.setOf_and, regionBetween, Set.mem_setOf_eq, Set.Ioo
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet.{u_1} (α := α × ℝ)
    ({a : α × ℝ | a.1 ∈ s} ∩
      {a : α × ℝ | Membership.mem (γ := Set ℝ) ({a_1 : ℝ | f a.1 < a_1} ∩ {a_1 : ℝ | a_1 < g a.1}) a.2})

Tactic:
MeasurableSet.inter ?_
      ((measurableSet_lt (hf.comp measurable_fst) measurable_snd).inter
        (measurableSet_lt measurable_snd (hg.comp measurable_fst)))

Premises used: Measurable.comp, measurable_snd, measurableSet_lt, measurable_fst, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
measurable_snd : MeasurableSet.{u_1} (α := α × ℝ) {a : α × ℝ | a.1 ∈ s}
⊢ MeasurableSet.{u_1} (α := α × ℝ)
    ({a : α × ℝ | a.1 ∈ s} ∩
      {a : α × ℝ | Membership.mem (γ := Set ℝ) ({a_1 : ℝ | f a.1 < a_1} ∩ {a_1 : ℝ | a_1 < g a.1}) a.2})

Tactic:
refine
    MeasurableSet.inter ?_
      ((measurableSet_lt (hf.comp measurable_fst) measurable_snd).inter
        (measurableSet_lt measurable_snd (hg.comp measurable_fst)))

Premises used: Measurable.comp, measurable_snd, measurableSet_lt, measurable_fst, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet.{u_1} (α := α × ℝ) {a : α × ℝ | a.1 ∈ s}

Tactic:
measurable_fst hs

Premises used: Set.preimage, measurable_fst
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet.{u_1} (α := α × ℝ) {a : α × ℝ | a.1 ∈ s}

Tactic:
exact measurable_fst hs

Premises used: measurable_fst
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
dsimp :
  MeasurableSet.{u_1} (α := α × ℝ)
    ({a : α × ℝ | a.1 ∈ s} ∩
      {a : α × ℝ | Membership.mem (γ := Set ℝ) ({a_1 : ℝ | f a.1 < a_1} ∩ {a_1 : ℝ | a_1 ≤ g a.1}) a.2})
⊢ MeasurableSet.{u_1} (α := α × ℝ) {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Ioc (f p.1) (g p.1)}

Tactic:
dsimp only [regionBetween, Ioc, mem_setOf_eq, setOf_and]

Premises used: Set.Ioc, Set.setOf_and, regionBetween, Set.mem_setOf_eq
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet.{u_1} (α := α × ℝ)
    ({a : α × ℝ | a.1 ∈ s} ∩
      {a : α × ℝ | Membership.mem (γ := Set ℝ) ({a_1 : ℝ | f a.1 < a_1} ∩ {a_1 : ℝ | a_1 ≤ g a.1}) a.2})

Tactic:
MeasurableSet.inter ?_
      ((measurableSet_lt (hf.comp measurable_fst) measurable_snd).inter
        (measurableSet_le measurable_snd (hg.comp measurable_fst)))

Premises used: measurableSet_le, Measurable.comp, measurable_snd, measurableSet_lt, measurable_fst, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
measurable_snd : MeasurableSet.{u_1} (α := α × ℝ) {a : α × ℝ | a.1 ∈ s}
⊢ MeasurableSet.{u_1} (α := α × ℝ)
    ({a : α × ℝ | a.1 ∈ s} ∩
      {a : α × ℝ | Membership.mem (γ := Set ℝ) ({a_1 : ℝ | f a.1 < a_1} ∩ {a_1 : ℝ | a_1 ≤ g a.1}) a.2})

Tactic:
refine
    MeasurableSet.inter ?_
      ((measurableSet_lt (hf.comp measurable_fst) measurable_snd).inter
        (measurableSet_le measurable_snd (hg.comp measurable_fst)))

Premises used: measurableSet_le, Measurable.comp, measurable_snd, measurableSet_lt, measurable_fst, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
dsimp :
  MeasurableSet.{u_1} (α := α × ℝ)
    ({a : α × ℝ | a.1 ∈ s} ∩
      {a : α × ℝ | Membership.mem (γ := Set ℝ) ({a_1 : ℝ | f a.1 ≤ a_1} ∩ {a_1 : ℝ | a_1 < g a.1}) a.2})
⊢ MeasurableSet.{u_1} (α := α × ℝ) {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Ico (f p.1) (g p.1)}

Tactic:
dsimp only [regionBetween, Ico, mem_setOf_eq, setOf_and]

Premises used: Set.setOf_and, regionBetween, Set.mem_setOf_eq, Set.Ico