awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun (n : ℕ) ↦
      ((s + 1).Gammaℝ * -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) +
            (s + 1).Gammaℝ * -I * -(↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * -(↑n : ℂ))) /
          HPow.hPow (α := ℂ) (↑n : ℂ) s /
        2)
    (completedSinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
refine :
  ∀ (n : ℕ),
    (s + 1).Gammaℝ * (↑(Real.sin (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
      ((s + 1).Gammaℝ * -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) +
            (s + 1).Gammaℝ * -I * -(↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * -(↑n : ℂ))) /
          HPow.hPow (α := ℂ) (↑n : ℂ) s /
        2
⊢ HasSum (fun (n : ℕ) ↦ (s + 1).Gammaℝ * (↑(Real.sin (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (completedSinZeta (↑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 : ℕ) ↦
      ((s + 1).Gammaℝ * -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) +
            (s + 1).Gammaℝ * -I * -(↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * -(↑n : ℂ))) /
          HPow.hPow (α := ℂ) (↑n : ℂ) s /
        2)
    (completedSinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
n : ℕ
rw :
  (s + 1).Gammaℝ * (↑(Real.sin (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    ((s + 1).Gammaℝ * -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) +
          (s + 1).Gammaℝ * -I * -(↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * -(↑n : ℂ))) /
        2 /
      HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ (s + 1).Gammaℝ * (↑(Real.sin (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    ((s + 1).Gammaℝ * -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) +
          (s + 1).Gammaℝ * -I * -(↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * -(↑n : ℂ))) /
        HPow.hPow (α := ℂ) (↑n : ℂ) s /
      2

Tactic:
rw [div_right_comm]

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

Tactic:
rcases eq_or_ne n 0 with rfl | h

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

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

Tactic:
simp_rw [Int.sign_natCast_of_ne_zero h, Int.cast_one, ofReal_sin, Complex.sin]

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

Tactic:
simp only [← mul_div_assoc, push_cast, mul_assoc (Gammaℝ _), ← mul_add]

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

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

Tactic:
rw [mul_one, mul_neg_one, neg_neg, neg_mul I, ← sub_eq_neg_add, ← mul_sub, mul_comm,
    mul_neg, neg_mul]

Premises used: mul_sub, sub_eq_neg_add, neg_neg, mul_comm, neg_mul, mul_neg_one, mul_one, mul_neg, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun (n : ℕ) ↦
      ((s + 1).Gammaℝ * -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) +
            (s + 1).Gammaℝ * -I * -(↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * -(↑n : ℂ))) /
          HPow.hPow (α := ℂ) (↑n : ℂ) s /
        2)
    (completedSinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
n : ℕ
h : n ≠ 0
inr : -(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I) = -(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))
inr₁ : 2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I = 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)
⊢ I * (cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) - cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) =
    I * (cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) - cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)))

Tactic:
congr 3
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun (n : ℕ) ↦
      ((s + 1).Gammaℝ * -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) +
            (s + 1).Gammaℝ * -I * -(↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * -(↑n : ℂ))) /
          HPow.hPow (α := ℂ) (↑n : ℂ) s /
        2)
    (completedSinZeta (↑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 : ℕ) ↦
      ((s + 1).Gammaℝ * -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) +
            (s + 1).Gammaℝ * -I * -(↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * -(↑n : ℂ))) /
          HPow.hPow (α := ℂ) (↑n : ℂ) s /
        2)
    (completedSinZeta (↑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
r : (n : ℤ) → ℝ := fun (n : ℤ) ↦ (↑n : ℝ) + a
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ 1 / 2
t : ℝ
ht : 0 < t
⊢ HasSum (fun (n : ℤ) ↦ c n * (↑(r n) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r n) 2 * t)) : ℂ))
    ((↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)

Tactic:
((hasSum_ofReal.mpr (hasSum_int_oddKernel a ht)).div_const 2).congr_fun fun n ↦ ?_

Premises used: Iff.mpr, HasSum.congr_fun, Complex.hasSum_ofReal, HasSum.div_const, HurwitzZeta.hasSum_int_oddKernel, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
r : (n : ℤ) → ℝ := fun (n : ℤ) ↦ (↑n : ℝ) + a
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ 1 / 2
t : ℝ
ht : 0 < t
refine :
  ∀ (n : ℤ),
    c n * (↑(r n) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r n) 2 * t)) : ℂ) =
      (↑(((↑n : ℝ) + a) * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) / 2
⊢ HasSum (fun (n : ℤ) ↦ c n * (↑(r n) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r n) 2 * t)) : ℂ))
    ((↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)

Tactic:
refine ((hasSum_ofReal.mpr (hasSum_int_oddKernel a ht)).div_const 2).congr_fun fun n ↦ ?_

Premises used: Iff.mpr, HasSum.congr_fun, Complex.hasSum_ofReal, HasSum.div_const, HurwitzZeta.hasSum_int_oddKernel, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
r : (n : ℤ) → ℝ := fun (n : ℤ) ↦ (↑n : ℝ) + a
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ 1 / 2
t : ℝ
ht : 0 < t
n : ℤ
⊢ c n * (↑(r n) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r n) 2 * t)) : ℂ) =
    (↑(((↑n : ℝ) + a) * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) / 2

Tactic:
simp [r, c, push_cast, div_mul_eq_mul_div, -one_div]

Premises used: div_mul_eq_mul_div, one_div
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
r : (n : ℤ) → ℝ := fun (n : ℤ) ↦ (↑n : ℝ) + a
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ 1 / 2
⊢ ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑(r n) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r n) 2 * t)) : ℂ))
      ((↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)

Tactic:
have hF t (ht : 0 < t) : HasSum (fun n ↦ c n * r n * rexp (-π * (r n) ^ 2 * t))
      (oddKernel a t / 2) := by
    refine ((hasSum_ofReal.mpr (hasSum_int_oddKernel a ht)).div_const 2).congr_fun fun n ↦ ?_
    simp [r, c, push_cast, div_mul_eq_mul_div, -one_div]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
r : (n : ℤ) → ℝ := fun (n : ℤ) ↦ (↑n : ℝ) + a
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ 1 / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑(r n) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r n) 2 * t)) : ℂ))
      ((↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
simp_rw : Summable (α := ℝ) fun (i : ℤ) ↦ ‖1 / 2‖ * (1 / |r i| ^ s.re)
⊢ Summable (α := ℝ) fun (i : ℤ) ↦ ‖c i‖ / |r i| ^ s.re

Tactic:
simp_rw [c, ← mul_one_div ‖_‖]

Premises used: Norm.norm, mul_one_div
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
r : (n : ℤ) → ℝ := fun (n : ℤ) ↦ (↑n : ℝ) + a
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ 1 / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑(r n) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r n) 2 * t)) : ℂ))
      ((↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
hf : Summable (α := ℝ) fun (i : ℤ) ↦ 1 / |r i| ^ s.re
⊢ Summable (α := ℝ) fun (i : ℤ) ↦ ‖1 / 2‖ * (1 / |r i| ^ s.re)

Tactic:
apply Summable.mul_left

Premises used: Summable.mul_left
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
r : (n : ℤ) → ℝ := fun (n : ℤ) ↦ (↑n : ℝ) + a
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ 1 / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑(r n) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r n) 2 * t)) : ℂ))
      ((↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
hf hf₁ hf₂ hf₃ : 1 < s.re
⊢ Summable (α := ℝ) fun (i : ℤ) ↦ 1 / |r i| ^ s.re

Tactic:
rwa [summable_one_div_int_add_rpow]

Premises used: Real.summable_one_div_int_add_rpow
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
r : (n : ℤ) → ℝ := fun (n : ℤ) ↦ (↑n : ℝ) + a
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ 1 / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑(r n) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r n) 2 * t)) : ℂ))
      ((↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
h_sum : Summable (α := ℝ) fun (i : ℤ) ↦ ‖c i‖ / |r i| ^ s.re
⊢ HasSum (fun (i : ℤ) ↦ (s + 1).Gammaℝ * c i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s)
    (HDiv.hDiv (α := ℂ) (mellin (fun (t : ℝ) ↦ (↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)) ((s + 1) / 2))
      2)

Tactic:
have := mellin_div_const .. ▸ hasSum_mellin_pi_mul_sq' (zero_lt_one.trans hs) hF h_sum
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
r : (n : ℤ) → ℝ := fun (n : ℤ) ↦ (↑n : ℝ) + a
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ 1 / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑(r n) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r n) 2 * t)) : ℂ))
      ((↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
h_sum : Summable (α := ℝ) fun (i : ℤ) ↦ ‖c i‖ / |r i| ^ s.re
this :
  HasSum (fun (i : ℤ) ↦ (s + 1).Gammaℝ * c i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s)
    (HDiv.hDiv (α := ℂ) (mellin (fun (t : ℝ) ↦ (↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)) ((s + 1) / 2))
      2)
⊢ HasSum
    (fun (n : ℤ) ↦
      (s + 1).Gammaℝ * (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2)
    (completedHurwitzZetaOdd (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
this.congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun, HurwitzZeta.completedHurwitzZetaOdd, StrongFEPair.Λ
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
r : (n : ℤ) → ℝ := fun (n : ℤ) ↦ (↑n : ℝ) + a
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ 1 / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑(r n) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r n) 2 * t)) : ℂ))
      ((↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
h_sum : Summable (α := ℝ) fun (i : ℤ) ↦ ‖c i‖ / |r i| ^ s.re
this :
  HasSum (fun (i : ℤ) ↦ (s + 1).Gammaℝ * c i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s)
    (HDiv.hDiv (α := ℂ) (mellin (fun (t : ℝ) ↦ (↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)) ((s + 1) / 2))
      2)
refine :
  ∀ (n : ℤ),
    (s + 1).Gammaℝ * (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 =
      (s + 1).Gammaℝ * c n * (↑((SignType.sign : (a : ℝ) → SignType) (r n)) : ℂ) / (↑|r n| : ℂ) ^ s
⊢ HasSum
    (fun (n : ℤ) ↦
      (s + 1).Gammaℝ * (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2)
    (completedHurwitzZetaOdd (↑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
r : (n : ℤ) → ℝ := fun (n : ℤ) ↦ (↑n : ℝ) + a
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ 1 / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑(r n) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r n) 2 * t)) : ℂ))
      ((↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
h_sum : Summable (α := ℝ) fun (i : ℤ) ↦ ‖c i‖ / |r i| ^ s.re
this :
  HasSum (fun (i : ℤ) ↦ (s + 1).Gammaℝ * c i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s)
    (HDiv.hDiv (α := ℂ) (mellin (fun (t : ℝ) ↦ (↑(oddKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)) ((s + 1) / 2))
      2)
n : ℤ
⊢ (s + 1).Gammaℝ * (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 =
    (s + 1).Gammaℝ * c n * (↑((SignType.sign : (a : ℝ) → SignType) (r n)) : ℂ) / (↑|r n| : ℂ) ^ s

Tactic:
simp only [r, c, mul_one_div, div_mul_eq_mul_div, div_right_comm]

Premises used: div_right_comm, div_mul_eq_mul_div, mul_one_div
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
s : ℂ
simp_rw : completedHurwitzZetaOdd (-a) s / (s + 1).Gammaℝ = -(completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)
simp_rw₁ : -completedHurwitzZetaOdd a s / (s + 1).Gammaℝ = -(completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)
⊢ hurwitzZetaOdd (-a) s = -hurwitzZetaOdd a s

Tactic:
simp_rw [hurwitzZetaOdd, completedHurwitzZetaOdd_neg, neg_div]

Premises used: neg_div, HurwitzZeta.hurwitzZetaOdd, HurwitzZeta.completedHurwitzZetaOdd_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
⊢ Differentiable ℂ (hurwitzZetaOdd a)

Tactic:
(differentiable_completedHurwitzZetaOdd a).mul <| differentiable_Gammaℝ_inv.comp <|
    differentiable_id.add <| differentiable_const _

Premises used: HurwitzZeta.hurwitzZetaOdd, Complex.differentiable_Gammaℝ_inv, DivInvMonoid.div', differentiable_const, Differentiable.mul, differentiable_id, Differentiable.comp, Differentiable.add, HurwitzZeta.differentiable_completedHurwitzZetaOdd
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
s : ℂ
simp_rw : completedSinZeta (-a) s / (s + 1).Gammaℝ = -(completedSinZeta a s / (s + 1).Gammaℝ)
simp_rw₁ : -completedSinZeta a s / (s + 1).Gammaℝ = -(completedSinZeta a s / (s + 1).Gammaℝ)
⊢ sinZeta (-a) s = -sinZeta a s

Tactic:
simp_rw [sinZeta, completedSinZeta_neg, neg_div]

Premises used: neg_div, HurwitzZeta.completedSinZeta_neg, HurwitzZeta.sinZeta
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
⊢ Differentiable ℂ (sinZeta a)

Tactic:
(differentiable_completedSinZeta a).mul <| differentiable_Gammaℝ_inv.comp <|
    differentiable_id.add <| differentiable_const _

Premises used: Complex.differentiable_Gammaℝ_inv, DivInvMonoid.div', differentiable_const, HurwitzZeta.sinZeta, Differentiable.mul, differentiable_id, Differentiable.comp, Differentiable.add, HurwitzZeta.differentiable_completedSinZeta
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun (n : ℤ) ↦ (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2)
    (hurwitzZetaOdd (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
((hasSum_int_completedHurwitzZetaOdd a hs).div_const (Gammaℝ _)).congr_fun fun n ↦ ?_

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

Tactic:
refine ((hasSum_int_completedHurwitzZetaOdd a hs).div_const (Gammaℝ _)).congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun, Complex.Gammaℝ, HurwitzZeta.hasSum_int_completedHurwitzZetaOdd, HasSum.div_const
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
⊢ 0 < s.re + 1

Tactic:
positivity
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
⊢ 0 < (s + 1).re

Tactic:
have : 0 < re (s + 1) := by rw [add_re, one_re]; positivity
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
this : 0 < (s + 1).re
⊢ (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 =
    (s + 1).Gammaℝ * (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 /
      (s + 1).Gammaℝ

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

Premises used: div_right_comm, Complex.Gammaℝ, mul_div_cancel_left₀, Complex.Gammaℝ_ne_zero_of_re_pos