awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
rw : 1 / τ = -I / (-I * τ)
rw₁ : 1 / τ = -I / -I / τ
⊢ 1 / τ = -I / HPow.hPow (β := ℂ) (-I * τ) 1
have rw₂ : 1 / τ = 1 / τ
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
⊢ jacobiTheta₂' z τ = -2 * (↑π : ℂ) / (-I * τ) ^ (3 / 2) * jacobiTheta₂'' z (-1 / τ)
have inr : 1 / (-I * τ) ^ (3 / 2) *
    (-I * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))) =
  1 / (-I * τ) ^ (3 / 2) * (-2 * (↑π : ℂ) * jacobiTheta₂'' z (-1 / τ))
Tactic: rw [jacobiTheta₂'_functional_equation, ← mul_one_div _ τ, mul_right_comm _ (cexp _),
    (by rw [cpow_one, ← div_div, div_self (neg_ne_zero.mpr I_ne_zero)] :
      1 / τ = -I / (-I * τ) ^ (1 : ℂ)), div_mul_div_comm,
    ← cpow_add _ _ (mul_ne_zero (neg_ne_zero.mpr I_ne_zero) hτ), ← div_mul_eq_mul_div,
    (by norm_num : (1 / 2 + 1 : ℂ) = 3 / 2), mul_assoc (1 / _), mul_assoc (1 / _),
    ← mul_one_div (-2 * π : ℂ), mul_comm _ (1 / _), mul_assoc (1 / _)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
⊢ 1 / (-I * τ) ^ (3 / 2) *
      (-I * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) *
        (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ))) =
    1 / (-I * τ) ^ (3 / 2) * (-2 * (↑π : ℂ) * jacobiTheta₂'' z (-1 / τ))
have inr : -I * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) *
    (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ)) =
  -2 * (↑π : ℂ) * jacobiTheta₂'' z (-1 / τ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
⊢ -I * cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ) *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-1 / τ)) =
    -2 * (↑π : ℂ) * jacobiTheta₂'' z (-1 / τ)
have inr : I *
    (cexp (-((↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ)) *
      -(jacobiTheta₂' (z / τ) (-(1 / τ)) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)))) =
  I *
    (cexp (-((↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ)) *
      (-jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * (↑π : ℂ) * I)))
Tactic: rw [jacobiTheta₂'', div_add' _ _ _ two_pi_I_ne_zero, ← mul_div_assoc, ← mul_div_assoc,
    ← div_mul_eq_mul_div (-2 * π : ℂ), mul_assoc, aux1, mul_div z (-1), mul_neg_one, neg_div τ z,
    jacobiTheta₂_neg_left, jacobiTheta₂'_neg_left, neg_mul, ← mul_neg, ← mul_neg,
    mul_div, mul_neg_one, neg_div, neg_mul, neg_mul, neg_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
⊢ I *
      (cexp (-((↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ)) *
        -(jacobiTheta₂' (z / τ) (-(1 / τ)) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)))) =
    I *
      (cexp (-((↑π : ℂ) * I * HPow.hPow (β := ℕ) z 2 / τ)) *
        (-jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * (↑π : ℂ) * I)))
have inr : -(jacobiTheta₂' (z / τ) (-(1 / τ)) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ))) =
  -jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * (↑π : ℂ) * I)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
⊢ -(jacobiTheta₂' (z / τ) (-(1 / τ)) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ))) =
    -jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * (↑π : ℂ) * I)
have inr : 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)) - jacobiTheta₂' (z / τ) (-(1 / τ)) =
  -jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * (↑π : ℂ) * I)
Tactic: rw [neg_sub, ← sub_eq_neg_add, mul_comm _ (_ * I), ← mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
inr :
  2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)) - jacobiTheta₂' (z / τ) (-(1 / τ)) =
    -jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * (↑π : ℂ) * I)
⊢ -(jacobiTheta₂' (z / τ) (-(1 / τ)) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ))) =
    -jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * (↑π : ℂ) * I)
have inr₁ : 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)) - jacobiTheta₂' (z / τ) (-(1 / τ)) =
  z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * (↑π : ℂ) * I) - jacobiTheta₂' (z / τ) (-(1 / τ))
Tactic: rw [neg_sub, ← sub_eq_neg_add, mul_comm _ (_ * I), ← mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
inr :
  2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)) - jacobiTheta₂' (z / τ) (-(1 / τ)) =
    -jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * (↑π : ℂ) * I)
inr₁ :
  2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)) - jacobiTheta₂' (z / τ) (-(1 / τ)) =
    z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * (↑π : ℂ) * I) - jacobiTheta₂' (z / τ) (-(1 / τ))
⊢ -(jacobiTheta₂' (z / τ) (-(1 / τ)) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ))) =
    -jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * (↑π : ℂ) * I)
have inr₂ : 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)) - jacobiTheta₂' (z / τ) (-(1 / τ)) =
  2 * (↑π : ℂ) * I * (z * jacobiTheta₂ (z / τ) (-(1 / τ))) - jacobiTheta₂' (z / τ) (-(1 / τ))
Tactic: rw [neg_sub, ← sub_eq_neg_add, mul_comm _ (_ * I), ← mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * (↑π : ℂ) / (2 * (↑π : ℂ) * I) = I
inr :
  2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)) - jacobiTheta₂' (z / τ) (-(1 / τ)) =
    -jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * (↑π : ℂ) * I)
inr₁ :
  2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)) - jacobiTheta₂' (z / τ) (-(1 / τ)) =
    z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * (↑π : ℂ) * I) - jacobiTheta₂' (z / τ) (-(1 / τ))
inr₂ :
  2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)) - jacobiTheta₂' (z / τ) (-(1 / τ)) =
    2 * (↑π : ℂ) * I * (z * jacobiTheta₂ (z / τ) (-(1 / τ))) - jacobiTheta₂' (z / τ) (-(1 / τ))
⊢ -(jacobiTheta₂' (z / τ) (-(1 / τ)) - 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ))) =
    -jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * (↑π : ℂ) * I)
have inr₃ : 2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)) - jacobiTheta₂' (z / τ) (-(1 / τ)) =
  2 * (↑π : ℂ) * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)) - jacobiTheta₂' (z / τ) (-(1 / τ))
Tactic: rw [neg_sub, ← sub_eq_neg_add, mul_comm _ (_ * I), ← mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a x : ℝ
⊢ (↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
have rw : jacobiTheta₂'' (↑a : ℂ) (I * (↑x : ℂ)) =
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
      (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
Tactic: rw [oddKernel_def, jacobiTheta₂'', ← mul_assoc ↑a I x,
    (by ring : ↑π * I * ↑a ^ 2 * (I * ↑x) = I ^ 2 * ↑π * ↑a ^ 2 * x), I_sq, neg_one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a x : ℝ
rw :
  jacobiTheta₂'' (↑a : ℂ) (I * (↑x : ℂ)) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
⊢ (↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
have rw₁ : cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (I * (↑x : ℂ))) *
    (jacobiTheta₂' ((↑a : ℂ) * (I * (↑x : ℂ))) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
      (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * (I * (↑x : ℂ))) (I * (↑x : ℂ))) =
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
      (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
Tactic: rw [oddKernel_def, jacobiTheta₂'', ← mul_assoc ↑a I x,
    (by ring : ↑π * I * ↑a ^ 2 * (I * ↑x) = I ^ 2 * ↑π * ↑a ^ 2 * x), I_sq, neg_one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a x : ℝ
rw :
  jacobiTheta₂'' (↑a : ℂ) (I * (↑x : ℂ)) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
rw₁ :
  cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (I * (↑x : ℂ))) *
      (jacobiTheta₂' ((↑a : ℂ) * (I * (↑x : ℂ))) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * (I * (↑x : ℂ))) (I * (↑x : ℂ))) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
⊢ (↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
have rw₂ : cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (I * (↑x : ℂ))) *
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
      (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))) =
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
      (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
Tactic: rw [oddKernel_def, jacobiTheta₂'', ← mul_assoc ↑a I x,
    (by ring : ↑π * I * ↑a ^ 2 * (I * ↑x) = I ^ 2 * ↑π * ↑a ^ 2 * x), I_sq, neg_one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a x : ℝ
rw :
  jacobiTheta₂'' (↑a : ℂ) (I * (↑x : ℂ)) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
rw₁ :
  cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (I * (↑x : ℂ))) *
      (jacobiTheta₂' ((↑a : ℂ) * (I * (↑x : ℂ))) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * (I * (↑x : ℂ))) (I * (↑x : ℂ))) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
rw₂ :
  cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (I * (↑x : ℂ))) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
⊢ (↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
have rw₃ : cexp (HPow.hPow (β := ℕ) I 2 * (↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
      (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))) =
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
      (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
Tactic: rw [oddKernel_def, jacobiTheta₂'', ← mul_assoc ↑a I x,
    (by ring : ↑π * I * ↑a ^ 2 * (I * ↑x) = I ^ 2 * ↑π * ↑a ^ 2 * x), I_sq, neg_one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a x : ℝ
rw :
  jacobiTheta₂'' (↑a : ℂ) (I * (↑x : ℂ)) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
rw₁ :
  cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (I * (↑x : ℂ))) *
      (jacobiTheta₂' ((↑a : ℂ) * (I * (↑x : ℂ))) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * (I * (↑x : ℂ))) (I * (↑x : ℂ))) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
rw₂ :
  cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (I * (↑x : ℂ))) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
rw₃ :
  cexp (HPow.hPow (β := ℕ) I 2 * (↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
⊢ (↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
have rw₄ : cexp (-1 * (↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
      (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))) =
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
      (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
Tactic: rw [oddKernel_def, jacobiTheta₂'', ← mul_assoc ↑a I x,
    (by ring : ↑π * I * ↑a ^ 2 * (I * ↑x) = I ^ 2 * ↑π * ↑a ^ 2 * x), I_sq, neg_one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a x : ℝ
rw :
  jacobiTheta₂'' (↑a : ℂ) (I * (↑x : ℂ)) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
rw₁ :
  cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (I * (↑x : ℂ))) *
      (jacobiTheta₂' ((↑a : ℂ) * (I * (↑x : ℂ))) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * (I * (↑x : ℂ))) (I * (↑x : ℂ))) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
rw₂ :
  cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (I * (↑x : ℂ))) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
rw₃ :
  cexp (HPow.hPow (β := ℕ) I 2 * (↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
rw₄ :
  cexp (-1 * (↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
⊢ (↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
have rw₅ : cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
      (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))) =
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
      (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
Tactic: rw [oddKernel_def, jacobiTheta₂'', ← mul_assoc ↑a I x,
    (by ring : ↑π * I * ↑a ^ 2 * (I * ↑x) = I ^ 2 * ↑π * ↑a ^ 2 * x), I_sq, neg_one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : x ≤ 0
a' : ℝ
⊢ oddKernel (↑a' : ℝ ⧸ AddSubgroup.zmultiples 1) x = 0
have H : (I * (↑x : ℂ)).im ≤ 0
Tactic: rw [← ofReal_eq_zero, oddKernel_def', jacobiTheta₂_undef, jacobiTheta₂'_undef, zero_div, zero_add,
    mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ oddKernel a x = 0
have H : ∀ (a' : ℝ), oddKernel (↑a' : ℝ ⧸ AddSubgroup.zmultiples 1) x = 0
Tactic: induction a using QuotientAddGroup.induction_on with | H a' =>
  rw [← ofReal_eq_zero, oddKernel_def', jacobiTheta₂_undef, jacobiTheta₂'_undef, zero_div, zero_add,
    mul_zero, mul_zero] <;>
  simpa
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : x ≤ 0
a : ℝ
⊢ sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x = 0
have H : (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ) = 0
Tactic: rw [← ofReal_eq_zero, sinKernel_def, jacobiTheta₂'_undef _ (by simpa), zero_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : x ≤ 0
a : ℝ
H : (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ) = 0
⊢ sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x = 0
have H₁ : jacobiTheta₂' (↑a : ℂ) (I * (↑x : ℂ)) / (-2 * (↑π : ℂ)) = 0
Tactic: rw [← ofReal_eq_zero, sinKernel_def, jacobiTheta₂'_undef _ (by simpa), zero_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : x ≤ 0
a : ℝ
H : (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ) = 0
H₁ : jacobiTheta₂' (↑a : ℂ) (I * (↑x : ℂ)) / (-2 * (↑π : ℂ)) = 0
⊢ sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x = 0
have H₂ : 0 / (-2 * (↑π : ℂ)) = 0
Tactic: rw [← ofReal_eq_zero, sinKernel_def, jacobiTheta₂'_undef _ (by simpa), zero_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : x ≤ 0
a : ℝ
H : (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ) = 0
H₁ : jacobiTheta₂' (↑a : ℂ) (I * (↑x : ℂ)) / (-2 * (↑π : ℂ)) = 0
H₂ : 0 / (-2 * (↑π : ℂ)) = 0
⊢ sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x = 0
have H₃ : Eq (α := ℂ) 0 0
Tactic: rw [← ofReal_eq_zero, sinKernel_def, jacobiTheta₂'_undef _ (by simpa), zero_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ sinKernel a x = 0
have H : ∀ (a : ℝ), sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x = 0
Tactic: induction a using QuotientAddGroup.induction_on with
  | H a => rw [← ofReal_eq_zero, sinKernel_def, jacobiTheta₂'_undef _ (by simpa), zero_div]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
x : ℝ
⊢ oddKernel (-a) x = -oddKernel a x
have H : ∀ (a : ℝ), oddKernel (-(↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) x = -oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x
Tactic: induction a using QuotientAddGroup.induction_on with
  | H a => simp [← ofReal_inj, ← QuotientAddGroup.mk_neg, oddKernel_def, jacobiTheta₂''_neg_left]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
x : ℝ
⊢ sinKernel (-a) x = -sinKernel a x
have H : ∀ (a : ℝ), sinKernel (-(↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) x = -sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x
Tactic: induction a using QuotientAddGroup.induction_on with
  | H a => simp [← ofReal_inj, ← QuotientAddGroup.mk_neg, sinKernel_def, jacobiTheta₂'_neg_left,
      neg_div]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
⊢ ContinuousOn (oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) (Ioi 0)
have H : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ)) (Ioi 0)
Tactic: suffices ContinuousOn (fun x ↦ (oddKernel a x : ℂ)) (Ioi 0) from
    (continuous_re.comp_continuousOn this).congr fun a _ ↦ (ofReal_re _).symm
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ)) (Ioi 0)
have H : ContinuousOn (Y := ℂ)
  (fun (x : ℝ) ↦
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))))
  (Ioi 0)
Tactic: simp_rw [oddKernel_def' a]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
⊢ ContinuousOn (Y := ℂ)
    (fun (x : ℝ) ↦
      cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
        (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
          (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))))
    (Ioi 0)
have H : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
  Continuous (Y := ℂ) fun (x : ℝ) ↦ cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ))
Tactic: refine fun x hx ↦ ((Continuous.continuousAt ?_).mul ?_).continuousWithinAt