awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : t + (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - (↑n₁ : ℝ)) * T = t + T + HSub.hSub (α := ℝ) (↑k : ℝ) (↑n₁ : ℝ) * T
⊢ a (k + 1) = t + T + HSub.hSub (α := ℝ) (↑k : ℝ) (↑n₁ : ℝ) * T

Tactic:
simp [a, Nat.cast_add]

Premises used: Nat.cast_add
-- 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₂
⊢ t + (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - (↑n₁ : ℝ)) * T = t + T + HSub.hSub (α := ℝ) (↑k : ℝ) (↑n₁ : ℝ) * T

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

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

Tactic:
simp_all
-- 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₁ t₂ : ℝ
hf : Periodic f T
hT : T ≠ 0
⊢ IntervalIntegrable f volume t₁ (t₁ + T) ↔ IntervalIntegrable f volume t₂ (t₂ + T)

Tactic:
⟨(hf.intervalIntegrable hT · t₂ (t₂ + T)), (hf.intervalIntegrable hT · t₁ (t₁ + T))⟩

Premises used: Function.Periodic.intervalIntegrable, HAdd.hAdd, Iff.intro
-- 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₁ t₂ : ℝ
hf : Periodic f T
hT : T ≠ 0
⊢ IntervalIntegrable f volume t₁ (t₁ + T) ↔ IntervalIntegrable f volume t₂ (t₂ + T)

Tactic:
exact ⟨(hf.intervalIntegrable hT · t₂ (t₂ + T)), (hf.intervalIntegrable hT · t₁ (t₁ + T))⟩
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
h₁f : Periodic f T
hT : T ≠ 0
h₂f : IntervalIntegrable f volume 0 T
a₁ a₂ : ℝ
h₂f₁ : IntervalIntegrable f volume 0 (0 + T)
⊢ IntervalIntegrable f volume a₁ a₂

Tactic:
apply h₁f.intervalIntegrable hT (t := 0)

Premises used: Function.Periodic.intervalIntegrable
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
h₁f : Periodic f T
hT : T ≠ 0
h₂f : IntervalIntegrable f volume 0 T
a₁ a₂ : ℝ
⊢ IntervalIntegrable f volume 0 (0 + T)

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
inr :
  ∀
    (this :
      ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T : ℝ} [inst_2 : NormedSpace ℝ E] (hf : Periodic f T)
        (t s : ℝ) (hT : 0 < T), Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t..t + T, f x) (∫ (x : ℝ) in s..s + T, f x))
    (hT : ¬0 < T), Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t..t + T, f x) (∫ (x : ℝ) in s..s + T, f x)
wlog :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T : ℝ} [inst_2 : NormedSpace ℝ E] (hf : Periodic f T)
    (t s : ℝ) (hT : 0 < T), Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t..t + T, f x) (∫ (x : ℝ) in s..s + T, f x)
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t..t + T, f x) (∫ (x : ℝ) in s..s + T, f x)

Tactic:
wlog hT : 0 < T
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T : ℝ} [inst_2 : NormedSpace ℝ E] (hf : Periodic f T)
    (t s : ℝ) (hT : 0 < T), Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t..t + T, f x) (∫ (x : ℝ) in s..s + T, f x)
hT : ¬0 < T
inr : ∀ (hT : T = 0), Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t..t + T, f x) (∫ (x : ℝ) in s..s + T, f x)
inr₁ : ∀ (hT : T < 0), Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t..t + T, f x) (∫ (x : ℝ) in s..s + T, f x)
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t..t + T, f x) (∫ (x : ℝ) in s..s + T, f x)

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

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 : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T : ℝ} [inst_2 : NormedSpace ℝ E] (hf : Periodic f T)
    (t s : ℝ) (hT : 0 < T), Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t..t + T, f x) (∫ (x : ℝ) in s..s + T, f x)
hT_1 : ¬0 < T
hT : T = 0
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t..t + T, f x) (∫ (x : ℝ) in s..s + T, f x)

Tactic:
aesop
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T : ℝ} [inst_2 : NormedSpace ℝ E] (hf : Periodic f T)
    (t s : ℝ) (hT : 0 < T), Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t..t + T, f x) (∫ (x : ℝ) in s..s + T, f x)
hT_1 : ¬0 < T
hT : T < 0
inr : Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t + T..t, f x) (∫ (x : ℝ) in s + T..s, f x)
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t..t + T, f x) (∫ (x : ℝ) in s..s + T, f x)

Tactic:
rw [← neg_inj, ← integral_symm, ← integral_symm]

Premises used: intervalIntegral.integral_symm, neg_inj
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T : ℝ} [inst_2 : NormedSpace ℝ E] (hf : Periodic f T)
    (t s : ℝ) (hT : 0 < T), Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t..t + T, f x) (∫ (x : ℝ) in s..s + T, f x)
hT_1 : ¬0 < T
hT : T < 0
⊢ 0 < -T

Tactic:
aesop
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T : ℝ} [inst_2 : NormedSpace ℝ E] (hf : Periodic f T)
    (t s : ℝ) (hT : 0 < T), Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t..t + T, f x) (∫ (x : ℝ) in s..s + T, f x)
hT_1 : ¬0 < T
hT : T < 0
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t + T..t, f x) (∫ (x : ℝ) in s + T..s, f x)

Tactic:
simpa only [← sub_eq_add_neg, add_sub_cancel_right] using
        this hf.neg (t + T) (s + T) (by aesop : 0 < -T)

Premises used: sub_eq_add_neg, Function.Periodic.neg, HAdd.hAdd, add_sub_cancel_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
inst_1 : NormedSpace ℝ E_1
E : Type u_1
inst_2 : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_3 : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
hT : 0 < T
simp :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc t (t + T))) fun (x : ℝ) ↦ f x)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc s (s + T))) fun (x : ℝ) ↦ f x)
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t..t + T, f x) (∫ (x : ℝ) in s..s + T, f x)

Tactic:
simp only [integral_of_le, hT.le, le_add_iff_nonneg_right]

Premises used: le_add_iff_nonneg_right, LT.lt.le, intervalIntegral.integral_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
inst_1 : NormedSpace ℝ E_1
E : Type u_1
inst_2 : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_3 : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
hT : 0 < T
⊢ @VAddInvariantMeasure ↥(zmultiples T) ℝ _ MeasureSpace.toMeasurableSpace volume

Tactic:
haveI : VAddInvariantMeasure (AddSubgroup.zmultiples T) ℝ volume :=
    ⟨fun c s _ => measure_preimage_add _ _ _⟩
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
inst_1 : NormedSpace ℝ E_1
E : Type u_1
inst_2 : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_3 : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
hT : 0 < T
this : @VAddInvariantMeasure ↥(zmultiples T) ℝ _ MeasureSpace.toMeasurableSpace volume
hs : IsAddFundamentalDomain (↥(zmultiples T)) (Ioc t (t + T)) volume
ht : IsAddFundamentalDomain (↥(zmultiples T)) (Ioc s (s + T)) volume
hf₁ : ∀ (g : ↥(zmultiples T)) (x : ℝ), f (g +ᵥ x) = f x
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc t (t + T))) fun (x : ℝ) ↦ f x)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc s (s + T))) fun (x : ℝ) ↦ f x)

Tactic:
apply IsAddFundamentalDomain.setIntegral_eq (G := AddSubgroup.zmultiples T)

Premises used: MeasureTheory.IsAddFundamentalDomain.setIntegral_eq
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
inst_1 : NormedSpace ℝ E_1
E : Type u_1
inst_2 : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_3 : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
hT : 0 < T
this : @VAddInvariantMeasure ↥(zmultiples T) ℝ _ MeasureSpace.toMeasurableSpace volume
⊢ IsAddFundamentalDomain (↥(zmultiples T)) (Ioc t (t + T)) volume

Tactic:
isAddFundamentalDomain_Ioc hT t

Premises used: Set.Mem, isAddFundamentalDomain_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
inst_1 : NormedSpace ℝ E_1
E : Type u_1
inst_2 : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_3 : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
hT : 0 < T
this : @VAddInvariantMeasure ↥(zmultiples T) ℝ _ MeasureSpace.toMeasurableSpace volume
⊢ IsAddFundamentalDomain (↥(zmultiples T)) (Ioc s (s + T)) volume

Tactic:
isAddFundamentalDomain_Ioc hT s

Premises used: Set.Mem, isAddFundamentalDomain_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
inst_1 : NormedSpace ℝ E_1
E : Type u_1
inst_2 : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_3 : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
hT : 0 < T
this : @VAddInvariantMeasure ↥(zmultiples T) ℝ _ MeasureSpace.toMeasurableSpace volume
⊢ ∀ (g : ↥(zmultiples T)) (x : ℝ), f (g +ᵥ x) = f x

Tactic:
hf.map_vadd_zmultiples

Premises used: Set.Mem, Function.Periodic.map_vadd_zmultiples
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
f_1 : ℝ → E_1
T_1 : ℝ
inst_1 : NormedSpace ℝ E_1
E : Type u_1
inst_2 : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_3 : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
hT : 0 < T
this : @VAddInvariantMeasure ↥(zmultiples T) ℝ _ MeasureSpace.toMeasurableSpace volume
⊢ IsAddFundamentalDomain (↥(zmultiples T)) (Ioc t (t + T)) volume

Tactic:
exacts [isAddFundamentalDomain_Ioc hT t, isAddFundamentalDomain_Ioc hT s, hf.map_vadd_zmultiples]

Premises used: isAddFundamentalDomain_Ioc, Function.Periodic.map_vadd_zmultiples
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
rw : ∫ (x : ℝ) in t..s + T, f x = HAdd.hAdd (α := E) (∫ (x : ℝ) in t..s, f x) (∫ (x : ℝ) in s..s + T, f x)
rw₁ rw₂ : Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t..s + T, f x) (∫ (x : ℝ) in t..s + T, f x)
⊢ ∫ (x : ℝ) in t..s + T, f x = HAdd.hAdd (α := E) (∫ (x : ℝ) in t..s, f x) (∫ (x : ℝ) in t..t + T, f x)

Tactic:
rw [hf.intervalIntegral_add_eq t s, integral_add_adjacent_intervals (h_int t s) (h_int s _)]

Premises used: intervalIntegral.integral_add_adjacent_intervals, Function.Periodic.intervalIntegral_add_eq
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
n : ℤ
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∫ (x : ℝ) in 0..n • T, f x = HSMul.hSMul (β := E) n (∫ (x : ℝ) in 0..T, f x)
⊢ ∫ (x : ℝ) in t..t + n • T, f x = HSMul.hSMul (β := E) n (∫ (x : ℝ) in t..t + T, f x)

Tactic:
simp only [hf.intervalIntegral_add_eq t 0, (hf.zsmul n).intervalIntegral_add_eq t 0, zero_add,
      this]

Premises used: zero_add, Function.Periodic.zsmul, OfNat.ofNat, Function.Periodic.intervalIntegral_add_eq
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
n : ℤ
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
suffices : ∫ (x : ℝ) in 0..n • T, f x = HSMul.hSMul (β := E) n (∫ (x : ℝ) in 0..T, f x)
⊢ ∫ (x : ℝ) in t..t + n • T, f x = HSMul.hSMul (β := E) n (∫ (x : ℝ) in t..t + T, f x)

Tactic:
suffices (∫ x in 0..(n • T), f x) = n • ∫ x in 0..T, f x by
    simp only [hf.intervalIntegral_add_eq t 0, (hf.zsmul n).intervalIntegral_add_eq t 0, zero_add,
      this]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
n : ℤ
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
⊢ ∫ (x : ℝ) in 0..HSMul.hSMul (α := ℕ) 0 T, f x = HSMul.hSMul (α := ℕ) (β := E) 0 (∫ (x : ℝ) in 0..T, f x)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
n : ℤ
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
m : ℕ
ih : ∫ (x : ℝ) in 0..m • T, f x = HSMul.hSMul (β := E) m (∫ (x : ℝ) in 0..T, f x)
⊢ ∫ (x : ℝ) in 0..(m + 1) • T, f x = HSMul.hSMul (β := E) (m + 1) (∫ (x : ℝ) in 0..T, f x)

Tactic:
simp only [succ_nsmul, hf.intervalIntegral_add_eq_add 0 (m • T) h_int, ih, zero_add]

Premises used: Function.Periodic.intervalIntegral_add_eq_add, zero_add, HSMul.hSMul, OfNat.ofNat, succ_nsmul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
n : ℤ
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
m : ℕ
zero : ∫ (x : ℝ) in 0..HSMul.hSMul (α := ℕ) 0 T, f x = HSMul.hSMul (α := ℕ) (β := E) 0 (∫ (x : ℝ) in 0..T, f x)
succ :
  ∀ (m : ℕ) (ih : ∫ (x : ℝ) in 0..m • T, f x = HSMul.hSMul (β := E) m (∫ (x : ℝ) in 0..T, f x)),
    ∫ (x : ℝ) in 0..(m + 1) • T, f x = HSMul.hSMul (β := E) (m + 1) (∫ (x : ℝ) in 0..T, f x)
⊢ ∫ (x : ℝ) in 0..m • T, f x = HSMul.hSMul (β := E) m (∫ (x : ℝ) in 0..T, f x)

Tactic:
induction m with
    | zero => simp
    | succ m ih =>
      simp only [succ_nsmul, hf.intervalIntegral_add_eq_add 0 (m • T) h_int, ih, zero_add]

Premises used: Function.Periodic.intervalIntegral_add_eq_add, zero_add, AddSubgroup.zero, HSMul.hSMul, OfNat.ofNat, succ_nsmul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
n : ℤ
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
⊢ ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = HSMul.hSMul (β := E) m (∫ (x : ℝ) in 0..T, f x)

Tactic:
have : ∀ m : ℕ, (∫ x in 0..m • T, f x) = m • ∫ x in 0..T, f x := fun m ↦ by
    induction m with
    | zero => simp
    | succ m ih =>
      simp only [succ_nsmul, hf.intervalIntegral_add_eq_add 0 (m • T) h_int, ih, zero_add]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
n : ℤ
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = HSMul.hSMul (β := E) m (∫ (x : ℝ) in 0..T, f x)
ofNat : ∀ (n : ℕ), ∫ (x : ℝ) in 0..Int.ofNat n • T, f x = HSMul.hSMul (β := E) (Int.ofNat n) (∫ (x : ℝ) in 0..T, f x)
negSucc :
  ∀ (n : ℕ), ∫ (x : ℝ) in 0..Int.negSucc n • T, f x = HSMul.hSMul (β := E) (Int.negSucc n) (∫ (x : ℝ) in 0..T, f x)
⊢ ∫ (x : ℝ) in 0..n • T, f x = HSMul.hSMul (β := E) n (∫ (x : ℝ) in 0..T, f x)

Tactic:
rcases n with n | n
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = HSMul.hSMul (β := E) m (∫ (x : ℝ) in 0..T, f x)
n : ℕ
⊢ ∫ (x : ℝ) in 0..Int.ofNat n • T, f x = HSMul.hSMul (β := E) (Int.ofNat n) (∫ (x : ℝ) in 0..T, f x)

Tactic:
simp [← this n]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = HSMul.hSMul (β := E) m (∫ (x : ℝ) in 0..T, f x)
n : ℕ
rw : -HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, f x)
| HSMul.hSMul (β := E) (Int.negSucc n) (∫ (x : ℝ) in 0..T, f x)

Tactic:
rw [negSucc_zsmul]

Premises used: negSucc_zsmul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = HSMul.hSMul (β := E) m (∫ (x : ℝ) in 0..T, f x)
n : ℕ
negSucc : ∫ (x : ℝ) in 0..Int.negSucc n • T, f x = -HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, f x)
⊢ ∫ (x : ℝ) in 0..Int.negSucc n • T, f x = HSMul.hSMul (β := E) (Int.negSucc n) (∫ (x : ℝ) in 0..T, f x)

Tactic:
conv_rhs => rw [negSucc_zsmul]

Premises used: negSucc_zsmul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = HSMul.hSMul (β := E) m (∫ (x : ℝ) in 0..T, f x)
n : ℕ
simp : HAdd.hAdd (α := ℝ) (-1) (-(↑n : ℝ)) * T + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * T = 0
⊢ Int.negSucc n • T + (n + 1) • T = 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = HSMul.hSMul (β := E) m (∫ (x : ℝ) in 0..T, f x)
n : ℕ
linarith :
  HAdd.hAdd (α := ℝ) (-1) (-(↑n : ℝ)) * T + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * T < 0 →
    HAdd.hAdd (α := ℝ) (-1) (-(↑n : ℝ)) * T + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * T - 0 = 0
linarith₁ :
  0 < HAdd.hAdd (α := ℝ) (-1) (-(↑n : ℝ)) * T + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * T →
    0 - (HAdd.hAdd (α := ℝ) (-1) (-(↑n : ℝ)) * T + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * T) = 0
⊢ HAdd.hAdd (α := ℝ) (-1) (-(↑n : ℝ)) * T + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * T = 0

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = HSMul.hSMul (β := E) m (∫ (x : ℝ) in 0..T, f x)
n : ℕ
⊢ Int.negSucc n • T + (n + 1) • T = 0

Tactic:
have h₀ : Int.negSucc n • T + (n + 1) • T = 0 := by simp; linarith
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = HSMul.hSMul (β := E) m (∫ (x : ℝ) in 0..T, f x)
n : ℕ
h₀ : Int.negSucc n • T + (n + 1) • T = 0
negSucc :
  ∫ (x : ℝ) in Int.negSucc n • T..0, (fun (x : ℝ) ↦ f (x + (n + 1) • T)) x =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, (fun (x : ℝ) ↦ f (x + (n + 1) • T)) x)
⊢ ∫ (x : ℝ) in 0..Int.negSucc n • T, f x = -HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, f x)

Tactic:
rw [integral_symm, ← (hf.nsmul (n + 1)).funext, neg_inj]

Premises used: Function.Periodic.funext, Function.Periodic.nsmul, intervalIntegral.integral_symm, HAdd.hAdd, neg_inj, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = HSMul.hSMul (β := E) m (∫ (x : ℝ) in 0..T, f x)
n : ℕ
h₀ : Int.negSucc n • T + (n + 1) • T = 0
negSucc negSucc₁ :
  ∫ (x : ℝ) in Int.negSucc n • T..0, f (x + (n + 1) • T) =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, f (x + (n + 1) • T))
negSucc₂ :
  ∫ (x : ℝ) in Int.negSucc n • T + (n + 1) • T..0 + (n + 1) • T, f x =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0 + (n + 1) • T..T + (n + 1) • T, f x)
negSucc₃ :
  ∫ (x : ℝ) in 0..0 + (n + 1) • T, f x =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0 + (n + 1) • T..T + (n + 1) • T, f x)
negSucc₄ :
  ∫ (x : ℝ) in 0..(n + 1) • T, f x = HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in (n + 1) • T..T + (n + 1) • T, f x)
negSucc₅ :
  HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, f x) =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in (n + 1) • T..T + (n + 1) • T, f x)
negSucc₆ :
  HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, f x) =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in (n + 1) • T..(n + 1) • T + T, f x)
negSucc₇ :
  HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, f x) = HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..0 + T, f x)
⊢ ∫ (x : ℝ) in Int.negSucc n • T..0, (fun (x : ℝ) ↦ f (x + (n + 1) • T)) x =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, (fun (x : ℝ) ↦ f (x + (n + 1) • T)) x)

Tactic:
simp_rw [integral_comp_add_right, h₀, zero_add, this (n + 1), add_comm T,
      hf.intervalIntegral_add_eq ((n + 1) • T) 0, zero_add]

Premises used: zero_add, add_comm, HAdd.hAdd, intervalIntegral.integral_comp_add_right, HSMul.hSMul, OfNat.ofNat, Function.Periodic.intervalIntegral_add_eq