awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1 ≠ -(↑n : ℂ)
h3 : (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).Gammaℂ ≠ 0
e_a : Complex.sin ((↑π : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₁ : Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2 + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₂ : Complex.sin ((↑π : ℂ) * ((↑k : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₃ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₄ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / 2)) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₅ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / (↑2 : ℂ))) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₆ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑(HDiv.hDiv (α := ℝ) 1 2) : ℂ))) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₇ : Complex.sin ((↑π : ℂ) * (↑((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2) : ℂ)) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₈ : Complex.sin (↑(π * ((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₉ : (↑(Real.sin (π * ((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2))) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₀ : (↑(Real.sin (((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2) * π)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₁ : (↑(Real.sin ((↑k : ℝ) * π + HDiv.hDiv (α := ℝ) 1 2 * π)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₂ : (↑(Real.sin ((↑k : ℝ) * π + π * (1 / 2))) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₃ : (↑(Real.sin ((↑k : ℝ) * π + π / 2)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₄ : (↑(Real.cos ((↑k : ℝ) * π)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₅ : (↑(Real.cos ((↑k : ℝ) * π - 0)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₆ : (↑(HPow.hPow (α := ℝ) (-1) k * Real.cos 0) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₇ : (↑(HPow.hPow (α := ℝ) (-1) k * 1) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₈ : (↑(HPow.hPow (α := ℝ) (-1) k) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₉ : (↑(-1) : ℂ) ^ k * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
⊢ Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
have e_a₂₀ : (-(↑1 : ℂ)) ^ k * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
Tactic: rw [mul_div_assoc, add_div, mul_div_cancel_left₀ _ two_ne_zero, ← ofReal_natCast,
    ← ofReal_one, ← ofReal_ofNat, ← ofReal_div, ← ofReal_add, ← ofReal_mul,
    ← ofReal_sin, mul_comm π, add_mul, mul_comm (1 / 2), mul_one_div, Real.sin_add_pi_div_two,
    ← sub_zero (k * π), cos_nat_mul_pi_sub, Real.cos_zero, mul_one,
    ofReal_pow, ofReal_neg, ofReal_one, pow_succ, mul_neg_one, mul_neg, ← mul_pow, neg_one_mul,
    neg_neg, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1 ≠ -(↑n : ℂ)
h3 : (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).Gammaℂ ≠ 0
e_a : Complex.sin ((↑π : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₁ : Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2 + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₂ : Complex.sin ((↑π : ℂ) * ((↑k : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₃ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₄ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / 2)) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₅ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / (↑2 : ℂ))) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₆ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑(HDiv.hDiv (α := ℝ) 1 2) : ℂ))) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₇ : Complex.sin ((↑π : ℂ) * (↑((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2) : ℂ)) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₈ : Complex.sin (↑(π * ((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₉ : (↑(Real.sin (π * ((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2))) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₀ : (↑(Real.sin (((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2) * π)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₁ : (↑(Real.sin ((↑k : ℝ) * π + HDiv.hDiv (α := ℝ) 1 2 * π)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₂ : (↑(Real.sin ((↑k : ℝ) * π + π * (1 / 2))) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₃ : (↑(Real.sin ((↑k : ℝ) * π + π / 2)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₄ : (↑(Real.cos ((↑k : ℝ) * π)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₅ : (↑(Real.cos ((↑k : ℝ) * π - 0)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₆ : (↑(HPow.hPow (α := ℝ) (-1) k * Real.cos 0) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₇ : (↑(HPow.hPow (α := ℝ) (-1) k * 1) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₈ : (↑(HPow.hPow (α := ℝ) (-1) k) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₉ : (↑(-1) : ℂ) ^ k * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₂₀ : (-(↑1 : ℂ)) ^ k * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
⊢ Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
have e_a₂₁ : HPow.hPow (α := ℂ) (-1) k * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
Tactic: rw [mul_div_assoc, add_div, mul_div_cancel_left₀ _ two_ne_zero, ← ofReal_natCast,
    ← ofReal_one, ← ofReal_ofNat, ← ofReal_div, ← ofReal_add, ← ofReal_mul,
    ← ofReal_sin, mul_comm π, add_mul, mul_comm (1 / 2), mul_one_div, Real.sin_add_pi_div_two,
    ← sub_zero (k * π), cos_nat_mul_pi_sub, Real.cos_zero, mul_one,
    ofReal_pow, ofReal_neg, ofReal_one, pow_succ, mul_neg_one, mul_neg, ← mul_pow, neg_one_mul,
    neg_neg, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1 ≠ -(↑n : ℂ)
h3 : (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).Gammaℂ ≠ 0
e_a : Complex.sin ((↑π : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₁ : Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2 + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₂ : Complex.sin ((↑π : ℂ) * ((↑k : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₃ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₄ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / 2)) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₅ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / (↑2 : ℂ))) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₆ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑(HDiv.hDiv (α := ℝ) 1 2) : ℂ))) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₇ : Complex.sin ((↑π : ℂ) * (↑((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2) : ℂ)) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₈ : Complex.sin (↑(π * ((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₉ : (↑(Real.sin (π * ((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2))) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₀ : (↑(Real.sin (((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2) * π)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₁ : (↑(Real.sin ((↑k : ℝ) * π + HDiv.hDiv (α := ℝ) 1 2 * π)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₂ : (↑(Real.sin ((↑k : ℝ) * π + π * (1 / 2))) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₃ : (↑(Real.sin ((↑k : ℝ) * π + π / 2)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₄ : (↑(Real.cos ((↑k : ℝ) * π)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₅ : (↑(Real.cos ((↑k : ℝ) * π - 0)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₆ : (↑(HPow.hPow (α := ℝ) (-1) k * Real.cos 0) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₇ : (↑(HPow.hPow (α := ℝ) (-1) k * 1) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₈ : (↑(HPow.hPow (α := ℝ) (-1) k) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₉ : (↑(-1) : ℂ) ^ k * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₂₀ : (-(↑1 : ℂ)) ^ k * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₂₁ : HPow.hPow (α := ℂ) (-1) k * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
⊢ Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
have e_a₂₂ : HPow.hPow (α := ℂ) (-1) k * (HPow.hPow (α := ℂ) (-1) k * -1) = -1
Tactic: rw [mul_div_assoc, add_div, mul_div_cancel_left₀ _ two_ne_zero, ← ofReal_natCast,
    ← ofReal_one, ← ofReal_ofNat, ← ofReal_div, ← ofReal_add, ← ofReal_mul,
    ← ofReal_sin, mul_comm π, add_mul, mul_comm (1 / 2), mul_one_div, Real.sin_add_pi_div_two,
    ← sub_zero (k * π), cos_nat_mul_pi_sub, Real.cos_zero, mul_one,
    ofReal_pow, ofReal_neg, ofReal_one, pow_succ, mul_neg_one, mul_neg, ← mul_pow, neg_one_mul,
    neg_neg, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1 ≠ -(↑n : ℂ)
h3 : (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).Gammaℂ ≠ 0
e_a : Complex.sin ((↑π : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₁ : Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2 + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₂ : Complex.sin ((↑π : ℂ) * ((↑k : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₃ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₄ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / 2)) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₅ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / (↑2 : ℂ))) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₆ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑(HDiv.hDiv (α := ℝ) 1 2) : ℂ))) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₇ : Complex.sin ((↑π : ℂ) * (↑((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2) : ℂ)) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₈ : Complex.sin (↑(π * ((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₉ : (↑(Real.sin (π * ((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2))) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₀ : (↑(Real.sin (((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2) * π)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₁ : (↑(Real.sin ((↑k : ℝ) * π + HDiv.hDiv (α := ℝ) 1 2 * π)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₂ : (↑(Real.sin ((↑k : ℝ) * π + π * (1 / 2))) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₃ : (↑(Real.sin ((↑k : ℝ) * π + π / 2)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₄ : (↑(Real.cos ((↑k : ℝ) * π)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₅ : (↑(Real.cos ((↑k : ℝ) * π - 0)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₆ : (↑(HPow.hPow (α := ℝ) (-1) k * Real.cos 0) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₇ : (↑(HPow.hPow (α := ℝ) (-1) k * 1) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₈ : (↑(HPow.hPow (α := ℝ) (-1) k) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₉ : (↑(-1) : ℂ) ^ k * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₂₀ : (-(↑1 : ℂ)) ^ k * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₂₁ : HPow.hPow (α := ℂ) (-1) k * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₂₂ : HPow.hPow (α := ℂ) (-1) k * (HPow.hPow (α := ℂ) (-1) k * -1) = -1
⊢ Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
have e_a₂₃ : HPow.hPow (α := ℂ) (-1) k * -HPow.hPow (α := ℂ) (-1) k = -1
Tactic: rw [mul_div_assoc, add_div, mul_div_cancel_left₀ _ two_ne_zero, ← ofReal_natCast,
    ← ofReal_one, ← ofReal_ofNat, ← ofReal_div, ← ofReal_add, ← ofReal_mul,
    ← ofReal_sin, mul_comm π, add_mul, mul_comm (1 / 2), mul_one_div, Real.sin_add_pi_div_two,
    ← sub_zero (k * π), cos_nat_mul_pi_sub, Real.cos_zero, mul_one,
    ofReal_pow, ofReal_neg, ofReal_one, pow_succ, mul_neg_one, mul_neg, ← mul_pow, neg_one_mul,
    neg_neg, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1 ≠ -(↑n : ℂ)
h3 : (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).Gammaℂ ≠ 0
e_a : Complex.sin ((↑π : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₁ : Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2 + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₂ : Complex.sin ((↑π : ℂ) * ((↑k : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₃ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₄ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / 2)) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₅ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / (↑2 : ℂ))) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₆ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑(HDiv.hDiv (α := ℝ) 1 2) : ℂ))) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₇ : Complex.sin ((↑π : ℂ) * (↑((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2) : ℂ)) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₈ : Complex.sin (↑(π * ((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₉ : (↑(Real.sin (π * ((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2))) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₀ : (↑(Real.sin (((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2) * π)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₁ : (↑(Real.sin ((↑k : ℝ) * π + HDiv.hDiv (α := ℝ) 1 2 * π)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₂ : (↑(Real.sin ((↑k : ℝ) * π + π * (1 / 2))) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₃ : (↑(Real.sin ((↑k : ℝ) * π + π / 2)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₄ : (↑(Real.cos ((↑k : ℝ) * π)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₅ : (↑(Real.cos ((↑k : ℝ) * π - 0)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₆ : (↑(HPow.hPow (α := ℝ) (-1) k * Real.cos 0) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₇ : (↑(HPow.hPow (α := ℝ) (-1) k * 1) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₈ : (↑(HPow.hPow (α := ℝ) (-1) k) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₉ : (↑(-1) : ℂ) ^ k * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₂₀ : (-(↑1 : ℂ)) ^ k * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₂₁ : HPow.hPow (α := ℂ) (-1) k * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₂₂ : HPow.hPow (α := ℂ) (-1) k * (HPow.hPow (α := ℂ) (-1) k * -1) = -1
e_a₂₃ : HPow.hPow (α := ℂ) (-1) k * -HPow.hPow (α := ℂ) (-1) k = -1
⊢ Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
have e_a₂₄ : -(HPow.hPow (α := ℂ) (-1) k * HPow.hPow (α := ℂ) (-1) k) = -1
Tactic: rw [mul_div_assoc, add_div, mul_div_cancel_left₀ _ two_ne_zero, ← ofReal_natCast,
    ← ofReal_one, ← ofReal_ofNat, ← ofReal_div, ← ofReal_add, ← ofReal_mul,
    ← ofReal_sin, mul_comm π, add_mul, mul_comm (1 / 2), mul_one_div, Real.sin_add_pi_div_two,
    ← sub_zero (k * π), cos_nat_mul_pi_sub, Real.cos_zero, mul_one,
    ofReal_pow, ofReal_neg, ofReal_one, pow_succ, mul_neg_one, mul_neg, ← mul_pow, neg_one_mul,
    neg_neg, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1 ≠ -(↑n : ℂ)
h3 : (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).Gammaℂ ≠ 0
e_a : Complex.sin ((↑π : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₁ : Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2 + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₂ : Complex.sin ((↑π : ℂ) * ((↑k : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₃ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₄ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / 2)) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₅ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / (↑2 : ℂ))) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₆ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑(HDiv.hDiv (α := ℝ) 1 2) : ℂ))) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₇ : Complex.sin ((↑π : ℂ) * (↑((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2) : ℂ)) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₈ : Complex.sin (↑(π * ((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₉ : (↑(Real.sin (π * ((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2))) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₀ : (↑(Real.sin (((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2) * π)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₁ : (↑(Real.sin ((↑k : ℝ) * π + HDiv.hDiv (α := ℝ) 1 2 * π)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₂ : (↑(Real.sin ((↑k : ℝ) * π + π * (1 / 2))) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₃ : (↑(Real.sin ((↑k : ℝ) * π + π / 2)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₄ : (↑(Real.cos ((↑k : ℝ) * π)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₅ : (↑(Real.cos ((↑k : ℝ) * π - 0)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₆ : (↑(HPow.hPow (α := ℝ) (-1) k * Real.cos 0) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₇ : (↑(HPow.hPow (α := ℝ) (-1) k * 1) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₈ : (↑(HPow.hPow (α := ℝ) (-1) k) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₉ : (↑(-1) : ℂ) ^ k * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₂₀ : (-(↑1 : ℂ)) ^ k * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₂₁ : HPow.hPow (α := ℂ) (-1) k * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₂₂ : HPow.hPow (α := ℂ) (-1) k * (HPow.hPow (α := ℂ) (-1) k * -1) = -1
e_a₂₃ : HPow.hPow (α := ℂ) (-1) k * -HPow.hPow (α := ℂ) (-1) k = -1
e_a₂₄ : -(HPow.hPow (α := ℂ) (-1) k * HPow.hPow (α := ℂ) (-1) k) = -1
⊢ Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
have e_a₂₅ : -HMul.hMul (α := ℂ) (-1) (-1) ^ k = -1
Tactic: rw [mul_div_assoc, add_div, mul_div_cancel_left₀ _ two_ne_zero, ← ofReal_natCast,
    ← ofReal_one, ← ofReal_ofNat, ← ofReal_div, ← ofReal_add, ← ofReal_mul,
    ← ofReal_sin, mul_comm π, add_mul, mul_comm (1 / 2), mul_one_div, Real.sin_add_pi_div_two,
    ← sub_zero (k * π), cos_nat_mul_pi_sub, Real.cos_zero, mul_one,
    ofReal_pow, ofReal_neg, ofReal_one, pow_succ, mul_neg_one, mul_neg, ← mul_pow, neg_one_mul,
    neg_neg, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1 ≠ -(↑n : ℂ)
h3 : (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).Gammaℂ ≠ 0
e_a : Complex.sin ((↑π : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₁ : Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2 + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₂ : Complex.sin ((↑π : ℂ) * ((↑k : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₃ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₄ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / 2)) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₅ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / (↑2 : ℂ))) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₆ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑(HDiv.hDiv (α := ℝ) 1 2) : ℂ))) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₇ : Complex.sin ((↑π : ℂ) * (↑((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2) : ℂ)) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₈ : Complex.sin (↑(π * ((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₉ : (↑(Real.sin (π * ((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2))) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₀ : (↑(Real.sin (((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2) * π)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₁ : (↑(Real.sin ((↑k : ℝ) * π + HDiv.hDiv (α := ℝ) 1 2 * π)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₂ : (↑(Real.sin ((↑k : ℝ) * π + π * (1 / 2))) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₃ : (↑(Real.sin ((↑k : ℝ) * π + π / 2)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₄ : (↑(Real.cos ((↑k : ℝ) * π)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₅ : (↑(Real.cos ((↑k : ℝ) * π - 0)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₆ : (↑(HPow.hPow (α := ℝ) (-1) k * Real.cos 0) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₇ : (↑(HPow.hPow (α := ℝ) (-1) k * 1) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₈ : (↑(HPow.hPow (α := ℝ) (-1) k) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₁₉ : (↑(-1) : ℂ) ^ k * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₂₀ : (-(↑1 : ℂ)) ^ k * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₂₁ : HPow.hPow (α := ℂ) (-1) k * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₂₂ : HPow.hPow (α := ℂ) (-1) k * (HPow.hPow (α := ℂ) (-1) k * -1) = -1
e_a₂₃ : HPow.hPow (α := ℂ) (-1) k * -HPow.hPow (α := ℂ) (-1) k = -1
e_a₂₄ : -(HPow.hPow (α := ℂ) (-1) k * HPow.hPow (α := ℂ) (-1) k) = -1
e_a₂₅ : -HMul.hMul (α := ℂ) (-1) (-1) ^ k = -1
⊢ Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
have e_a₂₆ : -HPow.hPow (α := ℂ) (- -1) k = -1
Tactic: rw [mul_div_assoc, add_div, mul_div_cancel_left₀ _ two_ne_zero, ← ofReal_natCast,
    ← ofReal_one, ← ofReal_ofNat, ← ofReal_div, ← ofReal_add, ← ofReal_mul,
    ← ofReal_sin, mul_comm π, add_mul, mul_comm (1 / 2), mul_one_div, Real.sin_add_pi_div_two,
    ← sub_zero (k * π), cos_nat_mul_pi_sub, Real.cos_zero, mul_one,
    ofReal_pow, ofReal_neg, ofReal_one, pow_succ, mul_neg_one, mul_neg, ← mul_pow, neg_one_mul,
    neg_neg, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this : hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) = 0
⊢ hurwitzZeta (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    -1 / HMul.hMul (α := ℂ) 2 (↑k : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
have rw : hurwitzZetaEven (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) +
    hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
  -1 / HMul.hMul (α := ℂ) 2 (↑k : ℂ) *
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
Tactic: rw [hurwitzZeta, this, add_zero, hurwitzZetaEven_one_sub_two_mul_nat hk hx]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this : hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) = 0
rw :
  hurwitzZetaEven (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) +
      hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    -1 / HMul.hMul (α := ℂ) 2 (↑k : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
⊢ hurwitzZeta (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    -1 / HMul.hMul (α := ℂ) 2 (↑k : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
have rw₁ : hurwitzZetaEven (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) + 0 =
  -1 / HMul.hMul (α := ℂ) 2 (↑k : ℂ) *
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
Tactic: rw [hurwitzZeta, this, add_zero, hurwitzZetaEven_one_sub_two_mul_nat hk hx]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this : hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) = 0
rw :
  hurwitzZetaEven (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) +
      hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    -1 / HMul.hMul (α := ℂ) 2 (↑k : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
rw₁ :
  hurwitzZetaEven (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) + 0 =
    -1 / HMul.hMul (α := ℂ) 2 (↑k : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
⊢ hurwitzZeta (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    -1 / HMul.hMul (α := ℂ) 2 (↑k : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
have rw₂ : hurwitzZetaEven (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
  -1 / HMul.hMul (α := ℂ) 2 (↑k : ℂ) *
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
Tactic: rw [hurwitzZeta, this, add_zero, hurwitzZetaEven_one_sub_two_mul_nat hk hx]