∀ {G : Type u_3} {A : Type u_4} [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A]
  [inst_3 : MeasurableSpace A] [inst_4 : TopologicalSpace A] [inst_5 : BorelSpace A] [inst_6 : ContinuousConstSMul G A]
  {μ : MeasureTheory.Measure A} (g : Gᵈᵐᵃ) [μ.Regular], (g • μ).Regular