-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
lemma hasSum_int_sinKernel (a : ℝ) {t : ℝ} (ht : 0 < t) : HasSum
    (fun n : ℤ ↦ -I * n * cexp (2 * π * I * a * n) * rexp (-π * n ^ 2 * t)) ↑(sinKernel a t)

Proof state:
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
⊢ HasSum (fun n => -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑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 ↦ ?_

Result:
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
n : ℤ
⊢ -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t)) = jacobiTheta₂'_term n (↑a) (I * ↑t) / (-2 * ↑π)

Proof state:
case refine_3
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
n : ℤ
⊢ -↑π * ↑n ^ 2 * ↑t = ↑π * I * ↑n ^ 2 * (I * ↑t)

Tactic:
simp [← mul_assoc, mul_comm _ I]

Result:
no goals

Proof state:
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]

Result:
no goals

Proof state:
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
n : ℤ
⊢ -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑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]

Result:
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
n : ℤ
⊢ -2 * ↑π * (-I * ↑n) * cexp (2 * ↑π * I * ↑a * ↑n + -↑π * ↑n ^ 2 * ↑t) =
    2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * ↑a + ↑π * I * ↑n ^ 2 * (I * ↑t))

Proof state:
case refine_2
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

Result:
no goals

Proof state:
a t : ℝ
ht : 0 < t
⊢ HasSum (fun n => -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) ↑(sinKernel (↑a) t)

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]

Result:
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
⊢ HasSum (fun n => -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) ↑(sinKernel (↑a) t)

Proof state:
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
⊢ HasSum (fun n => -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) ↑(sinKernel (↑a) t)

Tactic:
rw [sinKernel_def]

Result:
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
⊢ HasSum (fun n => -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t)))
    (jacobiTheta₂' (↑a) (I * ↑t) / (-2 * ↑π))

Proof state:
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
n : ℤ
⊢ -2 * ↑π * (-I * ↑n) * cexp (2 * ↑π * I * ↑a * ↑n + -↑π * ↑n ^ 2 * ↑t) =
    2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * ↑a + ↑π * I * ↑n ^ 2 * (I * ↑t))

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

Result:
case refine_1
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
n : ℤ
⊢ -2 * ↑π * (-I * ↑n) = 2 * ↑π * I * ↑n

case refine_2
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
n : ℤ
⊢ 2 * ↑π * I * ↑a * ↑n = 2 * ↑π * I * ↑n * ↑a

case refine_3
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
n : ℤ
⊢ -↑π * ↑n ^ 2 * ↑t = ↑π * I * ↑n ^ 2 * (I * ↑t)

Proof state:
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
⊢ 0 < (I * ↑t).im

Tactic:
rwa [I_mul_im, ofReal_re]

Result:
no goals

Proof state:
case refine_1
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
n : ℤ
⊢ -2 * ↑π * (-I * ↑n) = 2 * ↑π * I * ↑n

Tactic:
simp [mul_assoc]

Result:
no goals