awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw₅ :
  completedSinZeta a 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) * (completedSinZeta a s / (s + 1).Gammaℝ)
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
rw₅ :
  completedSinZeta a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
rw₆ :
  completedSinZeta a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (completedSinZeta a s / (s + 1).Gammaℝ)
⊢ 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) * (completedSinZeta a s / (s + 1).Gammaℝ)
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
rw₅ :
  completedSinZeta a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
rw₆ :
  completedSinZeta a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (completedSinZeta a s / (s + 1).Gammaℝ)
rw₇ :
  completedSinZeta a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) / (s + 1).Gammaℝ) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (completedSinZeta a s / (s + 1).Gammaℝ)
⊢ 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) * (completedSinZeta a s / (s + 1).Gammaℝ)
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
rw₅ :
  completedSinZeta a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
rw₆ :
  completedSinZeta a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (completedSinZeta a s / (s + 1).Gammaℝ)
rw₇ :
  completedSinZeta a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) / (s + 1).Gammaℝ) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (completedSinZeta a s / (s + 1).Gammaℝ)
rw₈ :
  completedSinZeta a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2)) / (s + 1).Gammaℝ =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (completedSinZeta a s / (s + 1).Gammaℝ)
⊢ 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) * completedSinZeta a s / (s + 1).Gammaℝ
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
rw₅ :
  completedSinZeta a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
rw₆ :
  completedSinZeta a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (completedSinZeta a s / (s + 1).Gammaℝ)
rw₇ :
  completedSinZeta a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) / (s + 1).Gammaℝ) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (completedSinZeta a s / (s + 1).Gammaℝ)
rw₈ :
  completedSinZeta a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2)) / (s + 1).Gammaℝ =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (completedSinZeta a s / (s + 1).Gammaℝ)
rw₉ :
  completedSinZeta a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2)) / (s + 1).Gammaℝ =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * completedSinZeta a s / (s + 1).Gammaℝ
⊢ hurwitzZetaOdd a (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s
have rw₁₀ : s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * completedSinZeta a s / (s + 1).Gammaℝ =
  s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * completedSinZeta a s / (s + 1).Gammaℝ
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 : ℂ)
⊢ sinZeta a (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
have rw : sinZeta a (1 - s) = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
Tactic: rw [← Gammaℂ, sinZeta, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv, inv_Gammaℝ_two_sub hs,
    completedSinZeta_one_sub, hurwitzZetaOdd, ← 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 : sinZeta a (1 - s) = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
⊢ sinZeta a (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
have rw₁ : completedSinZeta a (1 - s) / (1 - s + 1).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
Tactic: rw [← Gammaℂ, sinZeta, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv, inv_Gammaℝ_two_sub hs,
    completedSinZeta_one_sub, hurwitzZetaOdd, ← 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 : sinZeta a (1 - s) = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₁ : completedSinZeta a (1 - s) / (1 - s + 1).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
⊢ sinZeta a (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
have rw₂ : completedSinZeta a (1 - s) / (2 - s).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
Tactic: rw [← Gammaℂ, sinZeta, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv, inv_Gammaℝ_two_sub hs,
    completedSinZeta_one_sub, hurwitzZetaOdd, ← 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 : sinZeta a (1 - s) = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₁ : completedSinZeta a (1 - s) / (1 - s + 1).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₂ : completedSinZeta a (1 - s) / (2 - s).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
⊢ sinZeta a (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
have rw₃ : completedSinZeta a (1 - s) * (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
Tactic: rw [← Gammaℂ, sinZeta, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv, inv_Gammaℝ_two_sub hs,
    completedSinZeta_one_sub, hurwitzZetaOdd, ← 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 : sinZeta a (1 - s) = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₁ : completedSinZeta a (1 - s) / (1 - s + 1).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₂ : completedSinZeta a (1 - s) / (2 - s).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₃ : completedSinZeta a (1 - s) * (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
⊢ sinZeta a (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
have rw₄ : completedSinZeta a (1 - s) * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
  s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
Tactic: rw [← Gammaℂ, sinZeta, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv, inv_Gammaℝ_two_sub hs,
    completedSinZeta_one_sub, hurwitzZetaOdd, ← 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 : sinZeta a (1 - s) = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₁ : completedSinZeta a (1 - s) / (1 - s + 1).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₂ : completedSinZeta a (1 - s) / (2 - s).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₃ : completedSinZeta a (1 - s) * (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₄ :
  completedSinZeta a (1 - s) * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
⊢ sinZeta a (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
have rw₅ : completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
  s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
Tactic: rw [← Gammaℂ, sinZeta, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv, inv_Gammaℝ_two_sub hs,
    completedSinZeta_one_sub, hurwitzZetaOdd, ← 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 : sinZeta a (1 - s) = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₁ : completedSinZeta a (1 - s) / (1 - s + 1).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₂ : completedSinZeta a (1 - s) / (2 - s).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₃ : completedSinZeta a (1 - s) * (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₄ :
  completedSinZeta a (1 - s) * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₅ :
  completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
⊢ sinZeta a (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
have rw₆ : completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
  s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)
Tactic: rw [← Gammaℂ, sinZeta, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv, inv_Gammaℝ_two_sub hs,
    completedSinZeta_one_sub, hurwitzZetaOdd, ← 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 : sinZeta a (1 - s) = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₁ : completedSinZeta a (1 - s) / (1 - s + 1).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₂ : completedSinZeta a (1 - s) / (2 - s).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₃ : completedSinZeta a (1 - s) * (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₄ :
  completedSinZeta a (1 - s) * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₅ :
  completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₆ :
  completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)
⊢ sinZeta a (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
have rw₇ : completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) / (s + 1).Gammaℝ) =
  s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)
Tactic: rw [← Gammaℂ, sinZeta, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv, inv_Gammaℝ_two_sub hs,
    completedSinZeta_one_sub, hurwitzZetaOdd, ← 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 : sinZeta a (1 - s) = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₁ : completedSinZeta a (1 - s) / (1 - s + 1).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₂ : completedSinZeta a (1 - s) / (2 - s).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₃ : completedSinZeta a (1 - s) * (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₄ :
  completedSinZeta a (1 - s) * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₅ :
  completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₆ :
  completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)
rw₇ :
  completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) / (s + 1).Gammaℝ) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)
⊢ sinZeta a (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
have rw₈ : completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2)) / (s + 1).Gammaℝ =
  s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)
Tactic: rw [← Gammaℂ, sinZeta, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv, inv_Gammaℝ_two_sub hs,
    completedSinZeta_one_sub, hurwitzZetaOdd, ← 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 : sinZeta a (1 - s) = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₁ : completedSinZeta a (1 - s) / (1 - s + 1).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₂ : completedSinZeta a (1 - s) / (2 - s).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₃ : completedSinZeta a (1 - s) * (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₄ :
  completedSinZeta a (1 - s) * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₅ :
  completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₆ :
  completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)
rw₇ :
  completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) / (s + 1).Gammaℝ) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)
rw₈ :
  completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2)) / (s + 1).Gammaℝ =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)
⊢ sinZeta a (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
have rw₉ : completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2)) / (s + 1).Gammaℝ =
  s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * completedHurwitzZetaOdd a s / (s + 1).Gammaℝ
Tactic: rw [← Gammaℂ, sinZeta, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv, inv_Gammaℝ_two_sub hs,
    completedSinZeta_one_sub, hurwitzZetaOdd, ← 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 : sinZeta a (1 - s) = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₁ : completedSinZeta a (1 - s) / (1 - s + 1).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₂ : completedSinZeta a (1 - s) / (2 - s).Gammaℝ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₃ : completedSinZeta a (1 - s) * (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₄ :
  completedSinZeta a (1 - s) * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₅ :
  completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
rw₆ :
  completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)
rw₇ :
  completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) / (s + 1).Gammaℝ) =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)
rw₈ :
  completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2)) / (s + 1).Gammaℝ =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * (completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)
rw₉ :
  completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2)) / (s + 1).Gammaℝ =
    s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * completedHurwitzZetaOdd a s / (s + 1).Gammaℝ
⊢ sinZeta a (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * Complex.sin ((↑π : ℂ) * s / 2) * hurwitzZetaOdd a s
have rw₁₀ : s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * completedHurwitzZetaOdd a s / (s + 1).Gammaℝ =
  s.Gammaℂ * Complex.sin ((↑π : ℂ) * s / 2) * completedHurwitzZetaOdd a s / (s + 1).Gammaℝ
Tactic: rw [← Gammaℂ, sinZeta, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv, inv_Gammaℝ_two_sub hs,
    completedSinZeta_one_sub, hurwitzZetaOdd, ← div_eq_mul_inv, ← mul_div_assoc, ← mul_div_assoc,
    mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ cosZeta (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / 2 / (↑(2 * k)! : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
have rw : ∑' (b : ℕ), (↑(Real.cos (2 * π * x * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) (HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
  HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / 2 / (↑(2 * k)! : ℂ) *
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
Tactic: rw [← (hasSum_nat_cosZeta x (?_ : 1 < re (2 * k))).tsum_eq]