awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (hypothesis)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
⊢ HasSum
    (fun (n : ℤ) ↦
      (s + 1).Gammaℝ * -I * (↑n.sign : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) /
          HPow.hPow (α := ℂ) (↑|n| : ℂ) s /
        2)
    (completedSinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
Tactic: have hc (n : ℤ) : ‖c n‖ = 1 / 2 := by
    simp_rw [c, (by { push_cast; ring } : 2 * π * I * a * n = ↑(2 * π * a * n) * I), norm_div,
      RCLike.norm_ofNat, norm_mul, norm_neg, norm_I, one_mul, norm_exp_ofReal_mul_I]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
t : ℝ
ht : 0 < t
⊢ HasSum (fun (n : ℤ) ↦ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
    ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
have refine : ∀ (n : ℤ),
  c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) =
    -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) /
      2
Tactic: refine ((hasSum_int_sinKernel a ht).div_const 2).congr_fun fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
t : ℝ
ht : 0 < t
n : ℤ
⊢ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) =
    -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) /
      2
have rw : -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) * (↑n : ℂ) / 2 *
    (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) =
  -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
      (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) /
    2
Tactic: rw [div_mul_eq_mul_div, div_mul_eq_mul_div, mul_right_comm (-I)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
t : ℝ
ht : 0 < t
n : ℤ
rw :
  -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) * (↑n : ℂ) / 2 *
      (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) =
    -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) /
      2
⊢ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) =
    -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) /
      2
have rw₁ : -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) * (↑n : ℂ) *
      (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) /
    2 =
  -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
      (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) /
    2
Tactic: rw [div_mul_eq_mul_div, div_mul_eq_mul_div, mul_right_comm (-I)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
t : ℝ
ht : 0 < t
n : ℤ
rw :
  -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) * (↑n : ℂ) / 2 *
      (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) =
    -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) /
      2
rw₁ :
  -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) * (↑n : ℂ) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) /
      2 =
    -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) /
      2
⊢ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) =
    -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) /
      2
have rw₂ : -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
      (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) /
    2 =
  -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
      (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) /
    2
Tactic: rw [div_mul_eq_mul_div, div_mul_eq_mul_div, mul_right_comm (-I)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (hypothesis)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
⊢ HasSum
    (fun (n : ℤ) ↦
      (s + 1).Gammaℝ * -I * (↑n.sign : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) /
          HPow.hPow (α := ℂ) (↑|n| : ℂ) s /
        2)
    (completedSinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have hF : ∀ (t : ℝ) (ht : 0 < t),
  HasSum (fun (n : ℤ) ↦ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
    ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
Tactic: have hF t (ht : 0 < t) :
      HasSum (fun n ↦ c n * n * rexp (-π * n ^ 2 * t)) (sinKernel a t / 2) := by
    refine ((hasSum_int_sinKernel a ht).div_const 2).congr_fun fun n ↦ ?_
    rw [div_mul_eq_mul_div, div_mul_eq_mul_div, mul_right_comm (-I)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
⊢ Summable (α := ℝ) fun (i : ℤ) ↦ ‖c i‖ / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re
have simp_rw : Summable (α := ℝ) fun (i : ℤ) ↦ 1 / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re / 2
Tactic: simp_rw [hc, div_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
⊢ Summable (α := ℝ) fun (i : ℤ) ↦ 1 / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re / 2
have h : Summable (α := ℝ) fun (i : ℤ) ↦ 1 / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re
Tactic: apply Summable.div_const
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
⊢ Summable (α := ℝ) fun (i : ℤ) ↦ 1 / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re
have h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) |(↑(↑n : ℤ) : ℝ)| s.re
Tactic: apply Summable.of_nat_of_neg
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
h : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) |(↑(↑n : ℤ) : ℝ)| s.re
⊢ Summable (α := ℝ) fun (i : ℤ) ↦ 1 / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re
have h₁ : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) |(↑(-(↑n : ℤ)) : ℝ)| s.re
Tactic: apply Summable.of_nat_of_neg
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (hypothesis)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
⊢ HasSum
    (fun (n : ℤ) ↦
      (s + 1).Gammaℝ * -I * (↑n.sign : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) /
          HPow.hPow (α := ℂ) (↑|n| : ℂ) s /
        2)
    (completedSinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have h_sum : Summable (α := ℝ) fun (i : ℤ) ↦ ‖c i‖ / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re
Tactic: have h_sum : Summable fun i ↦ ‖c i‖ / |↑i| ^ s.re := by
    simp_rw [hc, div_right_comm]
    apply Summable.div_const
    apply Summable.of_nat_of_neg <;>
    simpa
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
h_sum : Summable (α := ℝ) fun (i : ℤ) ↦ ‖c i‖ / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re
⊢ HasSum
    (fun (n : ℤ) ↦
      (s + 1).Gammaℝ * -I * (↑n.sign : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) /
          HPow.hPow (α := ℂ) (↑|n| : ℂ) s /
        2)
    (completedSinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have refine : ∀ (n : ℤ),
  (s + 1).Gammaℝ * -I * (↑n.sign : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) /
        HPow.hPow (α := ℂ) (↑|n| : ℂ) s /
      2 =
    (s + 1).Gammaℝ * c n * (↑((SignType.sign : (a : ℝ) → SignType) (↑n : ℝ)) : ℂ) / (↑|(↑n : ℝ)| : ℂ) ^ s
Tactic: refine (mellin_div_const .. ▸ hasSum_mellin_pi_mul_sq' (zero_lt_one.trans hs) hF h_sum).congr_fun
    fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ -I * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ c n * (↑n : ℂ) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) / 2)
h_sum : Summable (α := ℝ) fun (i : ℤ) ↦ ‖c i‖ / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re
n : ℤ
⊢ (s + 1).Gammaℝ * -I * (↑n.sign : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) /
        HPow.hPow (α := ℂ) (↑|n| : ℂ) s /
      2 =
    (s + 1).Gammaℝ * c n * (↑((SignType.sign : (a : ℝ) → SignType) (↑n : ℝ)) : ℂ) / (↑|(↑n : ℝ)| : ℂ) ^ s
have simp : -((s + 1).Gammaℝ * I * (↑((SignType.sign : (a : ℤ) → SignType) n) : ℂ) *
          cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) /
      HPow.hPow (α := ℂ) (↑|n| : ℂ) s /
    2 =
  (s + 1).Gammaℝ * c n * (↑((SignType.sign : (a : ℤ) → SignType) n) : ℂ) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s
Tactic: simp [Int.sign_eq_sign, ← Int.cast_abs]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (hypothesis)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun (n : ℕ) ↦ (s + 1).Gammaℝ * (↑(Real.sin (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (completedSinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have this : HasSum
  (fun (n : ℕ) ↦
    (s + 1).Gammaℝ * -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) /
          HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s /
        2 +
      (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ℝ * -I * (↑(Int.sign 0) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) /
        HPow.hPow (α := ℂ) (↑|0| : ℂ) s /
      2)
Tactic: have := (hasSum_int_completedSinZeta a hs).nat_add_neg
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (hypothesis)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun (n : ℕ) ↦
      (s + 1).Gammaℝ * -I * (↑(Int.sign (↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) /
            HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s /
          2 +
        (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ℝ * -I * (↑(Int.sign 0) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) /
          HPow.hPow (α := ℂ) (↑|0| : ℂ) s /
        2)
⊢ HasSum (fun (n : ℕ) ↦ (s + 1).Gammaℝ * (↑(Real.sin (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (completedSinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have 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)
Tactic: simp_rw [Int.sign_zero, Int.cast_zero, mul_zero, zero_mul, zero_div, add_zero, abs_neg,
    Int.sign_neg, Nat.abs_cast, Int.cast_neg, Int.cast_natCast, ← add_div] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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)
⊢ HasSum (fun (n : ℕ) ↦ (s + 1).Gammaℝ * (↑(Real.sin (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (completedSinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have 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
Tactic: refine this.congr_fun fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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 : ℕ
⊢ (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
have 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
Tactic: rw [div_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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 : ℕ
⊢ (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
have 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
Tactic: rcases eq_or_ne n 0 with rfl | h
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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
⊢ (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
have 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
Tactic: rcases eq_or_ne n 0 with rfl | h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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
⊢ (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
have 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
Tactic: simp_rw [Int.sign_natCast_of_ne_zero h, Int.cast_one, ofReal_sin, Complex.sin]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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
⊢ (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
have 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
Tactic: simp only [← mul_div_assoc, push_cast, mul_assoc (Gammaℝ _), ← mul_add]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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
⊢ (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
have 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 : ℂ))
Tactic: congr 3
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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
⊢ (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 : ℂ))
have inr : I * (cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) - cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) =
  I * (cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) - 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]