awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
h2 : -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
h3 : (↑x : ℂ) ^ (3 / 2) ≠ 0
h4 : (↑x : ℂ).arg ≠ π
J : ℂ
inr : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (↑x : ℂ)⁻¹ ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₁ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / ((↑x : ℂ) ^ (3 / 2))⁻¹ * J / (-2 * (↑π : ℂ)))
⊢ J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (1 / (↑x : ℂ)) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
have inr₂ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
Tactic: rw [one_div (x : ℂ), inv_cpow _ _ h4, div_inv_eq_mul, one_div, ofReal_inv, ofReal_cpow hx.le,
    ofReal_div, ofReal_ofNat, ofReal_ofNat, ← mul_div_assoc _ _ (-2 * π : ℂ),
    eq_div_iff <| mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (ofReal_ne_zero.mpr pi_ne_zero),
    ← div_eq_inv_mul, eq_div_iff h3, mul_comm J _, mul_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
h2 : -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
h3 : (↑x : ℂ) ^ (3 / 2) ≠ 0
h4 : (↑x : ℂ).arg ≠ π
J : ℂ
inr : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (↑x : ℂ)⁻¹ ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₁ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / ((↑x : ℂ) ^ (3 / 2))⁻¹ * J / (-2 * (↑π : ℂ)))
inr₂ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
⊢ J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (1 / (↑x : ℂ)) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
have inr₃ : J = (↑(x ^ (3 / 2))⁻¹ : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
Tactic: rw [one_div (x : ℂ), inv_cpow _ _ h4, div_inv_eq_mul, one_div, ofReal_inv, ofReal_cpow hx.le,
    ofReal_div, ofReal_ofNat, ofReal_ofNat, ← mul_div_assoc _ _ (-2 * π : ℂ),
    eq_div_iff <| mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (ofReal_ne_zero.mpr pi_ne_zero),
    ← div_eq_inv_mul, eq_div_iff h3, mul_comm J _, mul_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
h2 : -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
h3 : (↑x : ℂ) ^ (3 / 2) ≠ 0
h4 : (↑x : ℂ).arg ≠ π
J : ℂ
inr : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (↑x : ℂ)⁻¹ ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₁ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / ((↑x : ℂ) ^ (3 / 2))⁻¹ * J / (-2 * (↑π : ℂ)))
inr₂ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₃ : J = (↑(x ^ (3 / 2))⁻¹ : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
⊢ J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (1 / (↑x : ℂ)) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
have inr₄ : J = (↑(x ^ (3 / 2)) : ℂ)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
Tactic: rw [one_div (x : ℂ), inv_cpow _ _ h4, div_inv_eq_mul, one_div, ofReal_inv, ofReal_cpow hx.le,
    ofReal_div, ofReal_ofNat, ofReal_ofNat, ← mul_div_assoc _ _ (-2 * π : ℂ),
    eq_div_iff <| mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (ofReal_ne_zero.mpr pi_ne_zero),
    ← div_eq_inv_mul, eq_div_iff h3, mul_comm J _, mul_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
h2 : -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
h3 : (↑x : ℂ) ^ (3 / 2) ≠ 0
h4 : (↑x : ℂ).arg ≠ π
J : ℂ
inr : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (↑x : ℂ)⁻¹ ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₁ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / ((↑x : ℂ) ^ (3 / 2))⁻¹ * J / (-2 * (↑π : ℂ)))
inr₂ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₃ : J = (↑(x ^ (3 / 2))⁻¹ : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₄ : J = (↑(x ^ (3 / 2)) : ℂ)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
⊢ J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (1 / (↑x : ℂ)) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
have inr₅ : J = ((↑x : ℂ) ^ (↑(3 / 2) : ℂ))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
Tactic: rw [one_div (x : ℂ), inv_cpow _ _ h4, div_inv_eq_mul, one_div, ofReal_inv, ofReal_cpow hx.le,
    ofReal_div, ofReal_ofNat, ofReal_ofNat, ← mul_div_assoc _ _ (-2 * π : ℂ),
    eq_div_iff <| mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (ofReal_ne_zero.mpr pi_ne_zero),
    ← div_eq_inv_mul, eq_div_iff h3, mul_comm J _, mul_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
h2 : -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
h3 : (↑x : ℂ) ^ (3 / 2) ≠ 0
h4 : (↑x : ℂ).arg ≠ π
J : ℂ
inr : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (↑x : ℂ)⁻¹ ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₁ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / ((↑x : ℂ) ^ (3 / 2))⁻¹ * J / (-2 * (↑π : ℂ)))
inr₂ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₃ : J = (↑(x ^ (3 / 2))⁻¹ : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₄ : J = (↑(x ^ (3 / 2)) : ℂ)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₅ : J = ((↑x : ℂ) ^ (↑(3 / 2) : ℂ))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
⊢ J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (1 / (↑x : ℂ)) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
have inr₆ : J = ((↑x : ℂ) ^ ((↑3 : ℂ) / (↑2 : ℂ)))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
Tactic: rw [one_div (x : ℂ), inv_cpow _ _ h4, div_inv_eq_mul, one_div, ofReal_inv, ofReal_cpow hx.le,
    ofReal_div, ofReal_ofNat, ofReal_ofNat, ← mul_div_assoc _ _ (-2 * π : ℂ),
    eq_div_iff <| mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (ofReal_ne_zero.mpr pi_ne_zero),
    ← div_eq_inv_mul, eq_div_iff h3, mul_comm J _, mul_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
h2 : -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
h3 : (↑x : ℂ) ^ (3 / 2) ≠ 0
h4 : (↑x : ℂ).arg ≠ π
J : ℂ
inr : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (↑x : ℂ)⁻¹ ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₁ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / ((↑x : ℂ) ^ (3 / 2))⁻¹ * J / (-2 * (↑π : ℂ)))
inr₂ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₃ : J = (↑(x ^ (3 / 2))⁻¹ : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₄ : J = (↑(x ^ (3 / 2)) : ℂ)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₅ : J = ((↑x : ℂ) ^ (↑(3 / 2) : ℂ))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₆ : J = ((↑x : ℂ) ^ ((↑3 : ℂ) / (↑2 : ℂ)))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
⊢ J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (1 / (↑x : ℂ)) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
have inr₇ : J = ((↑x : ℂ) ^ (3 / (↑2 : ℂ)))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
Tactic: rw [one_div (x : ℂ), inv_cpow _ _ h4, div_inv_eq_mul, one_div, ofReal_inv, ofReal_cpow hx.le,
    ofReal_div, ofReal_ofNat, ofReal_ofNat, ← mul_div_assoc _ _ (-2 * π : ℂ),
    eq_div_iff <| mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (ofReal_ne_zero.mpr pi_ne_zero),
    ← div_eq_inv_mul, eq_div_iff h3, mul_comm J _, mul_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
h2 : -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
h3 : (↑x : ℂ) ^ (3 / 2) ≠ 0
h4 : (↑x : ℂ).arg ≠ π
J : ℂ
inr : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (↑x : ℂ)⁻¹ ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₁ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / ((↑x : ℂ) ^ (3 / 2))⁻¹ * J / (-2 * (↑π : ℂ)))
inr₂ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₃ : J = (↑(x ^ (3 / 2))⁻¹ : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₄ : J = (↑(x ^ (3 / 2)) : ℂ)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₅ : J = ((↑x : ℂ) ^ (↑(3 / 2) : ℂ))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₆ : J = ((↑x : ℂ) ^ ((↑3 : ℂ) / (↑2 : ℂ)))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₇ : J = ((↑x : ℂ) ^ (3 / (↑2 : ℂ)))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
⊢ J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (1 / (↑x : ℂ)) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
have inr₈ : J = ((↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 3 2)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
Tactic: rw [one_div (x : ℂ), inv_cpow _ _ h4, div_inv_eq_mul, one_div, ofReal_inv, ofReal_cpow hx.le,
    ofReal_div, ofReal_ofNat, ofReal_ofNat, ← mul_div_assoc _ _ (-2 * π : ℂ),
    eq_div_iff <| mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (ofReal_ne_zero.mpr pi_ne_zero),
    ← div_eq_inv_mul, eq_div_iff h3, mul_comm J _, mul_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
h2 : -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
h3 : (↑x : ℂ) ^ (3 / 2) ≠ 0
h4 : (↑x : ℂ).arg ≠ π
J : ℂ
inr : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (↑x : ℂ)⁻¹ ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₁ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / ((↑x : ℂ) ^ (3 / 2))⁻¹ * J / (-2 * (↑π : ℂ)))
inr₂ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₃ : J = (↑(x ^ (3 / 2))⁻¹ : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₄ : J = (↑(x ^ (3 / 2)) : ℂ)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₅ : J = ((↑x : ℂ) ^ (↑(3 / 2) : ℂ))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₆ : J = ((↑x : ℂ) ^ ((↑3 : ℂ) / (↑2 : ℂ)))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₇ : J = ((↑x : ℂ) ^ (3 / (↑2 : ℂ)))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₈ : J = ((↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 3 2)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
⊢ J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (1 / (↑x : ℂ)) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
have inr₉ : J = ((↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 3 2)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J) / (-2 * (↑π : ℂ))
Tactic: rw [one_div (x : ℂ), inv_cpow _ _ h4, div_inv_eq_mul, one_div, ofReal_inv, ofReal_cpow hx.le,
    ofReal_div, ofReal_ofNat, ofReal_ofNat, ← mul_div_assoc _ _ (-2 * π : ℂ),
    eq_div_iff <| mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (ofReal_ne_zero.mpr pi_ne_zero),
    ← div_eq_inv_mul, eq_div_iff h3, mul_comm J _, mul_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
h2 : -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
h3 : (↑x : ℂ) ^ (3 / 2) ≠ 0
h4 : (↑x : ℂ).arg ≠ π
J : ℂ
inr : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (↑x : ℂ)⁻¹ ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₁ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / ((↑x : ℂ) ^ (3 / 2))⁻¹ * J / (-2 * (↑π : ℂ)))
inr₂ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₃ : J = (↑(x ^ (3 / 2))⁻¹ : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₄ : J = (↑(x ^ (3 / 2)) : ℂ)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₅ : J = ((↑x : ℂ) ^ (↑(3 / 2) : ℂ))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₆ : J = ((↑x : ℂ) ^ ((↑3 : ℂ) / (↑2 : ℂ)))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₇ : J = ((↑x : ℂ) ^ (3 / (↑2 : ℂ)))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₈ : J = ((↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 3 2)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₉ : J = ((↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 3 2)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J) / (-2 * (↑π : ℂ))
⊢ J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (1 / (↑x : ℂ)) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
have inr₁₀ : J * (-2 * (↑π : ℂ)) = ((↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 3 2)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J)
Tactic: rw [one_div (x : ℂ), inv_cpow _ _ h4, div_inv_eq_mul, one_div, ofReal_inv, ofReal_cpow hx.le,
    ofReal_div, ofReal_ofNat, ofReal_ofNat, ← mul_div_assoc _ _ (-2 * π : ℂ),
    eq_div_iff <| mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (ofReal_ne_zero.mpr pi_ne_zero),
    ← div_eq_inv_mul, eq_div_iff h3, mul_comm J _, mul_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
h2 : -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
h3 : (↑x : ℂ) ^ (3 / 2) ≠ 0
h4 : (↑x : ℂ).arg ≠ π
J : ℂ
inr : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (↑x : ℂ)⁻¹ ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₁ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / ((↑x : ℂ) ^ (3 / 2))⁻¹ * J / (-2 * (↑π : ℂ)))
inr₂ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₃ : J = (↑(x ^ (3 / 2))⁻¹ : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₄ : J = (↑(x ^ (3 / 2)) : ℂ)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₅ : J = ((↑x : ℂ) ^ (↑(3 / 2) : ℂ))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₆ : J = ((↑x : ℂ) ^ ((↑3 : ℂ) / (↑2 : ℂ)))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₇ : J = ((↑x : ℂ) ^ (3 / (↑2 : ℂ)))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₈ : J = ((↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 3 2)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₉ : J = ((↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 3 2)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J) / (-2 * (↑π : ℂ))
inr₁₀ : J * (-2 * (↑π : ℂ)) = ((↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 3 2)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J)
⊢ J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (1 / (↑x : ℂ)) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
have inr₁₁ : J * (-2 * (↑π : ℂ)) = -2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 3 2
Tactic: rw [one_div (x : ℂ), inv_cpow _ _ h4, div_inv_eq_mul, one_div, ofReal_inv, ofReal_cpow hx.le,
    ofReal_div, ofReal_ofNat, ofReal_ofNat, ← mul_div_assoc _ _ (-2 * π : ℂ),
    eq_div_iff <| mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (ofReal_ne_zero.mpr pi_ne_zero),
    ← div_eq_inv_mul, eq_div_iff h3, mul_comm J _, mul_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
h2 : -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
h3 : (↑x : ℂ) ^ (3 / 2) ≠ 0
h4 : (↑x : ℂ).arg ≠ π
J : ℂ
inr : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (↑x : ℂ)⁻¹ ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₁ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / ((↑x : ℂ) ^ (3 / 2))⁻¹ * J / (-2 * (↑π : ℂ)))
inr₂ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₃ : J = (↑(x ^ (3 / 2))⁻¹ : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₄ : J = (↑(x ^ (3 / 2)) : ℂ)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₅ : J = ((↑x : ℂ) ^ (↑(3 / 2) : ℂ))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₆ : J = ((↑x : ℂ) ^ ((↑3 : ℂ) / (↑2 : ℂ)))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₇ : J = ((↑x : ℂ) ^ (3 / (↑2 : ℂ)))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₈ : J = ((↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 3 2)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₉ : J = ((↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 3 2)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J) / (-2 * (↑π : ℂ))
inr₁₀ : J * (-2 * (↑π : ℂ)) = ((↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 3 2)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J)
inr₁₁ : J * (-2 * (↑π : ℂ)) = -2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 3 2
⊢ J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (1 / (↑x : ℂ)) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
have inr₁₂ : J * (-2 * (↑π : ℂ)) * (↑x : ℂ) ^ (3 / 2) = -2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J
Tactic: rw [one_div (x : ℂ), inv_cpow _ _ h4, div_inv_eq_mul, one_div, ofReal_inv, ofReal_cpow hx.le,
    ofReal_div, ofReal_ofNat, ofReal_ofNat, ← mul_div_assoc _ _ (-2 * π : ℂ),
    eq_div_iff <| mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (ofReal_ne_zero.mpr pi_ne_zero),
    ← div_eq_inv_mul, eq_div_iff h3, mul_comm J _, mul_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
h2 : -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
h3 : (↑x : ℂ) ^ (3 / 2) ≠ 0
h4 : (↑x : ℂ).arg ≠ π
J : ℂ
inr : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (↑x : ℂ)⁻¹ ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₁ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / ((↑x : ℂ) ^ (3 / 2))⁻¹ * J / (-2 * (↑π : ℂ)))
inr₂ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₃ : J = (↑(x ^ (3 / 2))⁻¹ : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₄ : J = (↑(x ^ (3 / 2)) : ℂ)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₅ : J = ((↑x : ℂ) ^ (↑(3 / 2) : ℂ))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₆ : J = ((↑x : ℂ) ^ ((↑3 : ℂ) / (↑2 : ℂ)))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₇ : J = ((↑x : ℂ) ^ (3 / (↑2 : ℂ)))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₈ : J = ((↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 3 2)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₉ : J = ((↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 3 2)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J) / (-2 * (↑π : ℂ))
inr₁₀ : J * (-2 * (↑π : ℂ)) = ((↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 3 2)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J)
inr₁₁ : J * (-2 * (↑π : ℂ)) = -2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 3 2
inr₁₂ : J * (-2 * (↑π : ℂ)) * (↑x : ℂ) ^ (3 / 2) = -2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J
⊢ J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (1 / (↑x : ℂ)) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
have inr₁₃ : -2 * (↑π : ℂ) * J * (↑x : ℂ) ^ (3 / 2) = -2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J
Tactic: rw [one_div (x : ℂ), inv_cpow _ _ h4, div_inv_eq_mul, one_div, ofReal_inv, ofReal_cpow hx.le,
    ofReal_div, ofReal_ofNat, ofReal_ofNat, ← mul_div_assoc _ _ (-2 * π : ℂ),
    eq_div_iff <| mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (ofReal_ne_zero.mpr pi_ne_zero),
    ← div_eq_inv_mul, eq_div_iff h3, mul_comm J _, mul_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * (↑(1 / x) : ℂ)) = I * (↑x : ℂ)
h2 : -I * (I * (↑(1 / x) : ℂ)) = 1 / (↑x : ℂ)
h3 : (↑x : ℂ) ^ (3 / 2) ≠ 0
h4 : (↑x : ℂ).arg ≠ π
J : ℂ
inr : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (↑x : ℂ)⁻¹ ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₁ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / ((↑x : ℂ) ^ (3 / 2))⁻¹ * J / (-2 * (↑π : ℂ)))
inr₂ : J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₃ : J = (↑(x ^ (3 / 2))⁻¹ : ℂ) * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₄ : J = (↑(x ^ (3 / 2)) : ℂ)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₅ : J = ((↑x : ℂ) ^ (↑(3 / 2) : ℂ))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₆ : J = ((↑x : ℂ) ^ ((↑3 : ℂ) / (↑2 : ℂ)))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₇ : J = ((↑x : ℂ) ^ (3 / (↑2 : ℂ)))⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₈ : J = ((↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 3 2)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
inr₉ : J = ((↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 3 2)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J) / (-2 * (↑π : ℂ))
inr₁₀ : J * (-2 * (↑π : ℂ)) = ((↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 3 2)⁻¹ * (-2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J)
inr₁₁ : J * (-2 * (↑π : ℂ)) = -2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J / (↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 3 2
inr₁₂ : J * (-2 * (↑π : ℂ)) * (↑x : ℂ) ^ (3 / 2) = -2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J
inr₁₃ : -2 * (↑π : ℂ) * J * (↑x : ℂ) ^ (3 / 2) = -2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J
⊢ J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (1 / (↑x : ℂ)) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
have inr₁₄ : -2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J = -2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J
Tactic: rw [one_div (x : ℂ), inv_cpow _ _ h4, div_inv_eq_mul, one_div, ofReal_inv, ofReal_cpow hx.le,
    ofReal_div, ofReal_ofNat, ofReal_ofNat, ← mul_div_assoc _ _ (-2 * π : ℂ),
    eq_div_iff <| mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (ofReal_ne_zero.mpr pi_ne_zero),
    ← div_eq_inv_mul, eq_div_iff h3, mul_comm J _, mul_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
x : ℝ
hx : 0 < x
⊢ oddKernel a x = 1 / x ^ (3 / 2) * sinKernel a (1 / x)
have inr : ∀ (a : ℝ),
  oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x =
    1 / x ^ (3 / 2) * sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) (1 / x)
Tactic: induction a using QuotientAddGroup.induction_on with | H a =>
  have h1 : -1 / (I * ↑(1 / x)) = I * x := by rw [one_div, ofReal_inv, mul_comm, ← div_div,
    div_inv_eq_mul, div_eq_mul_inv, inv_I, mul_neg, neg_one_mul, neg_mul, neg_neg, mul_comm]
  have h2 : (-I * (I * ↑(1 / x))) = 1 / x := by
    rw [← mul_assoc, neg_mul, I_mul_I, neg_neg, one_mul, ofReal_div, ofReal_one]
  have h3 : (x : ℂ) ^ (3 / 2 : ℂ) ≠ 0 := by
    simp only [Ne, cpow_eq_zero_iff, ofReal_eq_zero, hx.ne', false_and, not_false_eq_true]
  have h4 : arg x ≠ π := by rw [arg_ofReal_of_nonneg hx.le]; exact pi_ne_zero.symm
  rw [← ofReal_inj, oddKernel_def, ofReal_mul, sinKernel_def, jacobiTheta₂'_functional_equation',
    h1, h2]
  generalize jacobiTheta₂'' a (I * ↑x) = J
  rw [one_div (x : ℂ), inv_cpow _ _ h4, div_inv_eq_mul, one_div, ofReal_inv, ofReal_cpow hx.le,
    ofReal_div, ofReal_ofNat, ofReal_ofNat, ← mul_div_assoc _ _ (-2 * π : ℂ),
    eq_div_iff <| mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (ofReal_ne_zero.mpr pi_ne_zero),
    ← div_eq_inv_mul, eq_div_iff h3, mul_comm J _, mul_right_comm]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a x : ℝ
hx : 0 < x
⊢ HasSum (fun (n : ℤ) ↦ ((↑n : ℝ) + a) * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * x))
    (oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x)
have rw : HasSum (fun (x_1 : ℤ) ↦ (↑(((↑x_1 : ℝ) + a) * rexp (-π * HPow.hPow (β := ℕ) ((↑x_1 : ℝ) + a) 2 * x)) : ℂ))
  (cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
      (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))))
Tactic: rw [← hasSum_ofReal, oddKernel_def' a x]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a x : ℝ
hx : 0 < x
⊢ 0 < (I * (↑x : ℂ)).im
have rwa : 0 < (↑x : ℂ).re
Tactic: rwa [I_mul_im, ofReal_re]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a x : ℝ
hx : 0 < x
rwa : 0 < (↑x : ℂ).re
⊢ 0 < (I * (↑x : ℂ)).im
have rwa₁ : ℂ
Tactic: rwa [I_mul_im, ofReal_re]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (hypothesis)
Goal:
a x : ℝ
hx : 0 < x
⊢ HasSum (fun (x_1 : ℤ) ↦ (↑(((↑x_1 : ℝ) + a) * rexp (-π * HPow.hPow (β := ℕ) ((↑x_1 : ℝ) + a) 2 * x)) : ℂ))
    (cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))))
have h1 : HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
  (jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
Tactic: have h1 := hasSum_jacobiTheta₂_term (a * I * x) (by rwa [I_mul_im, ofReal_re])
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a x : ℝ
hx : 0 < x
h1 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
⊢ 0 < (I * (↑x : ℂ)).im
have rwa : 0 < (↑x : ℂ).re
Tactic: rwa [I_mul_im, ofReal_re]