-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ 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 :
  (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑(t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure : Set α → ℝ)
        i -
      (↑(t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure :
          Set α → ℝ)
        i
h₁ :
  (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
      (↑(t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure :
          Set α → ℝ)
        i
h₂ :
  (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
      (t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).real i
h₃ :
  (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    t.toJordanDecomposition.posPart.real i + (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
      (t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).real i
h₄ :
  (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    t.toJordanDecomposition.posPart.real i + (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
      (t.toJordanDecomposition.negPart.real i + (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).real i)
h₅ :
  (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    t.toJordanDecomposition.posPart.real i - t.toJordanDecomposition.negPart.real i +
      ((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
        (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).real i)
h₆ :
  (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑t.toJordanDecomposition.posPart.toSignedMeasure : Set α → ℝ) i - t.toJordanDecomposition.negPart.real i +
      ((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
        (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).real i)
⊢ (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑((t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
have h₇ : (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
  (↑t.toJordanDecomposition.posPart.toSignedMeasure : Set α → ℝ) i -
      (↑t.toJordanDecomposition.negPart.toSignedMeasure : Set α → ℝ) i +
    ((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
      (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).real i)
Tactic: rw [VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
      toSignedMeasure_apply_measurable hi, measureReal_add_apply, measureReal_add_apply,
      add_sub_add_comm, ← toSignedMeasure_apply_measurable hi,
      ← toSignedMeasure_apply_measurable hi, ← VectorMeasure.sub_apply,
      ← JordanDecomposition.toSignedMeasure, toSignedMeasure_toJordanDecomposition,
      VectorMeasure.add_apply, ← toSignedMeasure_apply_measurable hi,
      ← toSignedMeasure_apply_measurable hi,
      withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part hfi,
      VectorMeasure.sub_apply]