∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [Countable G],
  MeasureTheory.NullMeasurableSet s μ →
    (∀ (g : G), g ≠ 0 → MeasureTheory.AEDisjoint μ (g +ᵥ s) s) →
      (∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g +ᵥ x) μ μ) →
        μ Set.univ ≤ ∑' (g : G), μ (g +ᵥ s) → MeasureTheory.IsAddFundamentalDomain G s μ