-- Mathlib/MeasureTheory/Integral/Periodic.lean
theorem integral_preimage (t : ℝ) (f : AddCircle T → E) :
    (∫ a in Ioc t (t + T), f a) = ∫ b : AddCircle T, f b

Proof state:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this : ∫ (y : AddCircle T), f y ∂Measure.map (fun x => ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x
⊢ ∫ (a : ℝ) in Ioc t (t + T), f ↑a = ∫ (b : AddCircle T), f b

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

Result:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this : ∫ (y : AddCircle T), f y ∂Measure.map (fun x => ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x
⊢ ∫ (y : AddCircle T), f y ∂Measure.map (fun x => ↑↑x) volume =
    ∫ (b : AddCircle T), f b ∂Measure.map QuotientAddGroup.mk (volume.restrict (Ioc t (t + T)))

Proof state:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
⊢ ∫ (a : ℝ) in Ioc t (t + T), f ↑a = ∫ (b : AddCircle T), f b

Tactic:
have m : MeasurableSet (Ioc t (t + T)) := measurableSet_Ioc

Result:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
⊢ ∫ (a : ℝ) in Ioc t (t + T), f ↑a = ∫ (b : AddCircle T), f b

Proof state:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
⊢ ∫ (a : ℝ) in Ioc t (t + T), f ↑a = ∫ (b : AddCircle T), f b

Tactic:
have := integral_map_equiv (μ := volume) (measurableEquivIoc T t).symm f

Result:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this :
  ∫ (y : AddCircle T), f y ∂Measure.map (⇑(measurableEquivIoc T t).symm) volume =
    ∫ (x : ↑(Ioc t (t + T))), f ((measurableEquivIoc T t).symm x)
⊢ ∫ (a : ℝ) in Ioc t (t + T), f ↑a = ∫ (b : AddCircle T), f b

Proof state:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this : ∫ (y : AddCircle T), f y ∂Measure.map (fun x => ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x
⊢ (fun x => ↑↑x) = QuotientAddGroup.mk ∘ Subtype.val

Tactic:
ext1 x

Result:
case h
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this : ∫ (y : AddCircle T), f y ∂Measure.map (fun x => ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x
x : ↑(Ioc t (t + T))
⊢ ↑↑x = (QuotientAddGroup.mk ∘ Subtype.val) x

Proof state:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this : ∫ (y : AddCircle T), f y ∂Measure.map (fun x => ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x
⊢ ∫ (y : AddCircle T), f y ∂Measure.map (fun x => ↑↑x) volume =
    ∫ (b : AddCircle T), f b ∂Measure.map QuotientAddGroup.mk (volume.restrict (Ioc t (t + T)))

Tactic:
have : ((↑) : Ioc t (t + T) → AddCircle T) = ((↑) : ℝ → AddCircle T) ∘ ((↑) : _ → ℝ) := by
  ext1 x; rfl

Result:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this✝ : ∫ (y : AddCircle T), f y ∂Measure.map (fun x => ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x
this : (fun x => ↑↑x) = QuotientAddGroup.mk ∘ Subtype.val
⊢ ∫ (y : AddCircle T), f y ∂Measure.map (fun x => ↑↑x) volume =
    ∫ (b : AddCircle T), f b ∂Measure.map QuotientAddGroup.mk (volume.restrict (Ioc t (t + T)))

Proof state:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this :
  ∫ (y : AddCircle T), f y ∂Measure.map (⇑(measurableEquivIoc T t).symm) volume =
    ∫ (x : ↑(Ioc t (t + T))), f ((measurableEquivIoc T t).symm x)
⊢ ∫ (a : ℝ) in Ioc t (t + T), f ↑a = ∫ (b : AddCircle T), f b

Tactic:
simp only [measurableEquivIoc, equivIoc, QuotientAddGroup.equivIocMod, MeasurableEquiv.symm_mk,
  MeasurableEquiv.coe_mk, Equiv.coe_fn_symm_mk] at this

Result:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this : ∫ (y : AddCircle T), f y ∂Measure.map (fun x => ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x
⊢ ∫ (a : ℝ) in Ioc t (t + T), f ↑a = ∫ (b : AddCircle T), f b

Proof state:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this✝ : ∫ (y : AddCircle T), f y ∂Measure.map (fun x => ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x
this : (fun x => ↑↑x) = QuotientAddGroup.mk ∘ Subtype.val
⊢ ∫ (y : AddCircle T), f y ∂Measure.map (QuotientAddGroup.mk ∘ Subtype.val) volume =
    ∫ (y : AddCircle T), f y ∂Measure.map QuotientAddGroup.mk (volume.restrict (Ioc t (t + T)))

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

Result:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this✝ : ∫ (y : AddCircle T), f y ∂Measure.map (fun x => ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x
this : (fun x => ↑↑x) = QuotientAddGroup.mk ∘ Subtype.val
⊢ ∫ (y : AddCircle T), f y ∂Measure.map QuotientAddGroup.mk (Measure.map Subtype.val volume) =
    ∫ (y : AddCircle T),
      f y ∂Measure.map QuotientAddGroup.mk (Measure.map Subtype.val (Measure.comap Subtype.val volume))

Proof state:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this✝ : ∫ (y : AddCircle T), f y ∂Measure.map (fun x => ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x
this : (fun x => ↑↑x) = QuotientAddGroup.mk ∘ Subtype.val
⊢ ∫ (y : AddCircle T), f y ∂Measure.map QuotientAddGroup.mk (Measure.map Subtype.val volume) =
    ∫ (y : AddCircle T),
      f y ∂Measure.map QuotientAddGroup.mk (Measure.map Subtype.val (Measure.comap Subtype.val volume))

Tactic:
rfl

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this✝ : ∫ (y : AddCircle T), f y ∂Measure.map (fun x => ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x
this : (fun x => ↑↑x) = QuotientAddGroup.mk ∘ Subtype.val
⊢ ∫ (y : AddCircle T), f y ∂Measure.map (fun x => ↑↑x) volume =
    ∫ (b : AddCircle T), f b ∂Measure.map QuotientAddGroup.mk (volume.restrict (Ioc t (t + T)))

Tactic:
simp_rw [this]

Result:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this✝ : ∫ (y : AddCircle T), f y ∂Measure.map (fun x => ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x
this : (fun x => ↑↑x) = QuotientAddGroup.mk ∘ Subtype.val
⊢ ∫ (y : AddCircle T), f y ∂Measure.map (QuotientAddGroup.mk ∘ Subtype.val) volume =
    ∫ (y : AddCircle T), f y ∂Measure.map QuotientAddGroup.mk (volume.restrict (Ioc t (t + T)))

Proof state:
case h
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this : ∫ (y : AddCircle T), f y ∂Measure.map (fun x => ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x
x : ↑(Ioc t (t + T))
⊢ ↑↑x = (QuotientAddGroup.mk ∘ Subtype.val) x

Tactic:
rfl

Result:
no goals