awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum
    (fun (n : ℕ) ↦
      ((↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s -
          (↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s) /
        2)
    (hurwitzZetaOdd (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
(hasSum_int_hurwitzZetaOdd a hs).nat_add_neg_add_one.congr_fun fun n ↦ ?_

Premises used: HurwitzZeta.hasSum_int_hurwitzZetaOdd, HasSum.congr_fun, HasSum.nat_add_neg_add_one
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
refine :
  ∀ (n : ℕ),
    ((↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s -
          (↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s) /
        2 =
      (↑((SignType.sign : (a : ℝ) → SignType) ((↑(↑n : ℤ) : ℝ) + a)) : ℂ) / (↑|(↑(↑n : ℤ) : ℝ) + a| : ℂ) ^ s / 2 +
        (↑((SignType.sign : (a : ℝ) → SignType) ((↑(-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℝ) + a)) : ℂ) /
            (↑|(↑(-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℝ) + a| : ℂ) ^ s /
          2
⊢ HasSum
    (fun (n : ℕ) ↦
      ((↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s -
          (↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s) /
        2)
    (hurwitzZetaOdd (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
refine (hasSum_int_hurwitzZetaOdd a hs).nat_add_neg_add_one.congr_fun fun n ↦ ?_

Premises used: HurwitzZeta.hasSum_int_hurwitzZetaOdd, HasSum.congr_fun, HasSum.nat_add_neg_add_one
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
rw :
  (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
          2) =
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      (↑((SignType.sign : (a : ℝ) → SignType) (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a)) : ℂ) /
          (↑|-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a| : ℂ) ^ s /
        2
⊢ ((↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s -
        (↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
          (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s) /
      2 =
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑(↑n : ℤ) : ℝ) + a)) : ℂ) / (↑|(↑(↑n : ℤ) : ℝ) + a| : ℂ) ^ s / 2 +
      (↑((SignType.sign : (a : ℝ) → SignType) ((↑(-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℝ) + a)) : ℂ) /
          (↑|(↑(-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℝ) + a| : ℂ) ^ s /
        2

Tactic:
rw [Int.cast_neg, Int.cast_add, Int.cast_one, sub_div, sub_eq_add_neg, Int.cast_natCast]

Premises used: Int.cast_neg, Int.cast_natCast, sub_eq_add_neg, Int.cast_add, sub_div, Int.cast_one
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ -HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a = -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ -HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a = -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)

Tactic:
have : -(n + 1) + a = -(n + 1 - a) := by ring_nf
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun (n : ℕ) ↦ (1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s - 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s) / 2)
    (hurwitzZetaOdd (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
(hasSum_nat_hurwitzZetaOdd a hs).congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun, HurwitzZeta.hasSum_nat_hurwitzZetaOdd
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
refine :
  ∀ (n : ℕ),
    (1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s - 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s) / 2 =
      ((↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s -
          (↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s) /
        2
⊢ HasSum (fun (n : ℕ) ↦ (1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s - 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s) / 2)
    (hurwitzZetaOdd (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
refine (hasSum_nat_hurwitzZetaOdd a hs).congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun, HurwitzZeta.hasSum_nat_hurwitzZetaOdd
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
n : ℕ
this :
  ∀ (b : ℝ),
    0 ≤ b →
      (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + b)) : ℂ) / (↑|(↑n : ℝ) + b| : ℂ) ^ s =
        1 / ((↑n : ℂ) + (↑b : ℂ)) ^ s
⊢ (1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s - 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s) / 2 =
    ((↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s -
        (↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
          (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s) /
      2

Tactic:
simp only [add_sub_assoc, this a ha.1, this (1 - a) (sub_nonneg.mpr ha.2), push_cast]

Premises used: Iff.mpr, add_sub_assoc, HSub.hSub, And.right, And.left, OfNat.ofNat, sub_nonneg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
n : ℕ
suffices :
  ∀ (b : ℝ),
    0 ≤ b →
      (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + b)) : ℂ) / (↑|(↑n : ℝ) + b| : ℂ) ^ s =
        1 / ((↑n : ℂ) + (↑b : ℂ)) ^ s
⊢ (1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s - 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s) / 2 =
    ((↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s -
        (↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
          (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s) /
      2

Tactic:
suffices ∀ b : ℝ, 0 ≤ b → SignType.sign (n + b) / (↑|n + b| : ℂ) ^ s = 1 / (n + b) ^ s by
    simp only [add_sub_assoc, this a ha.1, this (1 - a) (sub_nonneg.mpr ha.2), push_cast]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb : 0 ≤ b
⊢ 0 ≤ (↑n : ℝ) + b

Tactic:
positivity
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb : 0 ≤ b
⊢ (↑n : ℂ) + (↑b : ℂ) = (↑((↑n : ℝ) + b) : ℂ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb : 0 ≤ b
rw :
  (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + b)) : ℂ) / (↑((↑n : ℝ) + b) : ℂ) ^ s =
    1 / (↑((↑n : ℝ) + b) : ℂ) ^ s
⊢ (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + b)) : ℂ) / (↑|(↑n : ℝ) + b| : ℂ) ^ s =
    1 / ((↑n : ℂ) + (↑b : ℂ)) ^ s

Tactic:
rw [abs_of_nonneg (by positivity), (by simp : (n : ℂ) + b = ↑(n + b))]

Premises used: abs_of_nonneg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb : 0 ≤ b
inl :
  ∀ (hb : 0 < (↑n : ℝ) + b),
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + b)) : ℂ) / (↑((↑n : ℝ) + b) : ℂ) ^ s =
      1 / (↑((↑n : ℝ) + b) : ℂ) ^ s
inr :
  ∀ (hb : 0 = (↑n : ℝ) + b),
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + b)) : ℂ) / (↑((↑n : ℝ) + b) : ℂ) ^ s =
      1 / (↑((↑n : ℝ) + b) : ℂ) ^ s
⊢ (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + b)) : ℂ) / (↑((↑n : ℝ) + b) : ℂ) ^ s =
    1 / (↑((↑n : ℝ) + b) : ℂ) ^ s

Tactic:
rcases lt_or_eq_of_le (by positivity : 0 ≤ n + b) with hb | hb

Premises used: lt_or_eq_of_le
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb_1 : 0 ≤ b
hb : 0 < (↑n : ℝ) + b
⊢ (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + b)) : ℂ) / (↑((↑n : ℝ) + b) : ℂ) ^ s =
    1 / (↑((↑n : ℝ) + b) : ℂ) ^ s

Tactic:
simp [sign_pos hb]

Premises used: sign_pos
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb_1 : 0 ≤ b
hb : 0 = (↑n : ℝ) + b
inr : (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℂ) / (↑0 : ℂ) ^ s = 1 / (↑0 : ℂ) ^ s
inr₁ : (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℂ) / HPow.hPow (α := ℂ) 0 s = 1 / HPow.hPow (α := ℂ) 0 s
inr₂ : HDiv.hDiv (α := ℂ) (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℂ) 0 = 1 / 0
inr₃ : 0 = 1 / 0
inr₄ inr₅ : Eq (α := ℂ) 0 0
⊢ (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + b)) : ℂ) / (↑((↑n : ℝ) + b) : ℂ) ^ s =
    1 / (↑((↑n : ℝ) + b) : ℂ) ^ s

Tactic:
rw [← hb, ofReal_zero, zero_cpow ((not_lt.mpr zero_le_one) ∘ (zero_re ▸ · ▸ hs)),
      div_zero, div_zero]

Premises used: Iff.mpr, Function.comp, zero_le_one, Complex.zero_cpow, Complex.ofReal_zero, not_lt, div_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum
    (fun (n : ℤ) ↦
      -I * (↑n.sign : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2)
    (completedSinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s / (s + 1).Gammaℝ)

Tactic:
((hasSum_int_completedSinZeta a hs).div_const (Gammaℝ (s + 1))).congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun, Complex.Gammaℝ, HasSum.div_const, HAdd.hAdd, OfNat.ofNat, HurwitzZeta.hasSum_int_completedSinZeta
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
refine :
  ∀ (n : ℤ),
    -I * (↑n.sign : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2 =
      (s + 1).Gammaℝ * -I * (↑n.sign : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) /
            HPow.hPow (α := ℂ) (↑|n| : ℂ) s /
          2 /
        (s + 1).Gammaℝ
⊢ HasSum
    (fun (n : ℤ) ↦
      -I * (↑n.sign : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2)
    (completedSinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s / (s + 1).Gammaℝ)

Tactic:
refine ((hasSum_int_completedSinZeta a hs).div_const (Gammaℝ (s + 1))).congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun, Complex.Gammaℝ, HasSum.div_const, HAdd.hAdd, OfNat.ofNat, HurwitzZeta.hasSum_int_completedSinZeta
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
this : 0 < (s + 1).re
⊢ -I * (↑n.sign : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2 =
    (s + 1).Gammaℝ * -I * (↑n.sign : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) /
          HPow.hPow (α := ℂ) (↑|n| : ℂ) s /
        2 /
      (s + 1).Gammaℝ

Tactic:
simp only [mul_assoc, div_right_comm _ _ (Gammaℝ _),
    mul_div_cancel_left₀ _ (Gammaℝ_ne_zero_of_re_pos this)]

Premises used: div_right_comm, Complex.Gammaℝ, mul_assoc, mul_div_cancel_left₀, Complex.Gammaℝ_ne_zero_of_re_pos
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) /
            HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s /
          2 +
        -I * (↑(Int.sign (-(↑n : ℤ))) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) /
            HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s /
          2)
    (sinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s +
      -I * (↑(Int.sign 0) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) / HPow.hPow (α := ℂ) (↑|0| : ℂ) s / 2)
⊢ HasSum
    (fun (n : ℕ) ↦
      -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2 +
        -(-I * (↑(Int.sign (↑n : ℤ)) : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) /
            HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2)
    (sinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 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

Premises used: Int.cast_neg, Int.cast_natCast, abs_neg, Nat.abs_cast, Int.cast_zero, zero_div, Complex.ne_zero_of_one_lt_re, Complex.zero_cpow, abs_zero, Int.sign_neg, add_zero, div_zero, mul_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2 +
        -(-I * (↑(Int.sign (↑n : ℤ)) : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) /
            HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2)
    (sinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
simp_rw :
  HasSum
    (fun (n : ℕ) ↦
      (cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I) - cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) * I / 2 /
        HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (sinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
⊢ HasSum (fun (n : ℕ) ↦ (↑(Real.sin (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (sinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
simp_rw [push_cast, Complex.sin]

Premises used: Complex.sin
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2 +
        -(-I * (↑(Int.sign (↑n : ℤ)) : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) /
            HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2)
    (sinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
⊢ HasSum
    (fun (n : ℕ) ↦
      (cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I) - cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) * I / 2 /
        HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (sinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
this.congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2 +
        -(-I * (↑(Int.sign (↑n : ℤ)) : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) /
            HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2)
    (sinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
refine :
  ∀ (n : ℕ),
    (cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I) - cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) * I / 2 /
        HPow.hPow (α := ℂ) (↑n : ℂ) s =
      -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2 +
        -(-I * (↑(Int.sign (↑n : ℤ)) : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) /
            HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2
⊢ HasSum
    (fun (n : ℕ) ↦
      (cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I) - cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) * I / 2 /
        HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (sinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
refine this.congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2 +
        -(-I * (↑(Int.sign (↑n : ℤ)) : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) /
            HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2)
    (sinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
n : ℕ
inl :
  ∀ (h : n ≠ 0),
    (cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I) - cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) * I / 2 /
        HPow.hPow (α := ℂ) (↑n : ℂ) s =
      -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2 +
        -(-I * (↑(Int.sign (↑n : ℤ)) : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) /
            HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2
inr :
  (cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑0 : ℂ)) * I) - cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑0 : ℂ) * I)) * I / 2 /
      HPow.hPow (α := ℂ) (↑0 : ℂ) s =
    -I * (↑(Int.sign (↑0 : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) / HPow.hPow (α := ℂ) (↑0 : ℂ) s /
        2 +
      -(-I * (↑(Int.sign (↑0 : ℤ)) : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ))) /
          HPow.hPow (α := ℂ) (↑0 : ℂ) s /
        2
⊢ (cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I) - cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) * I / 2 /
      HPow.hPow (α := ℂ) (↑n : ℂ) s =
    -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s /
        2 +
      -(-I * (↑(Int.sign (↑n : ℤ)) : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) /
          HPow.hPow (α := ℂ) (↑n : ℂ) s /
        2

Tactic:
rcases ne_or_eq n 0 with h | rfl

Premises used: ne_or_eq, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2 +
        -(-I * (↑(Int.sign (↑n : ℤ)) : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) /
            HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2)
    (sinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
n : ℕ
h : n ≠ 0
inl :
  (cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) * I - cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I) * I) /
        HPow.hPow (α := ℂ) (↑n : ℂ) s /
      2 =
    (cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) * I - cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) * I) /
        HPow.hPow (α := ℂ) (↑n : ℂ) s /
      2
⊢ (cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I) - cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) * I / 2 /
      HPow.hPow (α := ℂ) (↑n : ℂ) s =
    -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s /
        2 +
      -(-I * (↑(Int.sign (↑n : ℤ)) : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) /
          HPow.hPow (α := ℂ) (↑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]

Premises used: div_right_comm, sub_eq_neg_add, neg_neg, sub_mul, Int.sign_natCast_of_ne_zero, mul_comm, neg_mul, mul_one, OfNat.ofNat, Int.cast_one, add_div, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2 +
        -(-I * (↑(Int.sign (↑n : ℤ)) : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) /
            HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2)
    (sinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
n : ℕ
h : n ≠ 0
inl : -(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I) = -(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))
inl₁ : 2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I = 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)
⊢ (cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) * I - cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I) * I) /
        HPow.hPow (α := ℂ) (↑n : ℂ) s /
      2 =
    (cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) * I - cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) * I) /
        HPow.hPow (α := ℂ) (↑n : ℂ) s /
      2

Tactic:
congr 5
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2 +
        -(-I * (↑(Int.sign (↑n : ℤ)) : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) /
            HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2)
    (sinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
n : ℕ
h : n ≠ 0
⊢ -(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I) = -(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2 +
        -(-I * (↑(Int.sign (↑n : ℤ)) : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) /
            HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2)
    (sinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
n : ℕ
h : n ≠ 0
⊢ 2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I = 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2 +
        -(-I * (↑(Int.sign (↑n : ℤ)) : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) /
            HPow.hPow (α := ℂ) (↑n : ℂ) s /
          2)
    (sinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
⊢ (cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑0 : ℂ)) * I) - cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑0 : ℂ) * I)) * I / 2 /
      HPow.hPow (α := ℂ) (↑0 : ℂ) s =
    -I * (↑(Int.sign (↑0 : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) / HPow.hPow (α := ℂ) (↑0 : ℂ) s /
        2 +
      -(-I * (↑(Int.sign (↑0 : ℤ)) : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ))) /
          HPow.hPow (α := ℂ) (↑0 : ℂ) s /
        2

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ LSeriesHasSum (fun (x : ℕ) ↦ (↑(Real.sin (2 * π * a * (↑x : ℝ))) : ℂ)) s
    (sinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
(hasSum_nat_sinZeta a hs).congr_fun (LSeries.term_of_ne_zero' (ne_zero_of_one_lt_re hs) _)

Premises used: HasSum.congr_fun, HurwitzZeta.hasSum_nat_sinZeta, Complex.ne_zero_of_one_lt_re, LSeriesHasSum, LSeries.term_of_ne_zero'
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
n : ℕ
rw : -HMul.hMul (α := ℂ) 2 (↑n : ℂ) - 1 + 1 = -HMul.hMul (α := ℂ) 2 (↑n : ℂ)
rw₁ rw₂ : -HMul.hMul (α := ℂ) 2 (↑n : ℂ) = -HMul.hMul (α := ℂ) 2 (↑n : ℂ)
⊢ HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1 + 1 = -HMul.hMul (α := ℂ) 2 (↑n : ℂ)

Tactic:
rw [neg_mul, sub_add_cancel]

Premises used: neg_mul, sub_add_cancel
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
n : ℕ
rw :
  completedHurwitzZetaOdd a (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1) / (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1 + 1).Gammaℝ =
    0
rw₁ : completedHurwitzZetaOdd a (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1) / 0 = 0
rw₂ rw₃ : Eq (α := ℂ) 0 0
⊢ hurwitzZetaOdd a (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1) = 0

Tactic:
rw [hurwitzZetaOdd, Gammaℝ_eq_zero_iff.mpr ⟨n, by rw [neg_mul, sub_add_cancel]⟩, div_zero]

Premises used: Iff.mpr, HurwitzZeta.hurwitzZetaOdd, Complex.Gammaℝ_eq_zero_iff, Exists.intro, div_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
n : ℕ
rw : completedSinZeta a (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1) / (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1 + 1).Gammaℝ = 0
rw₁ : completedSinZeta a (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1) / 0 = 0
rw₂ rw₃ : Eq (α := ℂ) 0 0
⊢ sinZeta a (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1) = 0

Tactic:
rw [sinZeta, Gammaℝ_eq_zero_iff.mpr ⟨n, by rw [neg_mul, sub_add_cancel]⟩, div_zero]

Premises used: Iff.mpr, Complex.Gammaℝ_eq_zero_iff, HurwitzZeta.sinZeta, Exists.intro, div_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
⊢ 1 - s + 1 = 2 - s

Tactic:
ring