Measures with density without atoms

TODO: prove a version without topological assumptions, e.g. for σ-finite μ with NoAtoms' μ and f < ∞ almost everywhere.

theorem MeasureTheory.NoAtoms'.withDensity {α : Type u_1} [TopologicalSpace α] [T2Space α] [TopologicalSpace.PseudoMetrizableSpace α] [SigmaCompactSpace α] [MeasurableSpace α] [BorelSpace α] {μ : Measure α} [NullSingletonClass μ] {f : α → ENNReal} (hf : LocallyIntegrable f μ) : NoAtoms' (μ.withDensity f)

A version of MeasureTheory.Measure.nullSingletonClass_withDensity for NoAtoms'. Some assumption on f is needed: for f = ∞, every set of positive measure is an atom of μ.withDensity f.