-- Mathlib/NumberTheory/LSeries/ZMod.lean
/--
Relation between the completed L-function and the usual one (even case).
We state it this way around so it holds at the poles of the gamma factor as well
(except at `s = 0`, where it is genuinely false if `N > 1` and `Φ 0 ≠ 0`).
-/
lemma LFunction_eq_completed_div_gammaFactor_even (hΦ : Φ.Even) (s : ℂ) (hs : s ≠ 0 ∨ Φ 0 = 0) :
    LFunction Φ s = completedLFunction Φ s / Gammaℝ s

Proof state:
case e_a.e_f.h.inl
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : s ≠ 0 ∨ Φ 0 = 0
i : ZMod N
hi : i ≠ 0
⊢ Φ i * hurwitzZetaEven (toAddCircle i) s = Φ i * (completedHurwitzZetaEven (toAddCircle i) s / s.Gammaℝ)

Tactic:
rw [hurwitzZetaEven_def_of_ne_or_ne (.inl (hi ∘ toAddCircle_eq_zero.mp))]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : s ≠ 0 ∨ Φ 0 = 0
⊢ LFunction Φ s = completedLFunction Φ s / s.Gammaℝ

Tactic:
simp only [completedLFunction_def_even hΦ, LFunction_def_even hΦ, mul_div_assoc, sum_div]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : s ≠ 0 ∨ Φ 0 = 0
⊢ ↑N ^ (-s) * ∑ j : ZMod N, Φ j * hurwitzZetaEven (toAddCircle j) s =
    ↑N ^ (-s) * ∑ x : ZMod N, Φ x * (completedHurwitzZetaEven (toAddCircle x) s / s.Gammaℝ)

Proof state:
case e_a.e_f.h
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : s ≠ 0 ∨ Φ 0 = 0
i : ZMod N
⊢ Φ i * hurwitzZetaEven (toAddCircle i) s = Φ i * (completedHurwitzZetaEven (toAddCircle i) s / s.Gammaℝ)

Tactic:
rcases ne_or_eq i 0 with hi | rfl

Result:
case e_a.e_f.h.inl
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : s ≠ 0 ∨ Φ 0 = 0
i : ZMod N
hi : i ≠ 0
⊢ Φ i * hurwitzZetaEven (toAddCircle i) s = Φ i * (completedHurwitzZetaEven (toAddCircle i) s / s.Gammaℝ)

case e_a.e_f.h.inr
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : s ≠ 0 ∨ Φ 0 = 0
⊢ Φ 0 * hurwitzZetaEven (toAddCircle 0) s = Φ 0 * (completedHurwitzZetaEven (toAddCircle 0) s / s.Gammaℝ)

Proof state:
case e_a.e_f.h.inr.inr
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hΦ' : Φ 0 = 0
⊢ Φ 0 * hurwitzZetaEven (toAddCircle 0) s = Φ 0 * (completedHurwitzZetaEven (toAddCircle 0) s / s.Gammaℝ)

Tactic:
simp only [hΦ', map_zero, zero_mul]

Result:
no goals

Proof state:
case e_a.e_f.h.inr
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : s ≠ 0 ∨ Φ 0 = 0
⊢ Φ 0 * hurwitzZetaEven (toAddCircle 0) s = Φ 0 * (completedHurwitzZetaEven (toAddCircle 0) s / s.Gammaℝ)

Tactic:
rcases hs with hs | hΦ'

Result:
case e_a.e_f.h.inr.inl
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : s ≠ 0
⊢ Φ 0 * hurwitzZetaEven (toAddCircle 0) s = Φ 0 * (completedHurwitzZetaEven (toAddCircle 0) s / s.Gammaℝ)

case e_a.e_f.h.inr.inr
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hΦ' : Φ 0 = 0
⊢ Φ 0 * hurwitzZetaEven (toAddCircle 0) s = Φ 0 * (completedHurwitzZetaEven (toAddCircle 0) s / s.Gammaℝ)

Proof state:
case e_a.e_f.h.inr.inl
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : s ≠ 0
⊢ Φ 0 * hurwitzZetaEven (toAddCircle 0) s = Φ 0 * (completedHurwitzZetaEven (toAddCircle 0) s / s.Gammaℝ)

Tactic:
rw [hurwitzZetaEven_def_of_ne_or_ne (.inr hs)]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : s ≠ 0 ∨ Φ 0 = 0
⊢ ↑N ^ (-s) * ∑ j : ZMod N, Φ j * hurwitzZetaEven (toAddCircle j) s =
    ↑N ^ (-s) * ∑ x : ZMod N, Φ x * (completedHurwitzZetaEven (toAddCircle x) s / s.Gammaℝ)

Tactic:
congr 2 with i

Result:
case e_a.e_f.h
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : s ≠ 0 ∨ Φ 0 = 0
i : ZMod N
⊢ Φ i * hurwitzZetaEven (toAddCircle i) s = Φ i * (completedHurwitzZetaEven (toAddCircle i) s / s.Gammaℝ)