-- Mathlib/NumberTheory/LSeries/HurwitzZeta.lean
lemma hurwitzZeta_one_sub (a : UnitAddCircle) {s : ℂ}
    (hs : ∀ (n : ℕ), s ≠ -n) (hs' : a ≠ 0 ∨ s ≠ 1) :
    hurwitzZeta a (1 - s) = (2 * π) ^ (-s) * Gamma s *
    (exp (-π * I * s / 2) * expZeta a s + exp (π * I * s / 2) * expZeta (-a) s)

Proof state:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
x y : ℂ
⊢ 2 * x * Complex.Gamma s * ((y + cexp (-(↑π * s / 2) * I)) / 2) * cosZeta a s +
      2 * x * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - y) * I / 2) * sinZeta a s =
    x * Complex.Gamma s *
      (cexp (-(↑π * s / 2) * I) * (cosZeta a s + I * sinZeta a s) + y * (cosZeta a s + I * -sinZeta a s))

Tactic:
generalize (-(↑π * s / 2) * I).exp = z

Result:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
x y z : ℂ
⊢ 2 * x * Complex.Gamma s * ((y + z) / 2) * cosZeta a s + 2 * x * Complex.Gamma s * ((z - y) * I / 2) * sinZeta a s =
    x * Complex.Gamma s * (z * (cosZeta a s + I * sinZeta a s) + y * (cosZeta a s + I * -sinZeta a s))

Proof state:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
x : ℂ
⊢ 2 * x * Complex.Gamma s * ((cexp (↑π * s / 2 * I) + cexp (-(↑π * s / 2) * I)) / 2) * cosZeta a s +
      2 * x * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - cexp (↑π * s / 2 * I)) * I / 2) * sinZeta a s =
    x * Complex.Gamma s *
      (cexp (-(↑π * s / 2) * I) * (cosZeta a s + I * sinZeta a s) +
        cexp (↑π * s / 2 * I) * (cosZeta a s + I * -sinZeta a s))

Tactic:
generalize (↑π * s / 2 * I).exp = y

Result:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
x y : ℂ
⊢ 2 * x * Complex.Gamma s * ((y + cexp (-(↑π * s / 2) * I)) / 2) * cosZeta a s +
      2 * x * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - y) * I / 2) * sinZeta a s =
    x * Complex.Gamma s *
      (cexp (-(↑π * s / 2) * I) * (cosZeta a s + I * sinZeta a s) + y * (cosZeta a s + I * -sinZeta a s))

Proof state:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
⊢ ↑π * I * s / 2 = ↑π * s / 2 * I

Tactic:
ring

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
⊢ 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (↑π * s / 2 * I) + cexp (-(↑π * s / 2) * I)) / 2) * cosZeta a s +
      2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - cexp (↑π * s / 2 * I)) * I / 2) *
        sinZeta a s =
    (2 * ↑π) ^ (-s) * Complex.Gamma s *
      (cexp (-↑π * I * s / 2) * (cosZeta a s + I * sinZeta a s) +
        cexp (↑π * I * s / 2) * (cosZeta a s + I * -sinZeta a s))

Tactic:
rw [show ↑π * I * s / 2 = ↑π * s / 2 * I by ring,
  show -↑π * I * s / 2 = -(↑π * s / 2) * I by ring]

Result:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
⊢ 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (↑π * s / 2 * I) + cexp (-(↑π * s / 2) * I)) / 2) * cosZeta a s +
      2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - cexp (↑π * s / 2 * I)) * I / 2) *
        sinZeta a s =
    (2 * ↑π) ^ (-s) * Complex.Gamma s *
      (cexp (-(↑π * s / 2) * I) * (cosZeta a s + I * sinZeta a s) +
        cexp (↑π * s / 2 * I) * (cosZeta a s + I * -sinZeta a s))

Proof state:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
⊢ 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (↑π * s / 2 * I) + cexp (-(↑π * s / 2) * I)) / 2) * cosZeta a s +
      2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - cexp (↑π * s / 2 * I)) * I / 2) *
        sinZeta a s =
    (2 * ↑π) ^ (-s) * Complex.Gamma s *
      (cexp (-(↑π * s / 2) * I) * (cosZeta a s + I * sinZeta a s) +
        cexp (↑π * s / 2 * I) * (cosZeta a s + I * -sinZeta a s))

Tactic:
generalize (2 * π : ℂ) ^ (-s) = x

Result:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
x : ℂ
⊢ 2 * x * Complex.Gamma s * ((cexp (↑π * s / 2 * I) + cexp (-(↑π * s / 2) * I)) / 2) * cosZeta a s +
      2 * x * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - cexp (↑π * s / 2 * I)) * I / 2) * sinZeta a s =
    x * Complex.Gamma s *
      (cexp (-(↑π * s / 2) * I) * (cosZeta a s + I * sinZeta a s) +
        cexp (↑π * s / 2 * I) * (cosZeta a s + I * -sinZeta a s))

Proof state:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
x y z : ℂ
⊢ 2 * x * Complex.Gamma s * ((y + z) / 2) * cosZeta a s + 2 * x * Complex.Gamma s * ((z - y) * I / 2) * sinZeta a s =
    x * Complex.Gamma s * (z * (cosZeta a s + I * sinZeta a s) + y * (cosZeta a s + I * -sinZeta a s))

Tactic:
ring_nf

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
⊢ -↑π * I * s / 2 = -(↑π * s / 2) * I

Tactic:
ring

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
⊢ hurwitzZeta a (1 - s) =
    (2 * ↑π) ^ (-s) * Complex.Gamma s * (cexp (-↑π * I * s / 2) * expZeta a s + cexp (↑π * I * s / 2) * expZeta (-a) s)

Tactic:
rw [hurwitzZeta, hurwitzZetaEven_one_sub a hs hs', hurwitzZetaOdd_one_sub a hs,
  expZeta, expZeta, Complex.cos, Complex.sin, sinZeta_neg, cosZeta_neg]

Result:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
⊢ 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (↑π * s / 2 * I) + cexp (-(↑π * s / 2) * I)) / 2) * cosZeta a s +
      2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - cexp (↑π * s / 2 * I)) * I / 2) *
        sinZeta a s =
    (2 * ↑π) ^ (-s) * Complex.Gamma s *
      (cexp (-↑π * I * s / 2) * (cosZeta a s + I * sinZeta a s) +
        cexp (↑π * I * s / 2) * (cosZeta a s + I * -sinZeta a s))