α : Type u_1
β : Type ?u.638693
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t✝ s t : SignedMeasure α
μ : Measure α
inst✝¹ : HaveLebesgueDecomposition s μ
inst✝ : HaveLebesgueDecomposition t μ
⊢ s + t = singularPart s μ + singularPart t μ + withDensityᵥ μ (rnDeriv s μ + rnDeriv t μ)
α : Type u_1
β : Type ?u.638693
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t✝ s t : SignedMeasure α
μ : Measure α
inst✝¹ : HaveLebesgueDecomposition s μ
inst✝ : HaveLebesgueDecomposition t μ
⊢ singularPart (s + t) μ = singularPart s μ + singularPart t μ
refine'
  (eq_singularPart _ (s.rnDeriv μ + t.rnDeriv μ)
      ((mutuallySingular_singularPart s μ).add_left (mutuallySingular_singularPart t μ))
      _).symm
α : Type u_1
β : Type ?u.638693
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t✝ s t : SignedMeasure α
μ : Measure α
inst✝¹ : HaveLebesgueDecomposition s μ
inst✝ : HaveLebesgueDecomposition t μ
⊢ s + t = singularPart s μ + singularPart t μ + (withDensityᵥ μ (rnDeriv s μ) + withDensityᵥ μ (rnDeriv t μ))
α : Type u_1
β : Type ?u.638693
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t✝ s t : SignedMeasure α
μ : Measure α
inst✝¹ : HaveLebesgueDecomposition s μ
inst✝ : HaveLebesgueDecomposition t μ
⊢ s + t = singularPart s μ + singularPart t μ + withDensityᵥ μ (rnDeriv s μ + rnDeriv t μ)
erw [withDensityᵥ_add (integrable_rnDeriv s μ) (integrable_rnDeriv t μ)]
no goals
α : Type u_1
β : Type ?u.638693
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t✝ s t : SignedMeasure α
μ : Measure α
inst✝¹ : HaveLebesgueDecomposition s μ
inst✝ : HaveLebesgueDecomposition t μ
⊢ s + t = singularPart s μ + singularPart t μ + (withDensityᵥ μ (rnDeriv s μ) + withDensityᵥ μ (rnDeriv t μ))
rw [add_assoc, add_comm (t.singularPart μ), add_assoc, add_comm _ (t.singularPart μ),
  singularPart_add_withDensity_rnDeriv_eq, ← add_assoc,
  singularPart_add_withDensity_rnDeriv_eq]