awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
m : MeasurableSet (Ioc t (t + T))
⊢ 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 this : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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.{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 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)
Tactic: rw [← (AddCircle.measurePreserving_mk T t).map_eq, ← integral_subtype m, ← this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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)))
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)
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.{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)
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)
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 (α := (↑(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)
have 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)
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 (goal)
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) (∫ (a : ℝ) in t..t + T, f (↑a : ℝ ⧸ zmultiples T))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (b : AddCircle T) ↦ f b)
have rw : t ≤ t + T
Tactic: rw [integral_of_le, AddCircle.integral_preimage T t f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
⊢ t ≤ t + T
have linarith : t + T < t → t + T - t + (0 - T) = 0
Tactic: linarith [hT.out]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
f : ℝ → E
⊢ 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)
have 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)
Tactic: rw [← AddCircle.intervalIntegral_preimage T t]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
f : ℝ → E
⊢ Eq.{u_1 + 1} (α := E) (∫ (a : ℝ) in t..t + T, liftIoc T t f (↑a : ℝ ⧸ zmultiples T)) (∫ (a : ℝ) in t..t + T, f a)
have h : ∀ᵐ (x : ℝ), x ∈ uIoc t (t + T) → liftIoc T t f (↑x : ℝ ⧸ zmultiples T) = f x
Tactic: apply intervalIntegral.integral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
have h : ∀ (x : ℝ) (hx : x ∈ uIoc t (t + T)), liftIoc T t f (↑x : ℝ ⧸ zmultiples T) = f x
Tactic: refine .of_forall fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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)
⊢ t ≤ t + T
have linarith : t + T < t → t + 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)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
f : ℝ → E
x : ℝ
hx : x ∈ uIoc t (t + T)
⊢ liftIoc T t f (↑x : ℝ ⧸ zmultiples T) = f x
have hx₁ : x ∈ Ioc t (t + T)
Tactic: rw [uIoc_of_le (by linarith [hT.out])] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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)
⊢ liftIoc T t f (↑x : ℝ ⧸ zmultiples T) = f x
have h : f x = f x
Tactic: rw [liftIoc_coe_apply hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : ℝ → ℂ
p : ℝ≥0∞
hLp : MemLp (m0 := MeasureSpace.toMeasurableSpace) f p (Measure.restrict volume (Ioc t (t + T)))
⊢ MemLp (α := AddCircle T) (m0 := MeasureSpace.toMeasurableSpace) (AddCircle.liftIoc T t f) p volume
have 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
Tactic: simp only [AddCircle.liftIoc, Set.restrict_def, Function.comp_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : ℝ → ℂ
p : ℝ≥0∞
hLp : MemLp (m0 := MeasureSpace.toMeasurableSpace) f p (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
have 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)))
Tactic: apply hLp.comp_measurePreserving
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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)))
have 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)
Tactic: refine .comp (measurePreserving_subtype_coe measurableSet_Ioc) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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₂ : ℝ
⊢ IntervalIntegrable f volume a₁ a₂
have 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₂
Tactic: wlog hT : 0 < T
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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₂
⊢ IntervalIntegrable f volume a₁ a₂
have 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₂
Tactic: wlog hT : 0 < T
Cleared hypotheses: t, h₁f, hT, h₂f, a₁, a₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
⊢ IntervalIntegrable f volume a₁ a₂
have inr : ∀ (h : T = 0), IntervalIntegrable f volume a₁ a₂
Tactic: rcases (not_lt.1 hT).eq_or_lt with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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₂
⊢ IntervalIntegrable f volume a₁ a₂
have inr₁ : ∀ (h : T < 0), IntervalIntegrable f volume a₁ a₂
Tactic: rcases (not_lt.1 hT).eq_or_lt with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (hypothesis)
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₂
have hnT : 0 < -T
Tactic: have hnT : 0 < -T := by aesop
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
⊢ IntervalIntegrable f volume a₁ a₂
have 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₂
Tactic: nth_rw 1 [(by ring : t = (t + T) + (-T))] at h₂f
Cleared hypotheses: h₂f, a₁, a₂, this, hT, h, hnT
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
⊢ IntervalIntegrable f volume a₁ a₂
have obtain : ∀ (n₁ : ℕ) (hn₁ : (t - min a₁ a₂) / T ≤ (↑n₁ : ℝ)), IntervalIntegrable f volume a₁ a₂
Tactic: obtain ⟨n₁, hn₁⟩ := exists_nat_ge ((t - min a₁ a₂) / T)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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₁ : ℝ)
⊢ IntervalIntegrable f volume a₁ a₂
have obtain : ∀ (n₂ : ℕ) (hn₂ : (max a₁ a₂ - t) / T ≤ (↑n₂ : ℝ)), IntervalIntegrable f volume a₁ a₂
Tactic: obtain ⟨n₂, hn₂⟩ := exists_nat_ge ((max a₁ a₂ - t) / T)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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)
have rw : min (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T) ≤ min a₁ a₂ ∧ max a₁ a₂ ≤ max (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
Tactic: rw [Set.uIcc_subset_uIcc_iff_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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) ≤ min a₁ a₂ ∧ max a₁ a₂ ≤ max (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
have left : min (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T) ≤ min a₁ a₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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₂
⊢ min (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T) ≤ min a₁ a₂ ∧ max a₁ a₂ ≤ max (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
have right : max a₁ a₂ ≤ max (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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 ≤ min a₁ a₂
have linarith : min a₁ a₂ < t - (↑n₁ : ℝ) * T → min a₁ a₂ - (t - (↑n₁ : ℝ) * T) + (t - min a₁ a₂ - (↑n₁ : ℝ) * T) = 0
Tactic: linarith [(div_le_iff₀ hT).1 hn₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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) ≤ min a₁ a₂
have calc : min (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T) ≤ t - (↑n₁ : ℝ) * T
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₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
⊢ min (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T) ≤ min a₁ a₂
have calc₁ : 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₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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₂ : ℝ)
⊢ max a₁ a₂ ≤ t + (↑n₂ : ℝ) * T
have linarith : t + (↑n₂ : ℝ) * T < max a₁ a₂ → t + (↑n₂ : ℝ) * T - max a₁ a₂ + (max a₁ a₂ - t - (↑n₂ : ℝ) * T) = 0
Tactic: linarith [(div_le_iff₀ hT).1 hn₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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₂ : ℝ)
⊢ max a₁ a₂ ≤ max (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
have calc : max a₁ a₂ ≤ 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
⊢ max a₁ a₂ ≤ max (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
have calc₁ : t + (↑n₂ : ℝ) * T ≤ 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