∀ {G : Type u_3} [inst : AddGroup G] {mG : MeasurableSpace G} [MeasurableAdd₂ G] [MeasurableNeg G]
  {μ : MeasureTheory.Measure G} [MeasureTheory.SFinite μ] [μ.IsAddLeftInvariant] {f g : G → ENNReal},
  Measurable f →
    Measurable g → (μ.withDensity f).conv (μ.withDensity g) = μ.withDensity (MeasureTheory.lconvolution f g μ)