awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ k ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h :
  -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ) =
    -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ) +
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) 0 k)
        ((fourier 0 : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
h₁ :
  -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ) =
    -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ) +
      HMul.hMul (β := ℂ) (1 / 0) ((fourier 0 : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
h₂ :
  -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ) =
    -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ) +
      HMul.hMul (α := ℂ) (β := ℂ) (0 : ℂ) ((fourier 0 : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
h₃ :
  -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ) =
    -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ) + 0
h₄ h₅ :
  -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ) =
    -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ)
⊢ -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ) =
    -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ) +
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑0 : ℂ) k)
        ((fourier 0 : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)

Tactic:
rw [Int.cast_zero, zero_pow (by positivity : k ≠ 0), div_zero, zero_mul, add_zero]

Premises used: Int.cast_zero, MulZeroClass.zero_mul, add_zero, div_zero, zero_pow
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ 2 ≤ 2 * k

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

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

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
x_1 : ℕ
h :
  HAdd.hAdd (α := ℂ) (β := ℂ) ((fourier (↑x_1 : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
      ((fourier (-(↑x_1 : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) =
    HAdd.hAdd (α := ℂ) ((fourier (↑x_1 : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
      (HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (β := ℕ) (-1) 2 ^ k)
        ((fourier (-(↑x_1 : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
h₁ :
  HAdd.hAdd (α := ℂ) (β := ℂ) ((fourier (↑x_1 : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
      ((fourier (-(↑x_1 : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) =
    HAdd.hAdd (α := ℂ) ((fourier (↑x_1 : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
      (HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) 1 k)
        ((fourier (-(↑x_1 : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
h₂ :
  HAdd.hAdd (α := ℂ) (β := ℂ) ((fourier (↑x_1 : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
      ((fourier (-(↑x_1 : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) =
    HAdd.hAdd (α := ℂ) ((fourier (↑x_1 : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
      (HMul.hMul (α := ℂ) (β := ℂ) (1 : ℂ)
        ((fourier (-(↑x_1 : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
h₃ h₄ :
  HAdd.hAdd (α := ℂ) (β := ℂ) ((fourier (↑x_1 : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
      ((fourier (-(↑x_1 : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((fourier (↑x_1 : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
      ((fourier (-(↑x_1 : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
⊢ HAdd.hAdd (α := ℂ) (β := ℂ) ((fourier (↑x_1 : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
      ((fourier (-(↑x_1 : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) =
    HAdd.hAdd (α := ℂ) ((fourier (↑x_1 : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
      (HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (-1) (2 * k))
        ((fourier (-(↑x_1 : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))

Tactic:
rw [pow_mul (-1 : ℂ), neg_one_sq, one_pow, one_mul]

Premises used: one_pow, neg_one_sq, pow_mul, OfNat.ofNat, Neg.neg, one_mul
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
rw : -((2 * (↑π : ℂ)) ^ (2 * k) * I ^ (2 * k))
| -(2 * (↑π : ℂ) * I) ^ (2 * k)

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) * I ^ (2 * k)
| -((2 * (↑π : ℂ)) ^ (2 * k) * I ^ (2 * k))

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

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

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 ^ (2 * k)

Tactic:
rw [pow_mul, I_sq]

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

Tactic:
· rw [pow_mul, I_sq]

Premises used: pow_mul, 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) * I ^ (2 * k))
a : (2 * (↑π : ℂ)) ^ (2 * k) * I ^ (2 * k)
a₁ : (2 * (↑π : ℂ)) ^ (2 * k)
a₂ a₃ : I ^ (2 * k)
| -(2 * (↑π : ℂ) * I) ^ (2 * k)

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

Premises used: pow_mul, 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 * (2 * (↑π : ℂ)) ^ (2 * k) = -((2 * (↑π : ℂ)) ^ (2 * k) * HPow.hPow (α := ℂ) (-1) k)
⊢ HPow.hPow (α := ℂ) (-1) k * -1 * (2 * (↑π : ℂ)) ^ (2 * k) = -(2 * (↑π : ℂ) * I) ^ (2 * k)

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

Premises used: pow_mul, 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 * (2 * (↑π : ℂ)) ^ (2 * k) = -((2 * (↑π : ℂ)) ^ (2 * k) * HPow.hPow (α := ℂ) (-1) k)

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) *
        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) : ℂ))

Tactic:
have :
    HasSum (fun n : ℕ => 1 / (n : ℂ) ^ (2 * k) * (fourier n (x : 𝕌) + fourier (-n) (x : 𝕌)))
      ((-1 : ℂ) ^ (k + 1) * (2 * (π : ℂ)) ^ (2 * k) / (2 * k)! * bernoulliFun (2 * k) x) := by
    convert! hasSum_one_div_nat_pow_mul_fourier (by lia : 2 ≤ 2 * k) hx using 3
    · rw [pow_mul (-1 : ℂ), neg_one_sq, one_pow, one_mul]
    · rw [pow_add, pow_one]
      conv_rhs =>
        rw [mul_pow]
        congr
        congr
        · skip
        · rw [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) *
        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) : ℂ))
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) *
        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) : ℂ))
⊢ (↑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) *
        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
⊢ HasSum
    (fun (x_1 : ℕ) ↦
      (1 / HPow.hPow (α := ℂ) (↑x_1 : ℂ) (2 * k) *
            HAdd.hAdd (α := ℂ) (β := ℂ)
              ((fourier (↑x_1 : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
              ((fourier (-(↑x_1 : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) /
          2).re)
    (HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / (↑(2 * k)! : ℂ) * (↑(bernoulliFun (2 * k) x) : ℂ) /
        2).re

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

Premises used: HasSum.div_const, And.left, Iff.mp, OfNat.ofNat, Complex.hasSum_iff
-- 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 :
  ∀ (n : ℕ),
    1 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k) * Real.cos (2 * π * (↑n : ℝ) * x) =
      (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) : ℂ) /
          2).re
h₁ :
  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
⊢ HasSum (fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k) * Real.cos (2 * π * (↑n : ℝ) * x))
    (HPow.hPow (α := ℝ) (-1) (k + 1) * (2 * π) ^ (2 * k) / 2 / (↑(2 * k)! : ℝ) *
      Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))

Tactic:
convert! ((hasSum_iff _ _).mp (this.div_const 2)).1 with n

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

Tactic:
congr
-- 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 : ℕ
h : 1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k) = 1 / (↑(↑n : ℝ) : ℂ) ^ (2 * k)
⊢ 1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k) = (↑(1 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k)) : ℂ)

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) *
        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 : ℕ
⊢ 1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k) = 1 / (↑(↑n : ℝ) : ℂ) ^ (2 * k)

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) *
        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 : ℕ
h :
  (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑x : ℂ)) + cexp (2 * (↑π : ℂ) * I * -(↑n : ℂ) * (↑x : ℂ))) / 2 =
    (cexp (2 * (↑π : ℂ) * (↑n : ℂ) * (↑x : ℂ) * I) + cexp (-(2 * (↑π : ℂ) * (↑n : ℂ) * (↑x : ℂ)) * I)) / 2
⊢ HAdd.hAdd (α := ℂ) (β := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
        ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) /
      2 =
    (↑(Real.cos (2 * π * (↑n : ℝ) * x)) : ℂ)

Tactic:
rw [ofReal_cos, ofReal_mul, fourier_coe_apply, fourier_coe_apply, cos, ofReal_one, div_one,
        div_one, ofReal_mul, ofReal_mul, ofReal_two, Int.cast_neg, Int.cast_natCast,
        ofReal_natCast]

Premises used: Int.cast_neg, Int.cast_natCast, Complex.cos, fourier_coe_apply, Complex.ofReal_one, Complex.ofReal_natCast, Complex.ofReal_cos, div_one, 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
n : ℕ
h : 2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑x : ℂ) = 2 * (↑π : ℂ) * (↑n : ℂ) * (↑x : ℂ) * I
h₁ : 2 * (↑π : ℂ) * I * -(↑n : ℂ) * (↑x : ℂ) = -(2 * (↑π : ℂ) * (↑n : ℂ) * (↑x : ℂ)) * I
⊢ (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑x : ℂ)) + cexp (2 * (↑π : ℂ) * I * -(↑n : ℂ) * (↑x : ℂ))) / 2 =
    (cexp (2 * (↑π : ℂ) * (↑n : ℂ) * (↑x : ℂ) * I) + cexp (-(2 * (↑π : ℂ) * (↑n : ℂ) * (↑x : ℂ)) * I)) / 2

Tactic:
congr 3
-- 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