∀ {G : Type u_2} (A : Type u_1) [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A]
  [inst_3 : TopologicalSpace A] [inst_4 : IsTopologicalAddGroup A] [inst_5 : LocallyCompactSpace A]
  [inst_6 : ContinuousConstSMul G A], (DomMulAct.mk 1 • MeasureTheory.Measure.addHaar).IsAddLeftInvariant