awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
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
rw : 0 ≠ π
⊢ (↑x : ℂ).arg ≠ π

Tactic:
rw [arg_ofReal_of_nonneg hx.le]

Premises used: Complex.arg_ofReal_of_nonneg, LT.lt.le
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
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
⊢ 0 ≠ π

Tactic:
pi_ne_zero.symm

Premises used: Ne.symm, Real.pi_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
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
⊢ 0 ≠ π

Tactic:
exact pi_ne_zero.symm

Premises used: Ne.symm, Real.pi_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
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
⊢ (↑x : ℂ).arg ≠ π

Tactic:
have h4 : arg x ≠ π := by rw [arg_ofReal_of_nonneg hx.le]; exact pi_ne_zero.symm
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
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 ≠ π
inr :
  jacobiTheta₂'' (↑a : ℂ) (I * (↑x : ℂ)) =
    (↑(1 / x ^ (3 / 2)) : ℂ) *
      (-2 * (↑π : ℂ) / (1 / (↑x : ℂ)) ^ (3 / 2) * jacobiTheta₂'' (↑a : ℂ) (I * (↑x : ℂ)) / (-2 * (↑π : ℂ)))
⊢ oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x =
    1 / x ^ (3 / 2) * sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) (1 / x)

Tactic:
rw [← ofReal_inj, oddKernel_def, ofReal_mul, sinKernel_def, jacobiTheta₂'_functional_equation',
    h1, h2]

Premises used: HurwitzZeta.jacobiTheta₂'_functional_equation', HurwitzZeta.oddKernel_def, Complex.ofReal_inj, HurwitzZeta.sinKernel_def, Complex.ofReal_mul
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
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 ≠ π
inr : ∀ (J : ℂ), J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (1 / (↑x : ℂ)) ^ (3 / 2) * J / (-2 * (↑π : ℂ)))
⊢ jacobiTheta₂'' (↑a : ℂ) (I * (↑x : ℂ)) =
    (↑(1 / x ^ (3 / 2)) : ℂ) *
      (-2 * (↑π : ℂ) / (1 / (↑x : ℂ)) ^ (3 / 2) * jacobiTheta₂'' (↑a : ℂ) (I * (↑x : ℂ)) / (-2 * (↑π : ℂ)))

Tactic:
generalize jacobiTheta₂'' a (I * ↑x) = J

Premises used: HMul.hMul, HurwitzZeta.jacobiTheta₂'', Complex.ofReal, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
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
inr₁₄ inr₁₅ : -2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J = -2 * (↑π : ℂ) * (↑x : ℂ) ^ (3 / 2) * J
⊢ J = (↑(1 / x ^ (3 / 2)) : ℂ) * (-2 * (↑π : ℂ) / (1 / (↑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]

Premises used: Iff.mpr, Real.pi, HMul.hMul, Complex.ofReal_cpow, mul_div_assoc, Complex.ofReal_ne_zero, LT.lt.le, Complex.inv_cpow, Complex.ofReal, two_ne_zero, mul_right_comm, one_div, mul_comm, Complex.ofReal_div, neg_ne_zero, div_inv_eq_mul, mul_ne_zero, div_eq_inv_mul, Complex.ofReal_ofNat, OfNat.ofNat, eq_div_iff, Complex.ofReal_inv, Neg.neg, Real.pi_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
x : ℝ
hx : 0 < x
inr :
  ∀ (a : ℝ),
    oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x =
      1 / x ^ (3 / 2) * sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) (1 / x)
⊢ oddKernel a x = 1 / x ^ (3 / 2) * sinKernel a (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]

Premises used: Iff.mpr, Real.pi, HMul.hMul, HurwitzZeta.jacobiTheta₂'_functional_equation', Complex.ofReal_cpow, mul_div_assoc, Complex.ofReal_ne_zero, HurwitzZeta.oddKernel_def, LT.lt.le, Complex.ofReal, two_ne_zero, mul_right_comm, one_div, Complex.ofReal_div, Complex.ofReal_inj, neg_ne_zero, div_inv_eq_mul, HurwitzZeta.sinKernel_def, mul_ne_zero, div_eq_inv_mul, Complex.ofReal_ofNat, OfNat.ofNat, eq_div_iff, Complex.ofReal_inv, Neg.neg, Complex.ofReal_mul, Real.pi_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
hx : 0 < x
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 : ℂ))))
⊢ HasSum (fun (n : ℤ) ↦ ((↑n : ℝ) + a) * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * x))
    (oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x)

Tactic:
rw [← hasSum_ofReal, oddKernel_def' a x]

Premises used: HurwitzZeta.oddKernel_def', Complex.hasSum_ofReal
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
hx : 0 < x
rwa : 0 < (↑x : ℂ).re
rwa₁ : ℂ
rwa₂ : 0 < x
rwa₃ : ℝ
rwa₄ : 0 < x
rwa₅ : ℝ
rwa₆ : 0 < x
rwa₇ : ℝ
rwa₈ : 0 < x
rwa₉ : ℝ
⊢ 0 < (I * (↑x : ℂ)).im

Tactic:
rwa [I_mul_im, ofReal_re]

Premises used: Complex.ofReal_re, Complex.I_mul_im
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
hx : 0 < x
⊢ 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])
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
hx : 0 < x
h1 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
rwa : 0 < (↑x : ℂ).re
rwa₁ : ℂ
rwa₂ : 0 < x
rwa₃ : ℝ
rwa₄ : 0 < x
rwa₅ : ℝ
rwa₆ : 0 < x
rwa₇ : ℝ
rwa₈ : 0 < x
rwa₉ : ℝ
⊢ 0 < (I * (↑x : ℂ)).im

Tactic:
rwa [I_mul_im, ofReal_re]

Premises used: Complex.ofReal_re, Complex.I_mul_im
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
hx : 0 < x
h1 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
⊢ HasSum (fun (n : ℤ) ↦ jacobiTheta₂'_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))

Tactic:
have h2 := hasSum_jacobiTheta₂'_term (a * I * x) (by rwa [I_mul_im, ofReal_re])
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
hx : 0 < x
h1 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
h2 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂'_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑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 : ℂ))))

Tactic:
(((h2.div_const (2 * π * I)).add (h1.mul_left ↑a)).mul_left
    (cexp (-π * a ^ 2 * x))).congr_fun (fun n ↦ ?_)

Premises used: HasSum.congr_fun, HasSum.add, Real.pi, HMul.hMul, HasSum.mul_left, HasSum.div_const, Complex.ofReal, HPow.hPow, Complex.exp, OfNat.ofNat, Neg.neg, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
hx : 0 < x
h1 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
h2 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂'_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
refine :
  ∀ (n : ℤ),
    (↑(((↑n : ℝ) + a) * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * x)) : ℂ) =
      cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
        (jacobiTheta₂'_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
          (↑a : ℂ) * jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑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 : ℂ))))

Tactic:
refine (((h2.div_const (2 * π * I)).add (h1.mul_left ↑a)).mul_left
    (cexp (-π * a ^ 2 * x))).congr_fun (fun n ↦ ?_)

Premises used: HasSum.congr_fun, HasSum.add, Real.pi, HMul.hMul, HasSum.mul_left, HasSum.div_const, Complex.ofReal, HPow.hPow, Complex.exp, OfNat.ofNat, Neg.neg, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
hx : 0 < x
h1 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
h2 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂'_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
n : ℤ
rw :
  (↑(((↑n : ℝ) + a) * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * x)) : ℂ) =
    ((↑n : ℂ) + (↑a : ℂ)) *
      cexp
        (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ) +
          (2 * (↑π : ℂ) * I * (↑n : ℂ) * ((↑a : ℂ) * I * (↑x : ℂ)) +
            (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑x : ℂ))))
⊢ (↑(((↑n : ℝ) + a) * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * x)) : ℂ) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (jacobiTheta₂'_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)) / (2 * (↑π : ℂ) * I) +
        (↑a : ℂ) * jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))

Tactic:
rw [jacobiTheta₂'_term, mul_assoc (2 * π * I), mul_div_cancel_left₀ _ two_pi_I_ne_zero, ← add_mul,
    mul_left_comm, jacobiTheta₂_term, ← Complex.exp_add]

Premises used: add_mul, Real.pi, HMul.hMul, Complex.exp_add, jacobiTheta₂_term, jacobiTheta₂'_term, Complex.two_pi_I_ne_zero, mul_assoc, mul_div_cancel_left₀, mul_left_comm, Complex.ofReal, OfNat.ofNat, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
hx : 0 < x
h1 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
h2 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂'_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
n : ℤ
push_cast :
  ((↑n : ℂ) + (↑a : ℂ)) * cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 * (↑x : ℂ)) =
    ((↑n : ℂ) + (↑a : ℂ)) *
      cexp
        (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ) +
          (2 * (↑π : ℂ) * I * (↑n : ℂ) * ((↑a : ℂ) * I * (↑x : ℂ)) +
            (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑x : ℂ))))
⊢ (↑(((↑n : ℝ) + a) * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * x)) : ℂ) =
    ((↑n : ℂ) + (↑a : ℂ)) *
      cexp
        (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ) +
          (2 * (↑π : ℂ) * I * (↑n : ℂ) * ((↑a : ℂ) * I * (↑x : ℂ)) +
            (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑x : ℂ))))

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
hx : 0 < x
h1 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
h2 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂'_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
n : ℤ
simp :
  ((↑n : ℂ) + (↑a : ℂ)) * cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 * (↑x : ℂ)) =
    ((↑n : ℂ) + (↑a : ℂ)) *
      cexp
        ((-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 +
            (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑a : ℂ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2) * I) *
          (↑x : ℂ))
⊢ ((↑n : ℂ) + (↑a : ℂ)) * cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 * (↑x : ℂ)) =
    ((↑n : ℂ) + (↑a : ℂ)) *
      cexp
        (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ) +
          (2 * (↑π : ℂ) * I * (↑n : ℂ) * ((↑a : ℂ) * I * (↑x : ℂ)) +
            (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑x : ℂ))))

Tactic:
simp only [← mul_assoc, ← add_mul]

Premises used: add_mul, mul_assoc
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
hx : 0 < x
h1 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
h2 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂'_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
n : ℤ
congrm :
  -(↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 =
    -(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 +
      (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑a : ℂ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2) * I
⊢ ((↑n : ℂ) + (↑a : ℂ)) * cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 * (↑x : ℂ)) =
    ((↑n : ℂ) + (↑a : ℂ)) *
      cexp
        ((-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 +
            (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑a : ℂ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2) * I) *
          (↑x : ℂ))

Tactic:
congrm _ * cexp (?_ * x)

Premises used: HMul.hMul, Complex.ofReal, Complex.exp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
hx : 0 < x
h1 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
h2 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂'_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
n : ℤ
simp :
  -(↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 =
    -(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 +
      (2 * (↑π : ℂ) * (↑n : ℂ) * (↑a : ℂ) * -1 + (↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * -1)
⊢ -(↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 =
    -(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 +
      (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑a : ℂ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2) * I

Tactic:
simp only [mul_right_comm _ I, add_mul, mul_assoc _ I, I_mul_I]

Premises used: add_mul, mul_assoc, mul_right_comm, Complex.I_mul_I, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a x : ℝ
hx : 0 < x
h1 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
h2 :
  HasSum (fun (n : ℤ) ↦ jacobiTheta₂'_term n ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (jacobiTheta₂' ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
n : ℤ
⊢ -(↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 =
    -(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 +
      (2 * (↑π : ℂ) * (↑n : ℂ) * (↑a : ℂ) * -1 + (↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * -1)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a t : ℝ
ht : 0 < t
⊢ -2 * (↑π : ℂ) ≠ 0

Tactic:
simp only [neg_mul, ne_eq, neg_eq_zero, mul_eq_zero,
      OfNat.ofNat_ne_zero, ofReal_eq_zero, pi_ne_zero, or_self, not_false_eq_true]

Premises used: OfNat.ofNat_ne_zero, neg_eq_zero, mul_eq_zero, ne_eq, Complex.ofReal_eq_zero, or_self, neg_mul, not_false_eq_true, Real.pi_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a t : ℝ
ht : 0 < t
⊢ -2 * (↑π : ℂ) ≠ 0

Tactic:
have h : -2 * (π : ℂ) ≠ (0 : ℂ) := by
    simp only [neg_mul, ne_eq, neg_eq_zero, mul_eq_zero,
      OfNat.ofNat_ne_zero, ofReal_eq_zero, pi_ne_zero, or_self, not_false_eq_true]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a t : ℝ
ht : 0 < t
h : -2 * (↑π : ℂ) ≠ 0
rw :
  HasSum
    (fun (n : ℤ) ↦
      -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
    (jacobiTheta₂' (↑a : ℂ) (I * (↑t : ℂ)) / (-2 * (↑π : ℂ)))
⊢ HasSum
    (fun (n : ℤ) ↦
      -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
    (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)

Tactic:
rw [sinKernel_def]

Premises used: HurwitzZeta.sinKernel_def
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a t : ℝ
ht : 0 < t
h : -2 * (↑π : ℂ) ≠ 0
rwa : 0 < (↑t : ℂ).re
rwa₁ rwa₂ rwa₃ rwa₄ : 0 < t
⊢ 0 < (I * (↑t : ℂ)).im

Tactic:
rwa [I_mul_im, ofReal_re]

Premises used: Complex.ofReal_re, Complex.I_mul_im
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a t : ℝ
ht : 0 < t
h : -2 * (↑π : ℂ) ≠ 0
refine :
  ∀ (n : ℤ),
    -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) =
      jacobiTheta₂'_term n (↑a : ℂ) (I * (↑t : ℂ)) / (-2 * (↑π : ℂ))
⊢ HasSum
    (fun (n : ℤ) ↦
      -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
    (jacobiTheta₂' (↑a : ℂ) (I * (↑t : ℂ)) / (-2 * (↑π : ℂ)))

Tactic:
refine ((hasSum_jacobiTheta₂'_term a
    (by rwa [I_mul_im, ofReal_re])).div_const _).congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun, hasSum_jacobiTheta₂'_term, HasSum.div_const, Complex.ofReal
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a t : ℝ
ht : 0 < t
h : -2 * (↑π : ℂ) ≠ 0
n : ℤ
rw :
  -2 * (↑π : ℂ) * (-I * (↑n : ℂ)) *
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) + -(↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ)) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      cexp
        (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑a : ℂ) +
          (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑t : ℂ)))
⊢ -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
      (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) =
    jacobiTheta₂'_term n (↑a : ℂ) (I * (↑t : ℂ)) / (-2 * (↑π : ℂ))

Tactic:
rw [jacobiTheta₂'_term, jacobiTheta₂_term, ofReal_exp, mul_assoc (-I * n), ← Complex.exp_add,
    eq_div_iff h, ofReal_mul, ofReal_mul, ofReal_pow, ofReal_neg, ofReal_intCast,
    mul_comm _ (-2 * π : ℂ), ← mul_assoc]

Premises used: Int.cast, Real.pi, HMul.hMul, Complex.exp_add, jacobiTheta₂_term, jacobiTheta₂'_term, mul_assoc, Complex.ofReal_neg, Complex.ofReal_intCast, Complex.ofReal_exp, Complex.ofReal, mul_comm, OfNat.ofNat, eq_div_iff, Complex.ofReal_pow, Neg.neg, Complex.ofReal_mul, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a t : ℝ
ht : 0 < t
h : -2 * (↑π : ℂ) ≠ 0
n : ℤ
refine_1 : -2 * (↑π : ℂ) * (-I * (↑n : ℂ)) = 2 * (↑π : ℂ) * I * (↑n : ℂ)
refine_2 : 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) = 2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑a : ℂ)
refine_3 :
  -(↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ) =
    (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑t : ℂ))
⊢ -2 * (↑π : ℂ) * (-I * (↑n : ℂ)) *
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) + -(↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ)) =
    2 * (↑π : ℂ) * I * (↑n : ℂ) *
      cexp
        (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑a : ℂ) +
          (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑t : ℂ)))

Tactic:
congrm ?_ * cexp (?_ + ?_)

Premises used: HAdd.hAdd, Complex.exp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a t : ℝ
ht : 0 < t
h : -2 * (↑π : ℂ) ≠ 0
n : ℤ
⊢ -2 * (↑π : ℂ) * (-I * (↑n : ℂ)) = 2 * (↑π : ℂ) * I * (↑n : ℂ)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a t : ℝ
ht : 0 < t
h : -2 * (↑π : ℂ) ≠ 0
n : ℤ
⊢ 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) = 2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑a : ℂ)

Tactic:
mul_right_comm (2 * π * I) a n

Premises used: Int.cast, Real.pi, HMul.hMul, Complex.ofReal, mul_right_comm, OfNat.ofNat, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a t : ℝ
ht : 0 < t
h : -2 * (↑π : ℂ) ≠ 0
n : ℤ
⊢ 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) = 2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑a : ℂ)

Tactic:
exact mul_right_comm (2 * π * I) a n

Premises used: Int.cast, Real.pi, HMul.hMul, Complex.ofReal, mul_right_comm, OfNat.ofNat, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a t : ℝ
ht : 0 < t
h : -2 * (↑π : ℂ) ≠ 0
n : ℤ
⊢ -(↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ) =
    (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑t : ℂ))

Tactic:
simp [← mul_assoc, mul_comm _ I]

Premises used: mul_assoc, mul_comm, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a t : ℝ
ht : 0 < t
rw :
  HasSum
    (fun (x : ℕ) ↦
      (↑(HMul.hMul (α := ℝ) 2 (↑x : ℝ) * Real.sin (2 * π * a * (↑x : ℝ)) *
            rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑x : ℝ) 2 * t)) :
        ℂ))
    (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)
⊢ HasSum
    (fun (n : ℕ) ↦
      HMul.hMul (α := ℝ) 2 (↑n : ℝ) * Real.sin (2 * π * a * (↑n : ℝ)) *
        rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t))
    (sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t)

Tactic:
rw [← hasSum_ofReal]

Premises used: Complex.hasSum_ofReal