awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
hf : ¬Integrable f μ
hg : ¬Integrable g μ
neg :
  Eq (α := VectorMeasure α E)
    (if hf : Integrable f μ then
      { measureOf' := fun (s : Set α) ↦ if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0, empty' := ⋯,
        not_measurable' := ⋯, m_iUnion' := ⋯ }
    else 0)
    (μ.withDensityᵥ g)
neg₁ :
  Eq (α := VectorMeasure α E)
    (if hf : Integrable f μ then
      { measureOf' := fun (s : Set α) ↦ if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0, empty' := ⋯,
        not_measurable' := ⋯, m_iUnion' := ⋯ }
    else 0)
    (if hf : Integrable g μ then
      { measureOf' := fun (s : Set α) ↦ if MeasurableSet s then ∫ (x : α) in s, g x ∂μ else 0, empty' := ⋯,
        not_measurable' := ⋯, m_iUnion' := ⋯ }
    else 0)
neg₂ :
  Eq (α := VectorMeasure α E) 0
    (if hf : Integrable g μ then
      { measureOf' := fun (s : Set α) ↦ if MeasurableSet s then ∫ (x : α) in s, g x ∂μ else 0, empty' := ⋯,
        not_measurable' := ⋯, m_iUnion' := ⋯ }
    else 0)
⊢ Eq (α := VectorMeasure α E) (μ.withDensityᵥ f) (μ.withDensityᵥ g)
have neg₃ : Eq (α := VectorMeasure α E) 0 0
Tactic: rw [withDensityᵥ, withDensityᵥ, dif_neg hf, dif_neg hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ (μ.withDensityᵥ fun (x : α) ↦ (f x).toReal) = (μ.withDensity f).toSignedMeasure
have hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ
Tactic: have hfi := integrable_toReal_of_lintegral_ne_top hfm hf
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ
⊢ (μ.withDensityᵥ fun (x : α) ↦ (f x).toReal) = (μ.withDensity f).toSignedMeasure
have this : IsFiniteMeasure (μ.withDensity f)
Tactic: haveI := isFiniteMeasure_withDensity hf
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
⊢ (μ.withDensityᵥ fun (x : α) ↦ (f x).toReal) = (μ.withDensity f).toSignedMeasure
have h : ∀ (i : Set α) (hi : MeasurableSet i),
  (↑(μ.withDensityᵥ fun (x : α) ↦ (f x).toReal) : Set α → ℝ) i = (↑(μ.withDensity f).toSignedMeasure : Set α → ℝ) i
Tactic: ext i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
⊢ (↑(μ.withDensityᵥ fun (x : α) ↦ (f x).toReal) : Set α → ℝ) i = (↑(μ.withDensity f).toSignedMeasure : Set α → ℝ) i
have h : ∀ᵐ (x : α) ∂μ.restrict i, f x < ∞
Tactic: rw [withDensityᵥ_apply hfi hi, toSignedMeasure_apply_measurable hi, measureReal_def,
    withDensity_apply _ hi, integral_toReal hfm.restrict]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
⊢ ∀ᵐ (x : α) ∂μ.restrict i, f x < ∞
have h : ∫⁻ (x : α) in i, f x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
Tactic: refine ae_lt_top' hfm.restrict (ne_top_of_le_ne_top hf ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
| ∫⁻ (x : α), f x ∂μ
have rw : ∫⁻ (x : α) in Set.univ, f x ∂μ
Tactic: rw [← setLIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
⊢ ∫⁻ (x : α) in i, f x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
have h : ∫⁻ (x : α) in i, f x ∂μ ≤ ∫⁻ (x : α) in Set.univ, f x ∂μ
Tactic: conv_rhs => rw [← setLIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
⊢ μ.withDensityᵥ f =
    (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
      (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure
have this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
Tactic: haveI := isFiniteMeasure_withDensity_ofReal hfi.2
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
⊢ μ.withDensityᵥ f =
    (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
      (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure
have this₁ : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
Tactic: haveI := isFiniteMeasure_withDensity_ofReal hfi.neg.2
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
this_1 : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
⊢ μ.withDensityᵥ f =
    (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
      (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure
have h : ∀ (i : Set α) (hi : MeasurableSet i),
  (↑(μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
Tactic: ext i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
this_1 : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
⊢ (↑(μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
have h : ∫ (x : α) in i, f x ∂μ =
  (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
          (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
      Set α → ℝ)
    i
Tactic: rw [withDensityᵥ_apply hfi hi,
    integral_eq_lintegral_pos_part_sub_lintegral_neg_part hfi.integrableOn,
    VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
    toSignedMeasure_apply_measurable hi, measureReal_def, measureReal_def,
    withDensity_apply _ hi, withDensity_apply _ hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
this_1 : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
h :
  ∫ (x : α) in i, f x ∂μ =
    (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
⊢ (↑(μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
have h₁ : (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
  (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
          (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
      Set α → ℝ)
    i
Tactic: rw [withDensityᵥ_apply hfi hi,
    integral_eq_lintegral_pos_part_sub_lintegral_neg_part hfi.integrableOn,
    VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
    toSignedMeasure_apply_measurable hi, measureReal_def, measureReal_def,
    withDensity_apply _ hi, withDensity_apply _ hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
this_1 : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
h :
  ∫ (x : α) in i, f x ∂μ =
    (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
h₁ :
  (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
⊢ (↑(μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
have h₂ : (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
  (↑(μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure : Set α → ℝ) i -
    (↑(μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure : Set α → ℝ) i
Tactic: rw [withDensityᵥ_apply hfi hi,
    integral_eq_lintegral_pos_part_sub_lintegral_neg_part hfi.integrableOn,
    VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
    toSignedMeasure_apply_measurable hi, measureReal_def, measureReal_def,
    withDensity_apply _ hi, withDensity_apply _ hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
this_1 : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
h :
  ∫ (x : α) in i, f x ∂μ =
    (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
h₁ :
  (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
h₂ :
  (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    (↑(μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure : Set α → ℝ) i -
      (↑(μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure : Set α → ℝ) i
⊢ (↑(μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
have h₃ : (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
  (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
    (↑(μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure : Set α → ℝ) i
Tactic: rw [withDensityᵥ_apply hfi hi,
    integral_eq_lintegral_pos_part_sub_lintegral_neg_part hfi.integrableOn,
    VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
    toSignedMeasure_apply_measurable hi, measureReal_def, measureReal_def,
    withDensity_apply _ hi, withDensity_apply _ hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
this_1 : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
h :
  ∫ (x : α) in i, f x ∂μ =
    (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
h₁ :
  (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
h₂ :
  (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    (↑(μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure : Set α → ℝ) i -
      (↑(μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure : Set α → ℝ) i
h₃ :
  (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
      (↑(μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure : Set α → ℝ) i
⊢ (↑(μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
have h₄ : (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
  (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i - (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).real i
Tactic: rw [withDensityᵥ_apply hfi hi,
    integral_eq_lintegral_pos_part_sub_lintegral_neg_part hfi.integrableOn,
    VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
    toSignedMeasure_apply_measurable hi, measureReal_def, measureReal_def,
    withDensity_apply _ hi, withDensity_apply _ hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
this_1 : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
h :
  ∫ (x : α) in i, f x ∂μ =
    (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
h₁ :
  (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
h₂ :
  (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    (↑(μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure : Set α → ℝ) i -
      (↑(μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure : Set α → ℝ) i
h₃ :
  (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
      (↑(μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure : Set α → ℝ) i
h₄ :
  (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
      (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).real i
⊢ (↑(μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
have h₅ : (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
  ENNReal.toReal ((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x) : (a : Set α) → ℝ≥0∞) i) -
    (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).real i
Tactic: rw [withDensityᵥ_apply hfi hi,
    integral_eq_lintegral_pos_part_sub_lintegral_neg_part hfi.integrableOn,
    VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
    toSignedMeasure_apply_measurable hi, measureReal_def, measureReal_def,
    withDensity_apply _ hi, withDensity_apply _ hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
this_1 : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
h :
  ∫ (x : α) in i, f x ∂μ =
    (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
h₁ :
  (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
h₂ :
  (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    (↑(μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure : Set α → ℝ) i -
      (↑(μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure : Set α → ℝ) i
h₃ :
  (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
      (↑(μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure : Set α → ℝ) i
h₄ :
  (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
      (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).real i
h₅ :
  (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    ENNReal.toReal ((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x) : (a : Set α) → ℝ≥0∞) i) -
      (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).real i
⊢ (↑(μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
have h₆ : (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
  ENNReal.toReal ((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x) : (a : Set α) → ℝ≥0∞) i) -
    ENNReal.toReal ((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x) : (a : Set α) → ℝ≥0∞) i)
Tactic: rw [withDensityᵥ_apply hfi hi,
    integral_eq_lintegral_pos_part_sub_lintegral_neg_part hfi.integrableOn,
    VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
    toSignedMeasure_apply_measurable hi, measureReal_def, measureReal_def,
    withDensity_apply _ hi, withDensity_apply _ hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
this_1 : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
h :
  ∫ (x : α) in i, f x ∂μ =
    (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
h₁ :
  (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
h₂ :
  (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    (↑(μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure : Set α → ℝ) i -
      (↑(μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure : Set α → ℝ) i
h₃ :
  (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
      (↑(μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure : Set α → ℝ) i
h₄ :
  (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
      (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).real i
h₅ :
  (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    ENNReal.toReal ((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x) : (a : Set α) → ℝ≥0∞) i) -
      (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).real i
h₆ :
  (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    ENNReal.toReal ((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x) : (a : Set α) → ℝ≥0∞) i) -
      ENNReal.toReal ((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x) : (a : Set α) → ℝ≥0∞) i)
⊢ (↑(μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
have h₇ : (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
  (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal -
    ENNReal.toReal ((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x) : (a : Set α) → ℝ≥0∞) i)
Tactic: rw [withDensityᵥ_apply hfi hi,
    integral_eq_lintegral_pos_part_sub_lintegral_neg_part hfi.integrableOn,
    VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
    toSignedMeasure_apply_measurable hi, measureReal_def, measureReal_def,
    withDensity_apply _ hi, withDensity_apply _ hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ (↑(VectorMeasure.trim (μ.withDensityᵥ f) hm) : Set α → ℝ) i = ∫ (x : α) in i, f x ∂μ
have rw : (↑(μ.withDensityᵥ f) : Set α → ℝ) i = ∫ (x : α) in i, f x ∂μ
Tactic: rw [VectorMeasure.trim_measurableSet_eq hm hi, withDensityᵥ_apply hf (hm _ hi)]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.WithDensity (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
rw : (↑(μ.withDensityᵥ f) : Set α → ℝ) i = ∫ (x : α) in i, f x ∂μ
⊢ (↑(VectorMeasure.trim (μ.withDensityᵥ f) hm) : Set α → ℝ) i = ∫ (x : α) in i, f x ∂μ
have rw₁ : Eq (α := ℝ) (∫ (x : α) in i, f x ∂μ) (∫ (x : α) in i, f x ∂μ)
Tactic: rw [VectorMeasure.trim_measurableSet_eq hm hi, withDensityᵥ_apply hf (hm _ hi)]