awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ
hx : x ∈ Ioc a (a + T)
h₁ h₂ : (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Ioc a (a + T)) x hx) : ℝ) = x
⊢ (↑((equivIoc T a : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type)) (↑x : ℝ ⧸ zmultiples T)) : ℝ) = x

Tactic:
rw [equivIoc_coe_eq hx]

Premises used: AddCircle.equivIoc_coe_eq
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
⊢ MeasurableSet (Ioc t (t + T))

Tactic:
have m : MeasurableSet (Ioc t (t + T)) := measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
⊢ ∫⁻ (a : AddCircle T),
      f
        a ∂Measure.map (α := (↑(Ioc t (t + T)) : Type))
        (⇑(measurableEquivIoc T t).symm : (a : (↑(Ioc t (t + T)) : Type)) → AddCircle T) volume =
    ∫⁻ (a : (↑(Ioc t (t + T)) : Type)),
      f (((measurableEquivIoc T t).symm : (a : (↑(Ioc t (t + T)) : Type)) → AddCircle T) a)

Tactic:
have := lintegral_map_equiv (μ := volume) f (measurableEquivIoc T t).symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this :
  ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)) volume =
    ∫⁻ (a : (↑(Ioc t (t + T)) : Type)), f (↑(↑a : ℝ) : ℝ ⧸ zmultiples T)
rw :
  ∫⁻ (a : ℝ) in Ioc t (t + T), f (↑a : ℝ ⧸ zmultiples T) =
    ∫⁻ (b : AddCircle T), f b ∂Measure.map QuotientAddGroup.mk (Measure.restrict volume (Ioc t (t + T)))
⊢ ∫⁻ (a : ℝ) in Ioc t (t + T), f (↑a : ℝ ⧸ zmultiples T) = ∫⁻ (b : AddCircle T), f b

Tactic:
rw [← (AddCircle.measurePreserving_mk T t).map_eq]

Premises used: MeasureTheory.MeasurePreserving.map_eq, AddCircle.measurePreserving_mk
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this :
  ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)) volume =
    ∫⁻ (a : (↑(Ioc t (t + T)) : Type)), f (↑(↑a : ℝ) : ℝ ⧸ zmultiples T)
⊢ ∫⁻ (a : (↑(Ioc t (t + T)) : Type)), f (↑(↑a : ℝ) : ℝ ⧸ zmultiples T) =
    ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)) volume

Tactic:
this.symm

Premises used: Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this :
  ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)) volume =
    ∫⁻ (a : (↑(Ioc t (t + T)) : Type)), f (↑(↑a : ℝ) : ℝ ⧸ zmultiples T)
h :
  ∫⁻ (a : ℝ) in Ioc t (t + T), f (↑a : ℝ ⧸ zmultiples T) =
    ∫⁻ (a : (↑(Ioc t (t + T)) : Type)), f (↑(↑a : ℝ) : ℝ ⧸ zmultiples T)
h₁ :
  ∫⁻ (b : AddCircle T), f b ∂Measure.map QuotientAddGroup.mk (Measure.restrict volume (Ioc t (t + T))) =
    ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)) volume
⊢ ∫⁻ (a : ℝ) in Ioc t (t + T), f (↑a : ℝ ⧸ zmultiples T) =
    ∫⁻ (b : AddCircle T), f b ∂Measure.map QuotientAddGroup.mk (Measure.restrict volume (Ioc t (t + T)))

Tactic:
convert! this.symm using 1

Premises used: Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this :
  ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)) volume =
    ∫⁻ (a : (↑(Ioc t (t + T)) : Type)), f (↑(↑a : ℝ) : ℝ ⧸ zmultiples T)
h :
  ∫⁻ (a : ℝ),
      f
        (↑a :
          ℝ ⧸
            zmultiples
              T) ∂Measure.map (α := { x : ℝ // x ∈ Ioc t (t + T) }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T)))
        (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T))) volume) =
    ∫⁻ (a : (↑(Ioc t (t + T)) : Type)), f (↑(↑a : ℝ) : ℝ ⧸ zmultiples T)
⊢ ∫⁻ (a : ℝ) in Ioc t (t + T), f (↑a : ℝ ⧸ zmultiples T) =
    ∫⁻ (a : (↑(Ioc t (t + T)) : Type)), f (↑(↑a : ℝ) : ℝ ⧸ zmultiples T)

Tactic:
rw [← map_comap_subtype_coe m _]

Premises used: map_comap_subtype_coe
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this :
  ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)) volume =
    ∫⁻ (a : (↑(Ioc t (t + T)) : Type)), f (↑(↑a : ℝ) : ℝ ⧸ zmultiples T)
⊢ ∫⁻ (a : ℝ),
      f
        (↑a :
          ℝ ⧸
            zmultiples
              T) ∂Measure.map (α := { x : ℝ // x ∈ Ioc t (t + T) }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T)))
        (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T))) volume) =
    ∫⁻ (a : (↑(Ioc t (t + T)) : Type)), f (↑(↑a : ℝ) : ℝ ⧸ zmultiples T)

Tactic:
MeasurableEmbedding.lintegral_map (MeasurableEmbedding.subtype_coe m) _

Premises used: MeasurableEmbedding.lintegral_map, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this :
  ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)) volume =
    ∫⁻ (a : (↑(Ioc t (t + T)) : Type)), f (↑(↑a : ℝ) : ℝ ⧸ zmultiples T)
⊢ ∫⁻ (a : ℝ),
      f
        (↑a :
          ℝ ⧸
            zmultiples
              T) ∂Measure.map (α := { x : ℝ // x ∈ Ioc t (t + T) }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T)))
        (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T))) volume) =
    ∫⁻ (a : (↑(Ioc t (t + T)) : Type)), f (↑(↑a : ℝ) : ℝ ⧸ zmultiples T)

Tactic:
exact MeasurableEmbedding.lintegral_map (MeasurableEmbedding.subtype_coe m) _

Premises used: MeasurableEmbedding.lintegral_map, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this :
  ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)) volume =
    ∫⁻ (a : (↑(Ioc t (t + T)) : Type)), f (↑(↑a : ℝ) : ℝ ⧸ zmultiples T)
h :
  Eq (α := Measure (AddCircle T)) (Measure.map QuotientAddGroup.mk (Measure.restrict volume (Ioc t (t + T))))
    (Measure.map (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)) volume)
⊢ ∫⁻ (b : AddCircle T), f b ∂Measure.map QuotientAddGroup.mk (Measure.restrict volume (Ioc t (t + T))) =
    ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)) volume

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this :
  ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)) volume =
    ∫⁻ (a : (↑(Ioc t (t + T)) : Type)), f (↑(↑a : ℝ) : ℝ ⧸ zmultiples T)
h :
  ∀ (x : (↑(Ioc t (t + T)) : Type)),
    Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples T)) (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)
      ((QuotientAddGroup.mk ∘ Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T))) x)
⊢ Eq (α := (x : (↑(Ioc t (t + T)) : Type)) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples T))
    (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T))
    (QuotientAddGroup.mk ∘ Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T)))

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this :
  ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)) volume =
    ∫⁻ (a : (↑(Ioc t (t + T)) : Type)), f (↑(↑a : ℝ) : ℝ ⧸ zmultiples T)
x : (↑(Ioc t (t + T)) : Type)
⊢ Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples T)) (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)
    ((QuotientAddGroup.mk ∘ Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T))) x)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this :
  ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)) volume =
    ∫⁻ (a : (↑(Ioc t (t + T)) : Type)), f (↑(↑a : ℝ) : ℝ ⧸ zmultiples T)
⊢ Eq (α := (x : (↑(Ioc t (t + T)) : Type)) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples T))
    (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T))
    (QuotientAddGroup.mk ∘ Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T)))

Tactic:
have : ((↑) : Ioc t (t + T) → AddCircle T) = ((↑) : ℝ → AddCircle T) ∘ ((↑) : _ → ℝ) := by
      ext1 x; rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this_1 :
  ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)) volume =
    ∫⁻ (a : (↑(Ioc t (t + T)) : Type)), f (↑(↑a : ℝ) : ℝ ⧸ zmultiples T)
this :
  Eq (α := (x : (↑(Ioc t (t + T)) : Type)) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples T))
    (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T))
    (QuotientAddGroup.mk ∘ Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T)))
h :
  Eq (α := Measure (AddCircle T))
    (Measure.map QuotientAddGroup.mk
      (Measure.map (α := { x : ℝ // x ∈ Ioc t (t + T) }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T)))
        (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T))) volume)))
    (Measure.map QuotientAddGroup.mk
      (Measure.map (α := { x : ℝ // x ∈ Ioc t (t + T) }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T))) volume))
⊢ Eq (α := Measure (AddCircle T)) (Measure.map QuotientAddGroup.mk (Measure.restrict volume (Ioc t (t + T))))
    (Measure.map (α := (↑(Ioc t (t + T)) : Type))
      (QuotientAddGroup.mk ∘ Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T))) volume)

Tactic:
rw [← map_map AddCircle.measurable_mk' measurable_subtype_coe, ← map_comap_subtype_coe m]

Premises used: measurable_subtype_coe, AddCircle.measurable_mk', map_comap_subtype_coe, MeasureTheory.Measure.map_map
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this_1 :
  ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)) volume =
    ∫⁻ (a : (↑(Ioc t (t + T)) : Type)), f (↑(↑a : ℝ) : ℝ ⧸ zmultiples T)
this :
  Eq (α := (x : (↑(Ioc t (t + T)) : Type)) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples T))
    (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T))
    (QuotientAddGroup.mk ∘ Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T)))
⊢ Eq (α := Measure (AddCircle T))
    (Measure.map QuotientAddGroup.mk
      (Measure.map (α := { x : ℝ // x ∈ Ioc t (t + T) }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T)))
        (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T))) volume)))
    (Measure.map QuotientAddGroup.mk
      (Measure.map (α := { x : ℝ // x ∈ Ioc t (t + T) }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T))) volume))

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
⊢ MeasurableSet (Ioc t (t + T))

Tactic:
have m : MeasurableSet (Ioc t (t + T)) := measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ (QuotientAddGroup.measurableSpace (zmultiples T))
      (Measure.map (α := (↑(Ioc t (t + T)) : Type))
        (⇑(measurableEquivIoc T t).symm : (a : (↑(Ioc t (t + T)) : Type)) → AddCircle T) volume)
      fun (y : AddCircle T) ↦ f y)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : (↑(Ioc t (t + T)) : Type)) ↦
      f (((measurableEquivIoc T t).symm : (a : (↑(Ioc t (t + T)) : Type)) → AddCircle T) x))

Tactic:
have := integral_map_equiv (μ := volume) (measurableEquivIoc T t).symm f
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ (QuotientAddGroup.measurableSpace (zmultiples T))
      (Measure.map (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)) volume)
      fun (y : AddCircle T) ↦ f y)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : (↑(Ioc t (t + T)) : Type)) ↦
      f (↑(↑x : ℝ) : ℝ ⧸ zmultiples T))
rw :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ (QuotientAddGroup.measurableSpace (zmultiples T))
      (Measure.map (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)) volume)
      fun (y : AddCircle T) ↦ f y)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.map QuotientAddGroup.mk (Measure.restrict volume (Ioc t (t + T)))) fun (b : AddCircle T) ↦ f b)
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc t (t + T))) fun (a : ℝ) ↦
      f (↑a : ℝ ⧸ zmultiples T))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (b : AddCircle T) ↦ f b)

Tactic:
rw [← (AddCircle.measurePreserving_mk T t).map_eq, ← integral_subtype m, ← this]

Premises used: MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.integral_subtype, AddCircle.measurePreserving_mk
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ (QuotientAddGroup.measurableSpace (zmultiples T))
      (Measure.map (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)) volume)
      fun (y : AddCircle T) ↦ f y)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : (↑(Ioc t (t + T)) : Type)) ↦
      f (↑(↑x : ℝ) : ℝ ⧸ zmultiples T))
h :
  ∀ (x : (↑(Ioc t (t + T)) : Type)),
    Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples T)) (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)
      ((QuotientAddGroup.mk ∘ Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T))) x)
⊢ Eq (α := (x : (↑(Ioc t (t + T)) : Type)) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples T))
    (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T))
    (QuotientAddGroup.mk ∘ Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T)))

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ (QuotientAddGroup.measurableSpace (zmultiples T))
      (Measure.map (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)) volume)
      fun (y : AddCircle T) ↦ f y)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : (↑(Ioc t (t + T)) : Type)) ↦
      f (↑(↑x : ℝ) : ℝ ⧸ zmultiples T))
x : (↑(Ioc t (t + T)) : Type)
⊢ Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples T)) (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)
    ((QuotientAddGroup.mk ∘ Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T))) x)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ (QuotientAddGroup.measurableSpace (zmultiples T))
      (Measure.map (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)) volume)
      fun (y : AddCircle T) ↦ f y)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : (↑(Ioc t (t + T)) : Type)) ↦
      f (↑(↑x : ℝ) : ℝ ⧸ zmultiples T))
⊢ Eq (α := (x : (↑(Ioc t (t + T)) : Type)) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples T))
    (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T))
    (QuotientAddGroup.mk ∘ Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T)))

Tactic:
have : ((↑) : Ioc t (t + T) → AddCircle T) = ((↑) : ℝ → AddCircle T) ∘ ((↑) : _ → ℝ) := by
    ext1 x; rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this_1 :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ (QuotientAddGroup.measurableSpace (zmultiples T))
      (Measure.map (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)) volume)
      fun (y : AddCircle T) ↦ f y)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : (↑(Ioc t (t + T)) : Type)) ↦
      f (↑(↑x : ℝ) : ℝ ⧸ zmultiples T))
this :
  Eq (α := (x : (↑(Ioc t (t + T)) : Type)) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples T))
    (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T))
    (QuotientAddGroup.mk ∘ Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T)))
rw :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ (QuotientAddGroup.measurableSpace (zmultiples T))
      (Measure.map QuotientAddGroup.mk
        (Measure.map (α := { x : ℝ // x ∈ Ioc t (t + T) }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T))) volume))
      fun (y : AddCircle T) ↦ f y)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.map QuotientAddGroup.mk
        (Measure.map (α := { x : ℝ // x ∈ Ioc t (t + T) }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T)))
          (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T))) volume)))
      fun (y : AddCircle T) ↦ f y)
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ (QuotientAddGroup.measurableSpace (zmultiples T))
      (Measure.map (α := (↑(Ioc t (t + T)) : Type))
        (QuotientAddGroup.mk ∘ Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T))) volume)
      fun (y : AddCircle T) ↦ f y)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.map QuotientAddGroup.mk (Measure.restrict volume (Ioc t (t + T)))) fun (y : AddCircle T) ↦ f y)

Tactic:
rw [← map_map AddCircle.measurable_mk' measurable_subtype_coe, ← map_comap_subtype_coe m]

Premises used: measurable_subtype_coe, AddCircle.measurable_mk', map_comap_subtype_coe, MeasureTheory.Measure.map_map
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this_1 :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ (QuotientAddGroup.measurableSpace (zmultiples T))
      (Measure.map (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T)) volume)
      fun (y : AddCircle T) ↦ f y)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : (↑(Ioc t (t + T)) : Type)) ↦
      f (↑(↑x : ℝ) : ℝ ⧸ zmultiples T))
this :
  Eq (α := (x : (↑(Ioc t (t + T)) : Type)) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples T))
    (fun (x : (↑(Ioc t (t + T)) : Type)) ↦ (↑(↑x : ℝ) : ℝ ⧸ zmultiples T))
    (QuotientAddGroup.mk ∘ Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T)))
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ (QuotientAddGroup.measurableSpace (zmultiples T))
      (Measure.map QuotientAddGroup.mk
        (Measure.map (α := { x : ℝ // x ∈ Ioc t (t + T) }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T))) volume))
      fun (y : AddCircle T) ↦ f y)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.map QuotientAddGroup.mk
        (Measure.map (α := { x : ℝ // x ∈ Ioc t (t + T) }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T)))
          (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T))) volume)))
      fun (y : AddCircle T) ↦ f y)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
rw : t ≤ t + T
⊢ Eq.{u_1 + 1} (α := E) (∫ (a : ℝ) in t..t + T, f (↑a : ℝ ⧸ zmultiples T))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (b : AddCircle T) ↦ f b)

Tactic:
rw [integral_of_le, AddCircle.integral_preimage T t f]

Premises used: intervalIntegral.integral_of_le, AddCircle.integral_preimage
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
linarith : t + T < t → t + T - t + (0 - T) = 0
⊢ t ≤ t + T

Tactic:
linarith [hT.out]

Premises used: Fact.out
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
f : ℝ → E
rw : Eq.{u_1 + 1} (α := E) (∫ (a : ℝ) in t..t + T, liftIoc T t f (↑a : ℝ ⧸ zmultiples T)) (∫ (a : ℝ) in t..t + T, f a)
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : AddCircle T) ↦ liftIoc T t f a)
    (∫ (a : ℝ) in t..t + T, f a)

Tactic:
rw [← AddCircle.intervalIntegral_preimage T t]

Premises used: AddCircle.intervalIntegral_preimage
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ uIoc t (t + T) → liftIoc T t f (↑x : ℝ ⧸ zmultiples T) = f x
⊢ Eq.{u_1 + 1} (α := E) (∫ (a : ℝ) in t..t + T, liftIoc T t f (↑a : ℝ ⧸ zmultiples T)) (∫ (a : ℝ) in t..t + T, f a)

Tactic:
apply intervalIntegral.integral_congr_ae

Premises used: intervalIntegral.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
f : ℝ → E
⊢ ∀ᵐ (x : ℝ), x ∈ uIoc t (t + T) → liftIoc T t f (↑x : ℝ ⧸ zmultiples T) = f x

Tactic:
.of_forall fun x hx ↦ ?_

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
f : ℝ → E
h : ∀ (x : ℝ) (hx : x ∈ uIoc t (t + T)), liftIoc T t f (↑x : ℝ ⧸ zmultiples T) = f x
⊢ ∀ᵐ (x : ℝ), x ∈ uIoc t (t + T) → liftIoc T t f (↑x : ℝ ⧸ zmultiples T) = f x

Tactic:
refine .of_forall fun x hx ↦ ?_
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
f : ℝ → E
x : ℝ
hx : x ∈ uIoc t (t + T)
linarith : t + T < t → t + T - t + (0 - T) = 0
⊢ t ≤ t + T

Tactic:
linarith [hT.out]

Premises used: Fact.out
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
f : ℝ → E
x : ℝ
hx : x ∈ uIoc t (t + T)
⊢ x ∈ Ioc t (t + T)

Tactic:
rw [uIoc_of_le (by linarith [hT.out])] at hx

Premises used: Set.uIoc_of_le