awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (hypothesis)
Goal:
n : ℕ
inst : NeZero n
χ : DirichletCharacter ℂ n
hχ : χ ≠ 1
⊢ ContinuousOn (Y := ℂ) (fun (s : ℂ) ↦ -deriv (LFunction χ) s / LFunction χ s) {s : ℂ | LFunction χ s ≠ 0}
have h : Differentiable ℂ (LFunction χ)
Tactic: have h := differentiable_LFunction hχ
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
s : ℂ
⊢ hurwitzZetaEven a s = (hurwitzZeta a s + hurwitzZeta (-a) s) / 2
have simp : hurwitzZetaEven a s = (hurwitzZetaEven a s + hurwitzZetaOdd a s + (hurwitzZetaEven a s + -hurwitzZetaOdd a s)) / 2
Tactic: simp only [hurwitzZeta, hurwitzZetaEven_neg, hurwitzZetaOdd_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
s : ℂ
⊢ hurwitzZetaOdd a s = (hurwitzZeta a s - hurwitzZeta (-a) s) / 2
have simp : hurwitzZetaOdd a s = (hurwitzZetaEven a s + hurwitzZetaOdd a s - (hurwitzZetaEven a s + -hurwitzZetaOdd a s)) / 2
Tactic: simp only [hurwitzZeta, hurwitzZetaEven_neg, hurwitzZetaOdd_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun (n : ℕ) ↦ 1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s) (hurwitzZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have h : Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ 1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s) fun (b : ℕ) ↦
  (1 / ((↑b : ℂ) + (↑a : ℂ)) ^ s + 1 / (HAdd.hAdd (α := ℂ) (↑b : ℂ) 1 - (↑a : ℂ)) ^ s) / 2 +
    (1 / ((↑b : ℂ) + (↑a : ℂ)) ^ s - 1 / (HAdd.hAdd (α := ℂ) (↑b : ℂ) 1 - (↑a : ℂ)) ^ s) / 2
Tactic: convert!
    (hasSum_nat_hurwitzZetaEven_of_mem_Icc ha hs).add (hasSum_nat_hurwitzZetaOdd_of_mem_Icc ha hs)
    using 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ 1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s) fun (b : ℕ) ↦
    (1 / ((↑b : ℂ) + (↑a : ℂ)) ^ s + 1 / (HAdd.hAdd (α := ℂ) (↑b : ℂ) 1 - (↑a : ℂ)) ^ s) / 2 +
      (1 / ((↑b : ℂ) + (↑a : ℂ)) ^ s - 1 / (HAdd.hAdd (α := ℂ) (↑b : ℂ) 1 - (↑a : ℂ)) ^ s) / 2
have h : ∀ (n : ℕ),
  1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s =
    (1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s + 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s) / 2 +
      (1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s - 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s) / 2
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * hurwitzZeta a s) (𝓝[≠] 1) (𝓝 1)
have simp : Tendsto (fun (s : ℂ) ↦ (s - 1) * hurwitzZetaEven a s + (s - 1) * hurwitzZetaOdd a s) (𝓝[≠] 1)
  (𝓝 (1 + HSub.hSub (α := ℂ) 1 1 * hurwitzZetaOdd a 1))
Tactic: simp only [hurwitzZeta, mul_add, (by simp : 𝓝 (1 : ℂ) = 𝓝 (1 + (1 - 1) * hurwitzZetaOdd a 1))]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
⊢ Tendsto (fun (s : ℂ) ↦ (s - 1) * hurwitzZetaEven a s + (s - 1) * hurwitzZetaOdd a s) (𝓝[≠] 1)
    (𝓝 (1 + HSub.hSub (α := ℂ) 1 1 * hurwitzZetaOdd a 1))
have refine_1 : Tendsto (fun (s : ℂ) ↦ s - 1) (𝓝 1) (𝓝 (HSub.hSub (α := ℂ) 1 1))
Tactic: refine (hurwitzZetaEven_residue_one a).add ((Tendsto.mul ?_ ?_).mono_left nhdsWithin_le_nhds)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
refine_1 : Tendsto (fun (s : ℂ) ↦ s - 1) (𝓝 1) (𝓝 (HSub.hSub (α := ℂ) 1 1))
⊢ Tendsto (fun (s : ℂ) ↦ (s - 1) * hurwitzZetaEven a s + (s - 1) * hurwitzZetaOdd a s) (𝓝[≠] 1)
    (𝓝 (1 + HSub.hSub (α := ℂ) 1 1 * hurwitzZetaOdd a 1))
have refine_2 : Tendsto (hurwitzZetaOdd a) (𝓝 1) (𝓝 (hurwitzZetaOdd a 1))
Tactic: refine (hurwitzZetaEven_residue_one a).add ((Tendsto.mul ?_ ?_).mono_left nhdsWithin_le_nhds)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ hurwitzZeta a s - 1 / (s - 1) / s.Gammaℝ) 1
have simp : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ + hurwitzZetaOdd a s) 1
Tactic: simp only [hurwitzZeta, add_sub_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
⊢ Tendsto (fun (s : ℂ) ↦ hurwitzZeta a s - 1 / (s - 1) / s.Gammaℝ) (𝓝 1) (𝓝 (hurwitzZeta a 1))
have simp : Tendsto (fun (s : ℂ) ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ + hurwitzZetaOdd a s) (𝓝 1)
  (𝓝 (hurwitzZetaEven a 1 + hurwitzZetaOdd a 1))
Tactic: simp only [hurwitzZeta, add_sub_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a b : UnitAddCircle
⊢ Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦ hurwitzZeta a s - hurwitzZeta b s
have simp : Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦
  hurwitzZetaEven a s - hurwitzZetaEven b s + (hurwitzZetaOdd a s - hurwitzZetaOdd b s)
Tactic: simp only [hurwitzZeta, add_sub_add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a b : UnitAddCircle
⊢ Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦
    hurwitzZetaEven a s - hurwitzZetaEven b s + (hurwitzZetaOdd a s - hurwitzZetaOdd b s)
have refine_1 : Differentiable ℂ (hurwitzZetaOdd a)
Tactic: refine (differentiable_hurwitzZetaEven_sub_hurwitzZetaEven a b).add (.sub ?_ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a b : UnitAddCircle
refine_1 : Differentiable ℂ (hurwitzZetaOdd a)
⊢ Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦
    hurwitzZetaEven a s - hurwitzZetaEven b s + (hurwitzZetaOdd a s - hurwitzZetaOdd b s)
have refine_2 : Differentiable ℂ (hurwitzZetaOdd b)
Tactic: refine (differentiable_hurwitzZetaEven_sub_hurwitzZetaEven a b).add (.sub ?_ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
s : ℂ
⊢ cosZeta a s = (expZeta a s + expZeta (-a) s) / 2
have rw : cosZeta a s = (cosZeta a s + I * sinZeta a s + (cosZeta a s + I * -sinZeta a s)) / 2
Tactic: rw [expZeta, expZeta, cosZeta_neg, sinZeta_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
s : ℂ
⊢ sinZeta a s = (expZeta a s - expZeta (-a) s) / (2 * I)
have rw : sinZeta a s = (cosZeta a s + I * sinZeta a s - (cosZeta a s + I * -sinZeta a s)) / (2 * I)
Tactic: rw [expZeta, expZeta, cosZeta_neg, sinZeta_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun (n : ℕ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (expZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have h : Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
  fun (b : ℕ) ↦
  (↑(Real.cos (2 * π * a * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) s +
    I * ((↑(Real.sin (2 * π * a * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) s)
Tactic: convert! (hasSum_nat_cosZeta a hs).add ((hasSum_nat_sinZeta a hs).mul_left I) using 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    fun (b : ℕ) ↦
    (↑(Real.cos (2 * π * a * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) s +
      I * ((↑(Real.sin (2 * π * a * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) s)
have h : ∀ (n : ℕ),
  cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    (↑(Real.cos (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
      I * ((↑(Real.sin (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    (↑(Real.cos (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
      I * ((↑(Real.sin (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
have h : (Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) + Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I) /
    HPow.hPow (α := ℂ) (↑n : ℂ) s =
  Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
    I * (Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
Tactic: simp only [mul_right_comm _ I, ← cos_add_sin_I, push_cast]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ (Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) + Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I) /
      HPow.hPow (α := ℂ) (↑n : ℂ) s =
    Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
      I * (Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
have h : Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
    Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I / HPow.hPow (α := ℂ) (↑n : ℂ) s =
  Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
    I * (Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
Tactic: rw [add_div, mul_div, mul_comm _ I]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
h :
  Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
      Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
      I * (Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
⊢ (Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) + Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I) /
      HPow.hPow (α := ℂ) (↑n : ℂ) s =
    Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
      I * (Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
have h₁ : Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
    Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I / HPow.hPow (α := ℂ) (↑n : ℂ) s =
  Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
    I * Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s
Tactic: rw [add_div, mul_div, mul_comm _ I]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
h :
  Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
      Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
      I * (Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
h₁ :
  Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
      Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
      I * Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ (Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) + Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I) /
      HPow.hPow (α := ℂ) (↑n : ℂ) s =
    Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
      I * (Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
have h₂ : Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
    I * Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
  Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s +
    I * Complex.sin (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑n : ℂ) s
Tactic: rw [add_div, mul_div, mul_comm _ I]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 1 ∨ a ≠ 0
⊢ DifferentiableAt ℂ (expZeta a) s
have hf : DifferentiableAt ℂ (cosZeta a) s
Tactic: apply DifferentiableAt.add
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 1 ∨ a ≠ 0
hf : DifferentiableAt ℂ (cosZeta a) s
⊢ DifferentiableAt ℂ (expZeta a) s
have hg : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ I * sinZeta a s) s
Tactic: apply DifferentiableAt.add
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : a ≠ 0 ∨ s ≠ 1
⊢ hurwitzZeta a (1 - s) =
    (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
      (cexp (-(↑π : ℂ) * I * s / 2) * expZeta a s + cexp ((↑π : ℂ) * I * s / 2) * expZeta (-a) s)
have rw : 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * ((cexp ((↑π : ℂ) * s / 2 * I) + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) *
      cosZeta a s +
    2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
        ((cexp (-((↑π : ℂ) * s / 2) * I) - cexp ((↑π : ℂ) * s / 2 * I)) * I / 2) *
      sinZeta a s =
  (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
    (cexp (-(↑π : ℂ) * I * s / 2) * (cosZeta a s + I * sinZeta a s) +
      cexp ((↑π : ℂ) * I * s / 2) * (cosZeta a s + I * -sinZeta a s))
Tactic: rw [hurwitzZeta, hurwitzZetaEven_one_sub a hs hs', hurwitzZetaOdd_one_sub a hs,
    expZeta, expZeta, Complex.cos, Complex.sin, sinZeta_neg, cosZeta_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : a ≠ 0 ∨ s ≠ 1
⊢ 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * ((cexp ((↑π : ℂ) * s / 2 * I) + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) *
        cosZeta a s +
      2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
          ((cexp (-((↑π : ℂ) * s / 2) * I) - cexp ((↑π : ℂ) * s / 2 * I)) * I / 2) *
        sinZeta a s =
    (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
      (cexp (-(↑π : ℂ) * I * s / 2) * (cosZeta a s + I * sinZeta a s) +
        cexp ((↑π : ℂ) * I * s / 2) * (cosZeta a s + I * -sinZeta a s))
have rw : 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * ((cexp ((↑π : ℂ) * s / 2 * I) + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) *
      cosZeta a s +
    2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
        ((cexp (-((↑π : ℂ) * s / 2) * I) - cexp ((↑π : ℂ) * s / 2 * I)) * I / 2) *
      sinZeta a s =
  (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
    (cexp (-((↑π : ℂ) * s / 2) * I) * (cosZeta a s + I * sinZeta a s) +
      cexp ((↑π : ℂ) * s / 2 * I) * (cosZeta a s + I * -sinZeta a s))
Tactic: rw [show ↑π * I * s / 2 = ↑π * s / 2 * I by ring,
    show -↑π * I * s / 2 = -(↑π * s / 2) * I by ring]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : a ≠ 0 ∨ s ≠ 1
⊢ 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * ((cexp ((↑π : ℂ) * s / 2 * I) + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) *
        cosZeta a s +
      2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
          ((cexp (-((↑π : ℂ) * s / 2) * I) - cexp ((↑π : ℂ) * s / 2 * I)) * I / 2) *
        sinZeta a s =
    (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
      (cexp (-((↑π : ℂ) * s / 2) * I) * (cosZeta a s + I * sinZeta a s) +
        cexp ((↑π : ℂ) * s / 2 * I) * (cosZeta a s + I * -sinZeta a s))
have generalize : ∀ (x : ℂ),
  2 * x * Complex.Gamma s * ((cexp ((↑π : ℂ) * s / 2 * I) + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) * cosZeta a s +
      2 * x * Complex.Gamma s * ((cexp (-((↑π : ℂ) * s / 2) * I) - cexp ((↑π : ℂ) * s / 2 * I)) * I / 2) * sinZeta a s =
    x * Complex.Gamma s *
      (cexp (-((↑π : ℂ) * s / 2) * I) * (cosZeta a s + I * sinZeta a s) +
        cexp ((↑π : ℂ) * s / 2 * I) * (cosZeta a s + I * -sinZeta a s))
Tactic: generalize (2 * π : ℂ) ^ (-s) = x
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : a ≠ 0 ∨ s ≠ 1
x : ℂ
⊢ 2 * x * Complex.Gamma s * ((cexp ((↑π : ℂ) * s / 2 * I) + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) * cosZeta a s +
      2 * x * Complex.Gamma s * ((cexp (-((↑π : ℂ) * s / 2) * I) - cexp ((↑π : ℂ) * s / 2 * I)) * I / 2) * sinZeta a s =
    x * Complex.Gamma s *
      (cexp (-((↑π : ℂ) * s / 2) * I) * (cosZeta a s + I * sinZeta a s) +
        cexp ((↑π : ℂ) * s / 2 * I) * (cosZeta a s + I * -sinZeta a s))
have generalize : ∀ (y : ℂ),
  2 * x * Complex.Gamma s * ((y + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) * cosZeta a s +
      2 * x * Complex.Gamma s * ((cexp (-((↑π : ℂ) * s / 2) * I) - y) * I / 2) * sinZeta a s =
    x * Complex.Gamma s *
      (cexp (-((↑π : ℂ) * s / 2) * I) * (cosZeta a s + I * sinZeta a s) + y * (cosZeta a s + I * -sinZeta a s))
Tactic: generalize (↑π * s / 2 * I).exp = y
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : a ≠ 0 ∨ s ≠ 1
x y : ℂ
⊢ 2 * x * Complex.Gamma s * ((y + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) * cosZeta a s +
      2 * x * Complex.Gamma s * ((cexp (-((↑π : ℂ) * s / 2) * I) - y) * I / 2) * sinZeta a s =
    x * Complex.Gamma s *
      (cexp (-((↑π : ℂ) * s / 2) * I) * (cosZeta a s + I * sinZeta a s) + y * (cosZeta a s + I * -sinZeta a s))
have generalize : ∀ (z : ℂ),
  2 * x * Complex.Gamma s * ((y + z) / 2) * cosZeta a s + 2 * x * Complex.Gamma s * ((z - y) * I / 2) * sinZeta a s =
    x * Complex.Gamma s * (z * (cosZeta a s + I * sinZeta a s) + y * (cosZeta a s + I * -sinZeta a s))
Tactic: generalize (-(↑π * s / 2) * I).exp = z
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
n : ℕ
⊢ s ≠ -(↑n : ℂ)
have h : -(↑n : ℂ) = HSub.hSub (α := ℂ) 1 (↑(n + 1) : ℂ)
Tactic: convert! hs (n + 1) using 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
n : ℕ
⊢ -(↑n : ℂ) = HSub.hSub (α := ℂ) 1 (↑(n + 1) : ℂ)
have h : -(↑n : ℂ) = 1 - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (hypothesis)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
⊢ expZeta a (1 - s) =
    (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
      (cexp ((↑π : ℂ) * I * s / 2) * hurwitzZeta a s + cexp (-(↑π : ℂ) * I * s / 2) * hurwitzZeta (-a) s)
have hs' : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
Tactic: have hs' (n : ℕ) : s ≠ -↑n := by
    convert! hs (n + 1) using 1
    push_cast
    ring
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
hs' : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
⊢ expZeta a (1 - s) =
    (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
      (cexp ((↑π : ℂ) * I * s / 2) * hurwitzZeta a s + cexp (-(↑π : ℂ) * I * s / 2) * hurwitzZeta (-a) s)
have rw : 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * ((cexp ((↑π : ℂ) * s / 2 * I) + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) *
      hurwitzZetaEven a s +
    I *
      (2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
          ((cexp (-((↑π : ℂ) * s / 2) * I) - cexp ((↑π : ℂ) * s / 2 * I)) * I / 2) *
        hurwitzZetaOdd a s) =
  (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
    (cexp ((↑π : ℂ) * I * s / 2) * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
      cexp (-(↑π : ℂ) * I * s / 2) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))
Tactic: rw [expZeta, cosZeta_one_sub a hs, sinZeta_one_sub a hs', hurwitzZeta, hurwitzZeta,
    hurwitzZetaEven_neg, hurwitzZetaOdd_neg, Complex.cos, Complex.sin]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
hs' : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
⊢ 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * ((cexp ((↑π : ℂ) * s / 2 * I) + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) *
        hurwitzZetaEven a s +
      I *
        (2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
            ((cexp (-((↑π : ℂ) * s / 2) * I) - cexp ((↑π : ℂ) * s / 2 * I)) * I / 2) *
          hurwitzZetaOdd a s) =
    (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
      (cexp ((↑π : ℂ) * I * s / 2) * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
        cexp (-(↑π : ℂ) * I * s / 2) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))
have rw : 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * ((cexp ((↑π : ℂ) * s / 2 * I) + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) *
      hurwitzZetaEven a s +
    I *
      (2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
          ((cexp (-((↑π : ℂ) * s / 2) * I) - cexp ((↑π : ℂ) * s / 2 * I)) * I / 2) *
        hurwitzZetaOdd a s) =
  (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
    (cexp ((↑π : ℂ) * s / 2 * I) * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
      cexp (-((↑π : ℂ) * s / 2) * I) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))
Tactic: rw [show ↑π * I * s / 2 = ↑π * s / 2 * I by ring,
    show -↑π * I * s / 2 = -(↑π * s / 2) * I by ring]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
hs' : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
⊢ 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * ((cexp ((↑π : ℂ) * s / 2 * I) + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) *
        hurwitzZetaEven a s +
      I *
        (2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
            ((cexp (-((↑π : ℂ) * s / 2) * I) - cexp ((↑π : ℂ) * s / 2 * I)) * I / 2) *
          hurwitzZetaOdd a s) =
    (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s *
      (cexp ((↑π : ℂ) * s / 2 * I) * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
        cexp (-((↑π : ℂ) * s / 2) * I) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))
have generalize : ∀ (x : ℂ),
  2 * x * Complex.Gamma s * ((cexp ((↑π : ℂ) * s / 2 * I) + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) * hurwitzZetaEven a s +
      I *
        (2 * x * Complex.Gamma s * ((cexp (-((↑π : ℂ) * s / 2) * I) - cexp ((↑π : ℂ) * s / 2 * I)) * I / 2) *
          hurwitzZetaOdd a s) =
    x * Complex.Gamma s *
      (cexp ((↑π : ℂ) * s / 2 * I) * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
        cexp (-((↑π : ℂ) * s / 2) * I) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))
Tactic: generalize (2 * π : ℂ) ^ (-s) = x
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
hs' : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
x : ℂ
⊢ 2 * x * Complex.Gamma s * ((cexp ((↑π : ℂ) * s / 2 * I) + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) * hurwitzZetaEven a s +
      I *
        (2 * x * Complex.Gamma s * ((cexp (-((↑π : ℂ) * s / 2) * I) - cexp ((↑π : ℂ) * s / 2 * I)) * I / 2) *
          hurwitzZetaOdd a s) =
    x * Complex.Gamma s *
      (cexp ((↑π : ℂ) * s / 2 * I) * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
        cexp (-((↑π : ℂ) * s / 2) * I) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))
have generalize : ∀ (y : ℂ),
  2 * x * Complex.Gamma s * ((y + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) * hurwitzZetaEven a s +
      I * (2 * x * Complex.Gamma s * ((cexp (-((↑π : ℂ) * s / 2) * I) - y) * I / 2) * hurwitzZetaOdd a s) =
    x * Complex.Gamma s *
      (y * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
        cexp (-((↑π : ℂ) * s / 2) * I) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))
Tactic: generalize (↑π * s / 2 * I).exp = y
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZeta (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ HSub.hSub (α := ℂ) 1 (↑n : ℂ)
hs' : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
x y : ℂ
⊢ 2 * x * Complex.Gamma s * ((y + cexp (-((↑π : ℂ) * s / 2) * I)) / 2) * hurwitzZetaEven a s +
      I * (2 * x * Complex.Gamma s * ((cexp (-((↑π : ℂ) * s / 2) * I) - y) * I / 2) * hurwitzZetaOdd a s) =
    x * Complex.Gamma s *
      (y * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
        cexp (-((↑π : ℂ) * s / 2) * I) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))
have generalize : ∀ (z : ℂ),
  2 * x * Complex.Gamma s * ((y + z) / 2) * hurwitzZetaEven a s +
      I * (2 * x * Complex.Gamma s * ((z - y) * I / 2) * hurwitzZetaOdd a s) =
    x * Complex.Gamma s *
      (y * (hurwitzZetaEven a s + hurwitzZetaOdd a s) + z * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))
Tactic: generalize (-(↑π * s / 2) * I).exp = z