∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f g : α → ENNReal},
  Measurable f →
    Measurable g →
      ∀ {s : Set α}, MeasurableSet s → ∫⁻ (x : α) in s, g x ∂μ.withDensity f = ∫⁻ (x : α) in s, (f * g) x ∂μ