-- Mathlib/MeasureTheory/VectorMeasure/WithDensity.lean
theorem withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part {f : α → ℝ}
    (hfi : Integrable f μ) :
    μ.withDensityᵥ f =
      @toSignedMeasure α _ (μ.withDensity fun x => ENNReal.ofReal <| f x)
          (isFiniteMeasure_withDensity_ofReal hfi.2) -
        @toSignedMeasure α _ (μ.withDensity fun x => ENNReal.ofReal <| -f x)
          (isFiniteMeasure_withDensity_ofReal hfi.neg.2)

Proof state:
α : 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

Tactic:
haveI := isFiniteMeasure_withDensity_ofReal hfi.2

Result:
α : 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

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
this✝ : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
⊢ ↑(μ.withDensityᵥ f) i =
    ↑((μ.withDensity fun x => ENNReal.ofReal (f x)).toSignedMeasure -
          (μ.withDensity fun x => ENNReal.ofReal (-f x)).toSignedMeasure)
      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, withDensity_apply _ hi, withDensity_apply _ hi]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
this✝ : 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

Tactic:
ext i hi

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
this✝ : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
⊢ ↑(μ.withDensityᵥ f) i =
    ↑((μ.withDensity fun x => ENNReal.ofReal (f x)).toSignedMeasure -
          (μ.withDensity fun x => ENNReal.ofReal (-f x)).toSignedMeasure)
      i

Proof state:
α : 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

Tactic:
haveI := isFiniteMeasure_withDensity_ofReal hfi.neg.2

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
this✝ : 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