Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ -(s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure +
        ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure +
          (μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)).toSignedMeasure) +
      -(μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ)).toSignedMeasure =
    s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure

pp: case hfm
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ AEMeasurable (s.toJordanDecomposition.negPart.rnDeriv μ) μ

pp: case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : α), s.toJordanDecomposition.negPart.rnDeriv μ x ∂μ ≠ ∞

pp: case hfm
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ AEMeasurable (s.toJordanDecomposition.posPart.rnDeriv μ) μ

pp: case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : α), s.toJordanDecomposition.posPart.rnDeriv μ x ∂μ ≠ ∞

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ AEMeasurable (s.toJordanDecomposition.posPart.rnDeriv μ) μ

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : α), s.toJordanDecomposition.posPart.rnDeriv μ x ∂μ ≠ ∞

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ AEMeasurable (s.toJordanDecomposition.negPart.rnDeriv μ) μ

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : α), s.toJordanDecomposition.negPart.rnDeriv μ x ∂μ ≠ ∞

Tactic:
← toSignedMeasure_add,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ -(s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure +
        (s.toJordanDecomposition.posPart.singularPart μ +
            μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)).toSignedMeasure +
      -(μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ)).toSignedMeasure =
    s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure

case hfm
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ AEMeasurable (s.toJordanDecomposition.negPart.rnDeriv μ) μ

case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : α), s.toJordanDecomposition.negPart.rnDeriv μ x ∂μ ≠ ∞

case hfm
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ AEMeasurable (s.toJordanDecomposition.posPart.rnDeriv μ) μ

case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : α), s.toJordanDecomposition.posPart.rnDeriv μ x ∂μ ≠ ∞

α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ AEMeasurable (s.toJordanDecomposition.posPart.rnDeriv μ) μ

α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : α), s.toJordanDecomposition.posPart.rnDeriv μ x ∂μ ≠ ∞

α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ AEMeasurable (s.toJordanDecomposition.negPart.rnDeriv μ) μ

α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : α), s.toJordanDecomposition.negPart.rnDeriv μ x ∂μ ≠ ∞