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 ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : (i : ι) → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this :
  Eq (α := Set (ι → ℝ))
    (preimage (β := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
        (a : ι → ℝ) → ι → ℝ)
      (Set.pi (α := fun (a : ι) ↦ ℝ) univ fun (i : ι) ↦ s i))
    (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ (fun (x : ℝ) ↦ D i * x) ⁻¹' s i)
i : ι
A : D i ≠ 0
rw :
  ofReal |D i| * HMul.hMul (β := ℝ≥0∞) (ofReal |(D i)⁻¹|) ((volume : (a : Set ℝ) → ℝ≥0∞) (s i) : ℝ≥0∞) =
    (volume : (a : Set ℝ) → ℝ≥0∞) (s i)
rw₁ :
  HMul.hMul (β := ℝ≥0∞) (ofReal |D i| * ofReal |(D i)⁻¹|) ((volume : (a : Set ℝ) → ℝ≥0∞) (s i) : ℝ≥0∞) =
    (volume : (a : Set ℝ) → ℝ≥0∞) (s i)
rw₂ :
  HMul.hMul (β := ℝ≥0∞) (ofReal (|D i| * |(D i)⁻¹|)) ((volume : (a : Set ℝ) → ℝ≥0∞) (s i) : ℝ≥0∞) =
    (volume : (a : Set ℝ) → ℝ≥0∞) (s i)
rw₃ :
  HMul.hMul (β := ℝ≥0∞) (ofReal |D i * (D i)⁻¹|) ((volume : (a : Set ℝ) → ℝ≥0∞) (s i) : ℝ≥0∞) =
    (volume : (a : Set ℝ) → ℝ≥0∞) (s i)
rw₄ :
  HMul.hMul (β := ℝ≥0∞) (ofReal |1|) ((volume : (a : Set ℝ) → ℝ≥0∞) (s i) : ℝ≥0∞) = (volume : (a : Set ℝ) → ℝ≥0∞) (s i)
rw₅ :
  HMul.hMul (β := ℝ≥0∞) (ofReal 1) ((volume : (a : Set ℝ) → ℝ≥0∞) (s i) : ℝ≥0∞) = (volume : (a : Set ℝ) → ℝ≥0∞) (s i)
rw₆ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (s i) : ℝ≥0∞) =
    (volume : (a : Set ℝ) → ℝ≥0∞) (s i)
⊢ HMul.hMul (β := ℝ≥0∞) (ofReal |D i|) ((volume : (a : Set ℝ) → ℝ≥0∞) ((fun (x : ℝ) ↦ D i * x) ⁻¹' s i) : ℝ≥0∞) =
    (volume : (a : Set ℝ) → ℝ≥0∞) (s i)
have rw₇ : Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (s i) : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : (i : ι) → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this :
  Eq (α := Set (ι → ℝ))
    (preimage (β := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
        (a : ι → ℝ) → ι → ℝ)
      (Set.pi (α := fun (a : ι) ↦ ℝ) univ fun (i : ι) ↦ s i))
    (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ (fun (x : ℝ) ↦ D i * x) ⁻¹' s i)
⊢ HMul.hMul (β := ℝ≥0∞) (ofReal |∏ i : ι, D i|)
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
          ((⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
              (a : ι → ℝ) → ι → ℝ) ⁻¹'
            Set.pi (α := fun (i : ι) ↦ ℝ) univ s) :
        ℝ≥0∞) =
    ∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) (s x)
have B : ∀ (i : ι),
  HMul.hMul (β := ℝ≥0∞) (ofReal |D i|) ((volume : (a : Set ℝ) → ℝ≥0∞) ((fun (x : ℝ) ↦ D i * x) ⁻¹' s i) : ℝ≥0∞) =
    (volume : (a : Set ℝ) → ℝ≥0∞) (s i)
Tactic: have B : ∀ i, ofReal (abs (D i)) * volume ((D i * ·) ⁻¹' s i) = volume (s i) := by
    intro i
    have A : D i ≠ 0 := by
      simp only [det_diagonal, Ne] at h
      exact Finset.prod_ne_zero_iff.1 h i (Finset.mem_univ 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : (i : ι) → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this :
  Eq (α := Set (ι → ℝ))
    (preimage (β := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
        (a : ι → ℝ) → ι → ℝ)
      (Set.pi (α := fun (a : ι) ↦ ℝ) univ fun (i : ι) ↦ s i))
    (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ (fun (x : ℝ) ↦ D i * x) ⁻¹' s i)
B :
  ∀ (i : ι),
    HMul.hMul (β := ℝ≥0∞) (ofReal |D i|) ((volume : (a : Set ℝ) → ℝ≥0∞) ((fun (x : ℝ) ↦ D i * x) ⁻¹' s i) : ℝ≥0∞) =
      (volume : (a : Set ℝ) → ℝ≥0∞) (s i)
⊢ HMul.hMul (β := ℝ≥0∞) (ofReal |∏ i : ι, D i|)
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
          ((⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
              (a : ι → ℝ) → ι → ℝ) ⁻¹'
            Set.pi (α := fun (i : ι) ↦ ℝ) univ s) :
        ℝ≥0∞) =
    ∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) (s x)
have rw : Eq (α := ℝ≥0∞)
  (∏ x : ι,
    HMul.hMul (β := ℝ≥0∞) (ofReal |D x|) ((volume : (a : Set ℝ) → ℝ≥0∞) ((fun (x_1 : ℝ) ↦ D x * x_1) ⁻¹' s x) : ℝ≥0∞))
  (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) (s x))
Tactic: rw [this, volume_pi_pi, Finset.abs_prod,
    ENNReal.ofReal_prod_of_nonneg fun i _ => abs_nonneg (D i), ← Finset.prod_mul_distrib]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
t : TransvectionStruct ι ℝ
⊢ MeasurePreserving (α := ι → ℝ) (β := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
    (volume : Measure (ι → ℝ)) (volume : Measure (ι → ℝ))
have ht : Measurable (α := ι → ℝ) (β := ι → ℝ)
  (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
Tactic: have ht : Measurable (toLin' t.toMatrix) :=
    (toLin' t.toMatrix).continuous_of_finiteDimensional.measurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
t : TransvectionStruct ι ℝ
ht :
  Measurable (α := ι → ℝ) (β := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
⊢ MeasurePreserving (α := ι → ℝ) (β := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
    (volume : Measure (ι → ℝ)) (volume : Measure (ι → ℝ))
have refine : Eq (α := Measure (ι → ℝ))
  (Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
      (volume : Measure (ι → ℝ)) :
    Measure (ι → ℝ))
  (volume : Measure (ι → ℝ))
Tactic: refine ⟨ht, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
t : TransvectionStruct ι ℝ
ht :
  Measurable (α := ι → ℝ) (β := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
⊢ Eq (α := Measure (ι → ℝ))
    (Measure.map (α := ι → ℝ)
        (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
        (volume : Measure (ι → ℝ)) :
      Measure (ι → ℝ))
    (volume : Measure (ι → ℝ))
have refine : ∀ (s : (i : ι) → Set ℝ) (hs : ∀ (i : ι), MeasurableSet (s i)),
  Eq (α := ℝ≥0∞)
    (((Measure.map (α := ι → ℝ)
              (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
                (a : ι → ℝ) → ι → ℝ)
              (volume : Measure (ι → ℝ)) :
            Measure (ι → ℝ)) :
          (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (volume : (a : Set ℝ) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: refine (pi_eq fun s hs ↦ ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
t : TransvectionStruct ι ℝ
ht :
  Measurable (α := ι → ℝ) (β := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
s : (i : ι) → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map (α := ι → ℝ)
              (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
                (a : ι → ℝ) → ι → ℝ)
              (volume : Measure (ι → ℝ)) :
            Measure (ι → ℝ)) :
          (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (volume : (a : Set ℝ) → ℝ≥0∞) (s i) : ℝ≥0∞)
have h2s : MeasurableSet (Set.pi (α := fun (i : ι) ↦ ℝ) univ s)
Tactic: have h2s : MeasurableSet (univ.pi s) := .pi countable_univ fun i _ ↦ hs i
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
t : TransvectionStruct ι ℝ
ht :
  Measurable (α := ι → ℝ) (β := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
s : (i : ι) → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (Set.pi (α := fun (i : ι) ↦ ℝ) univ s)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map (α := ι → ℝ)
              (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
                (a : ι → ℝ) → ι → ℝ)
              (volume : Measure (ι → ℝ)) :
            Measure (ι → ℝ)) :
          (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (volume : (a : Set ℝ) → ℝ≥0∞) (s i) : ℝ≥0∞)
have simp_rw : ∫⁻ (a : (i : ι) → ℝ),
    (Set.pi (α := fun (i : ι) ↦ ℝ) univ s).indicator 1
      a ∂Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
      (volume : Measure (ι → ℝ)) =
  ∫⁻ (a : (i : ι) → ℝ),
    (Set.pi (α := fun (i : ι) ↦ ℝ) univ s).indicator 1 a ∂Measure.pi (α := fun (i : ι) ↦ ℝ) fun (i : ι) ↦ volume
Tactic: simp_rw [← pi_pi, ← lintegral_indicator_one h2s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
t : TransvectionStruct ι ℝ
ht :
  Measurable (α := ι → ℝ) (β := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
s : (i : ι) → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (Set.pi (α := fun (i : ι) ↦ ℝ) univ s)
⊢ ∫⁻ (a : (i : ι) → ℝ),
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ s).indicator 1
        a ∂Measure.map (α := ι → ℝ)
        (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
        (volume : Measure (ι → ℝ)) =
    ∫⁻ (a : (i : ι) → ℝ),
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ s).indicator 1 a ∂Measure.pi (α := fun (i : ι) ↦ ℝ) fun (i : ι) ↦ volume
have rw : (∫⁻ (a : ι → ℝ),
    (Set.pi (α := fun (i : ι) ↦ ℝ) univ s).indicator 1
      ((((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
        a) ∂Measure.pi (α := fun (a : ι) ↦ ℝ) fun (x : ι) ↦ volume) =
  ∫⁻ (a : (i : ι) → ℝ),
    (Set.pi (α := fun (i : ι) ↦ ℝ) univ s).indicator 1 a ∂Measure.pi (α := fun (i : ι) ↦ ℝ) fun (i : ι) ↦ volume
Tactic: rw [lintegral_map (measurable_one.indicator h2s) ht, volume_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
t : TransvectionStruct ι ℝ
ht :
  Measurable (α := ι → ℝ) (β := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
s : (i : ι) → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (Set.pi (α := fun (i : ι) ↦ ℝ) univ s)
⊢ (∫⁻ (a : ι → ℝ),
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ s).indicator 1
        ((((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
          a) ∂Measure.pi (α := fun (a : ι) ↦ ℝ) fun (x : ι) ↦ volume) =
    ∫⁻ (a : (i : ι) → ℝ),
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ s).indicator 1 a ∂Measure.pi (α := fun (i : ι) ↦ ℝ) fun (i : ι) ↦ volume
have refine : (lmarginal (X := fun (a : ι) ↦ ℝ) (fun (x : ι) ↦ volume) {t.i} fun (a : ι → ℝ) ↦
    (Set.pi (α := fun (i : ι) ↦ ℝ) univ s).indicator 1
      ((((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
        a)) =
  lmarginal (X := fun (a : ι) ↦ ℝ) (fun (x : ι) ↦ volume) {t.i} ((Set.pi (α := fun (i : ι) ↦ ℝ) univ s).indicator 1)
Tactic: refine lintegral_eq_of_lmarginal_eq {t.i} ((measurable_one.indicator h2s).comp ht)
    (measurable_one.indicator h2s) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
t : TransvectionStruct ι ℝ
ht :
  Measurable (α := ι → ℝ) (β := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
s : (i : ι) → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (Set.pi (α := fun (i : ι) ↦ ℝ) univ s)
⊢ (lmarginal (X := fun (a : ι) ↦ ℝ) (fun (x : ι) ↦ volume) {t.i} fun (a : ι → ℝ) ↦
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ s).indicator 1
        ((((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
          a)) =
    lmarginal (X := fun (a : ι) ↦ ℝ) (fun (x : ι) ↦ volume) {t.i} ((Set.pi (α := fun (i : ι) ↦ ℝ) univ s).indicator 1)
have simp_rw : Eq.{max (u_1 + 1) 1} (α := (x : (i : ι) → ℝ) → ℝ≥0∞)
  (fun (x : (a : ι) → ℝ) ↦
    ∫⁻ (xᵢ : ℝ),
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ s).indicator 1
        ((((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
          (Function.update (β := fun (a : ι) ↦ ℝ) x t.i xᵢ)))
  fun (x : (a : ι) → ℝ) ↦
  ∫⁻ (xᵢ : ℝ), (Set.pi (α := fun (i : ι) ↦ ℝ) univ s).indicator 1 (Function.update (β := fun (a : ι) ↦ ℝ) x t.i xᵢ)
Tactic: simp_rw [lmarginal_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
t : TransvectionStruct ι ℝ
ht :
  Measurable (α := ι → ℝ) (β := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
s : (i : ι) → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (Set.pi (α := fun (i : ι) ↦ ℝ) univ s)
⊢ Eq.{max (u_1 + 1) 1} (α := (x : (i : ι) → ℝ) → ℝ≥0∞)
    (fun (x : (a : ι) → ℝ) ↦
      ∫⁻ (xᵢ : ℝ),
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ s).indicator 1
          ((((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
              (a : ι → ℝ) → ι → ℝ)
            (Function.update (β := fun (a : ι) ↦ ℝ) x t.i xᵢ)))
    fun (x : (a : ι) → ℝ) ↦
    ∫⁻ (xᵢ : ℝ), (Set.pi (α := fun (i : ι) ↦ ℝ) univ s).indicator 1 (Function.update (β := fun (a : ι) ↦ ℝ) x t.i xᵢ)
have h : ∀ (x : (a : ι) → ℝ),
  ∫⁻ (xᵢ : ℝ),
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ s).indicator 1
        ((((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
          (Function.update (β := fun (a : ι) ↦ ℝ) x t.i xᵢ)) =
    ∫⁻ (xᵢ : ℝ), (Set.pi (α := fun (i : ι) ↦ ℝ) univ s).indicator 1 (Function.update (β := fun (a : ι) ↦ ℝ) x t.i xᵢ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
t : TransvectionStruct ι ℝ
ht :
  Measurable (α := ι → ℝ) (β := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
s : (i : ι) → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (Set.pi (α := fun (i : ι) ↦ ℝ) univ s)
x : (a : ι) → ℝ
⊢ ∫⁻ (xᵢ : ℝ),
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ s).indicator 1
        ((((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
          (Function.update (β := fun (a : ι) ↦ ℝ) x t.i xᵢ)) =
    ∫⁻ (xᵢ : ℝ), (Set.pi (α := fun (i : ι) ↦ ℝ) univ s).indicator 1 (Function.update (β := fun (a : ι) ↦ ℝ) x t.i xᵢ)
have h : ∀ (t_i t_j : ι) (t_hij : t_i ≠ t_j) (t_c : ℝ)
  (ht :
    Measurable (α := ι → ℝ) (β := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) { i := t_i, j := t_j, hij := t_hij, c := t_c }.toMatrix :
            (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
        (a : ι → ℝ) → ι → ℝ)),
  ∫⁻ (xᵢ : ℝ),
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ s).indicator 1
        ((((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ)
                { i := t_i, j := t_j, hij := t_hij, c := t_c : TransvectionStruct ι ℝ }.toMatrix :
              (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
            (a : ι → ℝ) → ι → ℝ)
          (Function.update (β := fun (a : ι) ↦ ℝ) x
            { i := t_i, j := t_j, hij := t_hij, c := t_c : TransvectionStruct ι ℝ }.i xᵢ)) =
    ∫⁻ (xᵢ : ℝ),
      (Set.pi (α := fun (i : ι) ↦ ℝ) univ s).indicator 1
        (Function.update (β := fun (a : ι) ↦ ℝ) x
          { i := t_i, j := t_j, hij := t_hij, c := t_c : TransvectionStruct ι ℝ }.i xᵢ)
Tactic: cases t with | mk t_i t_j t_hij t_c =>
  simp [transvection, single_mulVec, t_hij.symm, ← Function.update_add,
    lintegral_add_right_eq_self fun xᵢ ↦ indicator (univ.pi s) 1 (Function.update x t_i xᵢ)]
Cleared hypotheses: t, ht
-- 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
⊢ Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |M.det⁻¹|) volume
have hdiag : ∀ (D : ι → ℝ),
  (Matrix.diagonal D).det ≠ 0 →
    Measure.map (α := ι → ℝ)
        (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
          (a : ι → ℝ) → ι → ℝ)
        volume =
      HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |(Matrix.diagonal D).det⁻¹|) volume
Tactic: apply diagonal_transvection_induction_of_det_ne_zero _ M hM
-- 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
hdiag :
  ∀ (D : ι → ℝ),
    (Matrix.diagonal D).det ≠ 0 →
      Measure.map (α := ι → ℝ)
          (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
            (a : ι → ℝ) → ι → ℝ)
          volume =
        HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |(Matrix.diagonal D).det⁻¹|) volume
⊢ Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |M.det⁻¹|) volume
have htransvec : ∀ (t : TransvectionStruct ι ℝ),
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |t.toMatrix.det⁻¹|) volume
Tactic: apply diagonal_transvection_induction_of_det_ne_zero _ M hM
-- 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
hdiag :
  ∀ (D : ι → ℝ),
    (Matrix.diagonal D).det ≠ 0 →
      Measure.map (α := ι → ℝ)
          (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
            (a : ι → ℝ) → ι → ℝ)
          volume =
        HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |(Matrix.diagonal D).det⁻¹|) volume
htransvec :
  ∀ (t : TransvectionStruct ι ℝ),
    Measure.map (α := ι → ℝ)
        (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
        volume =
      HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |t.toMatrix.det⁻¹|) volume
⊢ Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |M.det⁻¹|) volume
have hmul : ∀ (A B : Matrix ι ι ℝ),
  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: apply diagonal_transvection_induction_of_det_ne_zero _ M hM
-- 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
| HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |(Matrix.diagonal D).det⁻¹|) volume
have rw : ofReal |(Matrix.diagonal D).det⁻¹| •
  HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |(Matrix.diagonal D).det|)
    (Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
        (a : ι → ℝ) → ι → ℝ)
      volume)
Tactic: rw [← smul_map_diagonal_volume_pi hD]
-- 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
⊢ Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
        (a : ι → ℝ) → ι → ℝ)
      volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |(Matrix.diagonal D).det⁻¹|) volume
have 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)
Tactic: conv_rhs => rw [← smul_map_diagonal_volume_pi hD]
-- 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
⊢ 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⁻¹| * ofReal |(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]