-- Mathlib/NumberTheory/LSeries/ZMod.lean
/-- Explicit formula for the L-function of `𝓕 Φ`, where `𝓕` is the discrete Fourier transform. -/
lemma LFunction_dft (Φ : ZMod N → ℂ) {s : ℂ} (hs : Φ 0 = 0 ∨ s ≠ 1) :
    LFunction (𝓕 Φ) s = ∑ j : ZMod N, Φ j * expZeta (toAddCircle (-j)) s

Proof state:
case e_f.h.e_f.h
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
this : ∀ (j : ZMod N), Φ j * LFunction (fun k => 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s
j k : ZMod N
⊢ ↑N ^ (-s) * ↑(toCircle (-(k * j))) * Φ k * hurwitzZeta (toAddCircle j) s =
    Φ k * ↑N ^ (-s) * ↑(toCircle (-k * j)) * hurwitzZeta (toAddCircle j) s

Tactic:
rw [mul_assoc (Φ _), mul_comm (Φ _), neg_mul]

Result:
no goals

Proof state:
case neg
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : ¬(-j ≠ 0 ∨ s ≠ 1)
⊢ Φ j * LFunction (fun k => 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s

Tactic:
simp only [neg_ne_zero, not_or, not_not] at h

Result:
case neg
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : j = 0 ∧ s = 1
⊢ Φ j * LFunction (fun k => 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
this : ∀ (j : ZMod N), Φ j * LFunction (fun k => 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s
⊢ ∑ i : ZMod N, ↑N ^ (-s) * ((fun k => ∑ j : ZMod N, 𝕖 (-(j * k)) • Φ j) i * hurwitzZeta (toAddCircle i) s) =
    ∑ y : ZMod N, ∑ x : ZMod N, Φ x * (↑N ^ (-s) * (𝕖 (-x * y) * hurwitzZeta (toAddCircle y) s))

Tactic:
simp only [sum_mul, mul_sum, Circle.smul_def, smul_eq_mul, stdAddChar_apply, ← mul_assoc]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
this : ∀ (j : ZMod N), Φ j * LFunction (fun k => 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s
⊢ ∑ x : ZMod N, ∑ x_1 : ZMod N, ↑N ^ (-s) * ↑(toCircle (-(x_1 * x))) * Φ x_1 * hurwitzZeta (toAddCircle x) s =
    ∑ x : ZMod N, ∑ x_1 : ZMod N, Φ x_1 * ↑N ^ (-s) * ↑(toCircle (-x_1 * x)) * hurwitzZeta (toAddCircle x) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
this : ∀ (j : ZMod N), Φ j * LFunction (fun k => 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s
⊢ ∑ i : ZMod N, ↑N ^ (-s) * (𝓕 Φ i * hurwitzZeta (toAddCircle i) s) =
    ∑ x : ZMod N, ∑ i : ZMod N, Φ x * (↑N ^ (-s) * (𝕖 (-x * i) * hurwitzZeta (toAddCircle i) s))

Tactic:
rw [dft_def, sum_comm]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
this : ∀ (j : ZMod N), Φ j * LFunction (fun k => 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s
⊢ ∑ i : ZMod N, ↑N ^ (-s) * ((fun k => ∑ j : ZMod N, 𝕖 (-(j * k)) • Φ j) i * hurwitzZeta (toAddCircle i) s) =
    ∑ y : ZMod N, ∑ x : ZMod N, Φ x * (↑N ^ (-s) * (𝕖 (-x * y) * hurwitzZeta (toAddCircle y) s))

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : j = 0 ∧ s = 1
⊢ Φ 0 = 0

Tactic:
tauto

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
this : ∀ (j : ZMod N), Φ j * LFunction (fun k => 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s
⊢ ∑ x : ZMod N, ∑ x_1 : ZMod N, ↑N ^ (-s) * ↑(toCircle (-(x_1 * x))) * Φ x_1 * hurwitzZeta (toAddCircle x) s =
    ∑ x : ZMod N, ∑ x_1 : ZMod N, Φ x_1 * ↑N ^ (-s) * ↑(toCircle (-x_1 * x)) * hurwitzZeta (toAddCircle x) s

Tactic:
congr 1 with j

Result:
case e_f.h
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
this : ∀ (j : ZMod N), Φ j * LFunction (fun k => 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s
j : ZMod N
⊢ ∑ x : ZMod N, ↑N ^ (-s) * ↑(toCircle (-(x * j))) * Φ x * hurwitzZeta (toAddCircle j) s =
    ∑ x : ZMod N, Φ x * ↑N ^ (-s) * ↑(toCircle (-x * j)) * hurwitzZeta (toAddCircle j) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
this : ∀ (j : ZMod N), Φ j * LFunction (fun k => 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s
⊢ LFunction (𝓕 Φ) s = ∑ j : ZMod N, Φ j * expZeta (toAddCircle (-j)) s

Tactic:
simp only [LFunction, ← this, mul_sum]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
this : ∀ (j : ZMod N), Φ j * LFunction (fun k => 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s
⊢ ∑ i : ZMod N, ↑N ^ (-s) * (𝓕 Φ i * hurwitzZeta (toAddCircle i) s) =
    ∑ x : ZMod N, ∑ i : ZMod N, Φ x * (↑N ^ (-s) * (𝕖 (-x * i) * hurwitzZeta (toAddCircle i) s))

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
⊢ Φ j * LFunction (fun k => 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s

Tactic:
by_cases h : -j ≠ 0 ∨ s ≠ 1

Result:
case pos
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : -j ≠ 0 ∨ s ≠ 1
⊢ Φ j * LFunction (fun k => 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s

case neg
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : ¬(-j ≠ 0 ∨ s ≠ 1)
⊢ Φ j * LFunction (fun k => 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s

Proof state:
case e_f.h
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
this : ∀ (j : ZMod N), Φ j * LFunction (fun k => 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s
j : ZMod N
⊢ ∑ x : ZMod N, ↑N ^ (-s) * ↑(toCircle (-(x * j))) * Φ x * hurwitzZeta (toAddCircle j) s =
    ∑ x : ZMod N, Φ x * ↑N ^ (-s) * ↑(toCircle (-x * j)) * hurwitzZeta (toAddCircle j) s

Tactic:
congr 1 with k

Result:
case e_f.h.e_f.h
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
this : ∀ (j : ZMod N), Φ j * LFunction (fun k => 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s
j k : ZMod N
⊢ ↑N ^ (-s) * ↑(toCircle (-(k * j))) * Φ k * hurwitzZeta (toAddCircle j) s =
    Φ k * ↑N ^ (-s) * ↑(toCircle (-k * j)) * hurwitzZeta (toAddCircle j) s

Proof state:
case pos
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : -j ≠ 0 ∨ s ≠ 1
⊢ Φ j * LFunction (fun k => 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s

Tactic:
rw [LFunction_stdAddChar_eq_expZeta _ _ h]

Result:
no goals

Proof state:
case neg
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : j = 0 ∧ s = 1
⊢ Φ j * LFunction (fun k => 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s

Tactic:
rw [h.1, show Φ 0 = 0 by tauto, zero_mul, zero_mul]

Result:
no goals