awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
U : Set (AddCircle T)
meas_U : MeasurableSet U
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) U : ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞) (QuotientAddGroup.mk ⁻¹' U ∩ Ioc t (t + T)) : ℝ≥0∞)

Tactic:
(isAddFundamentalDomain_Ioc' hT.out _).addProjection_respects_measure_apply
    (volume : Measure (AddCircle T)) meas_U

Premises used: MeasureTheory.MeasureSpace.volume, MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure_apply, isAddFundamentalDomain_Ioc', Fact.out
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
⊢ |T| = T

Tactic:
have hT' : |T| = T := abs_eq_self.mpr hT.out.le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
hε : ε < T / 2
rw : Icc (-ε) ε ⊆ I
⊢ Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε

Tactic:
rw [inter_eq_left, Real.closedBall_eq_Icc, zero_sub, zero_add]

Premises used: Set.inter_eq_left, Real.closedBall_eq_Icc, zero_add, zero_sub
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
hε : ε < T / 2
y : ℝ
hy₁ : -ε ≤ y
hy₂ : y ≤ ε
left : -(T / 2) < y
right : y ≤ T / 2
⊢ y ∈ I

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
hε : ε < T / 2
y : ℝ
hy₁ : -ε ≤ y
hy₂ : y ≤ ε
linarith : y ≤ -(T / 2) → 2 / 2 = 1
linarith₁ : y ≤ -(T / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : y ≤ -(T / 2) → GT.gt (α := ℝ) 2 0
linarith₃ : y ≤ -(T / 2) → 2 / 2 = 1
linarith₄ : y ≤ -(T / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : y ≤ -(T / 2) → GT.gt (α := ℝ) 2 0
linarith₆ : y ≤ -(T / 2) → 2 * ε - 1 * T + 2 * (-ε - y) + (2 * y - -(1 * T)) = 0
linarith₇ : y ≤ -(T / 2) → GT.gt (α := ℝ) 2 0
⊢ -(T / 2) < y

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
hε : ε < T / 2
y : ℝ
hy₁ : -ε ≤ y
hy₂ : y ≤ ε
linarith : T / 2 < y → 2 / 2 = 1
linarith₁ : T / 2 < y → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : T / 2 < y → GT.gt (α := ℝ) 2 0
linarith₃ : T / 2 < y → 2 / 2 = 1
linarith₄ : T / 2 < y → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : T / 2 < y → GT.gt (α := ℝ) 2 0
linarith₆ : T / 2 < y → 2 * ε - 1 * T + 2 * (y - ε) + (1 * T - 2 * y) = 0
linarith₇ : T / 2 < y → GT.gt (α := ℝ) 2 0
⊢ y ≤ T / 2

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
⊢ ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε

Tactic:
have h₁ : ε < T / 2 → Metric.closedBall (0 : ℝ) ε ∩ I = Metric.closedBall (0 : ℝ) ε := by
    intro hε
    rw [inter_eq_left, Real.closedBall_eq_Icc, zero_sub, zero_add]
    rintro y ⟨hy₁, hy₂⟩; constructor <;> linarith
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
rw : if ε < |T| / 2 then Metric.closedBall 0 ε ∩ I else I
| if ε < T / 2 then Metric.closedBall 0 ε else I

Tactic:
rw [← if_ctx_congr (Iff.rfl : ε < T / 2 ↔ ε < T / 2) h₁ fun _ => rfl, ← hT']

Premises used: if_ctx_congr, Iff.rfl, rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
conv_rhs :
  preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < |T| / 2 then Metric.closedBall 0 ε ∩ I else I
⊢ preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < T / 2 then Metric.closedBall 0 ε else I

Tactic:
conv_rhs => rw [← if_ctx_congr (Iff.rfl : ε < T / 2 ↔ ε < T / 2) h₁ fun _ => rfl, ← hT']

Premises used: if_ctx_congr, Iff.rfl, rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
hs : I ⊆ Metric.closedBall 0 (|T| / 2)
⊢ preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < |T| / 2 then Metric.closedBall 0 ε ∩ I else I

Tactic:
apply coe_real_preimage_closedBall_inter_eq

Premises used: AddCircle.coe_real_preimage_closedBall_inter_eq
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
⊢ I ⊆ Metric.closedBall 0 (|T| / 2)

Tactic:
simpa only [hT', Real.closedBall_eq_Icc, zero_add, zero_sub] using Ioc_subset_Icc_self

Premises used: Real.closedBall_eq_Icc, Set.Ioc_subset_Icc_self, zero_add, zero_sub
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
⊢ preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < T / 2 then Metric.closedBall 0 ε else I

Tactic:
have h₂ : (↑) ⁻¹' Metric.closedBall (0 : AddCircle T) ε ∩ I =
      if ε < T / 2 then Metric.closedBall (0 : ℝ) ε else I := by
    conv_rhs => rw [← if_ctx_congr (Iff.rfl : ε < T / 2 ↔ ε < T / 2) h₁ fun _ => rfl, ← hT']
    apply coe_real_preimage_closedBall_inter_eq
    simpa only [hT', Real.closedBall_eq_Icc, zero_add, zero_sub] using Ioc_subset_Icc_self
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ :
  preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < T / 2 then Metric.closedBall 0 ε else I
linarith : -(T / 2) + T < T / 2 → 2 / 2 = 1
linarith₁ : -(T / 2) + T < T / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : -(T / 2) + T < T / 2 → 2 / 2 = 1
linarith₃ : -(T / 2) + T < T / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : -(T / 2) + T < T / 2 → GT.gt (α := ℝ) 2 0
linarith₅ : -(T / 2) + T < T / 2 → -(1 * T) + 2 * T - 1 * T = 0
linarith₆ : T / 2 < -(T / 2) + T → 2 / 2 = 1
linarith₇ : T / 2 < -(T / 2) + T → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : T / 2 < -(T / 2) + T → 2 / 2 = 1
linarith₉ : T / 2 < -(T / 2) + T → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₀ : T / 2 < -(T / 2) + T → GT.gt (α := ℝ) 2 0
linarith₁₁ : T / 2 < -(T / 2) + T → 1 * T - (-(1 * T) + 2 * T) = 0
⊢ -(T / 2) + T = T / 2

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ :
  preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < T / 2 then Metric.closedBall 0 ε else I
rw : (volume : (a : Set ℝ) → ℝ≥0∞) (if ε < T / 2 then Metric.closedBall 0 ε else I) = ENNReal.ofReal (min T (2 * ε))
⊢ (volume : (a : Set (AddCircle T)) → ℝ≥0∞) (Metric.closedBall x ε) = ENNReal.ofReal (min T (2 * ε))

Tactic:
rw [addHaar_closedBall_center, add_projection_respects_measure T (-(T / 2))
    measurableSet_closedBall, (by linarith : -(T / 2) + T = T / 2), h₂]

Premises used: AddCircle.add_projection_respects_measure, HDiv.hDiv, measurableSet_closedBall, OfNat.ofNat, MeasureTheory.Measure.addHaar_closedBall_center, Neg.neg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ :
  preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < T / 2 then Metric.closedBall 0 ε else I
pos :
  ∀ (hε : ε < T / 2),
    (volume : (a : Set ℝ) → ℝ≥0∞) (if ε < T / 2 then Metric.closedBall 0 ε else I) = ENNReal.ofReal (min T (2 * ε))
neg :
  ∀ (hε : ¬ε < T / 2),
    (volume : (a : Set ℝ) → ℝ≥0∞) (if ε < T / 2 then Metric.closedBall 0 ε else I) = ENNReal.ofReal (min T (2 * ε))
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (if ε < T / 2 then Metric.closedBall 0 ε else I) = ENNReal.ofReal (min T (2 * ε))

Tactic:
by_cases hε : ε < T / 2
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ :
  preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < T / 2 then Metric.closedBall 0 ε else I
hε : ε < T / 2
linarith : T < 2 * ε → 2 / 2 = 1
linarith₁ : T < 2 * ε → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : T < 2 * ε → GT.gt (α := ℝ) 2 0
linarith₃ : T < 2 * ε → 2 * ε - 1 * T + (T - 2 * ε) = 0
⊢ 2 * ε ≤ T

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ :
  preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < T / 2 then Metric.closedBall 0 ε else I
hε : ε < T / 2
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (if ε < T / 2 then Metric.closedBall 0 ε else I) = ENNReal.ofReal (min T (2 * ε))

Tactic:
simp [hε, min_eq_right (by linarith : 2 * ε ≤ T)]

Premises used: min_eq_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ :
  preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < T / 2 then Metric.closedBall 0 ε else I
hε : ¬ε < T / 2
linarith : 2 * ε < T → 2 / 2 = 1
linarith₁ : 2 * ε < T → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 2 * ε < T → GT.gt (α := ℝ) 2 0
linarith₃ : 2 * ε < T → 1 * T - 2 * ε + (2 * ε - T) = 0
⊢ T ≤ 2 * ε

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ :
  preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < T / 2 then Metric.closedBall 0 ε else I
hε : ¬ε < T / 2
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (if ε < T / 2 then Metric.closedBall 0 ε else I) = ENNReal.ofReal (min T (2 * ε))

Tactic:
simp [I, hε, min_eq_left (by linarith : T ≤ 2 * ε)]

Premises used: min_eq_left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
⊢ IsUnifLocDoublingMeasure (α := AddCircle T) volume

Tactic:
⟨⟨Real.toNNReal 2, Filter.Eventually.of_forall fun ε x => ?_⟩⟩

Premises used: IsUnifLocDoublingMeasure.mk, Filter.Eventually.of_forall, Exists.intro, OfNat.ofNat, Real.toNNReal
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
refine :
  ∀ (ε : ℝ) (x : AddCircle T),
    (volume : (a : Set (AddCircle T)) → ℝ≥0∞) (Metric.closedBall x (2 * ε)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(Real.toNNReal 2) : ℝ≥0∞)
        ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (Metric.closedBall x ε) : ℝ≥0∞)
⊢ IsUnifLocDoublingMeasure (α := AddCircle T) volume

Tactic:
refine ⟨⟨Real.toNNReal 2, Filter.Eventually.of_forall fun ε x => ?_⟩⟩
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
ε : ℝ
x : AddCircle T
simp : ENNReal.ofReal (min T (2 * (2 * ε))) ≤ (↑(Real.toNNReal 2) : ℝ≥0∞) * ENNReal.ofReal (min T (2 * ε))
⊢ (volume : (a : Set (AddCircle T)) → ℝ≥0∞) (Metric.closedBall x (2 * ε)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(Real.toNNReal 2) : ℝ≥0∞)
      ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (Metric.closedBall x ε) : ℝ≥0∞)

Tactic:
simp only [volume_closedBall]

Premises used: AddCircle.volume_closedBall
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
ε : ℝ
x : AddCircle T
erw : ENNReal.ofReal (min T (2 * (2 * ε))) ≤ ENNReal.ofReal (2 * min T (2 * ε))
⊢ ENNReal.ofReal (min T (2 * (2 * ε))) ≤ (↑(Real.toNNReal 2) : ℝ≥0∞) * ENNReal.ofReal (min T (2 * ε))

Tactic:
erw [← ENNReal.ofReal_mul zero_le_two]

Premises used: ENNReal.ofReal_mul, zero_le_two
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
ε : ℝ
x : AddCircle T
h : min T (2 * (2 * ε)) ≤ 2 * min T (2 * ε)
⊢ ENNReal.ofReal (min T (2 * (2 * ε))) ≤ ENNReal.ofReal (2 * min T (2 * ε))

Tactic:
apply ENNReal.ofReal_le_ofReal

Premises used: ENNReal.ofReal_le_ofReal
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
ε : ℝ
x : AddCircle T
h : min T (2 * (2 * ε)) ≤ min (2 * T) (2 * (2 * ε))
⊢ min T (2 * (2 * ε)) ≤ 2 * min T (2 * ε)

Tactic:
rw [mul_min_of_nonneg _ _ (zero_le_two : (0 : ℝ) ≤ 2)]

Premises used: mul_min_of_nonneg, zero_le_two
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
ε : ℝ
x : AddCircle T
linarith : 2 * T < T → 2 * T - T + (0 - T) = 0
⊢ T ≤ 2 * T

Tactic:
linarith [hT.out]

Premises used: Fact.out
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
ε : ℝ
x : AddCircle T
⊢ min T (2 * (2 * ε)) ≤ min (2 * T) (2 * (2 * ε))

Tactic:
exact min_le_min (by linarith [hT.out]) (le_refl _)

Premises used: le_refl, min_le_min
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
⊢ Measurable (α := AddCircle T) (β := (↑(Ioc a (a + T)) : Type))
    (⇑(measurableEquivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type))

Tactic:
have h := (measurableEquivIoc T a).measurable
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
h :
  Measurable (α := AddCircle T) (β := (↑(Ioc a (a + T)) : Type))
    (⇑(measurableEquivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type))
⊢ MeasurePreserving (α := AddCircle T) (β := (↑(Ioc a (a + T)) : Type))
    (⇑(equivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type)) volume
    (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc a (a + T))) volume)

Tactic:
⟨h, ?_⟩

Premises used: MeasureTheory.MeasurePreserving.mk
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
h :
  Measurable (α := AddCircle T) (β := (↑(Ioc a (a + T)) : Type))
    (⇑(measurableEquivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type))
refine :
  Eq (α := Measure (↑(Ioc a (a + T)) : Type))
    (Measure.map (α := AddCircle T) (⇑(equivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type)) volume)
    (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc a (a + T))) volume)
⊢ MeasurePreserving (α := AddCircle T) (β := (↑(Ioc a (a + T)) : Type))
    (⇑(equivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type)) volume
    (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc a (a + T))) volume)

Tactic:
refine ⟨h, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
h :
  Measurable (α := AddCircle T) (β := (↑(Ioc a (a + T)) : Type))
    (⇑(measurableEquivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type))
h₁ :
  ∀ (s : Set (↑(Ioc a (a + T)) : Type)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((Measure.map (α := AddCircle T) (⇑(equivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type)) volume :
            (a : Set (↑(Ioc a (a + T)) : Type)) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc a (a + T))) volume :
            (a : Set (↑(Ioc a (a + T)) : Type)) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ Eq (α := Measure (↑(Ioc a (a + T)) : Type))
    (Measure.map (α := AddCircle T) (⇑(equivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type)) volume)
    (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc a (a + T))) volume)

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
h :
  Measurable (α := AddCircle T) (β := (↑(Ioc a (a + T)) : Type))
    (⇑(measurableEquivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type))
s : Set (↑(Ioc a (a + T)) : Type)
hs : MeasurableSet s
⊢ Measurable (α := AddCircle T) (β := (↑(Ioc a (a + T)) : Type))
    (⇑(equivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type))

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
h :
  Measurable (α := AddCircle T) (β := (↑(Ioc a (a + T)) : Type))
    (⇑(measurableEquivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type))
s : Set (↑(Ioc a (a + T)) : Type)
hs : MeasurableSet s
⊢ MeasurableSet (α := AddCircle T) ((⇑(equivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type)) ⁻¹' s)

Tactic:
h hs
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
h :
  Measurable (α := AddCircle T) (β := (↑(Ioc a (a + T)) : Type))
    (⇑(measurableEquivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type))
s : Set (↑(Ioc a (a + T)) : Type)
hs : MeasurableSet s
⊢ MeasurableSet (α := AddCircle T) ((⇑(equivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type)) ⁻¹' s)

Tactic:
exact h hs
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
h :
  Measurable (α := AddCircle T) (β := (↑(Ioc a (a + T)) : Type))
    (⇑(measurableEquivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type))
s : Set (↑(Ioc a (a + T)) : Type)
hs : MeasurableSet s
h₁ :
  Eq (α := ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞)
        (preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples T)) QuotientAddGroup.mk
            ((⇑(equivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type)) ⁻¹' s) ∩
          Ioc a (a + T)) :
      ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc a (a + T)) '' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (α := AddCircle T) (⇑(equivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type)) volume :
          (a : Set (↑(Ioc a (a + T)) : Type)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc a (a + T))) volume :
          (a : Set (↑(Ioc a (a + T)) : Type)) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
rw [comap_apply _ Subtype.val_injective (fun _ ↦ measurableSet_Ioc.subtype_image) _ hs,
    map_apply (by measurability) hs, add_projection_respects_measure T a (by exact h hs)]

Premises used: Subtype.val_injective, MeasureTheory.Measure.map_apply, AddCircle.add_projection_respects_measure, MeasureTheory.Measure.comap_apply, MeasurableSet.subtype_image, measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
h :
  Measurable (α := AddCircle T) (β := (↑(Ioc a (a + T)) : Type))
    (⇑(measurableEquivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type))
s : Set (↑(Ioc a (a + T)) : Type)
hs : MeasurableSet s
h₁ :
  preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples T)) QuotientAddGroup.mk
        ((⇑(equivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type)) ⁻¹' s) ∩
      Ioc a (a + T) =
    Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc a (a + T)) '' s
⊢ Eq (α := ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞)
        (preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples T)) QuotientAddGroup.mk
            ((⇑(equivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type)) ⁻¹' s) ∩
          Ioc a (a + T)) :
      ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc a (a + T)) '' s) : ℝ≥0∞)

Tactic:
congr!
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
h :
  Measurable (α := AddCircle T) (β := (↑(Ioc a (a + T)) : Type))
    (⇑(measurableEquivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type))
s : Set (↑(Ioc a (a + T)) : Type)
hs : MeasurableSet s
h₁ :
  ∀ (x : ℝ),
    x ∈
        preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples T)) QuotientAddGroup.mk
            ((⇑(equivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type)) ⁻¹' s) ∩
          Ioc a (a + T) ↔
      x ∈ Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc a (a + T)) '' s
⊢ preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples T)) QuotientAddGroup.mk
        ((⇑(equivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type)) ⁻¹' s) ∩
      Ioc a (a + T) =
    Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc a (a + T)) '' s

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
h :
  Measurable (α := AddCircle T) (β := (↑(Ioc a (a + T)) : Type))
    (⇑(measurableEquivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type))
s : Set (↑(Ioc a (a + T)) : Type)
hs : MeasurableSet s
x : ℝ
h₁ :
  Membership.mem (α := (↑(Ioc a (a + T)) : Type)) s
        ((equivIoc T a : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type)) (↑x : ℝ ⧸ zmultiples T) :
          (↑(Ioc a (a + T)) : Type)) ∧
      x ∈ Ioc a (a + T) ↔
    ∃ (x_1 : x ∈ Ioc a (a + T)), Subtype.mk (p := fun (a_1 : ℝ) ↦ a_1 ∈ Ioc a (a + T)) x ⋯ ∈ s
⊢ x ∈
      preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples T)) QuotientAddGroup.mk
          ((⇑(equivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type)) ⁻¹' s) ∩
        Ioc a (a + T) ↔
    x ∈ Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc a (a + T)) '' s

Tactic:
simp only [mem_inter_iff, mem_preimage, mem_image, Subtype.exists, exists_and_right,
    exists_eq_right]

Premises used: Set.mem_inter_iff, Set.mem_image, Subtype.exists, exists_eq_right, exists_and_right, Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
h :
  Measurable (α := AddCircle T) (β := (↑(Ioc a (a + T)) : Type))
    (⇑(measurableEquivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type))
s : Set (↑(Ioc a (a + T)) : Type)
hs : MeasurableSet s
x : ℝ
h₁ :
  (∃ (_ : x ∈ Ioc a (a + T)),
      Membership.mem (α := (↑(Ioc a (a + T)) : Type)) s
        ((equivIoc T a : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type)) (↑x : ℝ ⧸ zmultiples T) :
          (↑(Ioc a (a + T)) : Type))) ↔
    ∃ (x_1 : x ∈ Ioc a (a + T)), Subtype.mk (p := fun (a_1 : ℝ) ↦ a_1 ∈ Ioc a (a + T)) x ⋯ ∈ s
⊢ Membership.mem (α := (↑(Ioc a (a + T)) : Type)) s
        ((equivIoc T a : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type)) (↑x : ℝ ⧸ zmultiples T) :
          (↑(Ioc a (a + T)) : Type)) ∧
      x ∈ Ioc a (a + T) ↔
    ∃ (x_1 : x ∈ Ioc a (a + T)), Subtype.mk (p := fun (a_1 : ℝ) ↦ a_1 ∈ Ioc a (a + T)) x ⋯ ∈ s

Tactic:
rw [and_comm, ← exists_prop]

Premises used: and_comm, exists_prop
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
h :
  Measurable (α := AddCircle T) (β := (↑(Ioc a (a + T)) : Type))
    (⇑(measurableEquivIoc T a) : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type))
s : Set (↑(Ioc a (a + T)) : Type)
hs : MeasurableSet s
x : ℝ
h₁ :
  ∀ (hx : x ∈ Ioc a (a + T)),
    (↑((equivIoc T a : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type)) (↑x : ℝ ⧸ zmultiples T)) : ℝ) = x
⊢ (∃ (_ : x ∈ Ioc a (a + T)),
      Membership.mem (α := (↑(Ioc a (a + T)) : Type)) s
        ((equivIoc T a : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type)) (↑x : ℝ ⧸ zmultiples T) :
          (↑(Ioc a (a + T)) : Type))) ↔
    ∃ (x_1 : x ∈ Ioc a (a + T)), Subtype.mk (p := fun (a_1 : ℝ) ↦ a_1 ∈ Ioc a (a + T)) x ⋯ ∈ s

Tactic:
congr! with hx