awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
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) : ℂ))
⊢ 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) : ℂ))
have h₁ : HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) = -(2 * (↑π : ℂ) * I) ^ (2 * k)
Tactic: convert! hasSum_one_div_nat_pow_mul_fourier (by lia : 2 ≤ 2 * k) hx using 3
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
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) : ℂ))
have 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) : ℂ))
Tactic: rw [pow_mul (-1 : ℂ), neg_one_sq, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
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) : ℂ))
⊢ 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) : ℂ))
have 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) : ℂ))
Tactic: rw [pow_mul (-1 : ℂ), neg_one_sq, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
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) : ℂ))
⊢ 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) : ℂ))
have 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) : ℂ))
Tactic: rw [pow_mul (-1 : ℂ), neg_one_sq, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
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) : ℂ))
⊢ 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) : ℂ))
have 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) : ℂ)
Tactic: rw [pow_mul (-1 : ℂ), neg_one_sq, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
| -(2 * (↑π : ℂ) * I) ^ (2 * k)
have rw : -((2 * (↑π : ℂ)) ^ (2 * k) * I ^ (2 * k))
Tactic: rw [mul_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
| -((2 * (↑π : ℂ)) ^ (2 * k) * I ^ (2 * k))
have a : (2 * (↑π : ℂ)) ^ (2 * k) * I ^ (2 * k)
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
| (2 * (↑π : ℂ)) ^ (2 * k) * I ^ (2 * k)
have a : (2 * (↑π : ℂ)) ^ (2 * k)
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
a : (2 * (↑π : ℂ)) ^ (2 * k)
| (2 * (↑π : ℂ)) ^ (2 * k) * I ^ (2 * k)
have a₁ : I ^ (2 * k)
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
| I ^ (2 * k)
have a : HPow.hPow (α := ℂ) (-1) k
Tactic: rw [pow_mul, I_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
| I ^ (2 * k)
have a : HPow.hPow (β := ℕ) I 2 ^ k
Tactic: · rw [pow_mul, I_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
a : HPow.hPow (β := ℕ) I 2 ^ k
| I ^ (2 * k)
have a₁ : HPow.hPow (α := ℂ) (-1) k
Tactic: · rw [pow_mul, I_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
| -(2 * (↑π : ℂ) * I) ^ (2 * k)
have rw : -((2 * (↑π : ℂ)) ^ (2 * k) * I ^ (2 * k))
Tactic: rw [mul_pow]
        congr
        congr
        · skip
        · rw [pow_mul, I_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
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)
have a : (2 * (↑π : ℂ)) ^ (2 * k) * I ^ (2 * k)
Tactic: rw [mul_pow]
        congr
        congr
        · skip
        · rw [pow_mul, I_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
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)
| -(2 * (↑π : ℂ) * I) ^ (2 * k)
have a₁ : (2 * (↑π : ℂ)) ^ (2 * k)
Tactic: rw [mul_pow]
        congr
        congr
        · skip
        · rw [pow_mul, I_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
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)
| -(2 * (↑π : ℂ) * I) ^ (2 * k)
have a₂ : I ^ (2 * k)
Tactic: rw [mul_pow]
        congr
        congr
        · skip
        · rw [pow_mul, I_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ HPow.hPow (α := ℂ) (-1) k * -1 * (2 * (↑π : ℂ)) ^ (2 * k) = -(2 * (↑π : ℂ) * I) ^ (2 * k)
have h : HPow.hPow (α := ℂ) (-1) k * -1 * (2 * (↑π : ℂ)) ^ (2 * k) = -((2 * (↑π : ℂ)) ^ (2 * k) * HPow.hPow (α := ℂ) (-1) k)
Tactic: conv_rhs =>
        rw [mul_pow]
        congr
        congr
        · skip
        · rw [pow_mul, I_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (hypothesis)
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ 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))))
have 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) : ℂ))
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
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
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
have norm_cast : Eq (α := ℕ) 2 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (hypothesis)
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) : ℂ))
⊢ 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))))
have ofReal_two : (↑2 : ℂ) = 2
Tactic: have ofReal_two : ((2 : ℝ) : ℂ) = 2 := by norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
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 (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))))
have 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
Tactic: convert! ((hasSum_iff _ _).mp (this.div_const 2)).1 with n
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
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
⊢ 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))))
have 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
Tactic: convert! ((hasSum_iff _ _).mp (this.div_const 2)).1 with n
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
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) *
          HAdd.hAdd (α := ℂ) (β := ℂ)
            ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
            ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) /
        2).re
have 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)) : ℂ)
Tactic: convert! (ofReal_re _).symm
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
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) *
        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)) : ℂ)
have 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)) : ℂ)
Tactic: rw [ofReal_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
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) *
        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)) : ℂ)
have 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)) : ℂ)
Tactic: rw [← mul_div]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
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) *
      (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)) : ℂ)
have h : 1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k) = (↑(1 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k)) : ℂ)
Tactic: congr