α : Type u_1
β : Type ?u.647949
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
inst✝ : HaveLebesgueDecomposition s μ
r : ℝ
⊢ withDensityᵥ μ (rnDeriv (r • s) μ) = withDensityᵥ μ (r • rnDeriv s μ)
α : Type u_1
β : Type ?u.647949
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
inst✝ : HaveLebesgueDecomposition s μ
r : ℝ
⊢ rnDeriv (r • s) μ =ᶠ[ae μ] r • rnDeriv s μ
refine'
  Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _)
    ((integrable_rnDeriv _ _).smul r) _
α : Type u_1
β : Type ?u.647949
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
inst✝ : HaveLebesgueDecomposition s μ
r : ℝ
⊢ withDensityᵥ μ (rnDeriv (r • s) μ) = withDensityᵥ μ (r • rnDeriv s μ)
α : Type u_1
β : Type ?u.647949
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
inst✝ : HaveLebesgueDecomposition s μ
r : ℝ
⊢ withDensityᵥ μ (rnDeriv (r • s) μ) = withDensityᵥ μ (r • rnDeriv s μ)
change _ = μ.withDensityᵥ ((r : ℝ) • s.rnDeriv μ)
α : Type u_1
β : Type ?u.647949
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
inst✝ : HaveLebesgueDecomposition s μ
r : ℝ
⊢ r • s = r • singularPart s μ + r • withDensityᵥ μ (rnDeriv s μ)
α : Type u_1
β : Type ?u.647949
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
inst✝ : HaveLebesgueDecomposition s μ
r : ℝ
⊢ withDensityᵥ μ (rnDeriv (r • s) μ) = withDensityᵥ μ (r • rnDeriv s μ)
rw [withDensityᵥ_smul (rnDeriv s μ) (r : ℝ), ← add_right_inj ((r • s).singularPart μ),
  singularPart_add_withDensity_rnDeriv_eq, singularPart_smul]
α : Type u_1
β : Type ?u.647949
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
inst✝ : HaveLebesgueDecomposition s μ
r : ℝ
⊢ r • s = r • singularPart s μ + r • withDensityᵥ μ (rnDeriv s μ)
α : Type u_1
β : Type ?u.647949
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
inst✝ : HaveLebesgueDecomposition s μ
r : ℝ
⊢ r • s = r • singularPart s μ + r • withDensityᵥ μ (rnDeriv s μ)
change _ = _ + r • _
no goals
α : Type u_1
β : Type ?u.647949
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
inst✝ : HaveLebesgueDecomposition s μ
r : ℝ
⊢ r • s = r • singularPart s μ + r • withDensityᵥ μ (rnDeriv s μ)
rw [← smul_add, singularPart_add_withDensity_rnDeriv_eq]