α : Type u_1
β : Type ?u.53774
m : MeasurableSpace α
μ ν✝ μ₁ μ₂ ν : Measure α
inst✝¹ : HaveLebesgueDecomposition μ₁ ν
inst✝ : HaveLebesgueDecomposition μ₂ ν
⊢ μ₁ + μ₂ = singularPart μ₁ ν + singularPart μ₂ ν + withDensity ν fun a => rnDeriv μ₁ ν a + rnDeriv μ₂ ν a
α : Type u_1
β : Type ?u.53774
m : MeasurableSpace α
μ ν✝ μ₁ μ₂ ν : Measure α
inst✝¹ : HaveLebesgueDecomposition μ₁ ν
inst✝ : HaveLebesgueDecomposition μ₂ ν
⊢ singularPart (μ₁ + μ₂) ν = singularPart μ₁ ν + singularPart μ₂ ν
refine'
  (eq_singularPart ((measurable_rnDeriv μ₁ ν).add (measurable_rnDeriv μ₂ ν))
      ((haveLebesgueDecomposition_spec _ _).2.1.add_left
        (haveLebesgueDecomposition_spec _ _).2.1)
      _).symm
α : Type u_1
β : Type ?u.53774
m : MeasurableSpace α
μ ν✝ μ₁ μ₂ ν : Measure α
inst✝¹ : HaveLebesgueDecomposition μ₁ ν
inst✝ : HaveLebesgueDecomposition μ₂ ν
⊢ μ₁ + μ₂ =
    singularPart μ₁ ν + singularPart μ₂ ν + (withDensity ν (rnDeriv μ₁ ν) + withDensity ν fun a => rnDeriv μ₂ ν a)
α : Type u_1
β : Type ?u.53774
m : MeasurableSpace α
μ ν✝ μ₁ μ₂ ν : Measure α
inst✝¹ : HaveLebesgueDecomposition μ₁ ν
inst✝ : HaveLebesgueDecomposition μ₂ ν
⊢ μ₁ + μ₂ = singularPart μ₁ ν + singularPart μ₂ ν + withDensity ν fun a => rnDeriv μ₁ ν a + rnDeriv μ₂ ν a
erw [withDensity_add_left (measurable_rnDeriv μ₁ ν)]
α : Type u_1
β : Type ?u.53774
m : MeasurableSpace α
μ ν✝ μ₁ μ₂ ν : Measure α
inst✝¹ : HaveLebesgueDecomposition μ₁ ν
inst✝ : HaveLebesgueDecomposition μ₂ ν
⊢ μ₁ + μ₂ =
    (singularPart μ₁ ν + withDensity ν (rnDeriv μ₁ ν) + withDensity ν fun a => rnDeriv μ₂ ν a) + singularPart μ₂ ν
α : Type u_1
β : Type ?u.53774
m : MeasurableSpace α
μ ν✝ μ₁ μ₂ ν : Measure α
inst✝¹ : HaveLebesgueDecomposition μ₁ ν
inst✝ : HaveLebesgueDecomposition μ₂ ν
⊢ μ₁ + μ₂ =
    singularPart μ₁ ν + singularPart μ₂ ν + (withDensity ν (rnDeriv μ₁ ν) + withDensity ν fun a => rnDeriv μ₂ ν a)
conv_rhs => rw [add_assoc, add_comm (μ₂.singularPart ν), ← add_assoc, ← add_assoc]
no goals
α : Type u_1
β : Type ?u.53774
m : MeasurableSpace α
μ ν✝ μ₁ μ₂ ν : Measure α
inst✝¹ : HaveLebesgueDecomposition μ₁ ν
inst✝ : HaveLebesgueDecomposition μ₂ ν
⊢ μ₁ + μ₂ =
    (singularPart μ₁ ν + withDensity ν (rnDeriv μ₁ ν) + withDensity ν fun a => rnDeriv μ₂ ν a) + singularPart μ₂ ν
rw [← haveLebesgueDecomposition_add μ₁ ν, add_assoc, add_comm (ν.withDensity (μ₂.rnDeriv ν)),
  ← haveLebesgueDecomposition_add μ₂ ν]