α : Type u_1
β : Type ?u.301669
m : MeasurableSpace α
μ✝ ν : Measure α
s : SignedMeasure α
μ : Measure α
⊢ Measure.singularPart (toJordanDecomposition s).posPart μ + Measure.singularPart (toJordanDecomposition s).negPart μ ⟂ₘ
    VectorMeasure.ennrealToMeasure (toENNRealVectorMeasure μ)
α : Type u_1
β : Type ?u.301669
m : MeasurableSpace α
μ✝ ν : Measure α
s : SignedMeasure α
μ : Measure α
⊢ singularPart s μ ⟂ᵥ toENNRealVectorMeasure μ
rw [mutuallySingular_ennreal_iff, singularPart_totalVariation]
α : Type u_1
β : Type ?u.301669
m : MeasurableSpace α
μ✝ ν : Measure α
s : SignedMeasure α
μ : Measure α
⊢ Measure.singularPart (toJordanDecomposition s).posPart μ + Measure.singularPart (toJordanDecomposition s).negPart μ ⟂ₘ
    Equiv.toFun VectorMeasure.equivMeasure (Equiv.invFun VectorMeasure.equivMeasure μ)
α : Type u_1
β : Type ?u.301669
m : MeasurableSpace α
μ✝ ν : Measure α
s : SignedMeasure α
μ : Measure α
⊢ Measure.singularPart (toJordanDecomposition s).posPart μ + Measure.singularPart (toJordanDecomposition s).negPart μ ⟂ₘ
    VectorMeasure.ennrealToMeasure (toENNRealVectorMeasure μ)
change _ ⟂ₘ VectorMeasure.equivMeasure.toFun (VectorMeasure.equivMeasure.invFun μ)
α : Type u_1
β : Type ?u.301669
m : MeasurableSpace α
μ✝ ν : Measure α
s : SignedMeasure α
μ : Measure α
⊢ Measure.singularPart (toJordanDecomposition s).posPart μ + Measure.singularPart (toJordanDecomposition s).negPart μ ⟂ₘ
    μ
α : Type u_1
β : Type ?u.301669
m : MeasurableSpace α
μ✝ ν : Measure α
s : SignedMeasure α
μ : Measure α
⊢ Measure.singularPart (toJordanDecomposition s).posPart μ + Measure.singularPart (toJordanDecomposition s).negPart μ ⟂ₘ
    Equiv.toFun VectorMeasure.equivMeasure (Equiv.invFun VectorMeasure.equivMeasure μ)
rw [VectorMeasure.equivMeasure.right_inv μ]
no goals
α : Type u_1
β : Type ?u.301669
m : MeasurableSpace α
μ✝ ν : Measure α
s : SignedMeasure α
μ : Measure α
⊢ Measure.singularPart (toJordanDecomposition s).posPart μ + Measure.singularPart (toJordanDecomposition s).negPart μ ⟂ₘ
    μ
exact (mutuallySingular_singularPart _ _).add_left (mutuallySingular_singularPart _ _)