α : Type u_1
β : Type ?u.653242
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t✝ s t : SignedMeasure α
μ : Measure α
inst✝² : HaveLebesgueDecomposition s μ
inst✝¹ : HaveLebesgueDecomposition t μ
inst✝ : HaveLebesgueDecomposition (s + t) μ
⊢ withDensityᵥ μ (rnDeriv (s + t) μ) = withDensityᵥ μ (rnDeriv s μ + rnDeriv t μ)
α : Type u_1
β : Type ?u.653242
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t✝ s t : SignedMeasure α
μ : Measure α
inst✝² : HaveLebesgueDecomposition s μ
inst✝¹ : HaveLebesgueDecomposition t μ
inst✝ : HaveLebesgueDecomposition (s + t) μ
⊢ rnDeriv (s + t) μ =ᶠ[ae μ] rnDeriv s μ + rnDeriv t μ
refine'
  Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _)
    ((integrable_rnDeriv _ _).add (integrable_rnDeriv _ _)) _
no goals
α : Type u_1
β : Type ?u.653242
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t✝ s t : SignedMeasure α
μ : Measure α
inst✝² : HaveLebesgueDecomposition s μ
inst✝¹ : HaveLebesgueDecomposition t μ
inst✝ : HaveLebesgueDecomposition (s + t) μ
⊢ withDensityᵥ μ (rnDeriv (s + t) μ) = withDensityᵥ μ (rnDeriv s μ + rnDeriv t μ)
rw [← add_right_inj ((s + t).singularPart μ), singularPart_add_withDensity_rnDeriv_eq,
  withDensityᵥ_add (integrable_rnDeriv _ _) (integrable_rnDeriv _ _), singularPart_add,
  add_assoc, add_comm (t.singularPart μ), add_assoc, add_comm _ (t.singularPart μ),
  singularPart_add_withDensity_rnDeriv_eq, ← add_assoc,
  singularPart_add_withDensity_rnDeriv_eq]