awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (hypothesis)
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₂ : ℝ)
⊢ IntervalIntegrable f volume a₁ a₂
have this : 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
-- 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₂ : ℝ)
this : uIcc a₁ a₂ ⊆ uIcc (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
⊢ IntervalIntegrable f volume a₁ a₂
have apply : IntervalIntegrable f volume (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
Tactic: apply IntervalIntegrable.mono_set _ this
-- 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₂ : ℝ)
this : uIcc a₁ a₂ ⊆ uIcc (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
a : ℕ → ℝ := fun (n : ℕ) ↦ t + HSub.hSub (α := ℝ) (↑n : ℝ) (↑n₁ : ℝ) * T
⊢ IntervalIntegrable f volume (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
have rw : IntervalIntegrable f volume (a 0) (a (n₁ + n₂))
Tactic: rw [(by ring : t - n₁ * T = a 0), (by simp [a] : t + n₂ * T = a (n₁ + n₂))]
-- 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₂ : ℝ)
this : uIcc a₁ a₂ ⊆ uIcc (t - (↑n₁ : ℝ) * T) (t + (↑n₂ : ℝ) * T)
a : ℕ → ℝ := fun (n : ℕ) ↦ t + HSub.hSub (α := ℝ) (↑n : ℝ) (↑n₁ : ℝ) * T
⊢ IntervalIntegrable f volume (a 0) (a (n₁ + n₂))
have hint : ∀ k < n₁ + n₂, IntervalIntegrable f volume (a k) (a (k + 1))
Tactic: apply IntervalIntegrable.trans_iterate
-- 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₂ : ℝ)
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₂
⊢ IntervalIntegrable f volume (a k) (a (k + 1))
have h : f = fun (x : ℝ) ↦ f (x - HSub.hSub (α := ℝ) (↑k : ℝ) (↑n₁ : ℝ) * T)
Tactic: convert! (IntervalIntegrable.comp_sub_right h₂f ((k - n₁) * T) (by aesop)) using 1
-- 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₂ : ℝ)
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)
⊢ IntervalIntegrable f volume (a k) (a (k + 1))
have h₁ : a (k + 1) = t + T + HSub.hSub (α := ℝ) (↑k : ℝ) (↑n₁ : ℝ) * T
Tactic: convert! (IntervalIntegrable.comp_sub_right h₂f ((k - n₁) * T) (by aesop)) using 1
-- 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₂ : ℝ)
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 = fun (x : ℝ) ↦ f (x - HSub.hSub (α := ℝ) (↑k : ℝ) (↑n₁ : ℝ) * T)
have h : ∀ (x : ℝ), f x = f (x - HSub.hSub (α := ℝ) (↑k : ℝ) (↑n₁ : ℝ) * T)
Tactic: funext x
-- 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₂ : ℝ)
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₂
⊢ a (k + 1) = t + T + HSub.hSub (α := ℝ) (↑k : ℝ) (↑n₁ : ℝ) * T
have h : t + (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - (↑n₁ : ℝ)) * T = t + T + HSub.hSub (α := ℝ) (↑k : ℝ) (↑n₁ : ℝ) * T
Tactic: simp [a, Nat.cast_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T t₁ t₂ : ℝ
hf : Periodic f T
⊢ IntervalIntegrable f volume t₁ (t₁ + T) ↔ IntervalIntegrable f volume t₂ (t₂ + T)
have 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)
Tactic: wlog hT : T ≠ 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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)
⊢ IntervalIntegrable f volume t₁ (t₁ + T) ↔ IntervalIntegrable f volume t₂ (t₂ + T)
have 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)
Tactic: wlog hT : T ≠ 0
Cleared hypotheses: t₁, t₂, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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 a₁ a₂
have h₂f₁ : IntervalIntegrable f volume 0 (0 + T)
Tactic: apply h₁f.intervalIntegrable hT (t := 0)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t..t + T, f x) (∫ (x : ℝ) in s..s + T, f x)
have 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)
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 : ℝ
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)
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t..t + T, f x) (∫ (x : ℝ) in s..s + T, f x)
have 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)
Tactic: wlog hT : 0 < T
Cleared hypotheses: hf, t, s
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t..t + T, f x) (∫ (x : ℝ) in s..s + T, f x)
have inr : ∀ (hT : T = 0), 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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)
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t..t + T, f x) (∫ (x : ℝ) in s..s + T, f x)
have inr₁ : ∀ (hT : T < 0), 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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)
have inr : Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t + T..t, f x) (∫ (x : ℝ) in s + T..s, f x)
Tactic: rw [← neg_inj, ← integral_symm, ← integral_symm]
-- 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 : ℝ
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
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t..t + T, f x) (∫ (x : ℝ) in s..s + T, f x)
have 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)
Tactic: simp only [integral_of_le, hT.le, le_add_iff_nonneg_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (hypothesis)
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
⊢ 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)
have this : @VAddInvariantMeasure ↥(zmultiples T) ℝ _ MeasureSpace.toMeasurableSpace volume
Tactic: haveI : VAddInvariantMeasure (AddSubgroup.zmultiples T) ℝ volume :=
    ⟨fun c s _ => measure_preimage_add _ _ _⟩
-- 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 : ℝ
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
⊢ 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)
have hs : IsAddFundamentalDomain (↥(zmultiples T)) (Ioc t (t + T)) volume
Tactic: apply IsAddFundamentalDomain.setIntegral_eq (G := AddSubgroup.zmultiples 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 : ℝ
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
⊢ 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)
have ht : IsAddFundamentalDomain (↥(zmultiples T)) (Ioc s (s + T)) volume
Tactic: apply IsAddFundamentalDomain.setIntegral_eq (G := AddSubgroup.zmultiples 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 : ℝ
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
⊢ 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)
have hf₁ : ∀ (g : ↥(zmultiples T)) (x : ℝ), f (g +ᵥ x) = f x
Tactic: apply IsAddFundamentalDomain.setIntegral_eq (G := AddSubgroup.zmultiples T)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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₂
⊢ ∫ (x : ℝ) in t..s + T, f x = HAdd.hAdd (α := E) (∫ (x : ℝ) in t..s, f x) (∫ (x : ℝ) in t..t + T, f x)
have rw : ∫ (x : ℝ) in t..s + T, f x = HAdd.hAdd (α := E) (∫ (x : ℝ) in t..s, f x) (∫ (x : ℝ) in s..s + T, f x)
Tactic: rw [hf.intervalIntegral_add_eq t s, integral_add_adjacent_intervals (h_int t s) (h_int s _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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)
⊢ ∫ (x : ℝ) in t..s + T, f x = HAdd.hAdd (α := E) (∫ (x : ℝ) in t..s, f x) (∫ (x : ℝ) in t..t + T, f x)
have rw₁ : Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in t..s + T, f x) (∫ (x : ℝ) in t..s + T, f x)
Tactic: rw [hf.intervalIntegral_add_eq t s, integral_add_adjacent_intervals (h_int t s) (h_int s _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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 t..t + n • T, f x = HSMul.hSMul (β := E) n (∫ (x : ℝ) in t..t + T, f x)
have suffices : ∫ (x : ℝ) in 0..n • T, f x = HSMul.hSMul (β := E) n (∫ (x : ℝ) in 0..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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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)
have zero : ∫ (x : ℝ) in 0..HSMul.hSMul (α := ℕ) 0 T, f x = HSMul.hSMul (α := ℕ) (β := E) 0 (∫ (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]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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)
⊢ ∫ (x : ℝ) in 0..m • T, f x = HSMul.hSMul (β := E) m (∫ (x : ℝ) in 0..T, f x)
have 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)
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]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (hypothesis)
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..n • T, f x = HSMul.hSMul (β := E) n (∫ (x : ℝ) in 0..T, f x)
have this : ∀ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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)
⊢ ∫ (x : ℝ) in 0..n • T, f x = HSMul.hSMul (β := E) n (∫ (x : ℝ) in 0..T, f x)
have ofNat : ∀ (n : ℕ), ∫ (x : ℝ) in 0..Int.ofNat n • T, f x = HSMul.hSMul (β := E) (Int.ofNat n) (∫ (x : ℝ) in 0..T, f x)
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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)
⊢ ∫ (x : ℝ) in 0..n • T, f x = HSMul.hSMul (β := E) n (∫ (x : ℝ) in 0..T, f x)
have negSucc : ∀ (n : ℕ), ∫ (x : ℝ) in 0..Int.negSucc n • T, f x = HSMul.hSMul (β := E) (Int.negSucc n) (∫ (x : ℝ) in 0..T, f x)
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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 : ℕ
| HSMul.hSMul (β := E) (Int.negSucc n) (∫ (x : ℝ) in 0..T, f x)
have rw : -HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, f x)
Tactic: rw [negSucc_zsmul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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.negSucc n • T, f x = HSMul.hSMul (β := E) (Int.negSucc n) (∫ (x : ℝ) in 0..T, f x)
have negSucc : ∫ (x : ℝ) in 0..Int.negSucc n • T, f x = -HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, f x)
Tactic: conv_rhs => rw [negSucc_zsmul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
have simp : HAdd.hAdd (α := ℝ) (-1) (-(↑n : ℝ)) * T + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * T = 0
Tactic: simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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 : ℕ
⊢ HAdd.hAdd (α := ℝ) (-1) (-(↑n : ℝ)) * T + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * T = 0
have linarith : HAdd.hAdd (α := ℝ) (-1) (-(↑n : ℝ)) * T + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * T < 0 →
  HAdd.hAdd (α := ℝ) (-1) (-(↑n : ℝ)) * T + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * T - 0 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
⊢ HAdd.hAdd (α := ℝ) (-1) (-(↑n : ℝ)) * T + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * T = 0
have linarith₁ : 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