∀ {M : Type u_1} {α : Type u_2} [inst : VAdd M α] {x : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  (∀ (c : M) ⦃s : Set α⦄, MeasurableSet s → μ ((fun x => c +ᵥ x) ⁻¹' s) = μ s) →
    MeasureTheory.VAddInvariantMeasure M α μ