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) *
        HAdd.hAdd (α := ℂ) (β := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / (↑(2 * k)! : ℂ) * (↑(bernoulliFun (2 * k) x) : ℂ))
ofReal_two : (↑2 : ℂ) = 2
n : ℕ
⊢ 2 * (↑π : ℂ) * I * -(↑n : ℂ) * (↑x : ℂ) = -(2 * (↑π : ℂ) * (↑n : ℂ) * (↑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) *
        HAdd.hAdd (α := ℂ) (β := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / (↑(2 * k)! : ℂ) * (↑(bernoulliFun (2 * k) x) : ℂ))
ofReal_two : (↑2 : ℂ) = 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)))) :
        ℂ).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) *
        HAdd.hAdd (α := ℂ) (β := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / (↑(2 * k)! : ℂ) * (↑(bernoulliFun (2 * k) x) : ℂ))
ofReal_two : (↑2 : ℂ) = 2
h :
  HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / (↑(2 * k)! : ℂ) * (↑(bernoulliFun (2 * k) x) : ℂ) / 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 * k)! : ℂ) * (↑(bernoulliFun (2 * k) x) : ℂ) /
        2).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) *
        HAdd.hAdd (α := ℂ) (β := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / (↑(2 * k)! : ℂ) * (↑(bernoulliFun (2 * k) x) : ℂ))
ofReal_two : (↑2 : ℂ) = 2
h :
  HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / (↑(2 * k)! : ℂ) * (↑(bernoulliFun (2 * k) x) : ℂ) / 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 * k)! : ℂ) * (↑(bernoulliFun (2 * k) x) : ℂ) / 2 =
    (↑(HPow.hPow (α := ℝ) (-1) (k + 1) * (2 * π) ^ (2 * k) / 2 / (↑(2 * k)! : ℝ) *
          Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))) :
      ℂ)

Tactic:
rw [ofReal_mul, ofReal_div, ofReal_div, ofReal_mul, ofReal_pow, ofReal_pow, ofReal_neg,
      ofReal_natCast, ofReal_mul, ofReal_two, ofReal_one]

Premises used: Complex.ofReal_neg, Complex.ofReal_one, Complex.ofReal_natCast, Complex.ofReal_div, Complex.ofReal_pow, 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) *
        HAdd.hAdd (α := ℂ) (β := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / (↑(2 * k)! : ℂ) * (↑(bernoulliFun (2 * k) x) : ℂ))
ofReal_two : (↑2 : ℂ) = 2
⊢ HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / (↑(2 * k)! : ℂ) *
        (↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))) : ℂ) /
      2 =
    HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / 2 / (↑(2 * k)! : ℂ) *
      (↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))) : ℂ)

Tactic:
ring
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ 2 ≤ 2 * k + 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h :
  Eq (α := ℕ → ℂ)
    (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) : ℂ))
    fun (n : ℕ) ↦
    1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k + 1) *
      HAdd.hAdd (α := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
        (HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (-1) (2 * k + 1))
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
h₁ :
  HPow.hPow (α := ℂ) (-1) (k + 1) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
      (↑(bernoulliFun (2 * k + 1) x) : ℂ) =
    -(2 * (↑π : ℂ) * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) * (↑(bernoulliFun (2 * k + 1) x) : ℂ)
⊢ 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) : ℂ))

Tactic:
convert! hasSum_one_div_nat_pow_mul_fourier (by lia : 2 ≤ 2 * k + 1) hx using 1

Premises used: hasSum_one_div_nat_pow_mul_fourier
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h :
  ∀ (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) : ℂ) =
      1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k + 1) *
        HAdd.hAdd (α := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          (HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (-1) (2 * k + 1))
            ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
⊢ Eq (α := ℕ → ℂ)
    (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) : ℂ))
    fun (n : ℕ) ↦
    1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k + 1) *
      HAdd.hAdd (α := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
        (HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (-1) (2 * k + 1))
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))

Tactic:
ext1 n
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h : HPow.hPow (α := ℂ) (-1) (k + 1) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) = -(2 * (↑π : ℂ) * I) ^ (2 * k + 1)
⊢ HPow.hPow (α := ℂ) (-1) (k + 1) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
      (↑(bernoulliFun (2 * k + 1) x) : ℂ) =
    -(2 * (↑π : ℂ) * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) * (↑(bernoulliFun (2 * k + 1) x) : ℂ)

Tactic:
congr
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
rw : -((2 * (↑π : ℂ)) ^ (2 * k + 1) * I ^ (2 * k + 1))
| -(2 * (↑π : ℂ) * I) ^ (2 * k + 1)

Tactic:
rw [mul_pow]

Premises used: mul_pow
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
a : (2 * (↑π : ℂ)) ^ (2 * k + 1) * I ^ (2 * k + 1)
| -((2 * (↑π : ℂ)) ^ (2 * k + 1) * I ^ (2 * k + 1))

Tactic:
congr
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
a : (2 * (↑π : ℂ)) ^ (2 * k + 1)
a₁ : I ^ (2 * k + 1)
| (2 * (↑π : ℂ)) ^ (2 * k + 1) * I ^ (2 * k + 1)

Tactic:
congr
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
| (2 * (↑π : ℂ)) ^ (2 * k + 1)

Tactic:
· skip
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
a : HPow.hPow (α := ℂ) (-1) k * I
| I ^ (2 * k + 1)

Tactic:
rw [pow_add, pow_one, pow_mul, I_sq]

Premises used: pow_add, pow_mul, pow_one, Complex.I_sq
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
a : I ^ (2 * k) * HPow.hPow (β := ℕ) I 1
a₁ : I ^ (2 * k) * I
a₂ : HPow.hPow (β := ℕ) I 2 ^ k * I
a₃ : HPow.hPow (α := ℂ) (-1) k * I
| I ^ (2 * k + 1)

Tactic:
· rw [pow_add, pow_one, pow_mul, I_sq]

Premises used: pow_add, pow_mul, pow_one, Complex.I_sq
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
rw : -((2 * (↑π : ℂ)) ^ (2 * k + 1) * I ^ (2 * k + 1))
a : (2 * (↑π : ℂ)) ^ (2 * k + 1) * I ^ (2 * k + 1)
a₁ : (2 * (↑π : ℂ)) ^ (2 * k + 1)
a₂ a₃ : I ^ (2 * k + 1)
| -(2 * (↑π : ℂ) * I) ^ (2 * k + 1)

Tactic:
rw [mul_pow]
        congr
        congr
        · skip
        · rw [pow_add, pow_one, pow_mul, I_sq]

Premises used: pow_add, pow_mul, pow_one, Complex.I_sq, mul_pow
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h :
  HPow.hPow (α := ℂ) (-1) k * -1 * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) =
    -((2 * (↑π : ℂ)) ^ (2 * k + 1) * (HPow.hPow (α := ℂ) (-1) k * I))
⊢ HPow.hPow (α := ℂ) (-1) k * -1 * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) = -(2 * (↑π : ℂ) * I) ^ (2 * k + 1)

Tactic:
conv_rhs =>
        rw [mul_pow]
        congr
        congr
        · skip
        · rw [pow_add, pow_one, pow_mul, I_sq]

Premises used: pow_add, pow_mul, pow_one, Complex.I_sq, mul_pow
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ HPow.hPow (α := ℂ) (-1) k * -1 * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) =
    -((2 * (↑π : ℂ)) ^ (2 * k + 1) * (HPow.hPow (α := ℂ) (-1) k * I))

Tactic:
ring
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ 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) : ℂ))

Tactic:
have :
    HasSum (fun n : ℕ => 1 / (n : ℂ) ^ (2 * k + 1) * (fourier n (x : 𝕌) - fourier (-n) (x : 𝕌)))
      ((-1 : ℂ) ^ (k + 1) * I * (2 * π : ℂ) ^ (2 * k + 1) / (2 * k + 1)! *
        bernoulliFun (2 * k + 1) x) := by
    convert! hasSum_one_div_nat_pow_mul_fourier (by lia : 2 ≤ 2 * k + 1) hx using 1
    · ext1 n
      rw [pow_add (-1 : ℂ), pow_mul (-1 : ℂ), neg_one_sq, one_pow, one_mul, pow_one, ←
        neg_eq_neg_one_mul, ← sub_eq_add_neg]
    · congr
      rw [pow_add, pow_one]
      conv_rhs =>
        rw [mul_pow]
        congr
        congr
        · skip
        · rw [pow_add, pow_one, pow_mul, I_sq]
      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) : ℂ))
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ℕ) 2 2
⊢ (↑2 : ℂ) = 2

Tactic:
norm_cast
-- 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) : ℂ))
⊢ (↑2 : ℂ) = 2

Tactic:
have ofReal_two : ((2 : ℝ) : ℂ) = 2 := by norm_cast
-- 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
⊢ HasSum
    (fun (x_1 : ℕ) ↦
      (1 / HPow.hPow (α := ℂ) (↑x_1 : ℂ) (2 * k + 1) *
            HSub.hSub (α := ℂ) (β := ℂ)
              ((fourier (↑x_1 : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
              ((fourier (-(↑x_1 : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) /
          (2 * I)).re)
    (HPow.hPow (α := ℂ) (-1) (k + 1) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
          (↑(bernoulliFun (2 * k + 1) x) : ℂ) /
        (2 * I)).re

Tactic:
((hasSum_iff _ _).mp (this.div_const (2 * I))).1

Premises used: HMul.hMul, HasSum.div_const, And.left, Iff.mp, OfNat.ofNat, Complex.hasSum_iff, Complex.I
-- 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 :
  ∀ (x_1 : ℕ),
    1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) (2 * k + 1) * Real.sin (2 * π * (↑x_1 : ℝ) * x) =
      (1 / HPow.hPow (α := ℂ) (↑x_1 : ℂ) (2 * k + 1) *
            HSub.hSub (α := ℂ) (β := ℂ)
              ((fourier (↑x_1 : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
              ((fourier (-(↑x_1 : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) /
          (2 * I)).re
h₁ :
  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
⊢ HasSum (fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k + 1) * Real.sin (2 * π * (↑n : ℝ) * 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))))

Tactic:
convert! ((hasSum_iff _ _).mp (this.div_const (2 * I))).1

Premises used: HMul.hMul, HasSum.div_const, And.left, Iff.mp, OfNat.ofNat, Complex.hasSum_iff, Complex.I
-- 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) * Real.sin (2 * π * (↑x_1 : ℝ) * x) =
    (↑(1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) (2 * k + 1) * Real.sin (2 * π * (↑x_1 : ℝ) * x)) : ℂ).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
x_1 : ℕ
h :
  1 / HPow.hPow (α := ℂ) (↑x_1 : ℂ) (2 * k + 1) *
        HSub.hSub (α := ℂ) (β := ℂ)
          ((fourier (↑x_1 : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑x_1 : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) /
      (2 * I) =
    (↑(1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) (2 * k + 1) * Real.sin (2 * π * (↑x_1 : ℝ) * x)) : ℂ)
⊢ 1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) (2 * k + 1) * Real.sin (2 * π * (↑x_1 : ℝ) * x) =
    (1 / HPow.hPow (α := ℂ) (↑x_1 : ℂ) (2 * k + 1) *
          HSub.hSub (α := ℂ) (β := ℂ)
            ((fourier (↑x_1 : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
            ((fourier (-(↑x_1 : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) /
        (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
x_1 : ℕ
h :
  1 / HPow.hPow (α := ℂ) (↑x_1 : ℂ) (2 * k + 1) *
        HSub.hSub (α := ℂ) (β := ℂ)
          ((fourier (↑x_1 : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑x_1 : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) /
      (2 * I) =
    (↑(1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) (2 * k + 1)) : ℂ) * (↑(Real.sin (2 * π * (↑x_1 : ℝ) * x)) : ℂ)
⊢ 1 / HPow.hPow (α := ℂ) (↑x_1 : ℂ) (2 * k + 1) *
        HSub.hSub (α := ℂ) (β := ℂ)
          ((fourier (↑x_1 : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑x_1 : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) /
      (2 * I) =
    (↑(1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) (2 * k + 1) * Real.sin (2 * π * (↑x_1 : ℝ) * x)) : ℂ)

Tactic:
rw [ofReal_mul]

Premises used: 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 :
  1 / HPow.hPow (α := ℂ) (↑x_1 : ℂ) (2 * k + 1) *
      (HSub.hSub (α := ℂ) (β := ℂ)
          ((fourier (↑x_1 : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑x_1 : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) /
        (2 * I)) =
    (↑(1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) (2 * k + 1)) : ℂ) * (↑(Real.sin (2 * π * (↑x_1 : ℝ) * x)) : ℂ)
⊢ 1 / HPow.hPow (α := ℂ) (↑x_1 : ℂ) (2 * k + 1) *
        HSub.hSub (α := ℂ) (β := ℂ)
          ((fourier (↑x_1 : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑x_1 : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) /
      (2 * I) =
    (↑(1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) (2 * k + 1)) : ℂ) * (↑(Real.sin (2 * π * (↑x_1 : ℝ) * x)) : ℂ)

Tactic:
rw [← mul_div]

Premises used: mul_div
-- 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 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) (2 * k + 1)) : ℂ)
h₁ :
  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)) : ℂ)
⊢ 1 / HPow.hPow (α := ℂ) (↑x_1 : ℂ) (2 * k + 1) *
      (HSub.hSub (α := ℂ) (β := ℂ)
          ((fourier (↑x_1 : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          ((fourier (-(↑x_1 : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) /
        (2 * I)) =
    (↑(1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) (2 * k + 1)) : ℂ) * (↑(Real.sin (2 * π * (↑x_1 : ℝ) * x)) : ℂ)

Tactic:
congr