-- Mathlib/MeasureTheory/Integral/Periodic.lean
theorem intervalIntegral_add_zsmul_eq (hf : Periodic f T) (n : ℤ) (t : ℝ)
    (h_int : ∀ t₁ t₂, IntervalIntegrable f MeasureSpace.volume t₁ t₂) :
    ∫ x in t..t + n • T, f x = n • ∫ x in t..t + T, f x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : 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 = m • ∫ (x : ℝ) in 0 ..T, f x

Tactic:
induction' m with m ih

Result:
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
n : ℤ
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
⊢ ∫ (x : ℝ) in 0 ..0 • T, f x = 0 • ∫ (x : ℝ) in 0 ..T, f x

case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : 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 = m • ∫ (x : ℝ) in 0 ..T, f x
⊢ ∫ (x : ℝ) in 0 ..(m + 1) • T, f x = (m + 1) • ∫ (x : ℝ) in 0 ..T, f x

Proof state:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : 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 = m • ∫ (x : ℝ) in 0 ..T, f x
⊢ ∫ (x : ℝ) in 0 ..(m + 1) • T, f x = (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]

Result:
no goals

Proof state:
case negSucc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : 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 = m • ∫ (x : ℝ) in 0 ..T, f x
n : ℕ
h₀ : Int.negSucc n • T + (n + 1) • T = 0
⊢ ∫ (x : ℝ) in 0 ..Int.negSucc n • T, f x = -((n + 1) • ∫ (x : ℝ) in 0 ..T, f x)

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

Result:
case negSucc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : 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 = m • ∫ (x : ℝ) in 0 ..T, f x
n : ℕ
h₀ : Int.negSucc n • T + (n + 1) • T = 0
⊢ ∫ (x : ℝ) in Int.negSucc n • T..0, (fun x => f (x + (n + 1) • T)) x =
    (n + 1) • ∫ (x : ℝ) in 0 ..T, (fun x => f (x + (n + 1) • T)) x

Proof state:
case negSucc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : 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 = m • ∫ (x : ℝ) in 0 ..T, f x
n : ℕ
h₀ : Int.negSucc n • T + (n + 1) • T = 0
⊢ ∫ (x : ℝ) in Int.negSucc n • T..0, (fun x => f (x + (n + 1) • T)) x =
    (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]

Result:
no goals

Proof state:
case negSucc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : 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 = m • ∫ (x : ℝ) in 0 ..T, f x
n : ℕ
⊢ ∫ (x : ℝ) in 0 ..Int.negSucc n • T, f x = Int.negSucc n • ∫ (x : ℝ) in 0 ..T, f x

Tactic:
conv_rhs => rw [negSucc_zsmul]

Result:
case negSucc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : 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 = m • ∫ (x : ℝ) in 0 ..T, f x
n : ℕ
⊢ ∫ (x : ℝ) in 0 ..Int.negSucc n • T, f x = -((n + 1) • ∫ (x : ℝ) in 0 ..T, f x)

Proof state:
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
n : ℤ
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
⊢ ∫ (x : ℝ) in 0 ..0 • T, f x = 0 • ∫ (x : ℝ) in 0 ..T, f x

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : 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 = m • ∫ (x : ℝ) in 0 ..T, f x
n : ℕ
⊢ Int.negSucc n • T + (n + 1) • T = 0

Tactic:
simp

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : 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 = m • ∫ (x : ℝ) in 0 ..T, f x
n : ℕ
⊢ (-1 + -↑n) * T + (↑n + 1) * T = 0

Proof state:
case negSucc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : 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 = m • ∫ (x : ℝ) in 0 ..T, f x
n : ℕ
⊢ ∫ (x : ℝ) in 0 ..Int.negSucc n • T, f x = -((n + 1) • ∫ (x : ℝ) in 0 ..T, f x)

Tactic:
have h₀ : Int.negSucc n • T + (n + 1) • T = 0 := by simp; linarith

Result:
case negSucc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : 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 = m • ∫ (x : ℝ) in 0 ..T, f x
n : ℕ
h₀ : Int.negSucc n • T + (n + 1) • T = 0
⊢ ∫ (x : ℝ) in 0 ..Int.negSucc n • T, f x = -((n + 1) • ∫ (x : ℝ) in 0 ..T, f x)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : 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 = m • ∫ (x : ℝ) in 0 ..T, f x
n : ℕ
⊢ (-1 + -↑n) * T + (↑n + 1) * T = 0

Tactic:
linarith

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : 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 = 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]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
n : ℤ
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
⊢ ∫ (x : ℝ) in 0 ..n • T, f x = n • ∫ (x : ℝ) in 0 ..T, f x

Proof state:
case ofNat
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : 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 = m • ∫ (x : ℝ) in 0 ..T, f x
n : ℕ
⊢ ∫ (x : ℝ) in 0 ..Int.ofNat n • T, f x = Int.ofNat n • ∫ (x : ℝ) in 0 ..T, f x

Tactic:
simp [← this n]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : 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 = m • ∫ (x : ℝ) in 0 ..T, f x
⊢ ∫ (x : ℝ) in 0 ..n • T, f x = n • ∫ (x : ℝ) in 0 ..T, f x

Tactic:
rcases n with n | n

Result:
case ofNat
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : 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 = m • ∫ (x : ℝ) in 0 ..T, f x
n : ℕ
⊢ ∫ (x : ℝ) in 0 ..Int.ofNat n • T, f x = Int.ofNat n • ∫ (x : ℝ) in 0 ..T, f x

case negSucc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : 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 = m • ∫ (x : ℝ) in 0 ..T, f x
n : ℕ
⊢ ∫ (x : ℝ) in 0 ..Int.negSucc n • T, f x = Int.negSucc n • ∫ (x : ℝ) in 0 ..T, f x