no goals
α : Type u_1
β : Type ?u.640818
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t✝ s t : SignedMeasure α
μ : Measure α
inst✝¹ : HaveLebesgueDecomposition s μ
inst✝ : HaveLebesgueDecomposition t μ
⊢ singularPart (s - t) μ = singularPart s μ - singularPart t μ
rw [sub_eq_add_neg, sub_eq_add_neg, singularPart_add, singularPart_neg]