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

Tactic:
infer_instance

Result:
no goals

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))
⊢ t + μ.withDensityᵥ f =
    (t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x)).toSignedMeasure -
      (t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x)).toSignedMeasure

Tactic:
ext i hi

Result:
case h
α : 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))
i : Set α
hi : MeasurableSet i
⊢ ↑(t + μ.withDensityᵥ f) i =
    ↑((t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x)).toSignedMeasure -
          (t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x)).toSignedMeasure)
      i

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))
⊢ 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.neg.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))
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:
case h
α : 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))
i : Set α
hi : MeasurableSet i
⊢ ↑(t + μ.withDensityᵥ f) i =
    ↑((t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x)).toSignedMeasure -
          (t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x)).toSignedMeasure)
      i

Tactic:
rw [VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
    toSignedMeasure_apply_measurable hi, add_apply, add_apply, ENNReal.toReal_add,
    ENNReal.toReal_add, 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] <;>
  exact (measure_lt_top _ _).ne

Result:
no goals

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

Tactic:
haveI := isFiniteMeasure_withDensity_ofReal hfi.neg.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))
⊢ IsFiniteMeasure (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))
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

Tactic:
simp_rw [JordanDecomposition.toSignedMeasure, hadd]

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))
⊢ t + μ.withDensityᵥ f =
    (t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x)).toSignedMeasure -
      (t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x)).toSignedMeasure