-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
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)
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)
h₈ 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 - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal
⊢ (↑(μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑((μ.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]

Premises used: MeasureTheory.integral_eq_lintegral_pos_part_sub_lintegral_neg_part, MeasureTheory.withDensityᵥ_apply, MeasureTheory.Measure.toSignedMeasure_apply_measurable, MeasureTheory.Integrable.integrableOn, MeasureTheory.measureReal_def, MeasureTheory.VectorMeasure.sub_apply, MeasureTheory.withDensity_apply