-- Mathlib/NumberTheory/LSeries/ZMod.lean
theorem LFunction_one_sub (Φ : ZMod N → ℂ) {s : ℂ}
    (hs : ∀ (n : ℕ), s ≠ -n) (hs' : Φ 0 = 0 ∨ s ≠ 1) :
    LFunction Φ (1 - s) = N ^ (s - 1) * (2 * π) ^ (-s) * Gamma s *
      (cexp (π * I * s / 2) * LFunction (𝓕 Φ) s
       + cexp (-π * I * s / 2) * LFunction (𝓕 fun x ↦ Φ (-x)) s)

Proof state:
case e_a.e_a
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
⊢ ∑ x : ZMod N,
      Φ x *
        (cexp (-↑π * (I * s) / 2) * expZeta (toAddCircle x) s + cexp (↑π * (I * s) / 2) * expZeta (-toAddCircle x) s) =
    cexp (↑π * (I * s) / 2) * ∑ j : ZMod N, Φ j * expZeta (toAddCircle (-j)) s +
      cexp (-↑π * (I * s) / 2) * ∑ j : ZMod N, Φ (-j) * expZeta (toAddCircle (-j)) s

Tactic:
conv_rhs => enter [2, 2]; rw [← (Equiv.neg _).sum_comp _ _ (by simp), Equiv.neg_apply]

Result:
case e_a.e_a
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
⊢ ∑ x : ZMod N,
      Φ x *
        (cexp (-↑π * (I * s) / 2) * expZeta (toAddCircle x) s + cexp (↑π * (I * s) / 2) * expZeta (-toAddCircle x) s) =
    cexp (↑π * (I * s) / 2) * ∑ j : ZMod N, Φ j * expZeta (toAddCircle (-j)) s +
      cexp (-↑π * (I * s) / 2) * ∑ x : ZMod N, Φ (- -x) * expZeta (toAddCircle (- -x)) s

Proof state:
case inl
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
⊢ Φ 0 * hurwitzZeta (toAddCircle 0) (1 - s) =
    Φ 0 *
      ((2 * ↑π) ^ (-s) * Gamma s *
        (cexp (-↑π * I * s / 2) * expZeta (toAddCircle 0) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle 0) s))

Tactic:
rcases hs' with hΦ | hs'

Result:
case inl.inl
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hΦ : Φ 0 = 0
⊢ Φ 0 * hurwitzZeta (toAddCircle 0) (1 - s) =
    Φ 0 *
      ((2 * ↑π) ^ (-s) * Gamma s *
        (cexp (-↑π * I * s / 2) * expZeta (toAddCircle 0) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle 0) s))

case inl.inr
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : s ≠ 1
⊢ Φ 0 * hurwitzZeta (toAddCircle 0) (1 - s) =
    Φ 0 *
      ((2 * ↑π) ^ (-s) * Gamma s *
        (cexp (-↑π * I * s / 2) * expZeta (toAddCircle 0) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle 0) s))

Proof state:
case e_a.e_a
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
⊢ ∑ x : ZMod N,
      Φ x *
        (cexp (-↑π * (I * s) / 2) * expZeta (toAddCircle x) s + cexp (↑π * (I * s) / 2) * expZeta (-toAddCircle x) s) =
    cexp (↑π * (I * s) / 2) * ∑ j : ZMod N, Φ j * expZeta (toAddCircle (-j)) s +
      cexp (-↑π * (I * s) / 2) * ∑ x : ZMod N, Φ (- -x) * expZeta (toAddCircle (- -x)) s

Tactic:
simp_rw [neg_neg, mul_sum, ← sum_add_distrib, ← mul_assoc, mul_comm _ (Φ _), mul_assoc,
  ← mul_add, map_neg, add_comm]

Result:
no goals

Proof state:
case inl.inl
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hΦ : Φ 0 = 0
⊢ Φ 0 * hurwitzZeta (toAddCircle 0) (1 - s) =
    Φ 0 *
      ((2 * ↑π) ^ (-s) * Gamma s *
        (cexp (-↑π * I * s / 2) * expZeta (toAddCircle 0) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle 0) s))

Tactic:
simp only [hΦ, zero_mul]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
⊢ {a | (Equiv.neg (ZMod N)) a ≠ a} ⊆ ↑Finset.univ

Tactic:
simp

Result:
no goals

Proof state:
case inr
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
hj : j ≠ 0
⊢ Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
    Φ j *
      ((2 * ↑π) ^ (-s) * Gamma s *
        (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))

Tactic:
rw [hurwitzZeta_one_sub _ hs (Or.inl <| toAddCircle_eq_zero.not.mpr hj)]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
⊢ C *
      (↑N ^ (s - 1) *
        ∑ x : ZMod N,
          Φ x *
            (cexp (-↑π * (I * s) / 2) * expZeta (toAddCircle x) s +
              cexp (↑π * (I * s) / 2) * expZeta (-toAddCircle x) s)) =
    C *
      (↑N ^ (s - 1) *
        (cexp (↑π * (I * s) / 2) * LFunction (𝓕 Φ) s + cexp (-↑π * (I * s) / 2) * LFunction (𝓕 fun x => Φ (-x)) s))

Tactic:
congr 2

Result:
case e_a.e_a
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
⊢ ∑ x : ZMod N,
      Φ x *
        (cexp (-↑π * (I * s) / 2) * expZeta (toAddCircle x) s + cexp (↑π * (I * s) / 2) * expZeta (-toAddCircle x) s) =
    cexp (↑π * (I * s) / 2) * LFunction (𝓕 Φ) s + cexp (-↑π * (I * s) / 2) * LFunction (𝓕 fun x => Φ (-x)) s

Proof state:
case inl.inr
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : s ≠ 1
⊢ Φ 0 * hurwitzZeta (toAddCircle 0) (1 - s) =
    Φ 0 *
      ((2 * ↑π) ^ (-s) * Gamma s *
        (cexp (-↑π * I * s / 2) * expZeta (toAddCircle 0) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle 0) s))

Tactic:
rw [hurwitzZeta_one_sub _ hs (Or.inr hs')]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
⊢ ↑N ^ (-(1 - s)) *
      ∑ x : ZMod N,
        Φ x *
          (C *
            (cexp (-↑π * I * s / 2) * expZeta (toAddCircle x) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle x) s)) =
    ↑N ^ (s - 1) * C *
      (cexp (↑π * I * s / 2) * LFunction (𝓕 Φ) s + cexp (-↑π * I * s / 2) * LFunction (𝓕 fun x => Φ (-x)) s)

Tactic:
simp_rw [← mul_assoc, mul_comm _ C, mul_assoc, ← mul_sum, ← mul_assoc, mul_comm _ C, mul_assoc,
  neg_sub]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
⊢ C *
      (↑N ^ (s - 1) *
        ∑ x : ZMod N,
          Φ x *
            (cexp (-↑π * (I * s) / 2) * expZeta (toAddCircle x) s +
              cexp (↑π * (I * s) / 2) * expZeta (-toAddCircle x) s)) =
    C *
      (↑N ^ (s - 1) *
        (cexp (↑π * (I * s) / 2) * LFunction (𝓕 Φ) s + cexp (-↑π * (I * s) / 2) * LFunction (𝓕 fun x => Φ (-x)) s))