awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : 2 ≤ k
this :
  ∀ (n : ℤ),
    -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k =
      -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
have refine : Summable (α := ℝ) fun (a : ℤ) ↦ ‖1 / HPow.hPow (α := ℂ) (↑a : ℂ) k‖
Tactic: refine Summable.mul_left _ <| .of_norm ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : 2 ≤ k
this :
  ∀ (n : ℤ),
    -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k =
      -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
⊢ Eq (α := (x : ℤ) → ℝ) (fun (x : ℤ) ↦ ‖1 / HPow.hPow (α := ℂ) (↑x : ℂ) k‖) fun (x : ℤ) ↦
    |1 / HPow.hPow (α := ℝ) (↑x : ℝ) k|
have h : ∀ (x : ℤ), ‖1 / HPow.hPow (α := ℂ) (↑x : ℂ) k‖ = |1 / HPow.hPow (α := ℝ) (↑x : ℝ) k|
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (hypothesis)
Goal:
k : ℕ
hk : 2 ≤ k
this :
  ∀ (n : ℤ),
    -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k =
      -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
⊢ Summable (α := ℝ) fun (a : ℤ) ↦ ‖1 / HPow.hPow (α := ℂ) (↑a : ℂ) k‖
have this₁ : Eq (α := (x : ℤ) → ℝ) (fun (x : ℤ) ↦ ‖1 / HPow.hPow (α := ℂ) (↑x : ℂ) k‖) fun (x : ℤ) ↦
  |1 / HPow.hPow (α := ℝ) (↑x : ℝ) k|
Tactic: have : (fun x : ℤ => ‖1 / (x : ℂ) ^ k‖) = fun x : ℤ => |1 / (x : ℝ) ^ k| := by
    ext1 x
    simp only [one_div, norm_inv, norm_pow, norm_intCast, pow_abs, abs_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : 2 ≤ k
this_1 :
  ∀ (n : ℤ),
    -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k =
      -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
this :
  Eq (α := (x : ℤ) → ℝ) (fun (x : ℤ) ↦ ‖1 / HPow.hPow (α := ℂ) (↑x : ℂ) k‖) fun (x : ℤ) ↦
    |1 / HPow.hPow (α := ℝ) (↑x : ℝ) k|
⊢ Summable (α := ℝ) fun (a : ℤ) ↦ ‖1 / HPow.hPow (α := ℂ) (↑a : ℂ) k‖
have simp_rw : Summable (α := ℝ) fun (x : ℤ) ↦ |1 / HPow.hPow (α := ℝ) (↑x : ℝ) k|
Tactic: simp_rw [this]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : 2 ≤ k
this_1 :
  ∀ (n : ℤ),
    -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k =
      -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
this :
  Eq (α := (x : ℤ) → ℝ) (fun (x : ℤ) ↦ ‖1 / HPow.hPow (α := ℂ) (↑x : ℂ) k‖) fun (x : ℤ) ↦
    |1 / HPow.hPow (α := ℝ) (↑x : ℝ) k|
⊢ Summable (α := ℝ) fun (x : ℤ) ↦ |1 / HPow.hPow (α := ℝ) (↑x : ℝ) k|
have rwa : Summable (α := ℝ) fun (x : ℤ) ↦ 1 / HPow.hPow (α := ℝ) (↑x : ℝ) k
Tactic: rwa [summable_abs_iff, Real.summable_one_div_int_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : 2 ≤ k
this_1 :
  ∀ (n : ℤ),
    -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k =
      -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
this :
  Eq (α := (x : ℤ) → ℝ) (fun (x : ℤ) ↦ ‖1 / HPow.hPow (α := ℂ) (↑x : ℂ) k‖) fun (x : ℤ) ↦
    |1 / HPow.hPow (α := ℝ) (↑x : ℝ) k|
rwa : Summable (α := ℝ) fun (x : ℤ) ↦ 1 / HPow.hPow (α := ℝ) (↑x : ℝ) k
⊢ Summable (α := ℝ) fun (x : ℤ) ↦ |1 / HPow.hPow (α := ℝ) (↑x : ℝ) k|
have rwa₁ : 1 < k
Tactic: rwa [summable_abs_iff, Real.summable_one_div_int_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (hypothesis)
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this :
  ∀ {y : ℝ},
    Membership.mem (γ := Set ℝ) (Ico 0 1) y →
      HasSum
        (fun (n : ℤ) ↦
          HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
            ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
        (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
⊢ HasSum
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ))
have hx₁ : Membership.mem (γ := Set ℝ) (Ico 0 1) x ∨ x = 1
Tactic: rw [← Ico_insert_right (zero_le_one' ℝ), mem_insert_iff, or_comm] at hx
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx_1 : Membership.mem (γ := Set ℝ) (Icc 0 1) x
hx : Membership.mem (γ := Set ℝ) (Ico 0 1) x ∨ x = 1
this :
  ∀ {y : ℝ},
    Membership.mem (γ := Set ℝ) (Ico 0 1) y →
      HasSum
        (fun (n : ℤ) ↦
          HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
            ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
        (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
⊢ HasSum
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ))
have inl : ∀ (hx : Membership.mem (γ := Set ℝ) (Ico 0 1) x),
  HasSum
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ))
Tactic: rcases hx with (hx | rfl)
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx_1 : Membership.mem (γ := Set ℝ) (Icc 0 1) x
hx : Membership.mem (γ := Set ℝ) (Ico 0 1) x ∨ x = 1
this :
  ∀ {y : ℝ},
    Membership.mem (γ := Set ℝ) (Ico 0 1) y →
      HasSum
        (fun (n : ℤ) ↦
          HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
            ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
        (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
inl :
  ∀ (hx : Membership.mem (γ := Set ℝ) (Ico 0 1) x),
    HasSum
      (fun (n : ℤ) ↦
        HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
          ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
      (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ))
⊢ HasSum
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ))
have inr : ∀ (hx : Membership.mem (γ := Set ℝ) (Icc 0 1) 1)
  (this :
    ∀ {y : ℝ},
      Membership.mem (γ := Set ℝ) (Ico 0 1) y →
        HasSum
          (fun (n : ℤ) ↦
            HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
              ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
          (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))),
  HasSum
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑1 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k 1) : ℂ))
Tactic: rcases hx with (hx | rfl)
Cleared hypotheses: x, hx_1, hx, this
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : 2 ≤ k
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) 1
this :
  ∀ {y : ℝ},
    Membership.mem (γ := Set ℝ) (Ico 0 1) y →
      HasSum
        (fun (n : ℤ) ↦
          HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
            ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
        (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
⊢ HasSum
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑1 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k 1) : ℂ))
have h : Eq (α := ℤ → ℂ)
  (fun (n : ℤ) ↦
    HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
      ((fourier n : (a : AddCircle 1) → ℂ) (↑1 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
  fun (n : ℤ) ↦
  HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
    ((fourier n : (a : AddCircle 1) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
Tactic: convert! this (left_mem_Ico.mpr zero_lt_one) using 1
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : 2 ≤ k
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) 1
this :
  ∀ {y : ℝ},
    Membership.mem (γ := Set ℝ) (Ico 0 1) y →
      HasSum
        (fun (n : ℤ) ↦
          HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
            ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
        (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
h :
  Eq (α := ℤ → ℂ)
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑1 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    fun (n : ℤ) ↦
    HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
      ((fourier n : (a : AddCircle 1) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
⊢ HasSum
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑1 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k 1) : ℂ))
have h₁ : -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k 1) : ℂ) =
  -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k 0) : ℂ)
Tactic: convert! this (left_mem_Ico.mpr zero_lt_one) using 1
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : 2 ≤ k
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) 1
this :
  ∀ {y : ℝ},
    Membership.mem (γ := Set ℝ) (Ico 0 1) y →
      HasSum
        (fun (n : ℤ) ↦
          HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
            ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
        (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
⊢ Eq (α := ℤ → ℂ)
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑1 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    fun (n : ℤ) ↦
    HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
      ((fourier n : (a : AddCircle 1) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
have h : Eq (α := ℤ → ℂ)
  (fun (n : ℤ) ↦ HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k) ((fourier n : (a : AddCircle 1) → ℂ) 0 : ℂ))
  fun (n : ℤ) ↦
  HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
    ((fourier n : (a : AddCircle 1) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
Tactic: rw [AddCircle.coe_period, QuotientAddGroup.mk_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : 2 ≤ k
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) 1
this :
  ∀ {y : ℝ},
    Membership.mem (γ := Set ℝ) (Ico 0 1) y →
      HasSum
        (fun (n : ℤ) ↦
          HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
            ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
        (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
h :
  Eq (α := ℤ → ℂ)
    (fun (n : ℤ) ↦ HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k) ((fourier n : (a : AddCircle 1) → ℂ) 0 : ℂ))
    fun (n : ℤ) ↦
    HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
      ((fourier n : (a : AddCircle 1) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
⊢ Eq (α := ℤ → ℂ)
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑1 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    fun (n : ℤ) ↦
    HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
      ((fourier n : (a : AddCircle 1) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
have h₁ : Eq (α := ℤ → ℂ)
  (fun (n : ℤ) ↦ HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k) ((fourier n : (a : AddCircle 1) → ℂ) 0 : ℂ))
  fun (n : ℤ) ↦ HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k) ((fourier n : (a : AddCircle 1) → ℂ) 0 : ℂ)
Tactic: rw [AddCircle.coe_period, QuotientAddGroup.mk_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : 2 ≤ k
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) 1
this :
  ∀ {y : ℝ},
    Membership.mem (γ := Set ℝ) (Ico 0 1) y →
      HasSum
        (fun (n : ℤ) ↦
          HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
            ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
        (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
⊢ -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k 1) : ℂ) =
    -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k 0) : ℂ)
have h : -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k 0) : ℂ) =
  -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k 0) : ℂ)
Tactic: rw [bernoulliFun_endpoints_eq_of_ne_one (by lia : k ≠ 1)]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ HasSum
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ))
have suffices : ∀ {y : ℝ},
  Membership.mem (γ := Set ℝ) (Ico 0 1) y →
    HasSum
      (fun (n : ℤ) ↦
        HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
          ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
      (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
Tactic: suffices ∀ {y : ℝ}, y ∈ Ico (0 : ℝ) 1 →
      HasSum (fun (n : ℤ) ↦ 1 / (n : ℂ) ^ k * fourier n y)
        (-(2 * (π : ℂ) * I) ^ k / k ! * bernoulliFun k y) by
    rw [← Ico_insert_right (zero_le_one' ℝ), mem_insert_iff, or_comm] at hx
    rcases hx with (hx | rfl)
    · exact this hx
    · convert! this (left_mem_Ico.mpr zero_lt_one) using 1
      · rw [AddCircle.coe_period, QuotientAddGroup.mk_zero]
      · rw [bernoulliFun_endpoints_eq_of_ne_one (by lia : k ≠ 1)]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ico 0 1) y
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
⊢ ∀ (n : ℤ), fourierCoeff (T := 1) (⇑B : (a : 𝕌) → ℂ) n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
have rw : ∀ (n : ℤ), fourierCoeff (ofReal ∘ periodizedBernoulli k) n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
Tactic: rw [ContinuousMap.coe_mk]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (hypothesis)
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ico 0 1) y
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
⊢ HasSum
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
have step1 : ∀ (n : ℤ), fourierCoeff (T := 1) (⇑B : (a : 𝕌) → ℂ) n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
Tactic: have step1 : ∀ n : ℤ, fourierCoeff B n = -k ! / (2 * π * I * n) ^ k := by
    rw [ContinuousMap.coe_mk]; exact fourierCoeff_bernoulli_eq (by lia : k ≠ 0)
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (hypothesis)
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ico 0 1) y
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (T := 1) (⇑B : (a : 𝕌) → ℂ) n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
⊢ HasSum
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
have step2 : HasSum (α := ℂ)
  (fun (i : ℤ) ↦
    HSMul.hSMul (α := ℂ) (β := ℂ) (fourierCoeff (T := 1) (⇑B : (a : AddCircle 1) → ℂ) i)
      ((fourier i : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
  ((B : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
Tactic: have step2 :=
    has_pointwise_sum_fourier_series_of_summable
      ((summable_bernoulli_fourier hk).congr fun n => (step1 n).symm) y
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (hypothesis)
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ico 0 1) y
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (T := 1) (⇑B : (a : 𝕌) → ℂ) n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
step2 :
  HasSum (α := ℂ)
    (fun (i : ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := ℂ) (fourierCoeff (T := 1) (⇑B : (a : AddCircle 1) → ℂ) i)
        ((fourier i : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    ((B : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
⊢ HasSum
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
have step2₁ : HasSum (α := ℂ)
  (fun (i : ℤ) ↦
    HSMul.hSMul (β := ℂ) (-(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑i : ℂ)) ^ k)
      ((fourier i : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
  ((B : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
Tactic: simp_rw [step1] at step2
Cleared hypotheses: step2
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ico 0 1) y
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (T := 1) (⇑B : (a : 𝕌) → ℂ) n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
step2 :
  HasSum (α := ℂ)
    (fun (i : ℤ) ↦
      HSMul.hSMul (β := ℂ) (-(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑i : ℂ)) ^ k)
        ((fourier i : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    ((B : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
⊢ HasSum
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
have h : ∀ (n : ℤ),
  HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
      ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) =
    -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) *
      HSMul.hSMul (β := ℂ) (-(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
Tactic: convert! step2.mul_left (-(2 * ↑π * I) ^ k / (k ! : ℂ)) using 2 with n
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ico 0 1) y
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (T := 1) (⇑B : (a : 𝕌) → ℂ) n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
step2 :
  HasSum (α := ℂ)
    (fun (i : ℤ) ↦
      HSMul.hSMul (β := ℂ) (-(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑i : ℂ)) ^ k)
        ((fourier i : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    ((B : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
h :
  ∀ (n : ℤ),
    HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) =
      -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) *
        HSMul.hSMul (β := ℂ) (-(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k)
          ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
⊢ HasSum
    (fun (n : ℤ) ↦
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k y) : ℂ))
have h₁ : (↑(bernoulliFun k y) : ℂ) = (B : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1)
Tactic: convert! step2.mul_left (-(2 * ↑π * I) ^ k / (k ! : ℂ)) using 2 with n
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ico 0 1) y
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (T := 1) (⇑B : (a : 𝕌) → ℂ) n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
step2 :
  HasSum (α := ℂ)
    (fun (i : ℤ) ↦
      HSMul.hSMul (β := ℂ) (-(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑i : ℂ)) ^ k)
        ((fourier i : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    ((B : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
n : ℤ
⊢ HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
      ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) =
    -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) *
      HSMul.hSMul (β := ℂ) (-(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
have h : (2 * (↑π : ℂ) * I) ^ k ≠ 0
Tactic: rw [smul_eq_mul, ← mul_assoc, mul_div, mul_neg, div_mul_cancel₀, neg_neg, mul_pow _ (n : ℂ),
      ← div_div, div_self]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ico 0 1) y
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (T := 1) (⇑B : (a : 𝕌) → ℂ) n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
step2 :
  HasSum (α := ℂ)
    (fun (i : ℤ) ↦
      HSMul.hSMul (β := ℂ) (-(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑i : ℂ)) ^ k)
        ((fourier i : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    ((B : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
n : ℤ
h : (2 * (↑π : ℂ) * I) ^ k ≠ 0
⊢ HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
      ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) =
    -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) *
      HSMul.hSMul (β := ℂ) (-(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
have h₁ : Ne (α := ℂ) (↑k ! : ℂ) 0
Tactic: rw [smul_eq_mul, ← mul_assoc, mul_div, mul_neg, div_mul_cancel₀, neg_neg, mul_pow _ (n : ℂ),
      ← div_div, div_self]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ico 0 1) y
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (T := 1) (⇑B : (a : 𝕌) → ℂ) n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
step2 :
  HasSum (α := ℂ)
    (fun (i : ℤ) ↦
      HSMul.hSMul (β := ℂ) (-(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑i : ℂ)) ^ k)
        ((fourier i : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    ((B : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
n : ℤ
⊢ (2 * (↑π : ℂ) * I) ^ k ≠ 0
have h : ¬2 * (↑π : ℂ) * I = 0 ∨ ¬k ≠ 0
Tactic: rw [Ne, pow_eq_zero_iff', not_and_or]