∀ {T : ℝ},
  0 < T →
    ∀ (t : ℝ) (μ : autoParam (MeasureTheory.Measure ℝ) isAddFundamentalDomain_Ioc'._auto_1),
      MeasureTheory.IsAddFundamentalDomain (↥(AddSubgroup.zmultiples T).op) (Set.Ioc t (t + T)) μ