-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZMod (goal)
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
C : ℂ
e_a :
  ∑ x : ZMod N,
      Φ x *
        (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
          cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
    cexp ((↑π : ℂ) * (I * s) / 2) * ∑ j : ZMod N, Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s +
      cexp (-(↑π : ℂ) * (I * s) / 2) * ∑ x : ZMod N, Φ x * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s
e_a₁ :
  ∑ x : ZMod N,
      Φ x *
        (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
          cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
    HAdd.hAdd (α := ℂ)
      (∑ i : ZMod N,
        cexp ((↑π : ℂ) * (I * s) / 2) * (Φ i * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-i)) s))
      (∑ i : ZMod N,
        cexp (-(↑π : ℂ) * (I * s) / 2) * (Φ i * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) i) s))
e_a₂ :
  Eq (α := ℂ)
    (∑ x : ZMod N,
      Φ x *
        (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
          cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s))
    (∑ x : ZMod N,
      (cexp ((↑π : ℂ) * (I * s) / 2) * (Φ x * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-x)) s) +
        cexp (-(↑π : ℂ) * (I * s) / 2) * (Φ x * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s)))
e_a₃ :
  Eq (α := ℂ)
    (∑ x : ZMod N,
      Φ x *
        (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
          cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s))
    (∑ x : ZMod N,
      (cexp ((↑π : ℂ) * I * s / 2) * Φ x * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-x)) s +
        cexp (-(↑π : ℂ) * I * s / 2) * Φ x * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s))
⊢ ∑ x : ZMod N,
      Φ x *
        (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
          cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
    cexp ((↑π : ℂ) * (I * s) / 2) * ∑ j : ZMod N, Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s +
      cexp (-(↑π : ℂ) * (I * s) / 2) *
        ∑ x : ZMod N, Φ (- -x) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (- -x)) s
have e_a₄ : Eq (α := ℂ)
  (∑ x : ZMod N,
    Φ x *
      (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
        cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s))
  (∑ x : ZMod N,
    (Φ x * cexp ((↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-x)) s +
      Φ x * cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s))
Tactic: simp_rw [neg_neg, mul_sum, ← sum_add_distrib, ← mul_assoc, mul_comm _ (Φ _), mul_assoc,
    ← mul_add, map_neg, add_comm]