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
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)))
⊢ 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₁ : 1 < (HMul.hMul (α := ℂ) 2 (↑k : ℂ)).re
Tactic: rw [← (hasSum_nat_cosZeta x (?_ : 1 < re (2 * k))).tsum_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ ∑' (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)))
have refine_1 : ∑' (b : ℕ), (↑(Real.cos (2 * π * x * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) (HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
  (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 * k) * Real.cos (2 * π * (↑b : ℝ) * x)) : ℂ)
Tactic: refine Eq.trans ?_ <|
      (congr_arg ofReal (hasSum_one_div_nat_pow_mul_cos hk hx).tsum_eq).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
refine_1 :
  ∑' (b : ℕ), (↑(Real.cos (2 * π * x * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) (HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 * k) * Real.cos (2 * π * (↑b : ℝ) * x)) : ℂ)
⊢ ∑' (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)))
have refine_2 : (↑(HPow.hPow (α := ℝ) (-1) (k + 1) * (2 * π) ^ (2 * k) / 2 / (↑(2 * k)! : ℝ) *
        Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))) :
    ℂ) =
  HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / 2 / (↑(2 * k)! : ℂ) *
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
Tactic: refine Eq.trans ?_ <|
      (congr_arg ofReal (hasSum_one_div_nat_pow_mul_cos hk hx).tsum_eq).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ ∑' (b : ℕ), (↑(Real.cos (2 * π * x * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) (HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 * k) * Real.cos (2 * π * (↑b : ℝ) * x)) : ℂ)
have refine_1 : Eq (α := ℂ)
  (∑' (b : ℕ), (↑(Real.cos (2 * π * x * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) (HMul.hMul (α := ℂ) 2 (↑k : ℂ)))
  (∑' (a : ℕ), (↑(1 / HPow.hPow (α := ℝ) (↑a : ℝ) (2 * k) * Real.cos (2 * π * (↑a : ℝ) * x)) : ℂ))
Tactic: rw [ofReal_tsum]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ Eq (α := ℂ)
    (∑' (b : ℕ), (↑(Real.cos (2 * π * x * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) (HMul.hMul (α := ℂ) 2 (↑k : ℂ)))
    (∑' (a : ℕ), (↑(1 / HPow.hPow (α := ℝ) (↑a : ℝ) (2 * k) * Real.cos (2 * π * (↑a : ℝ) * x)) : ℂ))
have refine_1 : ∀ (n : ℕ),
  (↑(Real.cos (2 * π * x * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    (↑(1 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k) * Real.cos (2 * π * (↑n : ℝ) * x)) : ℂ)
Tactic: refine tsum_congr fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
⊢ (↑(Real.cos (2 * π * x * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    (↑(1 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k) * Real.cos (2 * π * (↑n : ℝ) * x)) : ℂ)
have refine_1 : Real.cos (2 * π * x * (↑n : ℝ)) / (↑(n ^ (2 * k)) : ℝ) =
  HDiv.hDiv (α := ℝ) 1 (↑(n ^ (2 * k)) : ℝ) * Real.cos (2 * π * (↑n : ℝ) * x)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ (↑(HPow.hPow (α := ℝ) (-1) (k + 1) * (2 * π) ^ (2 * k) / 2 / (↑(2 * k)! : ℝ) *
          Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))) :
      ℂ) =
    HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / 2 / (↑(2 * k)! : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
have refine_2 : HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / 2 / (↑(2 * k)! : ℂ) *
    (↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))) : ℂ) =
  HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / 2 / (↑(2 * k)! : ℂ) *
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / 2 / (↑(2 * k)! : ℂ) *
      (↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))) : ℂ) =
    HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / 2 / (↑(2 * k)! : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
have refine_2 : (↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))) : ℂ) =
  Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (hypothesis)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ (↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))) : ℂ) =
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
have this : Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)) =
  Polynomial.map ofRealHom (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))
Tactic: have : (Polynomial.bernoulli (2 * k)).map (algebraMap ℚ ℂ) = _ :=
        (Polynomial.map_map (algebraMap ℚ ℝ) ofRealHom _).symm
-- 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 :
  Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)) =
    Polynomial.map ofRealHom (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))
⊢ (↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))) : ℂ) =
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
have refine_2 : Eq (α := ℂ)
  ((ofRealHom : (a : ℝ) → ℂ) (Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))) : ℂ)
  (Polynomial.eval ((ofRealHom : (a : ℝ) → ℂ) x)
      (Polynomial.map ofRealHom (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))) :
    ℂ)
Tactic: rw [this, ← ofRealHom_eq_coe, ← ofRealHom_eq_coe]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ 1 < (HMul.hMul (α := ℂ) 2 (↑k : ℂ)).re
have norm_cast : 1 < 2 * k
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ sinZeta (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) =
    HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k + 1) / 2 / (↑(2 * k + 1)! : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
have rw : ∑' (b : ℕ), (↑(Real.sin (2 * π * x * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) =
  HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k + 1) / 2 / (↑(2 * k + 1)! : ℂ) *
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
Tactic: rw [← (hasSum_nat_sinZeta x (?_ : 1 < re (2 * k + 1))).tsum_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
rw :
  ∑' (b : ℕ),
      (↑(Real.sin (2 * π * x * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) =
    HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k + 1) / 2 / (↑(2 * k + 1)! : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
⊢ sinZeta (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) =
    HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k + 1) / 2 / (↑(2 * k + 1)! : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
have rw₁ : 1 < (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).re
Tactic: rw [← (hasSum_nat_sinZeta x (?_ : 1 < re (2 * k + 1))).tsum_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ ∑' (b : ℕ),
      (↑(Real.sin (2 * π * x * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) =
    HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k + 1) / 2 / (↑(2 * k + 1)! : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
have refine_1 : ∑' (b : ℕ), (↑(Real.sin (2 * π * x * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) =
  (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 * k + 1) * Real.sin (2 * π * (↑b : ℝ) * x)) : ℂ)
Tactic: refine Eq.trans ?_ <|
      (congr_arg ofReal (hasSum_one_div_nat_pow_mul_sin hk hx).tsum_eq).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
refine_1 :
  ∑' (b : ℕ),
      (↑(Real.sin (2 * π * x * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) =
    (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 * k + 1) * Real.sin (2 * π * (↑b : ℝ) * x)) : ℂ)
⊢ ∑' (b : ℕ),
      (↑(Real.sin (2 * π * x * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) =
    HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k + 1) / 2 / (↑(2 * k + 1)! : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
have refine_2 : (↑(HPow.hPow (α := ℝ) (-1) (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / (↑(2 * k + 1)! : ℝ) *
        Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) :
    ℂ) =
  HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k + 1) / 2 / (↑(2 * k + 1)! : ℂ) *
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
Tactic: refine Eq.trans ?_ <|
      (congr_arg ofReal (hasSum_one_div_nat_pow_mul_sin hk hx).tsum_eq).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ ∑' (b : ℕ),
      (↑(Real.sin (2 * π * x * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) =
    (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 * k + 1) * Real.sin (2 * π * (↑b : ℝ) * x)) : ℂ)
have refine_1 : Eq (α := ℂ)
  (∑' (b : ℕ),
    (↑(Real.sin (2 * π * x * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1))
  (∑' (a : ℕ), (↑(1 / HPow.hPow (α := ℝ) (↑a : ℝ) (2 * k + 1) * Real.sin (2 * π * (↑a : ℝ) * x)) : ℂ))
Tactic: rw [ofReal_tsum]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ Eq (α := ℂ)
    (∑' (b : ℕ),
      (↑(Real.sin (2 * π * x * (↑b : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑b : ℂ) (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1))
    (∑' (a : ℕ), (↑(1 / HPow.hPow (α := ℝ) (↑a : ℝ) (2 * k + 1) * Real.sin (2 * π * (↑a : ℝ) * x)) : ℂ))
have refine_1 : ∀ (n : ℕ),
  (↑(Real.sin (2 * π * x * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) =
    (↑(1 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k + 1) * Real.sin (2 * π * (↑n : ℝ) * x)) : ℂ)
Tactic: refine tsum_congr fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
⊢ (↑(Real.sin (2 * π * x * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) =
    (↑(1 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k + 1) * Real.sin (2 * π * (↑n : ℝ) * x)) : ℂ)
have refine_1 : Real.sin (2 * π * x * (↑n : ℝ)) / (↑(n ^ (2 * k + 1)) : ℝ) =
  HDiv.hDiv (α := ℝ) 1 (↑(n ^ (2 * k + 1)) : ℝ) * Real.sin (2 * π * (↑n : ℝ) * x)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ (↑(HPow.hPow (α := ℝ) (-1) (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / (↑(2 * k + 1)! : ℝ) *
          Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) :
      ℂ) =
    HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k + 1) / 2 / (↑(2 * k + 1)! : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
have refine_2 : HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k + 1) / 2 / (↑(2 * k + 1)! : ℂ) *
    (↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) : ℂ) =
  HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k + 1) / 2 / (↑(2 * k + 1)! : ℂ) *
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k + 1) / 2 / (↑(2 * k + 1)! : ℂ) *
      (↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) : ℂ) =
    HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k + 1) / 2 / (↑(2 * k + 1)! : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
have refine_2 : (↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) : ℂ) =
  Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (hypothesis)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ (↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) : ℂ) =
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
have this : Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)) =
  Polynomial.map ofRealHom (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))
Tactic: have : (Polynomial.bernoulli (2 * k + 1)).map (algebraMap ℚ ℂ) = _ :=
        (Polynomial.map_map (algebraMap ℚ ℝ) ofRealHom _).symm
-- 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 :
  Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)) =
    Polynomial.map ofRealHom (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))
⊢ (↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) : ℂ) =
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
have refine_2 : Eq (α := ℂ)
  ((ofRealHom : (a : ℝ) → ℂ) (Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) :
    ℂ)
  (Polynomial.eval ((ofRealHom : (a : ℝ) → ℂ) x)
      (Polynomial.map ofRealHom (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) :
    ℂ)
Tactic: rw [this, ← ofRealHom_eq_coe, ← ofRealHom_eq_coe]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ 1 < (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).re
have norm_cast : 1 < 2 * k + 1
Tactic: norm_cast
-- 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) / HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (HMul.hMul (α := ℂ) 2 (↑k : ℂ)).Gammaℂ *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
have rw : HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / 2 / (↑(2 * k)! : ℂ) *
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k))) =
  HPow.hPow (α := ℂ) (-1) (k + 1) / HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (HMul.hMul (α := ℂ) 2 (↑k : ℂ)).Gammaℂ *
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
Tactic: rw [cosZeta_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
⊢ HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / 2 / (↑(2 * k)! : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k))) =
    HPow.hPow (α := ℂ) (-1) (k + 1) / HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (HMul.hMul (α := ℂ) 2 (↑k : ℂ)).Gammaℂ *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
have e_a : HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / 2 / (↑(2 * k)! : ℂ) =
  HPow.hPow (α := ℂ) (-1) (k + 1) / HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (HMul.hMul (α := ℂ) 2 (↑k : ℂ)).Gammaℂ
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ HMul.hMul (α := ℂ) 2 (↑k : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1
have norm_cast : 2 * k = 2 * k - 1 + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ HMul.hMul (α := ℂ) 2 (↑k : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1
have lia : 2 * k = 2 * k - 1 + 1
Tactic: { norm_cast; lia }
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ (↑(2 * k)! : ℂ) = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ))
have rw : HMul.hMul (α := ℂ) 2 (↑k : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1
Tactic: rw [(by { norm_cast; lia } : 2 * (k : ℂ) = ↑(2 * k - 1) + 1), Complex.Gamma_nat_eq_factorial,
      ← Nat.cast_add_one, ← Nat.cast_mul, ← Nat.factorial_succ, Nat.sub_add_cancel (by lia)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
rw : HMul.hMul (α := ℂ) 2 (↑k : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1
⊢ (↑(2 * k)! : ℂ) = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ))
have rw₁ : (↑(2 * k)! : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1 * Complex.Gamma (HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1)
Tactic: rw [(by { norm_cast; lia } : 2 * (k : ℂ) = ↑(2 * k - 1) + 1), Complex.Gamma_nat_eq_factorial,
      ← Nat.cast_add_one, ← Nat.cast_mul, ← Nat.factorial_succ, Nat.sub_add_cancel (by lia)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
rw : HMul.hMul (α := ℂ) 2 (↑k : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1
rw₁ :
  (↑(2 * k)! : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1 * Complex.Gamma (HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1)
⊢ (↑(2 * k)! : ℂ) = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ))
have rw₂ : (↑(2 * k)! : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1 * (↑(2 * k - 1)! : ℂ)
Tactic: rw [(by { norm_cast; lia } : 2 * (k : ℂ) = ↑(2 * k - 1) + 1), Complex.Gamma_nat_eq_factorial,
      ← Nat.cast_add_one, ← Nat.cast_mul, ← Nat.factorial_succ, Nat.sub_add_cancel (by lia)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
rw : HMul.hMul (α := ℂ) 2 (↑k : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1
rw₁ :
  (↑(2 * k)! : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1 * Complex.Gamma (HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1)
rw₂ : (↑(2 * k)! : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1 * (↑(2 * k - 1)! : ℂ)
⊢ (↑(2 * k)! : ℂ) = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ))
have rw₃ : (↑(2 * k)! : ℂ) = HMul.hMul (α := ℂ) (↑(2 * k - 1 + 1) : ℂ) (↑(2 * k - 1)! : ℂ)
Tactic: rw [(by { norm_cast; lia } : 2 * (k : ℂ) = ↑(2 * k - 1) + 1), Complex.Gamma_nat_eq_factorial,
      ← Nat.cast_add_one, ← Nat.cast_mul, ← Nat.factorial_succ, Nat.sub_add_cancel (by lia)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
rw : HMul.hMul (α := ℂ) 2 (↑k : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1
rw₁ :
  (↑(2 * k)! : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1 * Complex.Gamma (HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1)
rw₂ : (↑(2 * k)! : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1 * (↑(2 * k - 1)! : ℂ)
rw₃ : (↑(2 * k)! : ℂ) = HMul.hMul (α := ℂ) (↑(2 * k - 1 + 1) : ℂ) (↑(2 * k - 1)! : ℂ)
⊢ (↑(2 * k)! : ℂ) = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ))
have rw₄ : Eq (α := ℂ) (↑(2 * k)! : ℂ) (↑((2 * k - 1 + 1) * (2 * k - 1)!) : ℂ)
Tactic: rw [(by { norm_cast; lia } : 2 * (k : ℂ) = ↑(2 * k - 1) + 1), Complex.Gamma_nat_eq_factorial,
      ← Nat.cast_add_one, ← Nat.cast_mul, ← Nat.factorial_succ, Nat.sub_add_cancel (by lia)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
rw : HMul.hMul (α := ℂ) 2 (↑k : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1
rw₁ :
  (↑(2 * k)! : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1 * Complex.Gamma (HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1)
rw₂ : (↑(2 * k)! : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1 * (↑(2 * k - 1)! : ℂ)
rw₃ : (↑(2 * k)! : ℂ) = HMul.hMul (α := ℂ) (↑(2 * k - 1 + 1) : ℂ) (↑(2 * k - 1)! : ℂ)
rw₄ : Eq (α := ℂ) (↑(2 * k)! : ℂ) (↑((2 * k - 1 + 1) * (2 * k - 1)!) : ℂ)
⊢ (↑(2 * k)! : ℂ) = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ))
have rw₅ : Eq (α := ℂ) (↑(2 * k)! : ℂ) (↑(2 * k - 1 + 1)! : ℂ)
Tactic: rw [(by { norm_cast; lia } : 2 * (k : ℂ) = ↑(2 * k - 1) + 1), Complex.Gamma_nat_eq_factorial,
      ← Nat.cast_add_one, ← Nat.cast_mul, ← Nat.factorial_succ, Nat.sub_add_cancel (by lia)]