α : Type u_1
β : Type ?u.646293
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
inst✝ : HaveLebesgueDecomposition s μ
⊢ withDensityᵥ μ (rnDeriv (-s) μ) = withDensityᵥ μ (-rnDeriv s μ)
α : Type u_1
β : Type ?u.646293
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
inst✝ : HaveLebesgueDecomposition s μ
⊢ rnDeriv (-s) μ =ᶠ[ae μ] -rnDeriv s μ
refine'
  Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _) (integrable_rnDeriv _ _).neg _
no goals
α : Type u_1
β : Type ?u.646293
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
inst✝ : HaveLebesgueDecomposition s μ
⊢ withDensityᵥ μ (rnDeriv (-s) μ) = withDensityᵥ μ (-rnDeriv s μ)
rw [withDensityᵥ_neg, ← add_right_inj ((-s).singularPart μ),
  singularPart_add_withDensity_rnDeriv_eq, singularPart_neg, ← neg_add,
  singularPart_add_withDensity_rnDeriv_eq]