awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
h :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    fun (b : ℕ) ↦
    (↑(Real.cos (2 * π * a * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) s +
      I * ((↑(Real.sin (2 * π * a * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) s)
⊢ HasSum (fun (n : ℕ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (expZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
convert! (hasSum_nat_cosZeta a hs).add ((hasSum_nat_sinZeta a hs).mul_left I) using 1

Premises used: HasSum.add, HurwitzZeta.hasSum_nat_sinZeta, HurwitzZeta.hasSum_nat_cosZeta, HasSum.mul_left, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
h :
  ∀ (n : ℕ),
    cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
      (↑(Real.cos (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
        I * ((↑(Real.sin (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    fun (b : ℕ) ↦
    (↑(Real.cos (2 * π * a * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) s +
      I * ((↑(Real.sin (2 * π * a * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) s)

Tactic:
ext1 n
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
h :
  (Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) + Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I) /
      HPow.hPow (α := ℂ) (↑n : ℂ) s =
    Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
      I * (Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
⊢ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    (↑(Real.cos (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
      I * ((↑(Real.sin (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s)

Tactic:
simp only [mul_right_comm _ I, ← cos_add_sin_I, push_cast]

Premises used: Complex.cos_add_sin_I, mul_right_comm, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
h :
  Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
      Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
      I * (Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
h₁ :
  Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
      Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
      I * Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s
h₂ h₃ :
  Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
      I * Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
      I * Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ (Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) + Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I) /
      HPow.hPow (α := ℂ) (↑n : ℂ) s =
    Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
      I * (Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s)

Tactic:
rw [add_div, mul_div, mul_comm _ I]

Premises used: mul_div, mul_comm, add_div, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 1 ∨ a ≠ 0
hf : DifferentiableAt ℂ (cosZeta a) s
hg : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ I * sinZeta a s) s
⊢ DifferentiableAt ℂ (expZeta a) s

Tactic:
apply DifferentiableAt.add

Premises used: DifferentiableAt.add
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 1 ∨ a ≠ 0
⊢ DifferentiableAt ℂ (cosZeta a) s

Tactic:
differentiableAt_cosZeta a hs

Premises used: HurwitzZeta.differentiableAt_cosZeta
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 1 ∨ a ≠ 0
⊢ DifferentiableAt ℂ (cosZeta a) s

Tactic:
exact differentiableAt_cosZeta a hs

Premises used: HurwitzZeta.differentiableAt_cosZeta
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 1 ∨ a ≠ 0
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ I * sinZeta a s) s

Tactic:
apply (differentiableAt_const _).mul (differentiableAt_sinZeta a s)

Premises used: DifferentiableAt.mul, differentiableAt_const, HurwitzZeta.differentiableAt_sinZeta
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
ha : a ≠ 0
⊢ Differentiable ℂ (expZeta a)

Tactic:
(differentiableAt_expZeta a · (Or.inr ha))

Premises used: Differentiable, Or.inr, HurwitzZeta.differentiableAt_expZeta
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ LSeriesHasSum (fun (x : ℕ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑x : ℂ))) s
    (expZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
(hasSum_expZeta_of_one_lt_re a hs).congr_fun
    (LSeries.term_of_ne_zero' (ne_zero_of_one_lt_re hs) _)

Premises used: HasSum.congr_fun, Complex.ne_zero_of_one_lt_re, LSeriesHasSum, HurwitzZeta.hasSum_expZeta_of_one_lt_re, LSeries.term_of_ne_zero'
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : a ≠ 0 ∨ s ≠ 1
rw :
  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))
⊢ 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]

Premises used: Complex.cos, Complex.sin, HurwitzZeta.hurwitzZetaEven_one_sub, HurwitzZeta.expZeta, HurwitzZeta.sinZeta_neg, HurwitzZeta.cosZeta_neg, HurwitzZeta.hurwitzZeta, HurwitzZeta.hurwitzZetaOdd_one_sub
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : a ≠ 0 ∨ s ≠ 1
⊢ (↑π : ℂ) * I * s / 2 = (↑π : ℂ) * s / 2 * I

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : a ≠ 0 ∨ s ≠ 1
⊢ -(↑π : ℂ) * I * s / 2 = -((↑π : ℂ) * s / 2) * I

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : a ≠ 0 ∨ s ≠ 1
rw :
  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))
⊢ 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]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : a ≠ 0 ∨ s ≠ 1
generalize :
  ∀ (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))
⊢ 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

Premises used: Real.pi, HMul.hMul, Complex.ofReal, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : a ≠ 0 ∨ s ≠ 1
x : ℂ
generalize :
  ∀ (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))
⊢ 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

Premises used: HMul.hMul, HDiv.hDiv, Complex.exp, OfNat.ofNat, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : a ≠ 0 ∨ s ≠ 1
x y : ℂ
generalize :
  ∀ (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))
⊢ 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

Premises used: HMul.hMul, HDiv.hDiv, Complex.exp, OfNat.ofNat, Neg.neg, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
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
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
n : ℕ
⊢ s ≠ HSub.hSub (α := ℂ) 1 (↑(n + 1) : ℂ)

Tactic:
hs (n + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
n : ℕ
h : -(↑n : ℂ) = HSub.hSub (α := ℂ) 1 (↑(n + 1) : ℂ)
⊢ s ≠ -(↑n : ℂ)

Tactic:
convert! hs (n + 1) using 1

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
n : ℕ
h : -(↑n : ℂ) = 1 - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1
⊢ -(↑n : ℂ) = HSub.hSub (α := ℂ) 1 (↑(n + 1) : ℂ)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
n : ℕ
⊢ -(↑n : ℂ) = 1 - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
⊢ ∀ (n : ℕ), s ≠ -(↑n : ℂ)

Tactic:
have hs' (n : ℕ) : s ≠ -↑n := by
    convert! hs (n + 1) using 1
    push_cast
    ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
hs' : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
rw :
  2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * ((cexp ((↑π : ℂ) * s / 2 * I) + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) *
        hurwitzZetaEven a s +
      I *
        (2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
            ((cexp (-((↑π : ℂ) * s / 2) * I) - cexp ((↑π : ℂ) * s / 2 * I)) * I / 2) *
          hurwitzZetaOdd a s) =
    (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
      (cexp ((↑π : ℂ) * I * s / 2) * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
        cexp (-(↑π : ℂ) * I * s / 2) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))
⊢ expZeta a (1 - s) =
    (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
      (cexp ((↑π : ℂ) * I * s / 2) * hurwitzZeta a s + cexp (-(↑π : ℂ) * I * s / 2) * hurwitzZeta (-a) s)

Tactic:
rw [expZeta, cosZeta_one_sub a hs, sinZeta_one_sub a hs', hurwitzZeta, hurwitzZeta,
    hurwitzZetaEven_neg, hurwitzZetaOdd_neg, Complex.cos, Complex.sin]

Premises used: Complex.cos, Complex.sin, HurwitzZeta.cosZeta_one_sub, HurwitzZeta.expZeta, HurwitzZeta.hurwitzZeta, HurwitzZeta.hurwitzZetaOdd_neg, HurwitzZeta.sinZeta_one_sub, HurwitzZeta.hurwitzZetaEven_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
hs' : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
⊢ (↑π : ℂ) * I * s / 2 = (↑π : ℂ) * s / 2 * I

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
hs' : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
⊢ -(↑π : ℂ) * I * s / 2 = -((↑π : ℂ) * s / 2) * I

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
hs' : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
rw :
  2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * ((cexp ((↑π : ℂ) * s / 2 * I) + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) *
        hurwitzZetaEven a s +
      I *
        (2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
            ((cexp (-((↑π : ℂ) * s / 2) * I) - cexp ((↑π : ℂ) * s / 2 * I)) * I / 2) *
          hurwitzZetaOdd a s) =
    (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
      (cexp ((↑π : ℂ) * s / 2 * I) * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
        cexp (-((↑π : ℂ) * s / 2) * I) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))
⊢ 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * ((cexp ((↑π : ℂ) * s / 2 * I) + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) *
        hurwitzZetaEven a s +
      I *
        (2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
            ((cexp (-((↑π : ℂ) * s / 2) * I) - cexp ((↑π : ℂ) * s / 2 * I)) * I / 2) *
          hurwitzZetaOdd a s) =
    (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
      (cexp ((↑π : ℂ) * I * s / 2) * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
        cexp (-(↑π : ℂ) * I * s / 2) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))

Tactic:
rw [show ↑π * I * s / 2 = ↑π * s / 2 * I by ring,
    show -↑π * I * s / 2 = -(↑π * s / 2) * I by ring]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
hs' : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
generalize :
  ∀ (x : ℂ),
    2 * x * Complex.Gamma s * ((cexp ((↑π : ℂ) * s / 2 * I) + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) *
          hurwitzZetaEven a s +
        I *
          (2 * x * Complex.Gamma s * ((cexp (-((↑π : ℂ) * s / 2) * I) - cexp ((↑π : ℂ) * s / 2 * I)) * I / 2) *
            hurwitzZetaOdd a s) =
      x * Complex.Gamma s *
        (cexp ((↑π : ℂ) * s / 2 * I) * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
          cexp (-((↑π : ℂ) * s / 2) * I) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))
⊢ 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * ((cexp ((↑π : ℂ) * s / 2 * I) + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) *
        hurwitzZetaEven a s +
      I *
        (2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
            ((cexp (-((↑π : ℂ) * s / 2) * I) - cexp ((↑π : ℂ) * s / 2 * I)) * I / 2) *
          hurwitzZetaOdd a s) =
    (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
      (cexp ((↑π : ℂ) * s / 2 * I) * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
        cexp (-((↑π : ℂ) * s / 2) * I) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))

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

Premises used: Real.pi, HMul.hMul, Complex.ofReal, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
hs' : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
x : ℂ
generalize :
  ∀ (y : ℂ),
    2 * x * Complex.Gamma s * ((y + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) * hurwitzZetaEven a s +
        I * (2 * x * Complex.Gamma s * ((cexp (-((↑π : ℂ) * s / 2) * I) - y) * I / 2) * hurwitzZetaOdd a s) =
      x * Complex.Gamma s *
        (y * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
          cexp (-((↑π : ℂ) * s / 2) * I) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))
⊢ 2 * x * Complex.Gamma s * ((cexp ((↑π : ℂ) * s / 2 * I) + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) * hurwitzZetaEven a s +
      I *
        (2 * x * Complex.Gamma s * ((cexp (-((↑π : ℂ) * s / 2) * I) - cexp ((↑π : ℂ) * s / 2 * I)) * I / 2) *
          hurwitzZetaOdd a s) =
    x * Complex.Gamma s *
      (cexp ((↑π : ℂ) * s / 2 * I) * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
        cexp (-((↑π : ℂ) * s / 2) * I) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))

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

Premises used: HMul.hMul, HDiv.hDiv, Complex.exp, OfNat.ofNat, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
hs' : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
x y : ℂ
generalize :
  ∀ (z : ℂ),
    2 * x * Complex.Gamma s * ((y + z) / 2) * hurwitzZetaEven a s +
        I * (2 * x * Complex.Gamma s * ((z - y) * I / 2) * hurwitzZetaOdd a s) =
      x * Complex.Gamma s *
        (y * (hurwitzZetaEven a s + hurwitzZetaOdd a s) + z * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))
⊢ 2 * x * Complex.Gamma s * ((y + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) * hurwitzZetaEven a s +
      I * (2 * x * Complex.Gamma s * ((cexp (-((↑π : ℂ) * s / 2) * I) - y) * I / 2) * hurwitzZetaOdd a s) =
    x * Complex.Gamma s *
      (y * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
        cexp (-((↑π : ℂ) * s / 2) * I) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))

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

Premises used: HMul.hMul, HDiv.hDiv, Complex.exp, OfNat.ofNat, Neg.neg, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
hs' : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
x y z : ℂ
ring_nf :
  x * Complex.Gamma s * y * hurwitzZetaEven a s -
          x * Complex.Gamma s * y * HPow.hPow (β := ℕ) I 2 * hurwitzZetaOdd a s +
        x * Complex.Gamma s * z * hurwitzZetaEven a s +
      x * Complex.Gamma s * z * HPow.hPow (β := ℕ) I 2 * hurwitzZetaOdd a s =
    x * Complex.Gamma s * y * hurwitzZetaEven a s + x * Complex.Gamma s * y * hurwitzZetaOdd a s +
        x * Complex.Gamma s * z * hurwitzZetaEven a s -
      x * Complex.Gamma s * z * hurwitzZetaOdd a s
⊢ 2 * x * Complex.Gamma s * ((y + z) / 2) * hurwitzZetaEven a s +
      I * (2 * x * Complex.Gamma s * ((z - y) * I / 2) * hurwitzZetaOdd a s) =
    x * Complex.Gamma s *
      (y * (hurwitzZetaEven a s + hurwitzZetaOdd a s) + z * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
hs' : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
x y z : ℂ
rw :
  x * Complex.Gamma s * y * hurwitzZetaEven a s - x * Complex.Gamma s * y * -1 * hurwitzZetaOdd a s +
        x * Complex.Gamma s * z * hurwitzZetaEven a s +
      x * Complex.Gamma s * z * -1 * hurwitzZetaOdd a s =
    x * Complex.Gamma s * y * hurwitzZetaEven a s + x * Complex.Gamma s * y * hurwitzZetaOdd a s +
        x * Complex.Gamma s * z * hurwitzZetaEven a s -
      x * Complex.Gamma s * z * hurwitzZetaOdd a s
⊢ x * Complex.Gamma s * y * hurwitzZetaEven a s -
          x * Complex.Gamma s * y * HPow.hPow (β := ℕ) I 2 * hurwitzZetaOdd a s +
        x * Complex.Gamma s * z * hurwitzZetaEven a s +
      x * Complex.Gamma s * z * HPow.hPow (β := ℕ) I 2 * hurwitzZetaOdd a s =
    x * Complex.Gamma s * y * hurwitzZetaEven a s + x * Complex.Gamma s * y * hurwitzZetaOdd a s +
        x * Complex.Gamma s * z * hurwitzZetaEven a s -
      x * Complex.Gamma s * z * hurwitzZetaOdd a s

Tactic:
rw [I_sq]

Premises used: Complex.I_sq
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZeta
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
hs' : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
x y z : ℂ
⊢ x * Complex.Gamma s * y * hurwitzZetaEven a s - x * Complex.Gamma s * y * -1 * hurwitzZetaOdd a s +
        x * Complex.Gamma s * z * hurwitzZetaEven a s +
      x * Complex.Gamma s * z * -1 * hurwitzZetaOdd a s =
    x * Complex.Gamma s * y * hurwitzZetaEven a s + x * Complex.Gamma s * y * hurwitzZetaOdd a s +
        x * Complex.Gamma s * z * hurwitzZetaEven a s -
      x * Complex.Gamma s * z * hurwitzZetaOdd a s

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
x ξ : ℝ
simp :
  rexp (-π * HPow.hPow (β := ℕ) (ξ + 1) 2 * x) *
      (cexp (-(↑π : ℂ) * I * (I * (↑x : ℂ) + 2 * ((↑ξ : ℂ) * I * (↑x : ℂ)))) *
          jacobiTheta₂ ((↑ξ : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))).re =
    rexp (-π * HPow.hPow (β := ℕ) ξ 2 * x) * (jacobiTheta₂ ((↑ξ : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))).re
⊢ Eq (α := ℝ)
    ((fun (ξ : ℝ) ↦ rexp (-π * HPow.hPow (β := ℕ) ξ 2 * x) * (jacobiTheta₂ ((↑ξ : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))).re)
      (ξ + 1))
    ((fun (ξ : ℝ) ↦ rexp (-π * HPow.hPow (β := ℕ) ξ 2 * x) * (jacobiTheta₂ ((↑ξ : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))).re)
      ξ)

Tactic:
simp only [ofReal_add, ofReal_one, add_mul, one_mul, jacobiTheta₂_add_left']

Premises used: add_mul, Complex.ofReal_add, Complex.ofReal_one, jacobiTheta₂_add_left', one_mul
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
x ξ : ℝ
ring_nf :
  cexp (-((↑π : ℂ) * HPow.hPow (β := ℕ) I 2 * (↑x : ℂ)) - (↑π : ℂ) * HPow.hPow (β := ℕ) I 2 * (↑x : ℂ) * (↑ξ : ℂ) * 2) =
    (↑(rexp (π * x + π * x * ξ * 2)) : ℂ)
⊢ cexp (-(↑π : ℂ) * I * (I * (↑x : ℂ) + 2 * ((↑ξ : ℂ) * I * (↑x : ℂ)))) = (↑(rexp (π * (x + 2 * ξ * x))) : ℂ)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
x ξ : ℝ
⊢ cexp (-((↑π : ℂ) * HPow.hPow (β := ℕ) I 2 * (↑x : ℂ)) - (↑π : ℂ) * HPow.hPow (β := ℕ) I 2 * (↑x : ℂ) * (↑ξ : ℂ) * 2) =
    (↑(rexp (π * x + π * x * ξ * 2)) : ℂ)

Tactic:
simp [I_sq]

Premises used: Complex.I_sq
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
x ξ : ℝ
⊢ cexp (-(↑π : ℂ) * I * (I * (↑x : ℂ) + 2 * ((↑ξ : ℂ) * I * (↑x : ℂ)))) = (↑(rexp (π * (x + 2 * ξ * x))) : ℂ)

Tactic:
have : cexp (-↑π * I * ((I * ↑x) + 2 * (↑ξ * I * ↑x))) = rexp (π * (x + 2 * ξ * x)) := by
        ring_nf
        simp [I_sq]