-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem fourier_add_half_inv_index {n : ℤ} (hn : n ≠ 0) (hT : 0 < T) (x : AddCircle T) :
    @fourier T n (x + ↑(T / 2 / n)) = -fourier n x

Proof state:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ ↑n ≠ 0

Tactic:
simpa using hn

Result:
no goals

Proof state:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
this : ↑n ≠ 0
⊢ ↑(n • x).toCircle * ↑(toCircle ↑(n • (T / 2 / ↑n))) = -(fourier n) x

Tactic:
have : (@toCircle T (n • (T / 2 / n) : ℝ) : ℂ) = -1 := by
  rw [zsmul_eq_mul, toCircle, Function.Periodic.lift_coe, Circle.coe_exp]
  replace hT := Complex.ofReal_ne_zero.mpr hT.ne'
  convert Complex.exp_pi_mul_I using 3
  field_simp; ring

Result:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
this✝ : ↑n ≠ 0
this : ↑(toCircle ↑(n • (T / 2 / ↑n))) = -1
⊢ ↑(n • x).toCircle * ↑(toCircle ↑(n • (T / 2 / ↑n))) = -(fourier n) x

Proof state:
case h.e'_2.h.e'_1.h.e'_5
T : ℝ
n : ℤ
hn : n ≠ 0
x : AddCircle T
this : ↑n ≠ 0
hT : ↑T ≠ 0
⊢ ↑(2 * π / T * (↑n * (T / 2 / ↑n))) = ↑π

Tactic:
field_simp

Result:
case h.e'_2.h.e'_1.h.e'_5
T : ℝ
n : ℤ
hn : n ≠ 0
x : AddCircle T
this : ↑n ≠ 0
hT : ↑T ≠ 0
⊢ 2 * ↑π * (↑n * ↑T) = ↑π * (↑T * (2 * ↑n))

Proof state:
T : ℝ
n : ℤ
hn : n ≠ 0
x : AddCircle T
this : ↑n ≠ 0
hT : ↑T ≠ 0
⊢ Complex.exp (↑(2 * π / T * (↑n * (T / 2 / ↑n))) * Complex.I) = -1

Tactic:
convert Complex.exp_pi_mul_I using 3

Result:
case h.e'_2.h.e'_1.h.e'_5
T : ℝ
n : ℤ
hn : n ≠ 0
x : AddCircle T
this : ↑n ≠ 0
hT : ↑T ≠ 0
⊢ ↑(2 * π / T * (↑n * (T / 2 / ↑n))) = ↑π

Proof state:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
this✝ : ↑n ≠ 0
this : ↑(toCircle ↑(n • (T / 2 / ↑n))) = -1
⊢ ↑(n • x).toCircle * -1 = -(fourier n) x

Tactic:
simp

Result:
no goals

Proof state:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
this : ↑n ≠ 0
⊢ ↑(toCircle ↑(n • (T / 2 / ↑n))) = -1

Tactic:
rw [zsmul_eq_mul, toCircle, Function.Periodic.lift_coe, Circle.coe_exp]

Result:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
this : ↑n ≠ 0
⊢ Complex.exp (↑(2 * π / T * (↑n * (T / 2 / ↑n))) * Complex.I) = -1

Proof state:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
this✝ : ↑n ≠ 0
this : ↑(toCircle ↑(n • (T / 2 / ↑n))) = -1
⊢ ↑(n • x).toCircle * ↑(toCircle ↑(n • (T / 2 / ↑n))) = -(fourier n) x

Tactic:
rw [this]

Result:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
this✝ : ↑n ≠ 0
this : ↑(toCircle ↑(n • (T / 2 / ↑n))) = -1
⊢ ↑(n • x).toCircle * -1 = -(fourier n) x

Proof state:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ (fourier n) (x + ↑(T / 2 / ↑n)) = -(fourier n) x

Tactic:
rw [fourier_apply, zsmul_add, ← QuotientAddGroup.mk_zsmul, toCircle_add, coe_mul_unitSphere]

Result:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ ↑(n • x).toCircle * ↑(toCircle ↑(n • (T / 2 / ↑n))) = -(fourier n) x

Proof state:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
this : ↑n ≠ 0
⊢ Complex.exp (↑(2 * π / T * (↑n * (T / 2 / ↑n))) * Complex.I) = -1

Tactic:
replace hT := Complex.ofReal_ne_zero.mpr hT.ne'

Result:
T : ℝ
n : ℤ
hn : n ≠ 0
x : AddCircle T
this : ↑n ≠ 0
hT : ↑T ≠ 0
⊢ Complex.exp (↑(2 * π / T * (↑n * (T / 2 / ↑n))) * Complex.I) = -1

Proof state:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ ↑(n • x).toCircle * ↑(toCircle ↑(n • (T / 2 / ↑n))) = -(fourier n) x

Tactic:
have : (n : ℂ) ≠ 0 := by simpa using hn

Result:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
this : ↑n ≠ 0
⊢ ↑(n • x).toCircle * ↑(toCircle ↑(n • (T / 2 / ↑n))) = -(fourier n) x

Proof state:
case h.e'_2.h.e'_1.h.e'_5
T : ℝ
n : ℤ
hn : n ≠ 0
x : AddCircle T
this : ↑n ≠ 0
hT : ↑T ≠ 0
⊢ 2 * ↑π * (↑n * ↑T) = ↑π * (↑T * (2 * ↑n))

Tactic:
ring

Result:
no goals