awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this :
  HasSum
    (fun (n : ℕ) ↦
      1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k + 1) *
        HSub.hSub (α := ℂ) (β := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (HPow.hPow (α := ℂ) (-1) (k + 1) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
      (↑(bernoulliFun (2 * k + 1) x) : ℂ))
ofReal_two : (↑2 : ℂ) = 2
x_1 : ℕ
h : 1 / HPow.hPow (α := ℂ) (↑x_1 : ℂ) (2 * k + 1) = 1 / (↑(↑x_1 : ℝ) : ℂ) ^ (2 * k + 1)
⊢ 1 / HPow.hPow (α := ℂ) (↑x_1 : ℂ) (2 * k + 1) = (↑(1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) (2 * k + 1)) : ℂ)

Tactic:
rw [ofReal_div, ofReal_one, ofReal_pow]

Premises used: Complex.ofReal_one, Complex.ofReal_div, Complex.ofReal_pow
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this :
  HasSum
    (fun (n : ℕ) ↦
      1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k + 1) *
        HSub.hSub (α := ℂ) (β := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (HPow.hPow (α := ℂ) (-1) (k + 1) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
      (↑(bernoulliFun (2 * k + 1) x) : ℂ))
ofReal_two : (↑2 : ℂ) = 2
x_1 : ℕ
⊢ 1 / HPow.hPow (α := ℂ) (↑x_1 : ℂ) (2 * k + 1) = 1 / (↑(↑x_1 : ℝ) : ℂ) ^ (2 * k + 1)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this :
  HasSum
    (fun (n : ℕ) ↦
      1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k + 1) *
        HSub.hSub (α := ℂ) (β := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (HPow.hPow (α := ℂ) (-1) (k + 1) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
      (↑(bernoulliFun (2 * k + 1) x) : ℂ))
ofReal_two : (↑2 : ℂ) = 2
x_1 : ℕ
h :
  (cexp (2 * (↑π : ℂ) * I * -(↑x_1 : ℂ) * (↑x : ℂ)) - cexp (2 * (↑π : ℂ) * I * (↑x_1 : ℂ) * (↑x : ℂ))) * I / 2 =
    (cexp (-(2 * (↑π : ℂ) * (↑x_1 : ℂ) * (↑x : ℂ)) * I) - cexp (2 * (↑π : ℂ) * (↑x_1 : ℂ) * (↑x : ℂ) * I)) * I / 2
⊢ HSub.hSub (α := ℂ) (β := ℂ) ((fourier (↑x_1 : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
        ((fourier (-(↑x_1 : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) /
      (2 * I) =
    (↑(Real.sin (2 * π * (↑x_1 : ℝ) * x)) : ℂ)

Tactic:
rw [ofReal_sin, ofReal_mul, fourier_coe_apply, fourier_coe_apply, sin, ofReal_one, div_one,
        div_one, ofReal_mul, ofReal_mul, ofReal_two, Int.cast_neg, Int.cast_natCast,
        ofReal_natCast, ← div_div, div_I, div_mul_eq_mul_div₀, ← neg_div, ← neg_mul, neg_sub]

Premises used: Int.cast_neg, Int.cast_natCast, neg_sub, neg_div, Complex.sin, fourier_coe_apply, Complex.ofReal_one, Complex.ofReal_natCast, Complex.div_I, Complex.ofReal_sin, neg_mul, div_div, div_one, div_mul_eq_mul_div₀, Complex.ofReal_mul
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this :
  HasSum
    (fun (n : ℕ) ↦
      1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k + 1) *
        HSub.hSub (α := ℂ) (β := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (HPow.hPow (α := ℂ) (-1) (k + 1) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
      (↑(bernoulliFun (2 * k + 1) x) : ℂ))
ofReal_two : (↑2 : ℂ) = 2
x_1 : ℕ
h : 2 * (↑π : ℂ) * I * -(↑x_1 : ℂ) * (↑x : ℂ) = -(2 * (↑π : ℂ) * (↑x_1 : ℂ) * (↑x : ℂ)) * I
h₁ : 2 * (↑π : ℂ) * I * (↑x_1 : ℂ) * (↑x : ℂ) = 2 * (↑π : ℂ) * (↑x_1 : ℂ) * (↑x : ℂ) * I
⊢ (cexp (2 * (↑π : ℂ) * I * -(↑x_1 : ℂ) * (↑x : ℂ)) - cexp (2 * (↑π : ℂ) * I * (↑x_1 : ℂ) * (↑x : ℂ))) * I / 2 =
    (cexp (-(2 * (↑π : ℂ) * (↑x_1 : ℂ) * (↑x : ℂ)) * I) - cexp (2 * (↑π : ℂ) * (↑x_1 : ℂ) * (↑x : ℂ) * I)) * I / 2

Tactic:
congr 4
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this :
  HasSum
    (fun (n : ℕ) ↦
      1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k + 1) *
        HSub.hSub (α := ℂ) (β := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (HPow.hPow (α := ℂ) (-1) (k + 1) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
      (↑(bernoulliFun (2 * k + 1) x) : ℂ))
ofReal_two : (↑2 : ℂ) = 2
x_1 : ℕ
⊢ 2 * (↑π : ℂ) * I * -(↑x_1 : ℂ) * (↑x : ℂ) = -(2 * (↑π : ℂ) * (↑x_1 : ℂ) * (↑x : ℂ)) * I

Tactic:
ring
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this :
  HasSum
    (fun (n : ℕ) ↦
      1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k + 1) *
        HSub.hSub (α := ℂ) (β := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (HPow.hPow (α := ℂ) (-1) (k + 1) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
      (↑(bernoulliFun (2 * k + 1) x) : ℂ))
ofReal_two : (↑2 : ℂ) = 2
x_1 : ℕ
⊢ 2 * (↑π : ℂ) * I * (↑x_1 : ℂ) * (↑x : ℂ) = 2 * (↑π : ℂ) * (↑x_1 : ℂ) * (↑x : ℂ) * I

Tactic:
ring
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this :
  HasSum
    (fun (n : ℕ) ↦
      1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k + 1) *
        HSub.hSub (α := ℂ) (β := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (HPow.hPow (α := ℂ) (-1) (k + 1) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
      (↑(bernoulliFun (2 * k + 1) x) : ℂ))
ofReal_two : (↑2 : ℂ) = 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)))) :
        ℂ).re

Tactic:
(ofReal_re _).symm

Premises used: Complex.ofReal_re, Eq.symm
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this :
  HasSum
    (fun (n : ℕ) ↦
      1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k + 1) *
        HSub.hSub (α := ℂ) (β := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (HPow.hPow (α := ℂ) (-1) (k + 1) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
      (↑(bernoulliFun (2 * k + 1) x) : ℂ))
ofReal_two : (↑2 : ℂ) = 2
h :
  HPow.hPow (α := ℂ) (-1) (k + 1) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
        (↑(bernoulliFun (2 * k + 1) x) : ℂ) /
      (2 * I) =
    (↑(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) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
          (↑(bernoulliFun (2 * k + 1) x) : ℂ) /
        (2 * I)).re

Tactic:
convert! (ofReal_re _).symm

Premises used: Complex.ofReal_re, Eq.symm
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this :
  HasSum
    (fun (n : ℕ) ↦
      1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k + 1) *
        HSub.hSub (α := ℂ) (β := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (HPow.hPow (α := ℂ) (-1) (k + 1) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
      (↑(bernoulliFun (2 * k + 1) x) : ℂ))
ofReal_two : (↑2 : ℂ) = 2
h :
  -(HPow.hPow (α := ℂ) (-1) (k + 1) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
            (↑(bernoulliFun (2 * k + 1) x) : ℂ) *
          I /
        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) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
        (↑(bernoulliFun (2 * k + 1) x) : ℂ) /
      (2 * I) =
    (↑(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 [ofReal_mul, ofReal_div, ofReal_div, ofReal_mul, ofReal_pow, ofReal_pow, ofReal_neg,
      ofReal_natCast, ofReal_mul, ofReal_two, ofReal_one, ← div_div, div_I,
      div_mul_eq_mul_div₀]

Premises used: Complex.ofReal_neg, Complex.ofReal_one, Complex.ofReal_natCast, Complex.div_I, Complex.ofReal_div, div_div, Complex.ofReal_pow, div_mul_eq_mul_div₀, Complex.ofReal_mul
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this :
  HasSum
    (fun (n : ℕ) ↦
      1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k + 1) *
        HSub.hSub (α := ℂ) (β := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (HPow.hPow (α := ℂ) (-1) (k + 1) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
      (↑(bernoulliFun (2 * k + 1) x) : ℂ))
ofReal_two : (↑2 : ℂ) = 2
α β γ δ : ℂ
⊢ α * I * β / γ * δ * I = HPow.hPow (β := ℕ) I 2 * α * β / γ * δ

Tactic:
ring
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this :
  HasSum
    (fun (n : ℕ) ↦
      1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k + 1) *
        HSub.hSub (α := ℂ) (β := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (HPow.hPow (α := ℂ) (-1) (k + 1) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
      (↑(bernoulliFun (2 * k + 1) x) : ℂ))
ofReal_two : (↑2 : ℂ) = 2
⊢ ∀ (α β γ δ : ℂ), α * I * β / γ * δ * I = HPow.hPow (β := ℕ) I 2 * α * β / γ * δ

Tactic:
have : ∀ α β γ δ : ℂ, α * I * β / γ * δ * I = I ^ 2 * α * β / γ * δ := by intros; ring
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this_1 :
  HasSum
    (fun (n : ℕ) ↦
      1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k + 1) *
        HSub.hSub (α := ℂ) (β := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (HPow.hPow (α := ℂ) (-1) (k + 1) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
      (↑(bernoulliFun (2 * k + 1) x) : ℂ))
ofReal_two : (↑2 : ℂ) = 2
this : ∀ (α β γ δ : ℂ), α * I * β / γ * δ * I = HPow.hPow (β := ℕ) I 2 * α * β / γ * δ
h :
  -(-1 * HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
          (↑(bernoulliFun (2 * k + 1) x) : ℂ) /
        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) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
            (↑(bernoulliFun (2 * k + 1) x) : ℂ) *
          I /
        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)))) : ℂ)

Tactic:
rw [this, I_sq]

Premises used: Complex.I_sq
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this_1 :
  HasSum
    (fun (n : ℕ) ↦
      1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k + 1) *
        HSub.hSub (α := ℂ) (β := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (HPow.hPow (α := ℂ) (-1) (k + 1) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
      (↑(bernoulliFun (2 * k + 1) x) : ℂ))
ofReal_two : (↑2 : ℂ) = 2
this : ∀ (α β γ δ : ℂ), α * I * β / γ * δ * I = HPow.hPow (β := ℕ) I 2 * α * β / γ * δ
⊢ -(-1 * HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
          (↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) : ℂ) /
        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)))) : ℂ)

Tactic:
ring
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
⊢ HasSum (fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k) * Real.cos (2 * π * (↑n : ℝ) * 0))
    (HPow.hPow (α := ℝ) (-1) (k + 1) * (2 * π) ^ (2 * k) / 2 / (↑(2 * k)! : ℝ) *
      Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))

Tactic:
hasSum_one_div_nat_pow_mul_cos hk (left_mem_Icc.mpr zero_le_one)

Premises used: Iff.mpr, hasSum_one_div_nat_pow_mul_cos, zero_le_one, Set.left_mem_Icc
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
h :
  ∀ (n : ℕ),
    1 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k) = 1 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k) * Real.cos (2 * π * (↑n : ℝ) * 0)
⊢ Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k)) fun (n : ℕ) ↦
    1 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k) * Real.cos (2 * π * (↑n : ℝ) * 0)

Tactic:
ext1 n
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
n : ℕ
h : 1 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k) = 1 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k) * Real.cos 0
h₁ : 1 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k) = 1 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k) * 1
h₂ h₃ : 1 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k) = 1 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k)
⊢ 1 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k) = 1 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k) * Real.cos (2 * π * (↑n : ℝ) * 0)

Tactic:
rw [mul_zero, Real.cos_zero, mul_one]

Premises used: MulZeroClass.mul_zero, mul_one, Real.cos_zero
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
h :
  HPow.hPow (α := ℝ) (-1) (k + 1) * HPow.hPow (α := ℝ) 2 (2 * k - 1) * π ^ (2 * k) * (↑(bernoulli (2 * k)) : ℝ) /
      (↑(2 * k)! : ℝ) =
    HPow.hPow (α := ℝ) (-1) (k + 1) * (2 * π) ^ (2 * k) / 2 / (↑(2 * k)! : ℝ) * (↑(bernoulli (2 * k)) : ℝ)
⊢ HPow.hPow (α := ℝ) (-1) (k + 1) * HPow.hPow (α := ℝ) 2 (2 * k - 1) * π ^ (2 * k) * (↑(bernoulli (2 * k)) : ℝ) /
      (↑(2 * k)! : ℝ) =
    HPow.hPow (α := ℝ) (-1) (k + 1) * (2 * π) ^ (2 * k) / 2 / (↑(2 * k)! : ℝ) *
      Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))

Tactic:
rw [Polynomial.eval_zero_map, Polynomial.bernoulli_eval_zero, eq_ratCast]

Premises used: Polynomial.bernoulli_eval_zero, Polynomial.eval_zero_map, eq_ratCast
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
rw : HPow.hPow (α := ℝ) 2 (2 * k - 1) * 2 = HPow.hPow (α := ℝ) 2 (2 * k)
⊢ HPow.hPow (α := ℝ) 2 (2 * k - 1) = HPow.hPow (α := ℝ) 2 (2 * k) / 2

Tactic:
rw [eq_div_iff (two_ne_zero' ℝ)]

Premises used: Real, two_ne_zero', eq_div_iff
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
a : HPow.hPow (α := ℝ) 2 (2 * k - 1)
a₁ : 2
| HPow.hPow (α := ℝ) 2 (2 * k - 1) * 2

Tactic:
congr
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
| HPow.hPow (α := ℝ) 2 (2 * k - 1)

Tactic:
· skip
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
a : HPow.hPow (α := ℝ) (β := ℕ) 2 1
| 2

Tactic:
rw [← pow_one (2 : ℝ)]

Premises used: pow_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
a : HPow.hPow (α := ℝ) (β := ℕ) 2 1
| 2

Tactic:
· rw [← pow_one (2 : ℝ)]

Premises used: pow_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
a : HPow.hPow (α := ℝ) 2 (2 * k - 1)
a₁ a₂ : 2
| HPow.hPow (α := ℝ) 2 (2 * k - 1) * 2

Tactic:
congr
      · skip
      · rw [← pow_one (2 : ℝ)]

Premises used: pow_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
conv_lhs : HPow.hPow (α := ℝ) 2 (2 * k - 1) * HPow.hPow (α := ℝ) (β := ℕ) 2 1 = HPow.hPow (α := ℝ) 2 (2 * k)
⊢ HPow.hPow (α := ℝ) 2 (2 * k - 1) * 2 = HPow.hPow (α := ℝ) 2 (2 * k)

Tactic:
conv_lhs =>
      congr
      · skip
      · rw [← pow_one (2 : ℝ)]

Premises used: pow_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
rw : 1 ≤ 2 * k
⊢ HPow.hPow (α := ℝ) 2 (2 * k - 1) * HPow.hPow (α := ℝ) (β := ℕ) 2 1 = HPow.hPow (α := ℝ) 2 (2 * k)

Tactic:
rw [← pow_add, Nat.sub_add_cancel]

Premises used: pow_add, Nat.sub_add_cancel
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
⊢ 1 ≤ 2 * k

Tactic:
lia
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
⊢ HPow.hPow (α := ℝ) 2 (2 * k - 1) = HPow.hPow (α := ℝ) 2 (2 * k) / 2

Tactic:
have : (2 : ℝ) ^ (2 * k - 1) = (2 : ℝ) ^ (2 * k) / 2 := by
    rw [eq_div_iff (two_ne_zero' ℝ)]
    conv_lhs =>
      congr
      · skip
      · rw [← pow_one (2 : ℝ)]
    rw [← pow_add, Nat.sub_add_cancel]
    lia
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
this : HPow.hPow (α := ℝ) 2 (2 * k - 1) = HPow.hPow (α := ℝ) 2 (2 * k) / 2
h :
  HPow.hPow (α := ℝ) (-1) (k + 1) * (HPow.hPow (α := ℝ) 2 (2 * k) / 2) * π ^ (2 * k) * (↑(bernoulli (2 * k)) : ℝ) /
      (↑(2 * k)! : ℝ) =
    HPow.hPow (α := ℝ) (-1) (k + 1) * (HPow.hPow (α := ℝ) 2 (2 * k) * π ^ (2 * k)) / 2 / (↑(2 * k)! : ℝ) *
      (↑(bernoulli (2 * k)) : ℝ)
⊢ HPow.hPow (α := ℝ) (-1) (k + 1) * HPow.hPow (α := ℝ) 2 (2 * k - 1) * π ^ (2 * k) * (↑(bernoulli (2 * k)) : ℝ) /
      (↑(2 * k)! : ℝ) =
    HPow.hPow (α := ℝ) (-1) (k + 1) * (2 * π) ^ (2 * k) / 2 / (↑(2 * k)! : ℝ) * (↑(bernoulli (2 * k)) : ℝ)

Tactic:
rw [this, mul_pow]

Premises used: mul_pow
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
this : HPow.hPow (α := ℝ) 2 (2 * k - 1) = HPow.hPow (α := ℝ) 2 (2 * k) / 2
⊢ HPow.hPow (α := ℝ) (-1) (k + 1) * (HPow.hPow (α := ℝ) 2 (2 * k) / 2) * π ^ (2 * k) * (↑(bernoulli (2 * k)) : ℝ) /
      (↑(2 * k)! : ℝ) =
    HPow.hPow (α := ℝ) (-1) (k + 1) * (HPow.hPow (α := ℝ) 2 (2 * k) * π ^ (2 * k)) / 2 / (↑(2 * k)! : ℝ) *
      (↑(bernoulli (2 * k)) : ℝ)

Tactic:
ring
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
⊢ HasSum (fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑n : ℝ) (HMul.hMul (α := ℕ) 2 1))
    (HPow.hPow (α := ℝ) (-1) (HAdd.hAdd (α := ℕ) 1 1) * HPow.hPow (α := ℝ) 2 (HMul.hMul (α := ℕ) 2 1 - 1) *
          π ^ HMul.hMul (α := ℕ) 2 1 *
        (↑(bernoulli (HMul.hMul (α := ℕ) 2 1)) : ℝ) /
      (↑(HMul.hMul (α := ℕ) 2 1)! : ℝ))

Tactic:
hasSum_zeta_nat one_ne_zero

Premises used: one_ne_zero, hasSum_zeta_nat
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
h :
  HPow.hPow (β := ℕ) π 2 / 6 =
    HPow.hPow (α := ℝ) (-1) (HAdd.hAdd (α := ℕ) 1 1) * HPow.hPow (α := ℝ) 2 (HMul.hMul (α := ℕ) 2 1 - 1) *
          π ^ HMul.hMul (α := ℕ) 2 1 *
        (↑(bernoulli (HMul.hMul (α := ℕ) 2 1)) : ℝ) /
      (↑(HMul.hMul (α := ℕ) 2 1)! : ℝ)
⊢ HasSum (fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2) (HPow.hPow (β := ℕ) π 2 / 6)

Tactic:
convert! hasSum_zeta_nat one_ne_zero using 1

Premises used: one_ne_zero, hasSum_zeta_nat
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
⊢ Ne (α := ℕ) 2 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
h :
  HPow.hPow (β := ℕ) π 2 / 6 =
    HPow.hPow (α := ℝ) (-1) (HAdd.hAdd (α := ℕ) 1 1) * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℕ) 2 1) *
          HPow.hPow (β := ℕ) π 2 *
        (↑(1 / 6) : ℝ) /
      (↑2! : ℝ)
⊢ HPow.hPow (β := ℕ) π 2 / 6 =
    HPow.hPow (α := ℝ) (-1) (HAdd.hAdd (α := ℕ) 1 1) * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℕ) 2 1) *
          HPow.hPow (β := ℕ) π 2 *
        (↑(bernoulli 2) : ℝ) /
      (↑2! : ℝ)

Tactic:
rw [bernoulli_eq_bernoulli'_of_ne_one (by decide : 2 ≠ 1), bernoulli'_two]

Premises used: bernoulli'_two, bernoulli_eq_bernoulli'_of_ne_one
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
h : HPow.hPow (β := ℕ) π 2 / 6 = 2 * HPow.hPow (β := ℕ) π 2 * 6⁻¹ / 2
⊢ HPow.hPow (β := ℕ) π 2 / 6 =
    HPow.hPow (α := ℝ) (-1) (HAdd.hAdd (α := ℕ) 1 1) * HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℕ) 2 1) *
          HPow.hPow (β := ℕ) π 2 *
        (↑(1 / 6) : ℝ) /
      (↑2! : ℝ)

Tactic:
simp [Nat.factorial]

Premises used: Nat.factorial
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
⊢ HPow.hPow (β := ℕ) π 2 / 6 = 2 * HPow.hPow (β := ℕ) π 2 * 6⁻¹ / 2

Tactic:
ring
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
⊢ HasSum (fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑n : ℝ) (HMul.hMul (α := ℕ) 2 2))
    (HPow.hPow (α := ℝ) (-1) (HAdd.hAdd (α := ℕ) 2 1) * HPow.hPow (α := ℝ) 2 (HMul.hMul (α := ℕ) 2 2 - 1) *
          π ^ HMul.hMul (α := ℕ) 2 2 *
        (↑(bernoulli (HMul.hMul (α := ℕ) 2 2)) : ℝ) /
      (↑(HMul.hMul (α := ℕ) 2 2)! : ℝ))

Tactic:
hasSum_zeta_nat two_ne_zero

Premises used: two_ne_zero, hasSum_zeta_nat
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
h :
  HPow.hPow (β := ℕ) π 4 / 90 =
    HPow.hPow (α := ℝ) (-1) (HAdd.hAdd (α := ℕ) 2 1) * HPow.hPow (α := ℝ) 2 (HMul.hMul (α := ℕ) 2 2 - 1) *
          π ^ HMul.hMul (α := ℕ) 2 2 *
        (↑(bernoulli (HMul.hMul (α := ℕ) 2 2)) : ℝ) /
      (↑(HMul.hMul (α := ℕ) 2 2)! : ℝ)
⊢ HasSum (fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 4) (HPow.hPow (β := ℕ) π 4 / 90)

Tactic:
convert! hasSum_zeta_nat two_ne_zero using 1

Premises used: two_ne_zero, hasSum_zeta_nat
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
h :
  HPow.hPow (β := ℕ) π 4 / 90 =
    HPow.hPow (α := ℝ) (β := ℕ) (-1) 3 * HPow.hPow (α := ℝ) (β := ℕ) 2 3 * HPow.hPow (β := ℕ) π 4 * (↑(-1 / 30) : ℝ) /
      (↑4! : ℝ)
h₁ : Ne (α := ℕ) 4 1
⊢ HPow.hPow (β := ℕ) π 4 / 90 =
    HPow.hPow (α := ℝ) (β := ℕ) (-1) 3 * HPow.hPow (α := ℝ) (β := ℕ) 2 3 * HPow.hPow (β := ℕ) π 4 *
        (↑(bernoulli 4) : ℝ) /
      (↑4! : ℝ)

Tactic:
rw [bernoulli_eq_bernoulli'_of_ne_one, bernoulli'_four]

Premises used: bernoulli'_four, bernoulli_eq_bernoulli'_of_ne_one
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
h :
  HPow.hPow (β := ℕ) π 4 / 90 =
    HPow.hPow (α := ℝ) (β := ℕ) (-1) 3 * HPow.hPow (α := ℝ) (β := ℕ) 2 3 * HPow.hPow (β := ℕ) π 4 *
        HDiv.hDiv (α := ℝ) (-1) 30 /
      24
⊢ HPow.hPow (β := ℕ) π 4 / 90 =
    HPow.hPow (α := ℝ) (β := ℕ) (-1) 3 * HPow.hPow (α := ℝ) (β := ℕ) 2 3 * HPow.hPow (β := ℕ) π 4 * (↑(-1 / 30) : ℝ) /
      (↑4! : ℝ)

Tactic:
simp [Nat.factorial]

Premises used: Nat.factorial
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
⊢ HPow.hPow (β := ℕ) π 4 / 90 =
    HPow.hPow (α := ℝ) (β := ℕ) (-1) 3 * HPow.hPow (α := ℝ) (β := ℕ) 2 3 * HPow.hPow (β := ℕ) π 4 *
        HDiv.hDiv (α := ℝ) (-1) 30 /
      24

Tactic:
ring
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
⊢ Ne (α := ℕ) 4 1

Tactic:
decide