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
| -(2 * (↑π : ℂ) * I) ^ (2 * k + 1)
have rw : -((2 * (↑π : ℂ)) ^ (2 * k + 1) * I ^ (2 * k + 1))
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 + 1) * I ^ (2 * k + 1))
have a : (2 * (↑π : ℂ)) ^ (2 * k + 1) * I ^ (2 * k + 1)
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 + 1) * I ^ (2 * k + 1)
have a : (2 * (↑π : ℂ)) ^ (2 * k + 1)
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 + 1)
| (2 * (↑π : ℂ)) ^ (2 * k + 1) * I ^ (2 * k + 1)
have a₁ : I ^ (2 * k + 1)
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 + 1)
have a : HPow.hPow (α := ℂ) (-1) k * I
Tactic: rw [pow_add, pow_one, 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 + 1)
have a : I ^ (2 * k) * HPow.hPow (β := ℕ) I 1
Tactic: · rw [pow_add, pow_one, 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 : I ^ (2 * k) * HPow.hPow (β := ℕ) I 1
| I ^ (2 * k + 1)
have a₁ : I ^ (2 * k) * I
Tactic: · rw [pow_add, pow_one, 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 : I ^ (2 * k) * HPow.hPow (β := ℕ) I 1
a₁ : I ^ (2 * k) * I
| I ^ (2 * k + 1)
have a₂ : HPow.hPow (β := ℕ) I 2 ^ k * I
Tactic: · rw [pow_add, pow_one, 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 : I ^ (2 * k) * HPow.hPow (β := ℕ) I 1
a₁ : I ^ (2 * k) * I
a₂ : HPow.hPow (β := ℕ) I 2 ^ k * I
| I ^ (2 * k + 1)
have a₃ : HPow.hPow (α := ℂ) (-1) k * I
Tactic: · rw [pow_add, pow_one, 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 + 1)
have rw : -((2 * (↑π : ℂ)) ^ (2 * k + 1) * I ^ (2 * k + 1))
Tactic: rw [mul_pow]
        congr
        congr
        · skip
        · rw [pow_add, pow_one, 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 + 1) * I ^ (2 * k + 1))
| -(2 * (↑π : ℂ) * I) ^ (2 * k + 1)
have a : (2 * (↑π : ℂ)) ^ (2 * k + 1) * I ^ (2 * k + 1)
Tactic: rw [mul_pow]
        congr
        congr
        · skip
        · rw [pow_add, pow_one, 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 + 1) * I ^ (2 * k + 1))
a : (2 * (↑π : ℂ)) ^ (2 * k + 1) * I ^ (2 * k + 1)
| -(2 * (↑π : ℂ) * I) ^ (2 * k + 1)
have a₁ : (2 * (↑π : ℂ)) ^ (2 * k + 1)
Tactic: rw [mul_pow]
        congr
        congr
        · skip
        · rw [pow_add, pow_one, 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 + 1) * I ^ (2 * k + 1))
a : (2 * (↑π : ℂ)) ^ (2 * k + 1) * I ^ (2 * k + 1)
a₁ : (2 * (↑π : ℂ)) ^ (2 * k + 1)
| -(2 * (↑π : ℂ) * I) ^ (2 * k + 1)
have a₂ : I ^ (2 * k + 1)
Tactic: rw [mul_pow]
        congr
        congr
        · skip
        · rw [pow_add, pow_one, 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 * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) = -(2 * (↑π : ℂ) * I) ^ (2 * k + 1)
have h : HPow.hPow (α := ℂ) (-1) k * -1 * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) =
  -((2 * (↑π : ℂ)) ^ (2 * k + 1) * (HPow.hPow (α := ℂ) (-1) k * I))
Tactic: conv_rhs =>
        rw [mul_pow]
        congr
        congr
        · skip
        · rw [pow_add, pow_one, 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 + 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))))
have 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) : ℂ))
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
-- 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 + 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
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 + 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) : ℂ))
⊢ 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))))
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 + 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 (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))))
have 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
Tactic: convert! ((hasSum_iff _ _).mp (this.div_const (2 * I))).1
-- 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 + 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
⊢ 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))))
have 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
Tactic: convert! ((hasSum_iff _ _).mp (this.div_const (2 * I))).1
-- 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 + 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) *
          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
have 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)) : ℂ)
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 + 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) *
        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)) : ℂ)
have 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)) : ℂ)
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 + 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) *
        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)) : ℂ)
have 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)) : ℂ)
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 + 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) *
      (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)) : ℂ)
have h : 1 / HPow.hPow (α := ℂ) (↑x_1 : ℂ) (2 * k + 1) = (↑(1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) (2 * k + 1)) : ℂ)
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
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)) : ℂ)
⊢ 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)) : ℂ)
have 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)) : ℂ)
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
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 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) (2 * k + 1)) : ℂ)
have h : 1 / HPow.hPow (α := ℂ) (↑x_1 : ℂ) (2 * k + 1) = 1 / (↑(↑x_1 : ℝ) : ℂ) ^ (2 * k + 1)
Tactic: rw [ofReal_div, ofReal_one, ofReal_pow]
-- 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 + 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 : ℕ
⊢ 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)) : ℂ)
have 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
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]
-- 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 + 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 : ℕ
⊢ (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
have h : 2 * (↑π : ℂ) * I * -(↑x_1 : ℂ) * (↑x : ℂ) = -(2 * (↑π : ℂ) * (↑x_1 : ℂ) * (↑x : ℂ)) * I
Tactic: congr 4
-- 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 + 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
⊢ (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
have h₁ : 2 * (↑π : ℂ) * I * (↑x_1 : ℂ) * (↑x : ℂ) = 2 * (↑π : ℂ) * (↑x_1 : ℂ) * (↑x : ℂ) * I
Tactic: congr 4
-- 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 + 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) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) *
          (↑(bernoulliFun (2 * k + 1) x) : ℂ) /
        (2 * I)).re
have 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)))) :
    ℂ)
Tactic: convert! (ofReal_re _).symm