awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
⊢ 2 * ε ≤ T
have linarith₂ : T < 2 * ε → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
⊢ 2 * ε ≤ T
have linarith₃ : T < 2 * ε → 2 * ε - 1 * T + (T - 2 * ε) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
⊢ T ≤ 2 * ε
have linarith : 2 * ε < T → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
⊢ T ≤ 2 * ε
have linarith₁ : 2 * ε < T → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
⊢ T ≤ 2 * ε
have linarith₂ : 2 * ε < T → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
⊢ T ≤ 2 * ε
have linarith₃ : 2 * ε < T → 1 * T - 2 * ε + (2 * ε - T) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
⊢ IsUnifLocDoublingMeasure (α := AddCircle T) volume
have 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∞)
Tactic: refine ⟨⟨Real.toNNReal 2, Filter.Eventually.of_forall fun ε x => ?_⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
ε : ℝ
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∞)
have simp : ENNReal.ofReal (min T (2 * (2 * ε))) ≤ (↑(Real.toNNReal 2) : ℝ≥0∞) * ENNReal.ofReal (min T (2 * ε))
Tactic: simp only [volume_closedBall]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
ε : ℝ
x : AddCircle T
⊢ ENNReal.ofReal (min T (2 * (2 * ε))) ≤ (↑(Real.toNNReal 2) : ℝ≥0∞) * ENNReal.ofReal (min T (2 * ε))
have erw : ENNReal.ofReal (min T (2 * (2 * ε))) ≤ ENNReal.ofReal (2 * min T (2 * ε))
Tactic: erw [← ENNReal.ofReal_mul zero_le_two]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
ε : ℝ
x : AddCircle T
⊢ ENNReal.ofReal (min T (2 * (2 * ε))) ≤ ENNReal.ofReal (2 * min T (2 * ε))
have h : min T (2 * (2 * ε)) ≤ 2 * min T (2 * ε)
Tactic: apply ENNReal.ofReal_le_ofReal
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
ε : ℝ
x : AddCircle T
⊢ min T (2 * (2 * ε)) ≤ 2 * min T (2 * ε)
have h : min T (2 * (2 * ε)) ≤ min (2 * T) (2 * (2 * ε))
Tactic: rw [mul_min_of_nonneg _ _ (zero_le_two : (0 : ℝ) ≤ 2)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
ε : ℝ
x : AddCircle T
⊢ T ≤ 2 * T
have linarith : 2 * T < T → 2 * T - T + (0 - T) = 0
Tactic: linarith [hT.out]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
a : ℝ
⊢ 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)
have h : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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)
have 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)
Tactic: refine ⟨h, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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))
⊢ 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)
have 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∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
⊢ 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∞)
have 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∞)
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)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
⊢ 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∞)
have 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
Tactic: congr!
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
⊢ 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
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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 : ℝ
⊢ 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
have 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 sorry ∈ s
Tactic: simp only [mem_inter_iff, mem_preimage, mem_image, Subtype.exists, exists_and_right,
    exists_eq_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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 : ℝ
⊢ 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
have 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 sorry ∈ s
Tactic: rw [and_comm, ← exists_prop]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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 : ℝ
⊢ (∃ (_ : 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
have h₁ : ∀ (hx : x ∈ Ioc a (a + T)),
  (↑((equivIoc T a : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type)) (↑x : ℝ ⧸ zmultiples T)) : ℝ) = x
Tactic: congr! with hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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)
⊢ (↑((equivIoc T a : (a_1 : AddCircle T) → (↑(Ioc a (a + T)) : Type)) (↑x : ℝ ⧸ zmultiples T)) : ℝ) = x
have h₁ : (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Ioc a (a + T)) x hx) : ℝ) = x
Tactic: rw [equivIoc_coe_eq hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
⊢ ∫⁻ (a : ℝ) in Ioc t (t + T), f (↑a : ℝ ⧸ zmultiples T) = ∫⁻ (b : AddCircle T), f b
have m : MeasurableSet (Ioc t (t + T))
Tactic: have m : MeasurableSet (Ioc t (t + T)) := measurableSet_Ioc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
⊢ ∫⁻ (a : ℝ) in Ioc t (t + T), f (↑a : ℝ ⧸ zmultiples T) = ∫⁻ (b : AddCircle T), f b
have this : ∫⁻ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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 : ℝ) in Ioc t (t + T), f (↑a : ℝ ⧸ zmultiples T) = ∫⁻ (b : AddCircle T), f b
have 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)))
Tactic: rw [← (AddCircle.measurePreserving_mk T t).map_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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 : ℝ) 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)))
have h : ∫⁻ (a : ℝ) in Ioc t (t + T), f (↑a : ℝ ⧸ zmultiples T) =
  ∫⁻ (a : (↑(Ioc t (t + T)) : Type)), f (↑(↑a : ℝ) : ℝ ⧸ zmultiples T)
Tactic: convert! this.symm using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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)
⊢ ∫⁻ (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)))
have 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
Tactic: convert! this.symm using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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 : ℝ) in Ioc t (t + T), f (↑a : ℝ ⧸ zmultiples T) =
    ∫⁻ (a : (↑(Ioc t (t + T)) : Type)), f (↑(↑a : ℝ) : ℝ ⧸ zmultiples T)
have 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)
Tactic: rw [← map_comap_subtype_coe m _]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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)
⊢ ∫⁻ (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
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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)))
have 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)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (hypothesis)
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 (α := 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)
have 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)))
Tactic: have : ((↑) : Ioc t (t + T) → AddCircle T) = ((↑) : ℝ → AddCircle T) ∘ ((↑) : _ → ℝ) := by
      ext1 x; rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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.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)
have 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))
Tactic: rw [← map_map AddCircle.measurable_mk' measurable_subtype_coe, ← map_comap_subtype_coe m]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
⊢ 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)
have m : MeasurableSet (Ioc t (t + T))
Tactic: have m : MeasurableSet (Ioc t (t + T)) := measurableSet_Ioc