-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem toJordanDecomposition_eq_of_eq_add_withDensity {f : α → ℝ} (hf : Measurable f)
    (hfi : Integrable f μ) (htμ : t ⟂ᵥ μ.toENNRealVectorMeasure) (hadd : s = t + μ.withDensityᵥ f) :
    s.toJordanDecomposition =
      @JordanDecomposition.mk α _
        (t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x))
        (t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x))
        (by haveI := isFiniteMeasure_withDensity_ofReal hfi.2; infer_instance)
        (by haveI := isFiniteMeasure_withDensity_ofReal hfi.neg.2; infer_instance)
        (jordanDecomposition_add_withDensity_mutuallySingular hf htμ)

Proof state:
α : 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✝ : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal ((-f) x))
⊢ s.toJordanDecomposition =
    JordanDecomposition.mk (t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x))
      (t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x)) ⋯

Tactic:
refine toJordanDecomposition_eq ?_

Result:
α : 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✝ : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal ((-f) x))
⊢ s =
    (JordanDecomposition.mk (t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x))
        (t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x)) ⋯).toSignedMeasure

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
⊢ s.toJordanDecomposition =
    JordanDecomposition.mk (t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x))
      (t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x)) ⋯

Tactic:
haveI := isFiniteMeasure_withDensity_ofReal hfi.2

Result:
α : 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 : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal (f x))
⊢ s.toJordanDecomposition =
    JordanDecomposition.mk (t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x))
      (t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x)) ⋯

Proof state:
α : 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 : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal (f x))
⊢ IsFiniteMeasure (t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x))

Tactic:
infer_instance

Result:
no goals