awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
⊢ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2 =
    s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2 / s.Gammaℝ
have 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ℝ
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))]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
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ℝ
⊢ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2 =
    s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2 / s.Gammaℝ
have 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
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))]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
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
⊢ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2 =
    s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2 / s.Gammaℝ
have rw₂ : cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2 =
  cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2
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))]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun (n : ℕ) ↦ (↑(Real.cos (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (cosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have 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)
Tactic: have := (hasSum_int_cosZeta a hs).nat_add_neg
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
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 : ℕ) ↦ (↑(Real.cos (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (cosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have 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)
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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
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 : ℕ) ↦ (↑(Real.cos (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (cosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have 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)
Tactic: simp_rw [push_cast, Complex.cos, neg_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
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 : ℕ
⊢ (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
have 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
Tactic: rw [show 2 * π * a * n * I = 2 * π * I * a * n by ring]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : a ≠ 0 ∨ s ≠ 1
⊢ hurwitzZetaEven a (1 - s) = completedHurwitzZetaEven a (1 - s) * (1 - s).Gammaℝ⁻¹
have rw : a ≠ 0 ∨ 1 - s ≠ 0
Tactic: rw [hurwitzZetaEven_def_of_ne_or_ne, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : a ≠ 0 ∨ s ≠ 1
⊢ hurwitzZetaEven a (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * Complex.cos ((↑π : ℂ) * s / 2) * cosZeta a s
have this : 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'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
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ℝ⁻¹
⊢ hurwitzZetaEven a (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * Complex.cos ((↑π : ℂ) * s / 2) * cosZeta a s
have rw : completedCosZeta a s * (s.Gammaℂ * Complex.cos ((↑π : ℂ) * s / 2) * s.Gammaℝ⁻¹) =
  s.Gammaℂ * Complex.cos ((↑π : ℂ) * s / 2) * (completedCosZeta a s / s.Gammaℝ)
Tactic: rw [this, completedHurwitzZetaEven_one_sub, inv_Gammaℝ_one_sub hs, cosZeta,
    Function.update_of_ne (by simpa using hs 0), ← Gammaℂ]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
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ℝ⁻¹
⊢ completedCosZeta a s * (s.Gammaℂ * Complex.cos ((↑π : ℂ) * s / 2) * s.Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.cos ((↑π : ℂ) * s / 2) * (completedCosZeta a s / s.Gammaℝ)
have generalize : ∀ (A : ℂ), completedCosZeta a s * (A * s.Gammaℝ⁻¹) = A * (completedCosZeta a s / s.Gammaℝ)
Tactic: generalize Gammaℂ s * cos (π * s / 2) = A
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
⊢ cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
have h : 1 - s ≠ 0
Tactic: rw [cosZeta, Function.update_of_ne, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
⊢ cosZeta a (1 - s) = s.Gammaℂ * Complex.cos ((↑π : ℂ) * s / 2) * hurwitzZetaEven a s
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
⊢ cosZeta a (1 - s) = s.Gammaℂ * Complex.cos ((↑π : ℂ) * s / 2) * hurwitzZetaEven a s
have rw : completedHurwitzZetaEven a s * (s.Gammaℂ * Complex.cos ((↑π : ℂ) * s / 2) * s.Gammaℝ⁻¹) =
  s.Gammaℂ * Complex.cos ((↑π : ℂ) * s / 2) * (completedHurwitzZetaEven a s / s.Gammaℝ)
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))]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
⊢ completedHurwitzZetaEven a s * (s.Gammaℂ * Complex.cos ((↑π : ℂ) * s / 2) * s.Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.cos ((↑π : ℂ) * s / 2) * (completedHurwitzZetaEven a s / s.Gammaℝ)
have generalize : ∀ (A : ℂ), completedHurwitzZetaEven a s * (A * s.Gammaℝ⁻¹) = A * (completedHurwitzZetaEven a s / s.Gammaℝ)
Tactic: generalize Gammaℂ s * cos (π * s / 2) = A
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z τ : ℂ
⊢ jacobiTheta₂'' (z + 1) τ = jacobiTheta₂'' z τ
have 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 * τ) τ)
Tactic: simp only [jacobiTheta₂'', add_mul z 1, one_mul, jacobiTheta₂'_add_left', jacobiTheta₂_add_left']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z τ : ℂ
⊢ 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 * τ) τ)
have 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)
Tactic: generalize jacobiTheta₂ (z * τ) τ = J
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
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)
have 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)
Tactic: generalize jacobiTheta₂' (z * τ) τ = J'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z τ J 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)
have 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)
Tactic: simp_rw [div_add' _ _ _ two_pi_I_ne_zero, ← mul_div_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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)
have 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))
Tactic: refine congr_arg (· / (2 * π * I)) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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)) =
    cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ) * (J' + z * J * (2 * (↑π : ℂ) * I))
have 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))
Tactic: rw [mul_left_comm _ (cexp _), ← mul_add, mul_assoc (cexp _), ← mul_add, ← mul_assoc (cexp _),
    ← Complex.exp_add]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z τ J J' : ℂ
⊢ 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))
have refine_1 : (↑π : ℂ) * I * HPow.hPow (β := ℕ) (z + 1) 2 * τ + -(↑π : ℂ) * I * (τ + 2 * (z * τ)) =
  (↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ
Tactic: congrm (cexp ?_ * ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z τ J J' : ℂ
refine_1 :
  (↑π : ℂ) * I * HPow.hPow (β := ℕ) (z + 1) 2 * τ + -(↑π : ℂ) * I * (τ + 2 * (z * τ)) =
    (↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 * τ
⊢ 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))
have refine_2 : J' - 2 * (↑π : ℂ) * I * J + (z * J + J) * (2 * (↑π : ℂ) * I) = J' + z * J * (2 * (↑π : ℂ) * I)
Tactic: congrm (cexp ?_ * ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z τ : ℂ
⊢ jacobiTheta₂' z τ = -2 * (↑π : ℂ) / (-I * τ) ^ (3 / 2) * jacobiTheta₂'' z (-1 / τ)
have inl : jacobiTheta₂' z 0 = -2 * (↑π : ℂ) / (-I * 0) ^ (3 / 2) * jacobiTheta₂'' z (-1 / 0)
Tactic: rcases eq_or_ne τ 0 with rfl | hτ
Cleared hypotheses: τ
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z τ : ℂ
inl : jacobiTheta₂' z 0 = -2 * (↑π : ℂ) / (-I * 0) ^ (3 / 2) * jacobiTheta₂'' z (-1 / 0)
⊢ jacobiTheta₂' z τ = -2 * (↑π : ℂ) / (-I * τ) ^ (3 / 2) * jacobiTheta₂'' z (-1 / τ)
have inr : ∀ (hτ : τ ≠ 0), jacobiTheta₂' z τ = -2 * (↑π : ℂ) / (-I * τ) ^ (3 / 2) * jacobiTheta₂'' z (-1 / τ)
Tactic: rcases eq_or_ne τ 0 with rfl | hτ
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z : ℂ
⊢ jacobiTheta₂' z 0 = -2 * (↑π : ℂ) / (-I * 0) ^ (3 / 2) * jacobiTheta₂'' z (-1 / 0)
have inl : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z : ℂ
inl : 0 = -2 * (↑π : ℂ) / (-I * 0) ^ (3 / 2) * jacobiTheta₂'' z (-1 / 0)
⊢ jacobiTheta₂' z 0 = -2 * (↑π : ℂ) / (-I * 0) ^ (3 / 2) * jacobiTheta₂'' z (-1 / 0)
have inl₁ : 0 = -2 * (↑π : ℂ) / HPow.hPow (α := ℂ) 0 (3 / 2) * jacobiTheta₂'' z (-1 / 0)
Tactic: rw [jacobiTheta₂'_undef _ (by simp), mul_zero, zero_cpow (by simp), div_zero, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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)
⊢ jacobiTheta₂' z 0 = -2 * (↑π : ℂ) / (-I * 0) ^ (3 / 2) * jacobiTheta₂'' z (-1 / 0)
have inl₂ : 0 = -2 * (↑π : ℂ) / 0 * jacobiTheta₂'' z (-1 / 0)
Tactic: rw [jacobiTheta₂'_undef _ (by simp), mul_zero, zero_cpow (by simp), div_zero, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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)
⊢ jacobiTheta₂' z 0 = -2 * (↑π : ℂ) / (-I * 0) ^ (3 / 2) * jacobiTheta₂'' z (-1 / 0)
have inl₃ : 0 = 0 * jacobiTheta₂'' z (-1 / 0)
Tactic: rw [jacobiTheta₂'_undef _ (by simp), mul_zero, zero_cpow (by simp), div_zero, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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)
⊢ jacobiTheta₂' z 0 = -2 * (↑π : ℂ) / (-I * 0) ^ (3 / 2) * jacobiTheta₂'' z (-1 / 0)
have inl₄ : Eq (α := ℂ) 0 0
Tactic: rw [jacobiTheta₂'_undef _ (by simp), mul_zero, zero_cpow (by simp), div_zero, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z τ : ℂ
hτ : τ ≠ 0
⊢ -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
have rw : -2 * (↑π : ℂ) = I * (2 * (↑π : ℂ) * 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z τ : ℂ
hτ : τ ≠ 0
rw : -2 * (↑π : ℂ) = I * (2 * (↑π : ℂ) * I)
⊢ -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
have rw₁ : -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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z τ : ℂ
hτ : τ ≠ 0
rw : -2 * (↑π : ℂ) = I * (2 * (↑π : ℂ) * I)
rw₁ : -2 * (↑π : ℂ) = 2 * (↑π : ℂ) * I * I
⊢ -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
have rw₂ : -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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z τ : ℂ
hτ : τ ≠ 0
rw : -2 * (↑π : ℂ) = I * (2 * (↑π : ℂ) * I)
rw₁ : -2 * (↑π : ℂ) = 2 * (↑π : ℂ) * I * I
rw₂ : -2 * (↑π : ℂ) = 2 * (↑π : ℂ) * (I * I)
⊢ -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
have rw₃ : -2 * (↑π : ℂ) = 2 * (↑π : ℂ) * -1
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z τ : ℂ
hτ : τ ≠ 0
rw : -2 * (↑π : ℂ) = I * (2 * (↑π : ℂ) * I)
rw₁ : -2 * (↑π : ℂ) = 2 * (↑π : ℂ) * I * I
rw₂ : -2 * (↑π : ℂ) = 2 * (↑π : ℂ) * (I * I)
rw₃ : -2 * (↑π : ℂ) = 2 * (↑π : ℂ) * -1
⊢ -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
have rw₄ : -(2 * (↑π : ℂ)) = 2 * (↑π : ℂ) * -1
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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
⊢ -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
have rw₅ : -(2 * (↑π : ℂ)) = -(2 * (↑π : ℂ) * 1)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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)
⊢ -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
have rw₆ : -(2 * (↑π : ℂ)) = -(2 * (↑π : ℂ))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (hypothesis)
Goal:
z τ : ℂ
hτ : τ ≠ 0
⊢ jacobiTheta₂' z τ = -2 * (↑π : ℂ) / (-I * τ) ^ (3 / 2) * jacobiTheta₂'' z (-1 / τ)
have aux1 : -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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
⊢ 1 / τ = -I / HPow.hPow (β := ℂ) (-I * τ) 1
have rw : 1 / τ = -I / (-I * τ)
Tactic: rw [cpow_one, ← div_div, div_self (neg_ne_zero.mpr I_ne_zero)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
rw : 1 / τ = -I / (-I * τ)
⊢ 1 / τ = -I / HPow.hPow (β := ℂ) (-I * τ) 1
have rw₁ : 1 / τ = -I / -I / τ
Tactic: rw [cpow_one, ← div_div, div_self (neg_ne_zero.mpr I_ne_zero)]