awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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)
rw₇ rw₈ : Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (s i) : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ 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:
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]

Premises used: mul_inv_cancel₀, Real.volume_preimage_mul_left, ENNReal.ofReal_mul, mul_assoc, abs_mul, ENNReal.ofReal_one, abs_one, abs_nonneg, one_mul
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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 : ι),
    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]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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)
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))
⊢ 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)

Tactic:
rw [this, volume_pi_pi, Finset.abs_prod,
    ENNReal.ofReal_prod_of_nonneg fun i _ => abs_nonneg (D i), ← Finset.prod_mul_distrib]

Premises used: Finset.prod_mul_distrib, MeasureTheory.volume_pi_pi, ENNReal.ofReal_prod_of_nonneg, abs_nonneg, Finset.abs_prod
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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)
⊢ 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:
simp only [B]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
t : TransvectionStruct ι ℝ
⊢ Measurable (α := ι → ℝ) (β := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)

Tactic:
have ht : Measurable (toLin' t.toMatrix) :=
    (toLin' t.toMatrix).continuous_of_finiteDimensional.measurable
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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 (ι → ℝ))

Tactic:
⟨ht, ?_⟩

Premises used: MeasureTheory.MeasurePreserving.mk
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
t : TransvectionStruct ι ℝ
ht :
  Measurable (α := ι → ℝ) (β := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
refine :
  Eq (α := Measure (ι → ℝ))
    (Measure.map (α := ι → ℝ)
        (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
        (volume : Measure (ι → ℝ)) :
      Measure (ι → ℝ))
    (volume : Measure (ι → ℝ))
⊢ MeasurePreserving (α := ι → ℝ) (β := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
    (volume : Measure (ι → ℝ)) (volume : Measure (ι → ℝ))

Tactic:
refine ⟨ht, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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 (ι → ℝ))

Tactic:
(pi_eq fun s hs ↦ ?_).symm

Premises used: MeasureTheory.Measure.pi_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
t : TransvectionStruct ι ℝ
ht :
  Measurable (α := ι → ℝ) (β := ι → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
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∞)
⊢ Eq (α := Measure (ι → ℝ))
    (Measure.map (α := ι → ℝ)
        (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) t.toMatrix : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
        (volume : Measure (ι → ℝ)) :
      Measure (ι → ℝ))
    (volume : Measure (ι → ℝ))

Tactic:
refine (pi_eq fun s hs ↦ ?_).symm

Premises used: MeasureTheory.Measure.pi_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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)
⊢ MeasurableSet (Set.pi (α := fun (i : ι) ↦ ℝ) univ s)

Tactic:
have h2s : MeasurableSet (univ.pi s) := .pi countable_univ fun i _ ↦ hs i
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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)
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
⊢ 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:
simp_rw [← pi_pi, ← lintegral_indicator_one h2s]

Premises used: MeasureTheory.lintegral_indicator_one, MeasureTheory.Measure.pi_pi
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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)
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
⊢ ∫⁻ (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:
rw [lintegral_map (measurable_one.indicator h2s) ht, volume_pi]

Premises used: MeasureTheory.volume_pi, Measurable.indicator, measurable_one, MeasureTheory.lintegral_map
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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

Tactic:
lintegral_eq_of_lmarginal_eq {t.i} ((measurable_one.indicator h2s).comp ht)
    (measurable_one.indicator h2s) ?_

Premises used: Measurable.comp, Matrix.TransvectionStruct.i, Measurable.indicator, measurable_one, Singleton.singleton, MeasureTheory.lintegral_eq_of_lmarginal_eq
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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)
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)
⊢ (∫⁻ (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:
refine lintegral_eq_of_lmarginal_eq {t.i} ((measurable_one.indicator h2s).comp ht)
    (measurable_one.indicator h2s) ?_

Premises used: Measurable.comp, Matrix.TransvectionStruct.i, Measurable.indicator, measurable_one, Singleton.singleton, MeasureTheory.lintegral_eq_of_lmarginal_eq
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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)
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ᵢ)
⊢ (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:
simp_rw [lmarginal_singleton]

Premises used: MeasureTheory.lmarginal_singleton
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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)
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ᵢ)
⊢ 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:
ext x
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
s : (i : ι) → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (Set.pi (α := fun (i : ι) ↦ ℝ) univ s)
x : (a : ι) → ℝ
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:
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ᵢ)]

Premises used: Function.update, Set.indicator, Set.univ, Ne.symm, Matrix.transvection, Set.pi, Matrix.single_mulVec, OfNat.ofNat, Function.update_add, MeasureTheory.lintegral_add_right_eq_self
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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 : ι) → ℝ
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ᵢ)
⊢ ∫⁻ (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:
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ᵢ)]

Premises used: Matrix.transvection, Matrix.single_mulVec, Function.update_add, Real.mk
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
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
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
⊢ Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |M.det⁻¹|) volume

Tactic:
apply diagonal_transvection_induction_of_det_ne_zero _ M hM

Premises used: Matrix.diagonal_transvection_induction_of_det_ne_zero