awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ I * (cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) - cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) =
    I * (cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) - cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)))
have inr : -(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I) = -(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
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 : ℂ)))
have inr₁ : 2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I = 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)
Tactic: congr 3
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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)
have refine : ∀ (n : ℤ),
  c n * (↑(r n) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r n) 2 * t)) : ℂ) =
    (↑(((↑n : ℝ) + a) * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) / 2
Tactic: refine ((hasSum_ofReal.mpr (hasSum_int_oddKernel a ht)).div_const 2).congr_fun fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (hypothesis)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
r : (n : ℤ) → ℝ := fun (n : ℤ) ↦ (↑n : ℝ) + a
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ 1 / 2
⊢ HasSum
    (fun (n : ℤ) ↦
      (s + 1).Gammaℝ * (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2)
    (completedHurwitzZetaOdd (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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)
⊢ Summable (α := ℝ) fun (i : ℤ) ↦ ‖c i‖ / |r i| ^ s.re
have simp_rw : Summable (α := ℝ) fun (i : ℤ) ↦ ‖1 / 2‖ * (1 / |r i| ^ s.re)
Tactic: simp_rw [c, ← mul_one_div ‖_‖]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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)
⊢ Summable (α := ℝ) fun (i : ℤ) ↦ ‖1 / 2‖ * (1 / |r i| ^ s.re)
have hf : Summable (α := ℝ) fun (i : ℤ) ↦ 1 / |r i| ^ s.re
Tactic: apply Summable.mul_left
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (hypothesis)
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 (n : ℤ) ↦
      (s + 1).Gammaℝ * (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2)
    (completedHurwitzZetaOdd (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have 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)
Tactic: have := mellin_div_const .. ▸ hasSum_mellin_pi_mul_sq' (zero_lt_one.trans hs) hF h_sum
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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)
have 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
Tactic: refine this.congr_fun fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
s : ℂ
⊢ hurwitzZetaOdd (-a) s = -hurwitzZetaOdd a s
have simp_rw : completedHurwitzZetaOdd (-a) s / (s + 1).Gammaℝ = -(completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)
Tactic: simp_rw [hurwitzZetaOdd, completedHurwitzZetaOdd_neg, neg_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
s : ℂ
simp_rw : completedHurwitzZetaOdd (-a) s / (s + 1).Gammaℝ = -(completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)
⊢ hurwitzZetaOdd (-a) s = -hurwitzZetaOdd a s
have simp_rw₁ : -completedHurwitzZetaOdd a s / (s + 1).Gammaℝ = -(completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)
Tactic: simp_rw [hurwitzZetaOdd, completedHurwitzZetaOdd_neg, neg_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
s : ℂ
⊢ sinZeta (-a) s = -sinZeta a s
have simp_rw : completedSinZeta (-a) s / (s + 1).Gammaℝ = -(completedSinZeta a s / (s + 1).Gammaℝ)
Tactic: simp_rw [sinZeta, completedSinZeta_neg, neg_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : UnitAddCircle
s : ℂ
simp_rw : completedSinZeta (-a) s / (s + 1).Gammaℝ = -(completedSinZeta a s / (s + 1).Gammaℝ)
⊢ sinZeta (-a) s = -sinZeta a s
have simp_rw₁ : -completedSinZeta a s / (s + 1).Gammaℝ = -(completedSinZeta a s / (s + 1).Gammaℝ)
Tactic: simp_rw [sinZeta, completedSinZeta_neg, neg_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
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)
have 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ℝ
Tactic: refine ((hasSum_int_completedHurwitzZetaOdd a hs).div_const (Gammaℝ _)).congr_fun fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (hypothesis)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
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ℝ
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 (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum
    (fun (n : ℕ) ↦
      ((↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s -
          (↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s) /
        2)
    (hurwitzZetaOdd (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have refine : ∀ (n : ℕ),
  ((↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s -
        (↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
          (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s) /
      2 =
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑(↑n : ℤ) : ℝ) + a)) : ℂ) / (↑|(↑(↑n : ℤ) : ℝ) + a| : ℂ) ^ s / 2 +
      (↑((SignType.sign : (a : ℝ) → SignType) ((↑(-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℝ) + a)) : ℂ) /
          (↑|(↑(-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℝ) + a| : ℂ) ^ s /
        2
Tactic: refine (hasSum_int_hurwitzZetaOdd a hs).nat_add_neg_add_one.congr_fun fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ ((↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s -
        (↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
          (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s) /
      2 =
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑(↑n : ℤ) : ℝ) + a)) : ℂ) / (↑|(↑(↑n : ℤ) : ℝ) + a| : ℂ) ^ s / 2 +
      (↑((SignType.sign : (a : ℝ) → SignType) ((↑(-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℝ) + a)) : ℂ) /
          (↑|(↑(-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℝ) + a| : ℂ) ^ s /
        2
have rw : (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
    -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
          (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
        2) =
  (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
    (↑((SignType.sign : (a : ℝ) → SignType) (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a)) : ℂ) /
        (↑|-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a| : ℂ) ^ s /
      2
Tactic: rw [Int.cast_neg, Int.cast_add, Int.cast_one, sub_div, sub_eq_add_neg, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (hypothesis)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
          2) =
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      (↑((SignType.sign : (a : ℝ) → SignType) (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a)) : ℂ) /
          (↑|-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a| : ℂ) ^ s /
        2
have this : -HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a = -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)
Tactic: have : -(n + 1) + a = -(n + 1 - a) := by ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
this : -HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a = -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)
⊢ (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
          2) =
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      (↑((SignType.sign : (a : ℝ) → SignType) (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a)) : ℂ) /
          (↑|-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a| : ℂ) ^ s /
        2
have rw : (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
    -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
          (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
        2) =
  (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
    (↑((SignType.sign : (a : ℝ) → SignType) (-(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a))) : ℂ) /
        (↑|(-(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a))| : ℂ) ^ s /
      2
Tactic: rw [this, Left.sign_neg, abs_neg, SignType.coe_neg, neg_div, neg_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
this : -HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a = -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)
rw :
  (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
          2) =
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      (↑((SignType.sign : (a : ℝ) → SignType) (-(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a))) : ℂ) /
          (↑|(-(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a))| : ℂ) ^ s /
        2
⊢ (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
          2) =
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      (↑((SignType.sign : (a : ℝ) → SignType) (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a)) : ℂ) /
          (↑|-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a| : ℂ) ^ s /
        2
have rw₁ : (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
    -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
          (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
        2) =
  (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
    (↑(-(SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
        (↑|(-(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a))| : ℂ) ^ s /
      2
Tactic: rw [this, Left.sign_neg, abs_neg, SignType.coe_neg, neg_div, neg_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
this : -HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a = -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)
rw :
  (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
          2) =
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      (↑((SignType.sign : (a : ℝ) → SignType) (-(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a))) : ℂ) /
          (↑|(-(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a))| : ℂ) ^ s /
        2
rw₁ :
  (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
          2) =
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      (↑(-(SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
          (↑|(-(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a))| : ℂ) ^ s /
        2
⊢ (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
          2) =
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      (↑((SignType.sign : (a : ℝ) → SignType) (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a)) : ℂ) /
          (↑|-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a| : ℂ) ^ s /
        2
have rw₂ : (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
    -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
          (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
        2) =
  (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
    (↑(-(SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
        (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
      2
Tactic: rw [this, Left.sign_neg, abs_neg, SignType.coe_neg, neg_div, neg_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
this : -HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a = -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)
rw :
  (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
          2) =
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      (↑((SignType.sign : (a : ℝ) → SignType) (-(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a))) : ℂ) /
          (↑|(-(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a))| : ℂ) ^ s /
        2
rw₁ :
  (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
          2) =
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      (↑(-(SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
          (↑|(-(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a))| : ℂ) ^ s /
        2
rw₂ :
  (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
          2) =
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      (↑(-(SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
          (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
        2
⊢ (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
          2) =
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      (↑((SignType.sign : (a : ℝ) → SignType) (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a)) : ℂ) /
          (↑|-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a| : ℂ) ^ s /
        2
have rw₃ : (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
    -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
          (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
        2) =
  (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
    -(↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
        (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
      2
Tactic: rw [this, Left.sign_neg, abs_neg, SignType.coe_neg, neg_div, neg_div]
-- 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
⊢ HasSum (fun (n : ℕ) ↦ (1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s - 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s) / 2)
    (hurwitzZetaOdd (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have refine : ∀ (n : ℕ),
  (1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s - 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s) / 2 =
    ((↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s -
        (↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
          (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s) /
      2
Tactic: refine (hasSum_nat_hurwitzZetaOdd a hs).congr_fun fun n ↦ ?_
-- 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 : ℕ
⊢ (1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s - 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s) / 2 =
    ((↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s -
        (↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
          (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s) /
      2
have suffices : ∀ (b : ℝ),
  0 ≤ b →
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + b)) : ℂ) / (↑|(↑n : ℝ) + b| : ℂ) ^ s =
      1 / ((↑n : ℂ) + (↑b : ℂ)) ^ s
Tactic: suffices ∀ b : ℝ, 0 ≤ b → SignType.sign (n + b) / (↑|n + b| : ℂ) ^ s = 1 / (n + b) ^ s by
    simp only [add_sub_assoc, this a ha.1, this (1 - a) (sub_nonneg.mpr ha.2), push_cast]
-- 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 : 0 ≤ b
⊢ (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + b)) : ℂ) / (↑|(↑n : ℝ) + b| : ℂ) ^ s =
    1 / ((↑n : ℂ) + (↑b : ℂ)) ^ s
have rw : (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + b)) : ℂ) / (↑((↑n : ℝ) + b) : ℂ) ^ s = 1 / (↑((↑n : ℝ) + b) : ℂ) ^ s
Tactic: rw [abs_of_nonneg (by positivity), (by simp : (n : ℂ) + b = ↑(n + b))]
-- 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 : 0 ≤ b
⊢ (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + b)) : ℂ) / (↑((↑n : ℝ) + b) : ℂ) ^ s =
    1 / (↑((↑n : ℝ) + b) : ℂ) ^ s
have inl : ∀ (hb : 0 < (↑n : ℝ) + b),
  (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + b)) : ℂ) / (↑((↑n : ℝ) + b) : ℂ) ^ s =
    1 / (↑((↑n : ℝ) + b) : ℂ) ^ s
Tactic: rcases lt_or_eq_of_le (by positivity : 0 ≤ n + b) with hb | hb
-- 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 : 0 ≤ b
inl :
  ∀ (hb : 0 < (↑n : ℝ) + b),
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + b)) : ℂ) / (↑((↑n : ℝ) + b) : ℂ) ^ s =
      1 / (↑((↑n : ℝ) + b) : ℂ) ^ s
⊢ (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + b)) : ℂ) / (↑((↑n : ℝ) + b) : ℂ) ^ s =
    1 / (↑((↑n : ℝ) + b) : ℂ) ^ s
have inr : ∀ (hb : 0 = (↑n : ℝ) + b),
  (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + b)) : ℂ) / (↑((↑n : ℝ) + b) : ℂ) ^ s =
    1 / (↑((↑n : ℝ) + b) : ℂ) ^ s
Tactic: rcases lt_or_eq_of_le (by positivity : 0 ≤ n + b) with hb | hb