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
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)) : ℂ)
⊢ 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₁ : 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: 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) *
        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 / HPow.hPow (α := ℝ) (↑n : ℝ) (2 * k)) : ℂ)
have h : 1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k) = 1 / (↑(↑n : ℝ) : ℂ) ^ (2 * k)
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) *
        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 : ℕ
⊢ 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)) : ℂ)
have h : (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑x : ℂ)) + cexp (2 * (↑π : ℂ) * I * -(↑n : ℂ) * (↑x : ℂ))) / 2 =
  (cexp (2 * (↑π : ℂ) * (↑n : ℂ) * (↑x : ℂ) * I) + cexp (-(2 * (↑π : ℂ) * (↑n : ℂ) * (↑x : ℂ)) * I)) / 2
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]
-- 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 : ℕ
⊢ (cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑x : ℂ)) + cexp (2 * (↑π : ℂ) * I * -(↑n : ℂ) * (↑x : ℂ))) / 2 =
    (cexp (2 * (↑π : ℂ) * (↑n : ℂ) * (↑x : ℂ) * I) + cexp (-(2 * (↑π : ℂ) * (↑n : ℂ) * (↑x : ℂ)) * I)) / 2
have h : 2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑x : ℂ) = 2 * (↑π : ℂ) * (↑n : ℂ) * (↑x : ℂ) * I
Tactic: congr 3
-- 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 : ℕ
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
have h₁ : 2 * (↑π : ℂ) * I * -(↑n : ℂ) * (↑x : ℂ) = -(2 * (↑π : ℂ) * (↑n : ℂ) * (↑x : ℂ)) * I
Tactic: congr 3
-- 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
⊢ 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
have 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)))) :
    ℂ)
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
⊢ 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)))) :
      ℂ)
have 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)))) : ℂ)
Tactic: rw [ofReal_mul, ofReal_div, ofReal_div, ofReal_mul, ofReal_pow, ofReal_pow, ofReal_neg,
      ofReal_natCast, ofReal_mul, ofReal_two, ofReal_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
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) : ℂ))
have 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) : ℂ))
Tactic: convert! hasSum_one_div_nat_pow_mul_fourier (by lia : 2 ≤ 2 * k + 1) hx using 1
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
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) : ℂ))
⊢ 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) : ℂ))
have 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) : ℂ)
Tactic: convert! hasSum_one_div_nat_pow_mul_fourier (by lia : 2 ≤ 2 * k + 1) hx using 1
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ 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) : ℂ))
have 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) : ℂ))
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
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) : ℂ))
have h : 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) * HPow.hPow (α := ℂ) (β := ℕ) (-1) 1)
        ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
Tactic: 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]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
h :
  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) * HPow.hPow (α := ℂ) (β := ℕ) (-1) 1)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
⊢ 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) : ℂ))
have h₁ : 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 * HPow.hPow (α := ℂ) (β := ℕ) (-1) 1)
        ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
Tactic: 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]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
h :
  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) * HPow.hPow (α := ℂ) (β := ℕ) (-1) 1)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
h₁ :
  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 * HPow.hPow (α := ℂ) (β := ℕ) (-1) 1)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
⊢ 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) : ℂ))
have h₂ : 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 k * HPow.hPow (α := ℂ) (β := ℕ) (-1) 1)
        ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
Tactic: 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]
-- 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 * k + 1)! : ℂ) *
      (↑(bernoulliFun (2 * k + 1) x) : ℂ) =
    -(2 * (↑π : ℂ) * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) * (↑(bernoulliFun (2 * k + 1) x) : ℂ)
have h : HPow.hPow (α := ℂ) (-1) (k + 1) * I * (2 * (↑π : ℂ)) ^ (2 * k + 1) = -(2 * (↑π : ℂ) * I) ^ (2 * k + 1)
Tactic: congr