-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
/-- Formula for `sinZeta` as a Dirichlet series in the convergence range, with sum over `ℕ`. -/
lemma hasSum_nat_sinZeta (a : ℝ) {s : ℂ} (hs : 1 < re s) :
    HasSum (fun n : ℕ ↦ Real.sin (2 * π * a * n) / (n : ℂ) ^ s) (sinZeta a s)

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n =>
      -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 +
        -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2)
    (sinZeta (↑a) s)
n : ℕ
⊢ (cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I / 2 / ↑n ^ s =
    -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 +
      -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2

Tactic:
rcases ne_or_eq n 0 with h | rfl

Result:
case inl
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n =>
      -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 +
        -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2)
    (sinZeta (↑a) s)
n : ℕ
h : n ≠ 0
⊢ (cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I / 2 / ↑n ^ s =
    -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 +
      -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2

case inr
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n =>
      -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 +
        -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2)
    (sinZeta (↑a) s)
⊢ (cexp (-(2 * ↑π * ↑a * ↑0) * I) - cexp (2 * ↑π * ↑a * ↑0 * I)) * I / 2 / ↑0 ^ s =
    -I * ↑(↑0).sign * cexp (2 * ↑π * I * ↑a * ↑0) / ↑0 ^ s / 2 +
      -(-I * ↑(↑0).sign) * cexp (-(2 * ↑π * I * ↑a * ↑0)) / ↑0 ^ s / 2

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n =>
      -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
        -I * ↑(-↑n).sign * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2)
    (sinZeta (↑a) s + -I * ↑(Int.sign 0) * cexp (2 * ↑π * I * ↑a * ↑0) / ↑|0| ^ s / 2)
⊢ HasSum (fun n => ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (sinZeta (↑a) s)

Tactic:
simp_rw [abs_neg, Int.sign_neg, Int.cast_neg, Nat.abs_cast, Int.cast_natCast, mul_neg, abs_zero,
  Int.cast_zero, zero_cpow (ne_zero_of_one_lt_re hs), div_zero, zero_div, add_zero] at this

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n =>
      -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 +
        -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2)
    (sinZeta (↑a) s)
⊢ HasSum (fun n => ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (sinZeta (↑a) s)

Proof state:
case inl
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n =>
      -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 +
        -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2)
    (sinZeta (↑a) s)
n : ℕ
h : n ≠ 0
⊢ (cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I / 2 / ↑n ^ s =
    -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 +
      -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2

Tactic:
simp only [neg_mul, sub_mul, div_right_comm _ (2 : ℂ), Int.sign_natCast_of_ne_zero h,
  Int.cast_one, mul_one, mul_comm I, neg_neg, ← add_div, ← sub_eq_neg_add]

Result:
case inl
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n =>
      -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 +
        -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2)
    (sinZeta (↑a) s)
n : ℕ
h : n ≠ 0
⊢ (cexp (-(2 * ↑π * ↑a * ↑n * I)) * I - cexp (2 * ↑π * ↑a * ↑n * I) * I) / ↑n ^ s / 2 =
    (cexp (-(2 * ↑π * I * ↑a * ↑n)) * I - cexp (2 * ↑π * I * ↑a * ↑n) * I) / ↑n ^ s / 2

Proof state:
case inl
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n =>
      -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 +
        -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2)
    (sinZeta (↑a) s)
n : ℕ
h : n ≠ 0
⊢ (cexp (-(2 * ↑π * ↑a * ↑n * I)) * I - cexp (2 * ↑π * ↑a * ↑n * I) * I) / ↑n ^ s / 2 =
    (cexp (-(2 * ↑π * I * ↑a * ↑n)) * I - cexp (2 * ↑π * I * ↑a * ↑n) * I) / ↑n ^ s / 2

Tactic:
congr 5 <;> ring

Result:
no goals

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n =>
      -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 +
        -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2)
    (sinZeta (↑a) s)
⊢ HasSum (fun n => ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (sinZeta (↑a) s)

Tactic:
simp_rw [push_cast, Complex.sin]

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n =>
      -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 +
        -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2)
    (sinZeta (↑a) s)
⊢ HasSum (fun n => (cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I / 2 / ↑n ^ s) (sinZeta (↑a) s)

Proof state:
case inr
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n =>
      -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 +
        -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2)
    (sinZeta (↑a) s)
⊢ (cexp (-(2 * ↑π * ↑a * ↑0) * I) - cexp (2 * ↑π * ↑a * ↑0 * I)) * I / 2 / ↑0 ^ s =
    -I * ↑(↑0).sign * cexp (2 * ↑π * I * ↑a * ↑0) / ↑0 ^ s / 2 +
      -(-I * ↑(↑0).sign) * cexp (-(2 * ↑π * I * ↑a * ↑0)) / ↑0 ^ s / 2

Tactic:
simp

Result:
no goals

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n =>
      -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 +
        -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2)
    (sinZeta (↑a) s)
⊢ HasSum (fun n => (cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I / 2 / ↑n ^ s) (sinZeta (↑a) s)

Tactic:
refine this.congr_fun fun n ↦ ?_

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n =>
      -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 +
        -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2)
    (sinZeta (↑a) s)
n : ℕ
⊢ (cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I / 2 / ↑n ^ s =
    -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 +
      -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n => ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (sinZeta (↑a) s)

Tactic:
have := (hasSum_int_sinZeta a hs).nat_add_neg

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n =>
      -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
        -I * ↑(-↑n).sign * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2)
    (sinZeta (↑a) s + -I * ↑(Int.sign 0) * cexp (2 * ↑π * I * ↑a * ↑0) / ↑|0| ^ s / 2)
⊢ HasSum (fun n => ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (sinZeta (↑a) s)