awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
rw :
  cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2 =
    s.Gammaℝ * (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s) / 2 / s.Gammaℝ
rw₁ :
  cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2 =
    s.Gammaℝ * (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s) / s.Gammaℝ / 2
rw₂ rw₃ :
  cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2 =
    cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2
⊢ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2 =
    s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2 / s.Gammaℝ

Tactic:
rw [mul_div_assoc _ (cexp _), div_right_comm _ (2 : ℂ),
    mul_div_cancel_left₀ _ (Gammaℝ_ne_zero_of_re_pos (zero_lt_one.trans hs))]

Premises used: div_right_comm, mul_div_assoc, mul_div_cancel_left₀, zero_lt_one, Complex.Gammaℝ_ne_zero_of_re_pos, LT.lt.trans, Complex.exp, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum
    (fun (n : ℕ) ↦
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
        cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s / 2)
    (cosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s +
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) / HPow.hPow (α := ℂ) (↑|0| : ℂ) s / 2)

Tactic:
have := (hasSum_int_cosZeta a hs).nat_add_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun (n : ℕ) ↦
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
        cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s / 2)
    (cosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s +
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) / HPow.hPow (α := ℂ) (↑|0| : ℂ) s / 2)
⊢ HasSum
    (fun (n : ℕ) ↦
      (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)))) / 2 /
        HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (cosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
simp_rw [abs_neg, Int.cast_neg, Nat.abs_cast, Int.cast_natCast, mul_neg, abs_zero, Int.cast_zero,
    zero_cpow (ne_zero_of_one_lt_re hs), div_zero, zero_div, add_zero, ← add_div,
    div_right_comm _ _ (2 : ℂ)] at this

Premises used: Int.cast_neg, Int.cast_natCast, abs_neg, div_right_comm, Nat.abs_cast, Int.cast_zero, zero_div, Complex.ne_zero_of_one_lt_re, Complex.zero_cpow, abs_zero, add_zero, OfNat.ofNat, div_zero, mul_neg, add_div
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun (n : ℕ) ↦
      (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)))) / 2 /
        HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (cosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
simp_rw :
  HasSum
    (fun (n : ℕ) ↦
      (cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I) + cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I))) / 2 /
        HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (cosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
⊢ HasSum (fun (n : ℕ) ↦ (↑(Real.cos (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (cosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
simp_rw [push_cast, Complex.cos, neg_mul]

Premises used: Complex.cos, neg_mul
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun (n : ℕ) ↦
      (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)))) / 2 /
        HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (cosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
n : ℕ
⊢ 2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I = 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun (n : ℕ) ↦
      (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)))) / 2 /
        HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (cosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
n : ℕ
rw rw₁ :
  (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)))) / 2 /
      HPow.hPow (α := ℂ) (↑n : ℂ) s =
    (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)))) / 2 /
      HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ (cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I) + cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I))) / 2 /
      HPow.hPow (α := ℂ) (↑n : ℂ) s =
    (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)))) / 2 /
      HPow.hPow (α := ℂ) (↑n : ℂ) s

Tactic:
rw [show 2 * π * a * n * I = 2 * π * I * a * n by ring]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun (n : ℕ) ↦
      (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)))) / 2 /
        HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (cosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
⊢ HasSum
    (fun (n : ℕ) ↦
      (cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I) + cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I))) / 2 /
        HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (cosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
exact this.congr_fun fun n ↦ by rw [show 2 * π * a * n * I = 2 * π * I * a * n by ring]

Premises used: HasSum.congr_fun
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ LSeriesHasSum (fun (x : ℕ) ↦ (↑(Real.cos (2 * π * a * (↑x : ℝ))) : ℂ)) s
    (cosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
(hasSum_nat_cosZeta 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_nat_cosZeta, LSeries.term_of_ne_zero'
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : a ≠ 0 ∨ s ≠ 1
rw : a ≠ 0 ∨ 1 - s ≠ 0
⊢ hurwitzZetaEven a (1 - s) = completedHurwitzZetaEven a (1 - s) * (1 - s).Gammaℝ⁻¹

Tactic:
rw [hurwitzZetaEven_def_of_ne_or_ne, div_eq_mul_inv]

Premises used: HurwitzZeta.hurwitzZetaEven_def_of_ne_or_ne, div_eq_mul_inv
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : a ≠ 0 ∨ s ≠ 1
⊢ a ≠ 0 ∨ 1 - s ≠ 0

Tactic:
simpa [sub_eq_zero, eq_comm (a := s)] using hs'

Premises used: sub_eq_zero, eq_comm
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : a ≠ 0 ∨ s ≠ 1
⊢ hurwitzZetaEven a (1 - s) = completedHurwitzZetaEven a (1 - s) * (1 - s).Gammaℝ⁻¹

Tactic:
have : hurwitzZetaEven a (1 - s) = completedHurwitzZetaEven a (1 - s) * (Gammaℝ (1 - s))⁻¹ := by
    rw [hurwitzZetaEven_def_of_ne_or_ne, div_eq_mul_inv]
    simpa [sub_eq_zero, eq_comm (a := s)] using hs'
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : a ≠ 0 ∨ s ≠ 1
this : hurwitzZetaEven a (1 - s) = completedHurwitzZetaEven a (1 - s) * (1 - s).Gammaℝ⁻¹
⊢ s ≠ 0

Tactic:
simpa using hs 0

Premises used: OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : a ≠ 0 ∨ s ≠ 1
this : hurwitzZetaEven a (1 - s) = completedHurwitzZetaEven a (1 - s) * (1 - s).Gammaℝ⁻¹
rw :
  completedCosZeta a s * (s.Gammaℂ * Complex.cos ((↑π : ℂ) * s / 2) * s.Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.cos ((↑π : ℂ) * s / 2) * (completedCosZeta a s / s.Gammaℝ)
⊢ hurwitzZetaEven a (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * Complex.cos ((↑π : ℂ) * s / 2) * cosZeta a s

Tactic:
rw [this, completedHurwitzZetaEven_one_sub, inv_Gammaℝ_one_sub hs, cosZeta,
    Function.update_of_ne (by simpa using hs 0), ← Gammaℂ]

Premises used: Complex.Gammaℂ, HurwitzZeta.cosZeta, HurwitzZeta.completedHurwitzZetaEven_one_sub, Complex.inv_Gammaℝ_one_sub, Function.update_of_ne
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : a ≠ 0 ∨ s ≠ 1
this : hurwitzZetaEven a (1 - s) = completedHurwitzZetaEven a (1 - s) * (1 - s).Gammaℝ⁻¹
generalize : ∀ (A : ℂ), completedCosZeta a s * (A * s.Gammaℝ⁻¹) = A * (completedCosZeta a s / s.Gammaℝ)
⊢ completedCosZeta a s * (s.Gammaℂ * Complex.cos ((↑π : ℂ) * s / 2) * s.Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.cos ((↑π : ℂ) * s / 2) * (completedCosZeta a s / s.Gammaℝ)

Tactic:
generalize Gammaℂ s * cos (π * s / 2) = A

Premises used: Real.pi, HMul.hMul, Complex.Gammaℂ, Complex.cos, HDiv.hDiv, Complex.ofReal, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : a ≠ 0 ∨ s ≠ 1
this : hurwitzZetaEven a (1 - s) = completedHurwitzZetaEven a (1 - s) * (1 - s).Gammaℝ⁻¹
A : ℂ
⊢ completedCosZeta a s * (A * s.Gammaℝ⁻¹) = A * (completedCosZeta a s / s.Gammaℝ)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
h : 1 - s ≠ 0
⊢ cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹

Tactic:
rw [cosZeta, Function.update_of_ne, div_eq_mul_inv]

Premises used: HurwitzZeta.cosZeta, div_eq_mul_inv, Function.update_of_ne
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
⊢ 1 - s ≠ 0

Tactic:
simpa [sub_eq_zero] using (hs 0).symm

Premises used: sub_eq_zero, Ne.symm, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
⊢ cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹

Tactic:
have : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (Gammaℝ (1 - s))⁻¹ := by
    rw [cosZeta, Function.update_of_ne, div_eq_mul_inv]
    simpa [sub_eq_zero] using (hs 0).symm
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
n : ℕ
⊢ s ≠ -(↑n : ℂ)

Tactic:
simpa using hs (n + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
⊢ s ≠ 0

Tactic:
simpa using hs 1

Premises used: OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
rw :
  completedHurwitzZetaEven a s * (s.Gammaℂ * Complex.cos ((↑π : ℂ) * s / 2) * s.Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.cos ((↑π : ℂ) * s / 2) * (completedHurwitzZetaEven a s / s.Gammaℝ)
⊢ cosZeta a (1 - s) = s.Gammaℂ * Complex.cos ((↑π : ℂ) * s / 2) * hurwitzZetaEven a s

Tactic:
rw [this, completedCosZeta_one_sub, inv_Gammaℝ_one_sub (fun n ↦ by simpa using hs (n + 1)),
    hurwitzZetaEven_def_of_ne_or_ne (Or.inr (by simpa using hs 1))]

Premises used: HurwitzZeta.hurwitzZetaEven_def_of_ne_or_ne, HurwitzZeta.completedCosZeta_one_sub, Complex.inv_Gammaℝ_one_sub, Or.inr
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
generalize : ∀ (A : ℂ), completedHurwitzZetaEven a s * (A * s.Gammaℝ⁻¹) = A * (completedHurwitzZetaEven a s / s.Gammaℝ)
⊢ completedHurwitzZetaEven a s * (s.Gammaℂ * Complex.cos ((↑π : ℂ) * s / 2) * s.Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.cos ((↑π : ℂ) * s / 2) * (completedHurwitzZetaEven a s / s.Gammaℝ)

Tactic:
generalize Gammaℂ s * cos (π * s / 2) = A

Premises used: Real.pi, HMul.hMul, Complex.Gammaℂ, Complex.cos, HDiv.hDiv, Complex.ofReal, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
A : ℂ
⊢ completedHurwitzZetaEven a s * (A * s.Gammaℝ⁻¹) = A * (completedHurwitzZetaEven a s / s.Gammaℝ)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z τ : ℂ
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (jacobiTheta₂'' z τ) =
    jacobiTheta₂'' ((starRingEnd ℂ : (a : ℂ) → ℂ) z) (-(starRingEnd ℂ : (a : ℂ) → ℂ) τ)

Tactic:
simp [jacobiTheta₂'', jacobiTheta₂'_conj, jacobiTheta₂_conj, ← exp_conj, map_ofNat, div_neg,
    neg_div, jacobiTheta₂'_neg_left]

Premises used: jacobiTheta₂_conj, neg_div, jacobiTheta₂'_conj, HurwitzZeta.jacobiTheta₂'', map_ofNat, jacobiTheta₂'_neg_left, div_neg, Complex.exp_conj
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z τ : ℂ
simp :
  cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (z + 1) 2 * τ) *
      (cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) *
            (jacobiTheta₂' (z * τ) τ - 2 * (↑π : ℂ) * I * jacobiTheta₂ (z * τ) τ) /
          (2 * (↑π : ℂ) * I) +
        (z * (cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * jacobiTheta₂ (z * τ) τ) +
          cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * jacobiTheta₂ (z * τ) τ)) =
    cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ) *
      (jacobiTheta₂' (z * τ) τ / (2 * (↑π : ℂ) * I) + z * jacobiTheta₂ (z * τ) τ)
⊢ jacobiTheta₂'' (z + 1) τ = jacobiTheta₂'' z τ

Tactic:
simp only [jacobiTheta₂'', add_mul z 1, one_mul, jacobiTheta₂'_add_left', jacobiTheta₂_add_left']

Premises used: add_mul, HurwitzZeta.jacobiTheta₂'', jacobiTheta₂'_add_left', jacobiTheta₂_add_left', OfNat.ofNat, one_mul
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z τ : ℂ
generalize :
  ∀ (J : ℂ),
    cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (z + 1) 2 * τ) *
        (cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * (jacobiTheta₂' (z * τ) τ - 2 * (↑π : ℂ) * I * J) /
            (2 * (↑π : ℂ) * I) +
          (z * (cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * J) + cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * J)) =
      cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ) * (jacobiTheta₂' (z * τ) τ / (2 * (↑π : ℂ) * I) + z * J)
⊢ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (z + 1) 2 * τ) *
      (cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) *
            (jacobiTheta₂' (z * τ) τ - 2 * (↑π : ℂ) * I * jacobiTheta₂ (z * τ) τ) /
          (2 * (↑π : ℂ) * I) +
        (z * (cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * jacobiTheta₂ (z * τ) τ) +
          cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * jacobiTheta₂ (z * τ) τ)) =
    cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ) *
      (jacobiTheta₂' (z * τ) τ / (2 * (↑π : ℂ) * I) + z * jacobiTheta₂ (z * τ) τ)

Tactic:
generalize jacobiTheta₂ (z * τ) τ = J

Premises used: HMul.hMul, jacobiTheta₂
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z τ J : ℂ
generalize :
  ∀ (J' : ℂ),
    cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (z + 1) 2 * τ) *
        (cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * (J' - 2 * (↑π : ℂ) * I * J) / (2 * (↑π : ℂ) * I) +
          (z * (cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * J) + cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * J)) =
      cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ) * (J' / (2 * (↑π : ℂ) * I) + z * J)
⊢ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (z + 1) 2 * τ) *
      (cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * (jacobiTheta₂' (z * τ) τ - 2 * (↑π : ℂ) * I * J) /
          (2 * (↑π : ℂ) * I) +
        (z * (cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * J) + cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * J)) =
    cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ) * (jacobiTheta₂' (z * τ) τ / (2 * (↑π : ℂ) * I) + z * J)

Tactic:
generalize jacobiTheta₂' (z * τ) τ = J'

Premises used: HMul.hMul, jacobiTheta₂'
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z τ J J' : ℂ
simp_rw :
  cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (z + 1) 2 * τ) *
        (cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * (J' - 2 * (↑π : ℂ) * I * J) +
          (z * (cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * J) + cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * J) *
            (2 * (↑π : ℂ) * I)) /
      (2 * (↑π : ℂ) * I) =
    cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ) * (J' + z * J * (2 * (↑π : ℂ) * I)) / (2 * (↑π : ℂ) * I)
⊢ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (z + 1) 2 * τ) *
      (cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * (J' - 2 * (↑π : ℂ) * I * J) / (2 * (↑π : ℂ) * I) +
        (z * (cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * J) + cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * J)) =
    cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ) * (J' / (2 * (↑π : ℂ) * I) + z * J)

Tactic:
simp_rw [div_add' _ _ _ two_pi_I_ne_zero, ← mul_div_assoc]

Premises used: Complex.two_pi_I_ne_zero, mul_div_assoc, div_add'
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z τ J J' : ℂ
⊢ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (z + 1) 2 * τ) *
        (cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * (J' - 2 * (↑π : ℂ) * I * J) +
          (z * (cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * J) + cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * J) *
            (2 * (↑π : ℂ) * I)) /
      (2 * (↑π : ℂ) * I) =
    cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ) * (J' + z * J * (2 * (↑π : ℂ) * I)) / (2 * (↑π : ℂ) * I)

Tactic:
congr_arg (· / (2 * π * I)) ?_

Premises used: Real.pi, HMul.hMul, HDiv.hDiv, Complex.ofReal, congr_arg, OfNat.ofNat, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z τ J J' : ℂ
refine :
  cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (z + 1) 2 * τ) *
      (cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * (J' - 2 * (↑π : ℂ) * I * J) +
        (z * (cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * J) + cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * J) *
          (2 * (↑π : ℂ) * I)) =
    cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ) * (J' + z * J * (2 * (↑π : ℂ) * I))
⊢ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (z + 1) 2 * τ) *
        (cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * (J' - 2 * (↑π : ℂ) * I * J) +
          (z * (cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * J) + cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * J) *
            (2 * (↑π : ℂ) * I)) /
      (2 * (↑π : ℂ) * I) =
    cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ) * (J' + z * J * (2 * (↑π : ℂ) * I)) / (2 * (↑π : ℂ) * I)

Tactic:
refine congr_arg (· / (2 * π * I)) ?_

Premises used: Real.pi, HMul.hMul, HDiv.hDiv, Complex.ofReal, congr_arg, OfNat.ofNat, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z τ J J' : ℂ
rw :
  cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (z + 1) 2 * τ + -(↑π : ℂ) * I * (τ + 2 * (z * τ))) *
      (J' - 2 * (↑π : ℂ) * I * J + (z * J + J) * (2 * (↑π : ℂ) * I)) =
    cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ) * (J' + z * J * (2 * (↑π : ℂ) * I))
⊢ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (z + 1) 2 * τ) *
      (cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * (J' - 2 * (↑π : ℂ) * I * J) +
        (z * (cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * J) + cexp (-(↑π : ℂ) * I * (τ + 2 * (z * τ))) * J) *
          (2 * (↑π : ℂ) * I)) =
    cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ) * (J' + z * J * (2 * (↑π : ℂ) * I))

Tactic:
rw [mul_left_comm _ (cexp _), ← mul_add, mul_assoc (cexp _), ← mul_add, ← mul_assoc (cexp _),
    ← Complex.exp_add]

Premises used: Complex.exp_add, mul_assoc, mul_left_comm, Complex.exp, mul_add
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z τ J J' : ℂ
refine_1 :
  (↑π : ℂ) * I * HPow.hPow (β := ℕ) (z + 1) 2 * τ + -(↑π : ℂ) * I * (τ + 2 * (z * τ)) =
    (↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ
refine_2 : J' - 2 * (↑π : ℂ) * I * J + (z * J + J) * (2 * (↑π : ℂ) * I) = J' + z * J * (2 * (↑π : ℂ) * I)
⊢ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (z + 1) 2 * τ + -(↑π : ℂ) * I * (τ + 2 * (z * τ))) *
      (J' - 2 * (↑π : ℂ) * I * J + (z * J + J) * (2 * (↑π : ℂ) * I)) =
    cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ) * (J' + z * J * (2 * (↑π : ℂ) * I))

Tactic:
congrm (cexp ?_ * ?_)

Premises used: HMul.hMul, Complex.exp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z τ J J' : ℂ
⊢ (↑π : ℂ) * I * HPow.hPow (β := ℕ) (z + 1) 2 * τ + -(↑π : ℂ) * I * (τ + 2 * (z * τ)) =
    (↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z τ J J' : ℂ
⊢ J' - 2 * (↑π : ℂ) * I * J + (z * J + J) * (2 * (↑π : ℂ) * I) = J' + z * J * (2 * (↑π : ℂ) * I)

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z τ : ℂ
⊢ jacobiTheta₂'' (-z) τ = -jacobiTheta₂'' z τ

Tactic:
simp [jacobiTheta₂'', jacobiTheta₂'_neg_left, neg_div, -neg_add_rev, ← neg_add]

Premises used: neg_add_rev, neg_div, HurwitzZeta.jacobiTheta₂'', neg_add, jacobiTheta₂'_neg_left
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z τ : ℂ
inl : jacobiTheta₂' z 0 = -2 * (↑π : ℂ) / (-I * 0) ^ (3 / 2) * jacobiTheta₂'' z (-1 / 0)
inr : ∀ (hτ : τ ≠ 0), jacobiTheta₂' z τ = -2 * (↑π : ℂ) / (-I * τ) ^ (3 / 2) * jacobiTheta₂'' z (-1 / τ)
⊢ jacobiTheta₂' z τ = -2 * (↑π : ℂ) / (-I * τ) ^ (3 / 2) * jacobiTheta₂'' z (-1 / τ)

Tactic:
rcases eq_or_ne τ 0 with rfl | hτ

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z : ℂ
⊢ im 0 ≤ 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z : ℂ
⊢ 3 / 2 ≠ 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z : ℂ
inl : 0 = -2 * (↑π : ℂ) / (-I * 0) ^ (3 / 2) * jacobiTheta₂'' z (-1 / 0)
inl₁ : 0 = -2 * (↑π : ℂ) / HPow.hPow (α := ℂ) 0 (3 / 2) * jacobiTheta₂'' z (-1 / 0)
inl₂ : 0 = -2 * (↑π : ℂ) / 0 * jacobiTheta₂'' z (-1 / 0)
inl₃ : 0 = 0 * jacobiTheta₂'' z (-1 / 0)
inl₄ inl₅ : Eq (α := ℂ) 0 0
⊢ jacobiTheta₂' z 0 = -2 * (↑π : ℂ) / (-I * 0) ^ (3 / 2) * jacobiTheta₂'' z (-1 / 0)

Tactic:
rw [jacobiTheta₂'_undef _ (by simp), mul_zero, zero_cpow (by simp), div_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, Complex.zero_cpow, jacobiTheta₂'_undef, div_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z τ : ℂ
hτ : τ ≠ 0
rw : -2 * (↑π : ℂ) = I * (2 * (↑π : ℂ) * I)
rw₁ : -2 * (↑π : ℂ) = 2 * (↑π : ℂ) * I * I
rw₂ : -2 * (↑π : ℂ) = 2 * (↑π : ℂ) * (I * I)
rw₃ : -2 * (↑π : ℂ) = 2 * (↑π : ℂ) * -1
rw₄ : -(2 * (↑π : ℂ)) = 2 * (↑π : ℂ) * -1
rw₅ : -(2 * (↑π : ℂ)) = -(2 * (↑π : ℂ) * 1)
rw₆ rw₇ : -(2 * (↑π : ℂ)) = -(2 * (↑π : ℂ))
⊢ -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I

Tactic:
rw [div_eq_iff two_pi_I_ne_zero, mul_comm I, mul_assoc _ I I, I_mul_I, neg_mul, mul_neg,
      mul_one]

Premises used: Complex.two_pi_I_ne_zero, mul_assoc, div_eq_iff, Complex.I_mul_I, mul_comm, neg_mul, mul_one, mul_neg, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z τ : ℂ
hτ : τ ≠ 0
⊢ -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I

Tactic:
have aux1 : (-2 * π : ℂ) / (2 * π * I) = I := by
    rw [div_eq_iff two_pi_I_ne_zero, mul_comm I, mul_assoc _ I I, I_mul_I, neg_mul, mul_neg,
      mul_one]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
rw : 1 / τ = -I / (-I * τ)
rw₁ : 1 / τ = -I / -I / τ
rw₂ rw₃ : 1 / τ = 1 / τ
⊢ 1 / τ = -I / HPow.hPow (β := ℂ) (-I * τ) 1

Tactic:
rw [cpow_one, ← div_div, div_self (neg_ne_zero.mpr I_ne_zero)]

Premises used: Iff.mpr, Complex.I_ne_zero, Complex.cpow_one, neg_ne_zero, div_div, div_self
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
⊢ 1 / 2 + 1 = 3 / 2

Tactic:
norm_num