α : Type u_1
β : Type ?u.43416
m : MeasurableSpace α
μ ν✝ ν : Measure α
⊢ 0 = 0 + withDensity ν 0
α : Type u_1
β : Type ?u.43416
m : MeasurableSpace α
μ ν✝ ν : Measure α
⊢ singularPart 0 ν = 0
refine' (eq_singularPart measurable_zero MutuallySingular.zero_left _).symm
no goals
α : Type u_1
β : Type ?u.43416
m : MeasurableSpace α
μ ν✝ ν : Measure α
⊢ 0 = 0 + withDensity ν 0
rw [zero_add, withDensity_zero]