-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
lemma hasSum_nat_sinKernel (a : ℝ) {t : ℝ} (ht : 0 < t) :
    HasSum (fun n : ℕ ↦ 2 * n * Real.sin (2 * π * a * n) * rexp (-π * n ^ 2 * t))
    (sinKernel ↑a t)

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

Tactic:
rw [← mul_div_assoc, ← div_mul_eq_mul_div, ← div_mul_eq_mul_div, div_self two_ne_zero, one_mul,
  neg_mul, neg_mul, neg_neg, mul_comm _ I, ← mul_assoc, mul_comm _ I, neg_mul,
  ← sub_eq_neg_add, mul_sub]

Result:
case e_a
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n =>
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
n : ℕ
⊢ I * ↑n * cexp (-(2 * ↑π * ↑a * ↑n * I)) - I * ↑n * cexp (2 * ↑π * ↑a * ↑n * I) =
    I * ↑n * cexp (-(2 * ↑π * I * ↑a * ↑n)) - I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n)

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

Tactic:
push_cast

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

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

Tactic:
simp_rw [Int.cast_neg, neg_sq, mul_neg, ofReal_mul, Int.cast_natCast, ofReal_natCast,
    ofReal_ofNat, ← add_mul, ofReal_sin, Complex.sin]

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

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

Tactic:
congr 3 <;> ring

Result:
no goals

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

Tactic:
refine this.congr_fun fun n ↦ ?_

Result:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n =>
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
n : ℕ
⊢ ↑(2 * ↑n * Real.sin (2 * π * a * ↑n) * rexp (-π * ↑n ^ 2 * t)) =
    -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
      -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t))

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

Tactic:
rw [← hasSum_ofReal]

Result:
a t : ℝ
ht : 0 < t
⊢ HasSum (fun x => ↑(2 * ↑x * Real.sin (2 * π * a * ↑x) * rexp (-π * ↑x ^ 2 * t))) ↑(sinKernel (↑a) t)

Proof state:
a t : ℝ
ht : 0 < t
⊢ HasSum (fun x => ↑(2 * ↑x * Real.sin (2 * π * a * ↑x) * rexp (-π * ↑x ^ 2 * t))) ↑(sinKernel (↑a) t)

Tactic:
have := (hasSum_int_sinKernel a ht).nat_add_neg

Result:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n =>
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    (↑(sinKernel (↑a) t) + -I * ↑0 * cexp (2 * ↑π * I * ↑a * ↑0) * ↑(rexp (-π * ↑0 ^ 2 * t)))
⊢ HasSum (fun x => ↑(2 * ↑x * Real.sin (2 * π * a * ↑x) * rexp (-π * ↑x ^ 2 * t))) ↑(sinKernel (↑a) t)

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

Tactic:
congr 1

Result:
case e_a
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n =>
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
n : ℕ
⊢ 2 * ↑n * ((cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I / 2) =
    -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) + -(-I * ↑n) * cexp (-(2 * ↑π * I * ↑a * ↑n))

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

Tactic:
simp only [Int.cast_zero, sq (0 : ℂ), zero_mul, mul_zero, add_zero] at this

Result:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n =>
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
⊢ HasSum (fun x => ↑(2 * ↑x * Real.sin (2 * π * a * ↑x) * rexp (-π * ↑x ^ 2 * t))) ↑(sinKernel (↑a) t)