awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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
have inr : (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℂ) / (↑0 : ℂ) ^ s = 1 / (↑0 : ℂ) ^ s
Tactic: rw [← hb, ofReal_zero, zero_cpow ((not_lt.mpr zero_le_one) ∘ (zero_re ▸ · ▸ hs)),
      div_zero, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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
⊢ (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + b)) : ℂ) / (↑((↑n : ℝ) + b) : ℂ) ^ s =
    1 / (↑((↑n : ℝ) + b) : ℂ) ^ s
have inr₁ : (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℂ) / HPow.hPow (α := ℂ) 0 s = 1 / HPow.hPow (α := ℂ) 0 s
Tactic: rw [← hb, ofReal_zero, zero_cpow ((not_lt.mpr zero_le_one) ∘ (zero_re ▸ · ▸ hs)),
      div_zero, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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
⊢ (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + b)) : ℂ) / (↑((↑n : ℝ) + b) : ℂ) ^ s =
    1 / (↑((↑n : ℝ) + b) : ℂ) ^ s
have inr₂ : HDiv.hDiv (α := ℂ) (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℂ) 0 = 1 / 0
Tactic: rw [← hb, ofReal_zero, zero_cpow ((not_lt.mpr zero_le_one) ∘ (zero_re ▸ · ▸ hs)),
      div_zero, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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
⊢ (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + b)) : ℂ) / (↑((↑n : ℝ) + b) : ℂ) ^ s =
    1 / (↑((↑n : ℝ) + b) : ℂ) ^ s
have inr₃ : 0 = 1 / 0
Tactic: rw [← hb, ofReal_zero, zero_cpow ((not_lt.mpr zero_le_one) ∘ (zero_re ▸ · ▸ hs)),
      div_zero, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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
⊢ (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + b)) : ℂ) / (↑((↑n : ℝ) + b) : ℂ) ^ s =
    1 / (↑((↑n : ℝ) + b) : ℂ) ^ s
have inr₄ : Eq (α := ℂ) 0 0
Tactic: rw [← hb, ofReal_zero, zero_cpow ((not_lt.mpr zero_le_one) ∘ (zero_re ▸ · ▸ hs)),
      div_zero, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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ℝ)
have 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ℝ
Tactic: refine ((hasSum_int_completedSinZeta a hs).div_const (Gammaℝ (s + 1))).congr_fun fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (hypothesis)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
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ℝ
have this : 0 < (s + 1).re
Tactic: have : 0 < re (s + 1) := by rw [add_re, one_re]; positivity
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (hypothesis)
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 : ℕ) ↦ (↑(Real.sin (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (sinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have 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)
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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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 : ℕ) ↦ (↑(Real.sin (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (sinZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have 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)
Tactic: simp_rw [push_cast, Complex.sin]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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)
have 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
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 : ℕ) ↦
      -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 : ℕ
⊢ (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
have 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
Tactic: rcases ne_or_eq n 0 with h | rfl
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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
⊢ (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
have 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
Tactic: rcases ne_or_eq n 0 with h | rfl
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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
⊢ (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
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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
⊢ (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
have inl : -(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I) = -(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))
Tactic: congr 5
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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 : ℂ))
⊢ (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
have inl₁ : 2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I = 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)
Tactic: congr 5
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
n : ℕ
⊢ HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1 + 1 = -HMul.hMul (α := ℂ) 2 (↑n : ℂ)
have rw : -HMul.hMul (α := ℂ) 2 (↑n : ℂ) - 1 + 1 = -HMul.hMul (α := ℂ) 2 (↑n : ℂ)
Tactic: rw [neg_mul, sub_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
n : ℕ
rw : -HMul.hMul (α := ℂ) 2 (↑n : ℂ) - 1 + 1 = -HMul.hMul (α := ℂ) 2 (↑n : ℂ)
⊢ HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1 + 1 = -HMul.hMul (α := ℂ) 2 (↑n : ℂ)
have rw₁ : -HMul.hMul (α := ℂ) 2 (↑n : ℂ) = -HMul.hMul (α := ℂ) 2 (↑n : ℂ)
Tactic: rw [neg_mul, sub_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
n : ℕ
⊢ hurwitzZetaOdd a (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1) = 0
have rw : completedHurwitzZetaOdd a (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1) / (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1 + 1).Gammaℝ = 0
Tactic: rw [hurwitzZetaOdd, Gammaℝ_eq_zero_iff.mpr ⟨n, by rw [neg_mul, sub_add_cancel]⟩, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
n : ℕ
rw :
  completedHurwitzZetaOdd a (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1) / (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1 + 1).Gammaℝ =
    0
⊢ hurwitzZetaOdd a (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1) = 0
have rw₁ : completedHurwitzZetaOdd a (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1) / 0 = 0
Tactic: rw [hurwitzZetaOdd, Gammaℝ_eq_zero_iff.mpr ⟨n, by rw [neg_mul, sub_add_cancel]⟩, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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
⊢ hurwitzZetaOdd a (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1) = 0
have rw₂ : Eq (α := ℂ) 0 0
Tactic: rw [hurwitzZetaOdd, Gammaℝ_eq_zero_iff.mpr ⟨n, by rw [neg_mul, sub_add_cancel]⟩, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
n : ℕ
⊢ sinZeta a (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1) = 0
have rw : completedSinZeta a (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1) / (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1 + 1).Gammaℝ = 0
Tactic: rw [sinZeta, Gammaℝ_eq_zero_iff.mpr ⟨n, by rw [neg_mul, sub_add_cancel]⟩, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
n : ℕ
rw : completedSinZeta a (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1) / (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1 + 1).Gammaℝ = 0
⊢ sinZeta a (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1) = 0
have rw₁ : completedSinZeta a (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1) / 0 = 0
Tactic: rw [sinZeta, Gammaℝ_eq_zero_iff.mpr ⟨n, by rw [neg_mul, sub_add_cancel]⟩, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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
⊢ sinZeta a (HMul.hMul (α := ℂ) (-2) (↑n : ℂ) - 1) = 0
have rw₂ : Eq (α := ℂ) 0 0
Tactic: rw [sinZeta, Gammaℝ_eq_zero_iff.mpr ⟨n, by rw [neg_mul, sub_add_cancel]⟩, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
⊢ hurwitzZetaOdd a (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
have rw : hurwitzZetaOdd a (1 - s) = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
Tactic: rw [← Gammaℂ, hurwitzZetaOdd, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv,
    inv_Gammaℝ_two_sub hs, completedHurwitzZetaOdd_one_sub, sinZeta, ← div_eq_mul_inv,
    ← mul_div_assoc, ← mul_div_assoc, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
rw : hurwitzZetaOdd a (1 - s) = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
⊢ hurwitzZetaOdd a (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
have rw₁ : completedHurwitzZetaOdd a (1 - s) / (1 - s + 1).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
Tactic: rw [← Gammaℂ, hurwitzZetaOdd, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv,
    inv_Gammaℝ_two_sub hs, completedHurwitzZetaOdd_one_sub, sinZeta, ← div_eq_mul_inv,
    ← mul_div_assoc, ← mul_div_assoc, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
rw : hurwitzZetaOdd a (1 - s) = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
rw₁ : completedHurwitzZetaOdd a (1 - s) / (1 - s + 1).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
⊢ hurwitzZetaOdd a (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
have rw₂ : completedHurwitzZetaOdd a (1 - s) / (2 - s).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
Tactic: rw [← Gammaℂ, hurwitzZetaOdd, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv,
    inv_Gammaℝ_two_sub hs, completedHurwitzZetaOdd_one_sub, sinZeta, ← div_eq_mul_inv,
    ← mul_div_assoc, ← mul_div_assoc, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
rw : hurwitzZetaOdd a (1 - s) = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
rw₁ : completedHurwitzZetaOdd a (1 - s) / (1 - s + 1).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
rw₂ : completedHurwitzZetaOdd a (1 - s) / (2 - s).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
⊢ hurwitzZetaOdd a (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
have rw₃ : completedHurwitzZetaOdd a (1 - s) * (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
Tactic: rw [← Gammaℂ, hurwitzZetaOdd, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv,
    inv_Gammaℝ_two_sub hs, completedHurwitzZetaOdd_one_sub, sinZeta, ← div_eq_mul_inv,
    ← mul_div_assoc, ← mul_div_assoc, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
rw : hurwitzZetaOdd a (1 - s) = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
rw₁ : completedHurwitzZetaOdd a (1 - s) / (1 - s + 1).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
rw₂ : completedHurwitzZetaOdd a (1 - s) / (2 - s).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
rw₃ : completedHurwitzZetaOdd a (1 - s) * (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
⊢ hurwitzZetaOdd a (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
have rw₄ : completedHurwitzZetaOdd a (1 - s) * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
  s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
Tactic: rw [← Gammaℂ, hurwitzZetaOdd, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv,
    inv_Gammaℝ_two_sub hs, completedHurwitzZetaOdd_one_sub, sinZeta, ← div_eq_mul_inv,
    ← mul_div_assoc, ← mul_div_assoc, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
rw : hurwitzZetaOdd a (1 - s) = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
rw₁ : completedHurwitzZetaOdd a (1 - s) / (1 - s + 1).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
rw₂ : completedHurwitzZetaOdd a (1 - s) / (2 - s).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
rw₃ : completedHurwitzZetaOdd a (1 - s) * (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
rw₄ :
  completedHurwitzZetaOdd a (1 - s) * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
⊢ hurwitzZetaOdd a (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
have rw₅ : completedSinZeta a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
  s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
Tactic: rw [← Gammaℂ, hurwitzZetaOdd, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv,
    inv_Gammaℝ_two_sub hs, completedHurwitzZetaOdd_one_sub, sinZeta, ← div_eq_mul_inv,
    ← mul_div_assoc, ← mul_div_assoc, mul_comm]