∀ {G : Type u_1} {mG : MeasurableSpace G} [inst : Group G] [MeasurableMul₂ G] [MeasurableInv G]
  {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] [MeasureTheory.SFinite μ] {f g k : G → ENNReal},
  AEMeasurable f μ →
    AEMeasurable g μ →
      AEMeasurable k μ →
        MeasureTheory.mlconvolution f (MeasureTheory.mlconvolution g k μ) μ =
          MeasureTheory.mlconvolution (MeasureTheory.mlconvolution f g μ) k μ