awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
a : ι → ℝ
r : ℝ
hr : 0 < r
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (ball a r) = ofReal ((2 * r) ^ Fintype.card ι)
have simp : ofReal (2 * r) ^ Finset.card.{u_1} (α := ι) Finset.univ = ofReal ((2 * r) ^ Fintype.card ι)
Tactic: simp only [MeasureTheory.volume_pi_ball a hr, volume_ball, Finset.prod_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
a : ι → ℝ
r : ℝ
hr : 0 ≤ r
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (closedBall a r) = ofReal ((2 * r) ^ Fintype.card ι)
have simp : ofReal (2 * r) ^ Finset.card.{u_1} (α := ι) Finset.univ = ofReal ((2 * r) ^ Fintype.card ι)
Tactic: simp only [MeasureTheory.volume_pi_closedBall a hr, volume_closedBall, Finset.prod_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
h : a ≠ 0
⊢ HSMul.hSMul (β := Measure ℝ) (ofReal |a|) (Measure.map (fun (x : ℝ) ↦ a * x) volume) = volume
have 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∞)
Tactic: refine (Real.measure_ext_Ioo_rat fun p q => ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
h : a ≠ 0
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∞)
have 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∞)
Tactic: rcases lt_or_gt_of_ne h with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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∞)
⊢ 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∞)
have 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∞)
Tactic: rcases lt_or_gt_of_ne h with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
h : a ≠ 0
| HSMul.hSMul (β := Measure ℝ) (ofReal |a⁻¹|) volume
have rw : Measure.map (fun (x : ℝ) ↦ a * x) 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
h : a ≠ 0
⊢ Measure.map (fun (x : ℝ) ↦ a * x) volume = HSMul.hSMul (β := Measure ℝ) (ofReal |a⁻¹|) volume
have conv_rhs : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
h : a ≠ 0
conv_rhs : Measure.map (fun (x : ℝ) ↦ a * x) volume = HSMul.hSMul (β := Measure ℝ) (ofReal |a⁻¹|) volume
⊢ Measure.map (fun (x : ℝ) ↦ a * x) volume = HSMul.hSMul (β := Measure ℝ) (ofReal |a⁻¹|) volume
have conv_rhs₁ : Eq (α := Measure ℝ) (Measure.map (fun (x : ℝ) ↦ a * x) volume) (Measure.map (fun (x : ℝ) ↦ a * x) 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
h : a ≠ 0
s : Set ℝ
⊢ (Measure.map (fun (x : ℝ) ↦ a * x) volume : (a : Set ℝ) → ℝ≥0∞) s =
    HMul.hMul (β := ℝ≥0∞) (ofReal |a⁻¹|) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
have rw : (HSMul.hSMul (β := Measure ℝ) (ofReal |a⁻¹|) volume : (a : Set ℝ) → ℝ≥0∞) s =
  HMul.hMul (β := ℝ≥0∞) (ofReal |a⁻¹|) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [map_volume_mul_left h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
h : a ≠ 0
s : Set ℝ
⊢ (Measure.map (fun (x : ℝ) ↦ x * a) volume : (a : Set ℝ) → ℝ≥0∞) s =
    HMul.hMul (β := ℝ≥0∞) (ofReal |a⁻¹|) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
have rw : (HSMul.hSMul (β := Measure ℝ) (ofReal |a⁻¹|) volume : (a : Set ℝ) → ℝ≥0∞) s =
  HMul.hMul (β := ℝ≥0∞) (ofReal |a⁻¹|) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [map_volume_mul_right h]
-- 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
⊢ HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |(Matrix.diagonal D).det|)
      (Measure.map (α := ι → ℝ)
        (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
          (a : ι → ℝ) → ι → ℝ)
        volume) =
    volume
have 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∞)
Tactic: refine (Measure.pi_eq fun s hs => ?_).symm
-- 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)
⊢ 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∞)
have 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)
Tactic: simp only [det_diagonal, Measure.coe_smul, smul_eq_mul, Pi.smul_apply]
-- 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)
⊢ 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)
have 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)
Tactic: rw [Measure.map_apply _ (MeasurableSet.univ_pi hs)]
-- 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)
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)
⊢ 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)
have rw₁ : Measurable (α := ι → ℝ) (β := (i : ι) → ℝ)
  (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) (Matrix.diagonal D) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
    (a : ι → ℝ) → ι → ℝ)
Tactic: rw [Measure.map_apply _ (MeasurableSet.univ_pi hs)]
-- 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)
⊢ 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)
have 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
Tactic: ext f
-- 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)
⊢ 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 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)
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']
-- 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)
i : ι
⊢ D i ≠ 0
have h₁ : ¬Eq (α := ℝ) (∏ i : ι, D i) 0
Tactic: simp only [det_diagonal, Ne] at h
Cleared hypotheses: h
-- 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)
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 A : 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)
-- 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
⊢ 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 : ofReal |D i| * HMul.hMul (β := ℝ≥0∞) (ofReal |(D i)⁻¹|) ((volume : (a : Set ℝ) → ℝ≥0∞) (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]
-- 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)
⊢ 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₁ : HMul.hMul (β := ℝ≥0∞) (ofReal |D i| * ofReal |(D i)⁻¹|) ((volume : (a : Set ℝ) → ℝ≥0∞) (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]
-- 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)
⊢ 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₂ : HMul.hMul (β := ℝ≥0∞) (ofReal (|D i| * |(D i)⁻¹|)) ((volume : (a : Set ℝ) → ℝ≥0∞) (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]
-- 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)
⊢ 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₃ : HMul.hMul (β := ℝ≥0∞) (ofReal |D i * (D i)⁻¹|) ((volume : (a : Set ℝ) → ℝ≥0∞) (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]
-- 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)
⊢ 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₄ : HMul.hMul (β := ℝ≥0∞) (ofReal |1|) ((volume : (a : Set ℝ) → ℝ≥0∞) (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]
-- 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)
⊢ 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₅ : HMul.hMul (β := ℝ≥0∞) (ofReal 1) ((volume : (a : Set ℝ) → ℝ≥0∞) (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]
-- 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)
⊢ 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₆ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (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]