awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
a b : ι → ℝ
⊢ Eq (α := ℝ≥0∞)
    (((volume : Measure ((i : ι) → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ico (a i) (b i)) :
      ℝ≥0∞)
    (∏ i : ι, ofReal (b i - a i) : ℝ≥0∞)

Tactic:
(measure_congr Measure.univ_pi_Ico_ae_eq_Icc).trans volume_Icc_pi

Premises used: MeasureTheory.measure_congr, Real.volume_Icc_pi, MeasureTheory.Measure.univ_pi_Ico_ae_eq_Icc, Eq.trans
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
a b : ι → ℝ
h : a ≤ b
⊢ ENNReal.toReal
      (((volume : Measure ((i : ι) → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ico (a i) (b i))) =
    ∏ i : ι, (b i - a i)

Tactic:
simp only [volume_pi_Ico, ENNReal.toReal_prod, ENNReal.toReal_ofReal (sub_nonneg.2 (h _))]

Premises used: Iff.mpr, Real.volume_pi_Ico, ENNReal.toReal_ofReal, ENNReal.toReal_prod, sub_nonneg
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
a : ι → ℝ
r : ℝ
hr : 0 < r
simp : ofReal (2 * r) ^ Finset.card.{u_1} (α := ι) Finset.univ = ofReal ((2 * r) ^ Fintype.card ι)
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (ball a r) = ofReal ((2 * r) ^ Fintype.card ι)

Tactic:
simp only [MeasureTheory.volume_pi_ball a hr, volume_ball, Finset.prod_const]

Premises used: Real.volume_ball, Finset.prod_const, MeasureTheory.volume_pi_ball
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
a : ι → ℝ
r : ℝ
hr : 0 < r
⊢ ofReal (2 * r) ^ Finset.card.{u_1} (α := ι) Finset.univ = ofReal ((2 * r) ^ Fintype.card ι)

Tactic:
(ENNReal.ofReal_pow (mul_nonneg zero_le_two hr.le) _).symm

Premises used: mul_nonneg, Fintype.card, LT.lt.le, zero_le_two, Eq.symm, ENNReal.ofReal_pow
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
a : ι → ℝ
r : ℝ
hr : 0 < r
⊢ ofReal (2 * r) ^ Finset.card.{u_1} (α := ι) Finset.univ = ofReal ((2 * r) ^ Fintype.card ι)

Tactic:
exact (ENNReal.ofReal_pow (mul_nonneg zero_le_two hr.le) _).symm

Premises used: mul_nonneg, LT.lt.le, zero_le_two, Eq.symm, ENNReal.ofReal_pow
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
a : ι → ℝ
r : ℝ
hr : 0 ≤ r
simp : ofReal (2 * r) ^ Finset.card.{u_1} (α := ι) Finset.univ = ofReal ((2 * r) ^ Fintype.card ι)
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (closedBall a r) = ofReal ((2 * r) ^ Fintype.card ι)

Tactic:
simp only [MeasureTheory.volume_pi_closedBall a hr, volume_closedBall, Finset.prod_const]

Premises used: Real.volume_closedBall, Finset.prod_const, MeasureTheory.volume_pi_closedBall
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
a : ι → ℝ
r : ℝ
hr : 0 ≤ r
⊢ ofReal (2 * r) ^ Finset.card.{u_1} (α := ι) Finset.univ = ofReal ((2 * r) ^ Fintype.card ι)

Tactic:
(ENNReal.ofReal_pow (mul_nonneg zero_le_two hr) _).symm

Premises used: mul_nonneg, Fintype.card, zero_le_two, Eq.symm, ENNReal.ofReal_pow
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
a : ι → ℝ
r : ℝ
hr : 0 ≤ r
⊢ ofReal (2 * r) ^ Finset.card.{u_1} (α := ι) Finset.univ = ofReal ((2 * r) ^ Fintype.card ι)

Tactic:
exact (ENNReal.ofReal_pow (mul_nonneg zero_le_two hr) _).symm

Premises used: mul_nonneg, zero_le_two, Eq.symm, ENNReal.ofReal_pow
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
⊢ LE.le (α := ℝ≥0∞) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∏ i : ι, ediam (Function.eval (β := fun (x : ι) ↦ ℝ) i '' s) : ℝ≥0∞)

Tactic:
calc
    volume s ≤ volume (pi univ fun i => closure (Function.eval i '' s)) :=
      volume.mono <|
        Subset.trans (subset_pi_eval_image univ s) <| pi_mono fun _ _ => subset_closure
    _ = ∏ i, volume (closure <| Function.eval i '' s) := volume_pi_pi _
    _ ≤ ∏ i : ι, ediam (Function.eval i '' s) :=
      Finset.prod_le_prod' fun _ _ => (volume_le_diam _).trans_eq (ediam_closure _)

Premises used: Trans.trans, LE.le.trans_eq, Finset.prod_le_prod', MeasureTheory.volume_pi_pi, Set.Subset.trans, subset_closure, Set.univ, Metric.ediam_closure, MeasureTheory.OuterMeasure.mono, Function.eval, MeasureTheory.Measure.toOuterMeasure, Real.volume_le_diam, closure, MeasureTheory.MeasureSpace.volume, Set.image, Set.pi_mono, Set.subset_pi_eval_image
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
⊢ ∏ _i : ι, (↑1 : ℝ≥0∞) * ediam s = ediam s ^ Fintype.card ι

Tactic:
simp only [ENNReal.coe_one, one_mul, Finset.prod_const, Fintype.card]

Premises used: Fintype.card, ENNReal.coe_one, Finset.prod_const, one_mul
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
h : a ≠ 0
⊢ HSMul.hSMul (β := Measure ℝ) (ofReal |a|) (Measure.map (fun (x : ℝ) ↦ a * x) volume) = volume

Tactic:
(Real.measure_ext_Ioo_rat fun p q => ?_).symm

Premises used: Real.measure_ext_Ioo_rat, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
h : a ≠ 0
refine :
  ∀ (p q : ℚ),
    Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ioo (↑p : ℝ) (↑q : ℝ)) : ℝ≥0∞)
      ((HSMul.hSMul (β := Measure ℝ) (ofReal |a|) (Measure.map (fun (x : ℝ) ↦ a * x) volume) : (a : Set ℝ) → ℝ≥0∞)
          (Ioo (↑p : ℝ) (↑q : ℝ)) :
        ℝ≥0∞)
⊢ HSMul.hSMul (β := Measure ℝ) (ofReal |a|) (Measure.map (fun (x : ℝ) ↦ a * x) volume) = volume

Tactic:
refine (Real.measure_ext_Ioo_rat fun p q => ?_).symm

Premises used: Real.measure_ext_Ioo_rat, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
h : a ≠ 0
p q : ℚ
inl :
  ∀ (h : a < 0),
    Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ioo (↑p : ℝ) (↑q : ℝ)) : ℝ≥0∞)
      ((HSMul.hSMul (β := Measure ℝ) (ofReal |a|) (Measure.map (fun (x : ℝ) ↦ a * x) volume) : (a : Set ℝ) → ℝ≥0∞)
          (Ioo (↑p : ℝ) (↑q : ℝ)) :
        ℝ≥0∞)
inr :
  ∀ (h : 0 < a),
    Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ioo (↑p : ℝ) (↑q : ℝ)) : ℝ≥0∞)
      ((HSMul.hSMul (β := Measure ℝ) (ofReal |a|) (Measure.map (fun (x : ℝ) ↦ a * x) volume) : (a : Set ℝ) → ℝ≥0∞)
          (Ioo (↑p : ℝ) (↑q : ℝ)) :
        ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ioo (↑p : ℝ) (↑q : ℝ)) : ℝ≥0∞)
    ((HSMul.hSMul (β := Measure ℝ) (ofReal |a|) (Measure.map (fun (x : ℝ) ↦ a * x) volume) : (a : Set ℝ) → ℝ≥0∞)
        (Ioo (↑p : ℝ) (↑q : ℝ)) :
      ℝ≥0∞)

Tactic:
rcases lt_or_gt_of_ne h with h | h

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
h_1 : a ≠ 0
p q : ℚ
h : a < 0
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ioo (↑p : ℝ) (↑q : ℝ)) : ℝ≥0∞)
    ((HSMul.hSMul (β := Measure ℝ) (ofReal |a|) (Measure.map (fun (x : ℝ) ↦ a * x) volume) : (a : Set ℝ) → ℝ≥0∞)
        (Ioo (↑p : ℝ) (↑q : ℝ)) :
      ℝ≥0∞)

Tactic:
simp only [Real.volume_Ioo, Measure.smul_apply, ← ENNReal.ofReal_mul (le_of_lt <| neg_pos.2 h),
      Measure.map_apply (measurable_const_mul a) measurableSet_Ioo, neg_sub_neg, neg_mul,
      preimage_const_mul_Ioo_of_neg _ _ h, abs_of_neg h, mul_sub, smul_eq_mul,
      mul_div_cancel₀ _ (ne_of_lt h)]

Premises used: Iff.mpr, mul_sub, neg_pos, abs_of_neg, MeasureTheory.Measure.map_apply, ENNReal.ofReal_mul, le_of_lt, MeasurableMul.measurable_const_mul, mul_div_cancel₀, measurableSet_Ioo, MeasureTheory.Measure.smul_apply, Set.preimage_const_mul_Ioo_of_neg, neg_sub_neg, neg_mul, smul_eq_mul, Real.volume_Ioo, ne_of_lt
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
h_1 : a ≠ 0
p q : ℚ
h : 0 < a
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ioo (↑p : ℝ) (↑q : ℝ)) : ℝ≥0∞)
    ((HSMul.hSMul (β := Measure ℝ) (ofReal |a|) (Measure.map (fun (x : ℝ) ↦ a * x) volume) : (a : Set ℝ) → ℝ≥0∞)
        (Ioo (↑p : ℝ) (↑q : ℝ)) :
      ℝ≥0∞)

Tactic:
simp only [Real.volume_Ioo, Measure.smul_apply, ← ENNReal.ofReal_mul (le_of_lt h),
      Measure.map_apply (measurable_const_mul a) measurableSet_Ioo, preimage_const_mul_Ioo₀ _ _ h,
      abs_of_pos h, mul_sub, mul_div_cancel₀ _ (ne_of_gt h), smul_eq_mul]

Premises used: Set.preimage_const_mul_Ioo₀, mul_sub, MeasureTheory.Measure.map_apply, ENNReal.ofReal_mul, le_of_lt, MeasurableMul.measurable_const_mul, ne_of_gt, mul_div_cancel₀, measurableSet_Ioo, MeasureTheory.Measure.smul_apply, abs_of_pos, smul_eq_mul, Real.volume_Ioo
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
h : a ≠ 0
rw : Measure.map (fun (x : ℝ) ↦ a * x) volume
| HSMul.hSMul (β := Measure ℝ) (ofReal |a⁻¹|) volume

Tactic:
rw [← Real.smul_map_volume_mul_left h, smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ←
      abs_mul, inv_mul_cancel₀ h, abs_one, ENNReal.ofReal_one, one_smul]

Premises used: ENNReal.ofReal_mul, Real.smul_map_volume_mul_left, abs_mul, smul_smul, ENNReal.ofReal_one, one_smul, abs_one, abs_nonneg, inv_mul_cancel₀
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
h : a ≠ 0
conv_rhs : Measure.map (fun (x : ℝ) ↦ a * x) volume = HSMul.hSMul (β := Measure ℝ) (ofReal |a⁻¹|) volume
conv_rhs₁ : Eq (α := Measure ℝ) (Measure.map (fun (x : ℝ) ↦ a * x) volume) (Measure.map (fun (x : ℝ) ↦ a * x) volume)
⊢ Measure.map (fun (x : ℝ) ↦ a * x) volume = HSMul.hSMul (β := Measure ℝ) (ofReal |a⁻¹|) volume

Tactic:
conv_rhs =>
    rw [← Real.smul_map_volume_mul_left h, smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ←
      abs_mul, inv_mul_cancel₀ h, abs_one, ENNReal.ofReal_one, one_smul]

Premises used: ENNReal.ofReal_mul, Real.smul_map_volume_mul_left, abs_mul, smul_smul, ENNReal.ofReal_one, one_smul, abs_one, abs_nonneg, inv_mul_cancel₀
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
h : a ≠ 0
s : Set ℝ
rw :
  (HSMul.hSMul (β := Measure ℝ) (ofReal |a⁻¹|) volume : (a : Set ℝ) → ℝ≥0∞) s =
    HMul.hMul (β := ℝ≥0∞) (ofReal |a⁻¹|) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (Measure.map (fun (x : ℝ) ↦ a * x) volume : (a : Set ℝ) → ℝ≥0∞) s =
    HMul.hMul (β := ℝ≥0∞) (ofReal |a⁻¹|) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [map_volume_mul_left h]

Premises used: Real.map_volume_mul_left
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
h : a ≠ 0
s : Set ℝ
⊢ (HSMul.hSMul (β := Measure ℝ) (ofReal |a⁻¹|) volume : (a : Set ℝ) → ℝ≥0∞) s =
    HMul.hMul (β := ℝ≥0∞) (ofReal |a⁻¹|) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
h : a ≠ 0
⊢ HSMul.hSMul (β := Measure ℝ) (ofReal |a|) (Measure.map (fun (x : ℝ) ↦ x * a) volume) = volume

Tactic:
simpa only [mul_comm] using Real.smul_map_volume_mul_left h

Premises used: Real.smul_map_volume_mul_left, mul_comm
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
h : a ≠ 0
⊢ Measure.map (fun (x : ℝ) ↦ x * a) volume = HSMul.hSMul (β := Measure ℝ) (ofReal |a⁻¹|) volume

Tactic:
simpa only [mul_comm] using Real.map_volume_mul_left h

Premises used: mul_comm, Real.map_volume_mul_left
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
h : a ≠ 0
s : Set ℝ
rw :
  (HSMul.hSMul (β := Measure ℝ) (ofReal |a⁻¹|) volume : (a : Set ℝ) → ℝ≥0∞) s =
    HMul.hMul (β := ℝ≥0∞) (ofReal |a⁻¹|) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (Measure.map (fun (x : ℝ) ↦ x * a) volume : (a : Set ℝ) → ℝ≥0∞) s =
    HMul.hMul (β := ℝ≥0∞) (ofReal |a⁻¹|) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [map_volume_mul_right h]

Premises used: Real.map_volume_mul_right
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
⊢ HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |(Matrix.diagonal D).det|)
      (Measure.map (α := ι → ℝ)
        (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
          (a : ι → ℝ) → ι → ℝ)
        volume) =
    volume

Tactic:
(Measure.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 ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
refine :
  ∀ (s : (i : ι) → Set ℝ) (hs : ∀ (i : ι), MeasurableSet (s i)),
    Eq (α := ℝ≥0∞)
      ((HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |(Matrix.diagonal D).det|)
              (Measure.map (α := ι → ℝ)
                (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
                  (a : ι → ℝ) → ι → ℝ)
                volume) :
            (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
          (Set.pi (α := fun (i : ι) ↦ ℝ) univ s) :
        ℝ≥0∞)
      (∏ i : ι, (volume : (a : Set ℝ) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |(Matrix.diagonal D).det|)
      (Measure.map (α := ι → ℝ)
        (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
          (a : ι → ℝ) → ι → ℝ)
        volume) =
    volume

Tactic:
refine (Measure.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 ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : (i : ι) → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
simp :
  HMul.hMul (β := ℝ≥0∞) (ofReal |∏ i : ι, D i|)
      (((Measure.map (α := ι → ℝ)
                (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
                  (a : ι → ℝ) → ι → ℝ)
                volume :
              Measure (ι → ℝ)) :
            (a : Set (ι → ℝ)) → ℝ≥0∞)
          (Set.pi (α := fun (i : ι) ↦ ℝ) univ s) :
        ℝ≥0∞) =
    ∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) (s x)
⊢ Eq (α := ℝ≥0∞)
    ((HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |(Matrix.diagonal D).det|)
            (Measure.map (α := ι → ℝ)
              (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
                (a : ι → ℝ) → ι → ℝ)
              volume) :
          (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (volume : (a : Set ℝ) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
simp only [det_diagonal, Measure.coe_smul, smul_eq_mul, Pi.smul_apply]

Premises used: Matrix.det_diagonal, MeasureTheory.Measure.coe_smul, smul_eq_mul, Pi.smul_apply
-- 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)
rw :
  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)
rw₁ :
  Measurable (α := ι → ℝ) (β := (i : ι) → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
      (a : ι → ℝ) → ι → ℝ)
⊢ HMul.hMul (β := ℝ≥0∞) (ofReal |∏ i : ι, D i|)
      (((Measure.map (α := ι → ℝ)
                (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
                  (a : ι → ℝ) → ι → ℝ)
                volume :
              Measure (ι → ℝ)) :
            (a : Set (ι → ℝ)) → ℝ≥0∞)
          (Set.pi (α := fun (i : ι) ↦ ℝ) univ s) :
        ℝ≥0∞) =
    ∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) (s x)

Tactic:
rw [Measure.map_apply _ (MeasurableSet.univ_pi hs)]

Premises used: MeasureTheory.Measure.map_apply, MeasurableSet.univ_pi
-- 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)
⊢ Measurable (α := ι → ℝ) (β := (i : ι) → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
      (a : ι → ℝ) → ι → ℝ)

Tactic:
Continuous.measurable (LinearMap.continuous_on_pi _)

Premises used: LinearMap.continuous_on_pi, Continuous.measurable
-- 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)
⊢ Measurable (α := ι → ℝ) (β := (i : ι) → ℝ)
    (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
      (a : ι → ℝ) → ι → ℝ)

Tactic:
exact Continuous.measurable (LinearMap.continuous_on_pi _)

Premises used: LinearMap.continuous_on_pi, Continuous.measurable
-- 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)
h₁ :
  ∀ (f : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ))
        (preimage (β := ι → ℝ)
          (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
            (a : ι → ℝ) → ι → ℝ)
          (Set.pi (α := fun (a : ι) ↦ ℝ) univ fun (i : ι) ↦ s i))
        f ↔
      Membership.mem (γ := Set (ι → ℝ))
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ (fun (x : ℝ) ↦ D i * x) ⁻¹' s i) f
⊢ 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)

Tactic:
ext f
-- 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)
f : ι → ℝ
⊢ Membership.mem (γ := Set (ι → ℝ))
      (preimage (β := ι → ℝ)
        (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
          (a : ι → ℝ) → ι → ℝ)
        (Set.pi (α := fun (a : ι) ↦ ℝ) univ fun (i : ι) ↦ s i))
      f ↔
    Membership.mem (γ := Set (ι → ℝ)) (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ (fun (x : ℝ) ↦ D i * x) ⁻¹' s i)
      f

Tactic:
simp only [LinearMap.coe_proj, smul_eq_mul, LinearMap.smul_apply, mem_univ_pi,
      mem_preimage, LinearMap.pi_apply, diagonal_toLin']

Premises used: LinearMap.smul_apply, LinearMap.coe_proj, LinearMap.pi_apply, Matrix.diagonal_toLin', smul_eq_mul, Set.mem_univ_pi, Set.mem_preimage
-- 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)
⊢ 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)

Tactic:
have :
    (Matrix.toLin' (diagonal D) ⁻¹' Set.pi Set.univ fun i : ι => s i) =
      Set.pi Set.univ fun i : ι => (D i * ·) ⁻¹' s i := by
    ext f
    simp only [LinearMap.coe_proj, smul_eq_mul, LinearMap.smul_apply, mem_univ_pi,
      mem_preimage, LinearMap.pi_apply, diagonal_toLin']
-- 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 : ι
⊢ ¬Eq (α := ℝ) (∏ i : ι, D i) 0

Tactic:
simp only [det_diagonal, Ne] at h

Premises used: Ne, Matrix.det_diagonal
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
D : ι → ℝ
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 : ι
h : ¬Eq (α := ℝ) (∏ i : ι, D i) 0
⊢ D i ≠ 0

Tactic:
Finset.prod_ne_zero_iff.1 h i (Finset.mem_univ i)

Premises used: Finset.mem_univ, Finset.prod_ne_zero_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
D : ι → ℝ
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 : ι
h : ¬Eq (α := ℝ) (∏ i : ι, D i) 0
⊢ D i ≠ 0

Tactic:
exact Finset.prod_ne_zero_iff.1 h i (Finset.mem_univ i)

Premises used: Finset.mem_univ, Finset.prod_ne_zero_iff, Iff.mp
-- 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 : ι
⊢ D i ≠ 0

Tactic:
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)