awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ∈ Ioc t (t + T)
h h₁ : f x = f x
⊢ liftIoc T t f (↑x : ℝ ⧸ zmultiples T) = f x

Tactic:
rw [liftIoc_coe_apply hx]

Premises used: AddCircle.liftIoc_coe_apply
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : ℝ → ℂ
p : ℝ≥0∞
hLp : MemLp (m0 := MeasureSpace.toMeasurableSpace) f p (Measure.restrict volume (Ioc t (t + T)))
simp :
  MemLp (ε := ℂ) (m0 := MeasureSpace.toMeasurableSpace)
    (fun (x : AddCircle T) ↦ f (↑((AddCircle.equivIoc T t : (a : AddCircle T) → (↑(Ioc t (t + T)) : Type)) x) : ℝ)) p
    volume
⊢ MemLp (α := AddCircle T) (m0 := MeasureSpace.toMeasurableSpace) (AddCircle.liftIoc T t f) p volume

Tactic:
simp only [AddCircle.liftIoc, Set.restrict_def, Function.comp_def]

Premises used: Set.restrict_def, AddCircle.liftIoc, Function.comp_def
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : ℝ → ℂ
p : ℝ≥0∞
hLp : MemLp (m0 := MeasureSpace.toMeasurableSpace) f p (Measure.restrict volume (Ioc t (t + T)))
apply :
  MeasurePreserving
    (fun (x : AddCircle T) ↦ (↑((AddCircle.equivIoc T t : (a : AddCircle T) → (↑(Ioc t (t + T)) : Type)) x) : ℝ)) volume
    (Measure.restrict volume (Ioc t (t + T)))
⊢ MemLp (ε := ℂ) (m0 := MeasureSpace.toMeasurableSpace)
    (fun (x : AddCircle T) ↦ f (↑((AddCircle.equivIoc T t : (a : AddCircle T) → (↑(Ioc t (t + T)) : Type)) x) : ℝ)) p
    volume

Tactic:
apply hLp.comp_measurePreserving

Premises used: MeasureTheory.MemLp.comp_measurePreserving
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : ℝ → ℂ
p : ℝ≥0∞
hLp : MemLp (m0 := MeasureSpace.toMeasurableSpace) f p (Measure.restrict volume (Ioc t (t + T)))
⊢ MeasurePreserving
    (fun (x : AddCircle T) ↦ (↑((AddCircle.equivIoc T t : (a : AddCircle T) → (↑(Ioc t (t + T)) : Type)) x) : ℝ)) volume
    (Measure.restrict volume (Ioc t (t + T)))

Tactic:
.comp (measurePreserving_subtype_coe measurableSet_Ioc) ?_

Premises used: MeasureTheory.measurePreserving_subtype_coe, MeasureTheory.MeasurePreserving.comp, measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : ℝ → ℂ
p : ℝ≥0∞
hLp : MemLp (m0 := MeasureSpace.toMeasurableSpace) f p (Measure.restrict volume (Ioc t (t + T)))
refine :
  MeasurePreserving (α := AddCircle T) (β := (↑(Ioc t (t + T)) : Type))
    (⇑(AddCircle.equivIoc T t) : (a : AddCircle T) → (↑(Ioc t (t + T)) : Type)) volume
    (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T))) volume)
⊢ MeasurePreserving
    (fun (x : AddCircle T) ↦ (↑((AddCircle.equivIoc T t : (a : AddCircle T) → (↑(Ioc t (t + T)) : Type)) x) : ℝ)) volume
    (Measure.restrict volume (Ioc t (t + T)))

Tactic:
refine .comp (measurePreserving_subtype_coe measurableSet_Ioc) ?_
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : ℝ → ℂ
p : ℝ≥0∞
hLp : MemLp (m0 := MeasureSpace.toMeasurableSpace) f p (Measure.restrict volume (Ioc t (t + T)))
⊢ MeasurePreserving (α := AddCircle T) (β := (↑(Ioc t (t + T)) : Type))
    (⇑(AddCircle.equivIoc T t) : (a : AddCircle T) → (↑(Ioc t (t + T)) : Type)) volume
    (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T))) volume)

Tactic:
AddCircle.measurePreserving_equivIoc T

Premises used: AddCircle.measurePreserving_equivIoc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : ℝ → ℂ
p : ℝ≥0∞
hLp : MemLp (m0 := MeasureSpace.toMeasurableSpace) f p (Measure.restrict volume (Ioc t (t + T)))
⊢ MeasurePreserving (α := AddCircle T) (β := (↑(Ioc t (t + T)) : Type))
    (⇑(AddCircle.equivIoc T t) : (a : AddCircle T) → (↑(Ioc t (t + T)) : Type)) volume
    (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioc t (t + T))) volume)

Tactic:
exact AddCircle.measurePreserving_equivIoc T

Premises used: AddCircle.measurePreserving_equivIoc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set UnitAddCircle) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
t : ℝ
⊢ MeasurePreserving (β := UnitAddCircle) QuotientAddGroup.mk (Measure.restrict volume (Ioc t (t + 1))) volume

Tactic:
AddCircle.measurePreserving_mk 1 t

Premises used: AddCircle.measurePreserving_mk, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
t : ℝ
f : UnitAddCircle → ℝ≥0∞
⊢ ∫⁻ (a : ℝ) in Ioc t (t + 1), f (↑a : ℝ ⧸ zmultiples 1) = ∫⁻ (b : UnitAddCircle), f b

Tactic:
AddCircle.lintegral_preimage 1 t f

Premises used: AddCircle.lintegral_preimage, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
f : UnitAddCircle → E
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc t (t + 1))) fun (a : ℝ) ↦
      f (↑a : ℝ ⧸ zmultiples 1))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (b : UnitAddCircle) ↦ f b)

Tactic:
AddCircle.integral_preimage 1 t f

Premises used: OfNat.ofNat, AddCircle.integral_preimage
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
f : UnitAddCircle → E
⊢ Eq.{u_1 + 1} (α := E) (∫ (a : ℝ) in t..t + 1, f (↑a : ℝ ⧸ zmultiples 1))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (b : UnitAddCircle) ↦ f b)

Tactic:
AddCircle.intervalIntegral_preimage 1 t f

Premises used: AddCircle.intervalIntegral_preimage, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
inr :
  ∀
    (this :
      ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T t : ℝ} (h₁f : Periodic f T) (hT : T ≠ 0)
        (h₂f : IntervalIntegrable f volume t (t + T)) (a₁ a₂ : ℝ) (hT : 0 < T), IntervalIntegrable f volume a₁ a₂)
    (hT : ¬0 < T), IntervalIntegrable f volume a₁ a₂
wlog :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T t : ℝ} (h₁f : Periodic f T) (hT : T ≠ 0)
    (h₂f : IntervalIntegrable f volume t (t + T)) (a₁ a₂ : ℝ) (hT : 0 < T), IntervalIntegrable f volume a₁ a₂
⊢ IntervalIntegrable f volume a₁ a₂

Tactic:
wlog hT : 0 < T
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T t : ℝ} (h₁f : Periodic f T) (hT : T ≠ 0)
    (h₂f : IntervalIntegrable f volume t (t + T)) (a₁ a₂ : ℝ) (hT : 0 < T), IntervalIntegrable f volume a₁ a₂
hT : ¬0 < T
inr : ∀ (h : T = 0), IntervalIntegrable f volume a₁ a₂
inr₁ : ∀ (h : T < 0), IntervalIntegrable f volume a₁ a₂
⊢ IntervalIntegrable f volume a₁ a₂

Tactic:
rcases (not_lt.1 hT).eq_or_lt with h | h

Premises used: LE.le.eq_or_lt, not_lt, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T t : ℝ} (h₁f : Periodic f T) (hT : T ≠ 0)
    (h₂f : IntervalIntegrable f volume t (t + T)) (a₁ a₂ : ℝ) (hT : 0 < T), IntervalIntegrable f volume a₁ a₂
hT : ¬0 < T
h : T = 0
⊢ IntervalIntegrable f volume a₁ a₂

Tactic:
tauto
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T t : ℝ} (h₁f : Periodic f T) (hT : T ≠ 0)
    (h₂f : IntervalIntegrable f volume t (t + T)) (a₁ a₂ : ℝ) (hT : 0 < T), IntervalIntegrable f volume a₁ a₂
hT : ¬0 < T
h : T < 0
⊢ 0 < -T

Tactic:
aesop
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T t : ℝ} (h₁f : Periodic f T) (hT : T ≠ 0)
    (h₂f : IntervalIntegrable f volume t (t + T)) (a₁ a₂ : ℝ) (hT : 0 < T), IntervalIntegrable f volume a₁ a₂
hT : ¬0 < T
h : T < 0
⊢ 0 < -T

Tactic:
have hnT : 0 < -T := by aesop
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T t : ℝ} (h₁f : Periodic f T) (hT : T ≠ 0)
    (h₂f : IntervalIntegrable f volume t (t + T)) (a₁ a₂ : ℝ) (hT : 0 < T), IntervalIntegrable f volume a₁ a₂
hT : ¬0 < T
h : T < 0
hnT : 0 < -T
⊢ t = t + T + -T

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T t : ℝ} (h₁f : Periodic f T) (hT : T ≠ 0)
    (h₂f : IntervalIntegrable f volume t (t + T)) (a₁ a₂ : ℝ) (hT : 0 < T), IntervalIntegrable f volume a₁ a₂
hT : ¬0 < T
h : T < 0
hnT : 0 < -T
inr :
  ∀ (h₂f : IntervalIntegrable f volume (t + T + -T) (t + T)) (a₁ a₂ : ℝ)
    (this :
      ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T t : ℝ} (h₁f : Periodic f T) (hT : T ≠ 0)
        (h₂f : IntervalIntegrable f volume t (t + T)) (a₁ a₂ : ℝ) (hT : 0 < T), IntervalIntegrable f volume a₁ a₂)
    (hT : ¬0 < T) (h : T < 0) (hnT : 0 < -T), IntervalIntegrable f volume a₁ a₂
⊢ IntervalIntegrable f volume a₁ a₂

Tactic:
nth_rw 1 [(by ring : t = (t + T) + (-T))] at h₂f
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume (t + T + -T) (t + T)
a₁ a₂ : ℝ
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T t : ℝ} (h₁f : Periodic f T) (hT : T ≠ 0)
    (h₂f : IntervalIntegrable f volume t (t + T)) (a₁ a₂ : ℝ) (hT : 0 < T), IntervalIntegrable f volume a₁ a₂
hT : ¬0 < T
h : T < 0
hnT : 0 < -T
⊢ IntervalIntegrable f volume a₁ a₂

Tactic:
apply this h₁f.neg hnT.ne' h₂f.symm _ _ hnT

Premises used: Function.Periodic.neg, LT.lt.ne', IntervalIntegrable.symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
E : Type u_1
inst_1 : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
obtain : ∀ (n₁ : ℕ) (hn₁ : (t - min a₁ a₂) / T ≤ (↑n₁ : ℝ)), IntervalIntegrable f volume a₁ a₂
⊢ IntervalIntegrable f volume a₁ a₂

Tactic:
obtain ⟨n₁, hn₁⟩ := exists_nat_ge ((t - min a₁ a₂) / T)

Premises used: HSub.hSub, exists_nat_ge, HDiv.hDiv, Min.min
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
E : Type u_1
inst_1 : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ (↑n₁ : ℝ)
obtain : ∀ (n₂ : ℕ) (hn₂ : (max a₁ a₂ - t) / T ≤ (↑n₂ : ℝ)), IntervalIntegrable f volume a₁ a₂
⊢ IntervalIntegrable f volume a₁ a₂

Tactic:
obtain ⟨n₂, hn₂⟩ := exists_nat_ge ((max a₁ a₂ - t) / T)

Premises used: HSub.hSub, exists_nat_ge, HDiv.hDiv, Max.max
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
E : Type u_1
inst_1 : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ (↑n₁ : ℝ)
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ (↑n₂ : ℝ)
rw : min (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T) ≤ min a₁ a₂ ∧ max a₁ a₂ ≤ max (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
⊢ uIcc a₁ a₂ ⊆ uIcc (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)

Tactic:
rw [Set.uIcc_subset_uIcc_iff_le]

Premises used: Set.uIcc_subset_uIcc_iff_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
E : Type u_1
inst_1 : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ (↑n₁ : ℝ)
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ (↑n₂ : ℝ)
left : min (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T) ≤ min a₁ a₂
right : max a₁ a₂ ≤ max (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
⊢ min (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T) ≤ min a₁ a₂ ∧ max a₁ a₂ ≤ max (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
E : Type u_1
inst_1 : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ (↑n₁ : ℝ)
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ (↑n₂ : ℝ)
⊢ min (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T) ≤ t - (↑n₁ : ℝ) * T

Tactic:
apply min_le_left

Premises used: min_le_left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
E : Type u_1
inst_1 : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ (↑n₁ : ℝ)
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ (↑n₂ : ℝ)
linarith : min a₁ a₂ < t - (↑n₁ : ℝ) * T → min a₁ a₂ - (t - (↑n₁ : ℝ) * T) + (t - min a₁ a₂ - (↑n₁ : ℝ) * T) = 0
⊢ t - (↑n₁ : ℝ) * T ≤ min a₁ a₂

Tactic:
linarith [(div_le_iff₀ hT).1 hn₁]

Premises used: div_le_iff₀, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
E : Type u_1
inst_1 : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ (↑n₁ : ℝ)
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ (↑n₂ : ℝ)
calc : min (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T) ≤ t - (↑n₁ : ℝ) * T
calc₁ : t - (↑n₁ : ℝ) * T ≤ min a₁ a₂
⊢ min (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T) ≤ min a₁ a₂

Tactic:
calc min (t - n₁ * T) (t + n₂ * T)
      _ ≤ (t - n₁ * T) := by apply min_le_left
      _ ≤ min a₁ a₂ := by linarith [(div_le_iff₀ hT).1 hn₁]

Premises used: HMul.hMul, HSub.hSub, Nat.cast, HAdd.hAdd, Min.min
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
E : Type u_1
inst_1 : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ (↑n₁ : ℝ)
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ (↑n₂ : ℝ)
linarith : t + (↑n₂ : ℝ) * T < max a₁ a₂ → t + (↑n₂ : ℝ) * T - max a₁ a₂ + (max a₁ a₂ - t - (↑n₂ : ℝ) * T) = 0
⊢ max a₁ a₂ ≤ t + (↑n₂ : ℝ) * T

Tactic:
linarith [(div_le_iff₀ hT).1 hn₂]

Premises used: div_le_iff₀, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
E : Type u_1
inst_1 : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ (↑n₁ : ℝ)
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ (↑n₂ : ℝ)
⊢ t + (↑n₂ : ℝ) * T ≤ max (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)

Tactic:
apply le_max_right

Premises used: le_max_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
E : Type u_1
inst_1 : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ (↑n₁ : ℝ)
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ (↑n₂ : ℝ)
calc : max a₁ a₂ ≤ t + (↑n₂ : ℝ) * T
calc₁ : t + (↑n₂ : ℝ) * T ≤ max (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
⊢ max a₁ a₂ ≤ max (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)

Tactic:
calc max a₁ a₂
      _ ≤ t + n₂ * T := by linarith [(div_le_iff₀ hT).1 hn₂]
      _ ≤ max (t - n₁ * T) (t + n₂ * T) := by apply le_max_right

Premises used: HMul.hMul, HSub.hSub, Nat.cast, HAdd.hAdd, Max.max
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
E : Type u_1
inst_1 : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ (↑n₁ : ℝ)
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ (↑n₂ : ℝ)
⊢ uIcc a₁ a₂ ⊆ uIcc (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)

Tactic:
have : Set.uIcc a₁ a₂ ⊆ Set.uIcc (t - n₁ * T) (t + n₂ * T) := by
    rw [Set.uIcc_subset_uIcc_iff_le]
    constructor
    · calc min (t - n₁ * T) (t + n₂ * T)
      _ ≤ (t - n₁ * T) := by apply min_le_left
      _ ≤ min a₁ a₂ := by linarith [(div_le_iff₀ hT).1 hn₁]
    · calc max a₁ a₂
      _ ≤ t + n₂ * T := by linarith [(div_le_iff₀ hT).1 hn₂]
      _ ≤ max (t - n₁ * T) (t + n₂ * T) := by apply le_max_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
E : Type u_1
inst_1 : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ (↑n₁ : ℝ)
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ (↑n₂ : ℝ)
this : uIcc a₁ a₂ ⊆ uIcc (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
apply : IntervalIntegrable f volume (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
⊢ IntervalIntegrable f volume a₁ a₂

Tactic:
apply IntervalIntegrable.mono_set _ this

Premises used: IntervalIntegrable.mono_set
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
E : Type u_1
inst_1 : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ (↑n₁ : ℝ)
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ (↑n₂ : ℝ)
this : uIcc a₁ a₂ ⊆ uIcc (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
a : ℕ → ℝ := fun (n : ℕ) ↦ t + HSub.hSub (α := ℝ) (↑n : ℝ) (↑n₁ : ℝ) * T
⊢ t - (↑n₁ : ℝ) * T = a 0

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
E : Type u_1
inst_1 : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ (↑n₁ : ℝ)
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ (↑n₂ : ℝ)
this : uIcc a₁ a₂ ⊆ uIcc (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
a : ℕ → ℝ := fun (n : ℕ) ↦ t + HSub.hSub (α := ℝ) (↑n : ℝ) (↑n₁ : ℝ) * T
⊢ t + (↑n₂ : ℝ) * T = a (n₁ + n₂)

Tactic:
simp [a]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
E : Type u_1
inst_1 : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ (↑n₁ : ℝ)
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ (↑n₂ : ℝ)
this : uIcc a₁ a₂ ⊆ uIcc (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
a : ℕ → ℝ := fun (n : ℕ) ↦ t + HSub.hSub (α := ℝ) (↑n : ℝ) (↑n₁ : ℝ) * T
rw : IntervalIntegrable f volume (a 0) (a (n₁ + n₂))
⊢ IntervalIntegrable f volume (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)

Tactic:
rw [(by ring : t - n₁ * T = a 0), (by simp [a] : t + n₂ * T = a (n₁ + n₂))]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
E : Type u_1
inst_1 : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ (↑n₁ : ℝ)
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ (↑n₂ : ℝ)
this : uIcc a₁ a₂ ⊆ uIcc (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
a : ℕ → ℝ := fun (n : ℕ) ↦ t + HSub.hSub (α := ℝ) (↑n : ℝ) (↑n₁ : ℝ) * T
hint : ∀ k < n₁ + n₂, IntervalIntegrable f volume (a k) (a (k + 1))
⊢ IntervalIntegrable f volume (a 0) (a (n₁ + n₂))

Tactic:
apply IntervalIntegrable.trans_iterate

Premises used: IntervalIntegrable.trans_iterate
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
E : Type u_1
inst_1 : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ (↑n₁ : ℝ)
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ (↑n₂ : ℝ)
this : uIcc a₁ a₂ ⊆ uIcc (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
a : ℕ → ℝ := fun (n : ℕ) ↦ t + HSub.hSub (α := ℝ) (↑n : ℝ) (↑n₁ : ℝ) * T
k : ℕ
hk : k < n₁ + n₂
⊢ ‖f (min t (t + T))‖ₑ ≠ ∞

Tactic:
aesop
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
E : Type u_1
inst_1 : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ (↑n₁ : ℝ)
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ (↑n₂ : ℝ)
this : uIcc a₁ a₂ ⊆ uIcc (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
a : ℕ → ℝ := fun (n : ℕ) ↦ t + HSub.hSub (α := ℝ) (↑n : ℝ) (↑n₁ : ℝ) * T
k : ℕ
hk : k < n₁ + n₂
h : f = fun (x : ℝ) ↦ f (x - HSub.hSub (α := ℝ) (↑k : ℝ) (↑n₁ : ℝ) * T)
h₁ : a (k + 1) = t + T + HSub.hSub (α := ℝ) (↑k : ℝ) (↑n₁ : ℝ) * T
⊢ IntervalIntegrable f volume (a k) (a (k + 1))

Tactic:
convert! (IntervalIntegrable.comp_sub_right h₂f ((k - n₁) * T) (by aesop)) using 1

Premises used: HMul.hMul, IntervalIntegrable.comp_sub_right, HSub.hSub, Nat.cast
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
E : Type u_1
inst_1 : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ (↑n₁ : ℝ)
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ (↑n₂ : ℝ)
this : uIcc a₁ a₂ ⊆ uIcc (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
a : ℕ → ℝ := fun (n : ℕ) ↦ t + HSub.hSub (α := ℝ) (↑n : ℝ) (↑n₁ : ℝ) * T
k : ℕ
hk : k < n₁ + n₂
h : ∀ (x : ℝ), f x = f (x - HSub.hSub (α := ℝ) (↑k : ℝ) (↑n₁ : ℝ) * T)
⊢ f = fun (x : ℝ) ↦ f (x - HSub.hSub (α := ℝ) (↑k : ℝ) (↑n₁ : ℝ) * T)

Tactic:
funext x
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
E : Type u_1
inst_1 : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT_1 : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ (↑n₁ : ℝ)
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ (↑n₂ : ℝ)
this : uIcc a₁ a₂ ⊆ uIcc (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
a : ℕ → ℝ := fun (n : ℕ) ↦ t + HSub.hSub (α := ℝ) (↑n : ℝ) (↑n₁ : ℝ) * T
k : ℕ
hk : k < n₁ + n₂
x : ℝ
⊢ f x = f (x - HSub.hSub (α := ℝ) (↑k : ℝ) (↑n₁ : ℝ) * T)

Tactic:
simpa using (h₁f.sub_int_mul_eq (k - n₁)).symm

Premises used: HSub.hSub, Function.Periodic.sub_int_mul_eq, Nat.cast, Eq.symm