awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
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ℝ
rw₁₀ 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ℝ
⊢ hurwitzZetaOdd a (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * Complex.sin ((↑π : ℂ) * s / 2) * sinZeta a s

Tactic:
rw [← Gammaℂ, hurwitzZetaOdd, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv,
    inv_Gammaℝ_two_sub hs, completedHurwitzZetaOdd_one_sub, sinZeta, ← div_eq_mul_inv,
    ← mul_div_assoc, ← mul_div_assoc, mul_comm]

Premises used: Complex.Gammaℂ, mul_div_assoc, HurwitzZeta.hurwitzZetaOdd, div_eq_mul_inv, HurwitzZeta.sinZeta, mul_comm, HurwitzZeta.completedHurwitzZetaOdd_one_sub, Complex.inv_Gammaℝ_two_sub
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
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ℝ
rw₁₀ 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ℝ
⊢ sinZeta a (1 - s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Complex.Gamma s * 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]

Premises used: Complex.Gammaℂ, mul_div_assoc, HurwitzZeta.hurwitzZetaOdd, HurwitzZeta.completedSinZeta_one_sub, div_eq_mul_inv, HurwitzZeta.sinZeta, mul_comm, Complex.inv_Gammaℝ_two_sub
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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)))
rw₁ : 1 < (HMul.hMul (α := ℂ) 2 (↑k : ℂ)).re
⊢ 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)))

Tactic:
rw [← (hasSum_nat_cosZeta x (?_ : 1 < re (2 * k))).tsum_eq]

Premises used: HurwitzZeta.hasSum_nat_cosZeta, HasSum.tsum_eq
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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)))

Tactic:
Eq.trans ?_ <|
      (congr_arg ofReal (hasSum_one_div_nat_pow_mul_cos hk hx).tsum_eq).trans ?_

Premises used: hasSum_one_div_nat_pow_mul_cos, Complex.ofReal, congr_arg, HasSum.tsum_eq, Eq.trans
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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)) : ℂ)
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)))
⊢ ∑' (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:
refine Eq.trans ?_ <|
      (congr_arg ofReal (hasSum_one_div_nat_pow_mul_cos hk hx).tsum_eq).trans ?_

Premises used: hasSum_one_div_nat_pow_mul_cos, Complex.ofReal, congr_arg, HasSum.tsum_eq, Eq.trans
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
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)) : ℂ))
⊢ ∑' (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:
rw [ofReal_tsum]

Premises used: Complex.ofReal_tsum
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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)) : ℂ))

Tactic:
tsum_congr fun n ↦ ?_

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
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)) : ℂ)
⊢ 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:
refine tsum_congr fun n ↦ ?_

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
refine_1 :
  Real.cos (2 * π * x * (↑n : ℝ)) / (↑(n ^ (2 * k)) : ℝ) =
    HDiv.hDiv (α := ℝ) 1 (↑(n ^ (2 * k)) : ℝ) * Real.cos (2 * π * (↑n : ℝ) * x)
⊢ (↑(Real.cos (2 * π * x * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    (↑(1 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k) * Real.cos (2 * π * (↑n : ℝ) * x)) : ℂ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
⊢ Real.cos (2 * π * x * (↑n : ℝ)) / (↑(n ^ (2 * k)) : ℝ) =
    HDiv.hDiv (α := ℝ) 1 (↑(n ^ (2 * k)) : ℝ) * Real.cos (2 * π * (↑n : ℝ) * x)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
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)))
⊢ (↑(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
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
refine_2 :
  (↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (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)))) : ℂ) =
    HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / 2 / (↑(2 * k)! : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ 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
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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)))
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)))) :
      ℂ)
⊢ (↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))) : ℂ) =
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Tactic:
rw [this, ← ofRealHom_eq_coe, ← ofRealHom_eq_coe]

Premises used: Complex.ofRealHom_eq_coe
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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)))
⊢ RingHom.comp (algebraMap ℂ ℂ) ofRealHom = ofRealHom.comp (algebraMap ℝ ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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)))
⊢ 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:
apply Polynomial.map_aeval_eq_aeval_map (by simp)

Premises used: Polynomial.map_aeval_eq_aeval_map
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
norm_cast : 1 < 2 * k
⊢ 1 < (HMul.hMul (α := ℂ) 2 (↑k : ℂ)).re

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ 1 < 2 * k

Tactic:
lia
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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)))
rw₁ : 1 < (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).re
⊢ 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)))

Tactic:
rw [← (hasSum_nat_sinZeta x (?_ : 1 < re (2 * k + 1))).tsum_eq]

Premises used: HurwitzZeta.hasSum_nat_sinZeta, HasSum.tsum_eq
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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)))

Tactic:
Eq.trans ?_ <|
      (congr_arg ofReal (hasSum_one_div_nat_pow_mul_sin hk hx).tsum_eq).trans ?_

Premises used: Complex.ofReal, congr_arg, HasSum.tsum_eq, hasSum_one_div_nat_pow_mul_sin, Eq.trans
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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)) : ℂ)
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)))
⊢ ∑' (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:
refine Eq.trans ?_ <|
      (congr_arg ofReal (hasSum_one_div_nat_pow_mul_sin hk hx).tsum_eq).trans ?_

Premises used: Complex.ofReal, congr_arg, HasSum.tsum_eq, hasSum_one_div_nat_pow_mul_sin, Eq.trans
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
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)) : ℂ))
⊢ ∑' (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:
rw [ofReal_tsum]

Premises used: Complex.ofReal_tsum
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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)) : ℂ))

Tactic:
tsum_congr fun n ↦ ?_

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
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)) : ℂ)
⊢ 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:
refine tsum_congr fun n ↦ ?_

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
refine_1 :
  Real.sin (2 * π * x * (↑n : ℝ)) / (↑(n ^ (2 * k + 1)) : ℝ) =
    HDiv.hDiv (α := ℝ) 1 (↑(n ^ (2 * k + 1)) : ℝ) * Real.sin (2 * π * (↑n : ℝ) * x)
⊢ (↑(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:
norm_cast
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
⊢ Real.sin (2 * π * x * (↑n : ℝ)) / (↑(n ^ (2 * k + 1)) : ℝ) =
    HDiv.hDiv (α := ℝ) 1 (↑(n ^ (2 * k + 1)) : ℝ) * Real.sin (2 * π * (↑n : ℝ) * x)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
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)))
⊢ (↑(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
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
refine_2 :
  (↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (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)))) : ℂ) =
    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:
congr 1
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ 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
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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)))
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)))) :
      ℂ)
⊢ (↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) : ℂ) =
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Tactic:
rw [this, ← ofRealHom_eq_coe, ← ofRealHom_eq_coe]

Premises used: Complex.ofRealHom_eq_coe
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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)))
⊢ RingHom.comp (algebraMap ℂ ℂ) ofRealHom = ofRealHom.comp (algebraMap ℝ ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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)))
⊢ 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:
apply Polynomial.map_aeval_eq_aeval_map (by simp)

Premises used: Polynomial.map_aeval_eq_aeval_map
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
norm_cast : 1 < 2 * k + 1
⊢ 1 < (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).re

Tactic:
norm_cast