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
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ico 0 1) y
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
⊢ k ≠ 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.ZetaValues
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 (ofReal ∘ periodizedBernoulli k) n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k

Tactic:
exact fourierCoeff_bernoulli_eq (by lia : k ≠ 0)

Premises used: fourierCoeff_bernoulli_eq
-- Module: Mathlib.NumberTheory.ZetaValues
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

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)
-- Module: Mathlib.NumberTheory.ZetaValues
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 (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
-- Module: Mathlib.NumberTheory.ZetaValues
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 (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
-- Module: Mathlib.NumberTheory.ZetaValues
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 (i : ℤ) ↦
      -(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) *
        HSMul.hSMul (β := ℂ) (-(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑i : ℂ)) ^ k)
          ((fourier i : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (HMul.hMul (β := ℂ) (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ))
      ((B : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))

Tactic:
step2.mul_left (-(2 * ↑π * I) ^ k / (k ! : ℂ))

Premises used: HMul.hMul, HDiv.hDiv, HasSum.mul_left, Nat.cast, HPow.hPow, Nat.factorial, OfNat.ofNat, Neg.neg, Complex.I
-- Module: Mathlib.NumberTheory.ZetaValues
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) : ℂ)
h₁ : (↑(bernoulliFun k y) : ℂ) = (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) : ℂ))

Tactic:
convert! step2.mul_left (-(2 * ↑π * I) ^ k / (k ! : ℂ)) using 2 with n

Premises used: HMul.hMul, HDiv.hDiv, HasSum.mul_left, Nat.cast, HPow.hPow, Nat.factorial, OfNat.ofNat, Neg.neg, Complex.I
-- Module: Mathlib.NumberTheory.ZetaValues
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
h₁ : Ne (α := ℂ) (↑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) : ℂ)

Tactic:
rw [smul_eq_mul, ← mul_assoc, mul_div, mul_neg, div_mul_cancel₀, neg_neg, mul_pow _ (n : ℂ),
      ← div_div, div_self]

Premises used: mul_div, Int.cast, div_mul_cancel₀, mul_assoc, neg_neg, smul_eq_mul, div_div, mul_pow, div_self, mul_neg
-- Module: Mathlib.NumberTheory.ZetaValues
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 = 0 ∨ ¬k ≠ 0
⊢ (2 * (↑π : ℂ) * I) ^ k ≠ 0

Tactic:
rw [Ne, pow_eq_zero_iff', not_and_or]

Premises used: pow_eq_zero_iff', Ne, not_and_or
-- Module: Mathlib.NumberTheory.ZetaValues
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 = 0 ∨ ¬k ≠ 0

Tactic:
Or.inl two_pi_I_ne_zero

Premises used: Complex.two_pi_I_ne_zero, Or.inl
-- Module: Mathlib.NumberTheory.ZetaValues
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 = 0 ∨ ¬k ≠ 0

Tactic:
exact Or.inl two_pi_I_ne_zero

Premises used: Complex.two_pi_I_ne_zero, Or.inl
-- Module: Mathlib.NumberTheory.ZetaValues
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 : ℤ
⊢ Ne (α := ℂ) (↑k ! : ℂ) 0

Tactic:
Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)

Premises used: Iff.mpr, Nat.factorial_ne_zero, Nat.cast_ne_zero
-- Module: Mathlib.NumberTheory.ZetaValues
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 : ℤ
⊢ Ne (α := ℂ) (↑k ! : ℂ) 0

Tactic:
exact Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)

Premises used: Iff.mpr, Nat.factorial_ne_zero, Nat.cast_ne_zero
-- Module: Mathlib.NumberTheory.ZetaValues
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) : ℂ)
rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := Set ℝ) (Ico 0 1) y
⊢ y ∈ Ico 0 (HAdd.hAdd (α := ℝ) 0 1)

Tactic:
rwa [zero_add]

Premises used: zero_add
-- Module: Mathlib.NumberTheory.ZetaValues
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 : (↑(bernoulliFun k y) : ℂ) = (ofReal ∘ periodizedBernoulli k) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1)
h₁ : (↑(bernoulliFun k y) : ℂ) = (↑(periodizedBernoulli k (↑y : ℝ ⧸ AddSubgroup.zmultiples 1)) : ℂ)
h₂ : bernoulliFun k y = periodizedBernoulli k (↑y : ℝ ⧸ AddSubgroup.zmultiples 1)
h₃ : bernoulliFun k y = AddCircle.liftIco 1 0 (bernoulliFun k) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1)
h₄ h₅ : bernoulliFun k y = bernoulliFun k y
⊢ (↑(bernoulliFun k y) : ℂ) = (B : (a : AddCircle 1) → ℂ) (↑y : ℝ ⧸ AddSubgroup.zmultiples 1)

Tactic:
rw [ContinuousMap.coe_mk, Function.comp_apply, ofReal_inj, periodizedBernoulli,
      AddCircle.liftIco_coe_apply (show y ∈ Ico 0 (0 + 1) by rwa [zero_add])]

Premises used: periodizedBernoulli, ContinuousMap.coe_mk, Complex.ofReal_inj, Function.comp_apply, AddCircle.liftIco_coe_apply
-- Module: Mathlib.NumberTheory.ZetaValues
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) : ℂ) +
        HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑(-(↑n : ℤ)) : ℂ) k)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ) +
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑0 : ℂ) k)
        ((fourier 0 : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))

Tactic:
(hasSum_one_div_pow_mul_fourier_mul_bernoulliFun hk hx).nat_add_neg

Premises used: hasSum_one_div_pow_mul_fourier_mul_bernoulliFun, HasSum.nat_add_neg
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h :
  Eq (α := ℕ → ℂ)
    (fun (n : ℕ) ↦
      1 / HPow.hPow (α := ℂ) (↑n : ℂ) k *
        HAdd.hAdd (α := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          (HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (-1) k)
            ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)))
    fun (n : ℕ) ↦
    HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑(↑n : ℤ) : ℂ) k)
        ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) +
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑(-(↑n : ℤ)) : ℂ) k)
        ((fourier (-(↑n : ℤ)) : (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 / HPow.hPow (α := ℂ) (↑0 : ℂ) k)
        ((fourier 0 : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
⊢ HasSum
    (fun (n : ℕ) ↦
      1 / HPow.hPow (α := ℂ) (↑n : ℂ) k *
        HAdd.hAdd (α := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          (HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (-1) k)
            ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)))
    (-(2 * (↑π : ℂ) * I) ^ k / (↑k ! : ℂ) * (↑(bernoulliFun k x) : ℂ))

Tactic:
convert! (hasSum_one_div_pow_mul_fourier_mul_bernoulliFun hk hx).nat_add_neg using 1

Premises used: hasSum_one_div_pow_mul_fourier_mul_bernoulliFun, HasSum.nat_add_neg
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h :
  ∀ (n : ℕ),
    1 / HPow.hPow (α := ℂ) (↑n : ℂ) k *
        HAdd.hAdd (α := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          (HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (-1) k)
            ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)) =
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑(↑n : ℤ) : ℂ) k)
          ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) +
        HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑(-(↑n : ℤ)) : ℂ) k)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
⊢ Eq (α := ℕ → ℂ)
    (fun (n : ℕ) ↦
      1 / HPow.hPow (α := ℂ) (↑n : ℂ) k *
        HAdd.hAdd (α := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
          (HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (-1) k)
            ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)))
    fun (n : ℕ) ↦
    HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑(↑n : ℤ) : ℂ) k)
        ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) +
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑(-(↑n : ℤ)) : ℂ) k)
        ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)

Tactic:
ext1 n
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
h :
  HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) +
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k * HPow.hPow (α := ℂ) (-1) k)
        ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) =
    HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑(↑n : ℤ) : ℂ) k)
        ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) +
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (-(↑(↑n : ℤ) : ℂ)) k)
        ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
⊢ 1 / HPow.hPow (α := ℂ) (↑n : ℂ) k *
      HAdd.hAdd (α := ℂ) ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
        (HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (-1) k)
          ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)) =
    HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑(↑n : ℤ) : ℂ) k)
        ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) +
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑(-(↑n : ℤ)) : ℂ) k)
        ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)

Tactic:
rw [Int.cast_neg, mul_add, ← mul_assoc]

Premises used: Int.cast_neg, mul_assoc, mul_add
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
rw :
  HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑(↑n : ℤ) : ℂ) k)
      ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) +
    HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (-1) k / HPow.hPow (α := ℂ) (↑(↑n : ℤ) : ℂ) k)
      ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
| HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑(↑n : ℤ) : ℂ) k)
      ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) +
    HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (-(↑(↑n : ℤ) : ℂ)) k)
      ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)

Tactic:
rw [neg_eq_neg_one_mul, mul_pow, ← div_div]

Premises used: neg_eq_neg_one_mul, div_div, mul_pow
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
h :
  HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) +
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k * HPow.hPow (α := ℂ) (-1) k)
        ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) =
    HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑(↑n : ℤ) : ℂ) k)
        ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) +
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (-1) k / HPow.hPow (α := ℂ) (↑(↑n : ℤ) : ℂ) k)
        ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
⊢ HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) +
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k * HPow.hPow (α := ℂ) (-1) k)
        ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) =
    HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑(↑n : ℤ) : ℂ) k)
        ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) +
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (-(↑(↑n : ℤ) : ℂ)) k)
        ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)

Tactic:
conv_rhs => rw [neg_eq_neg_one_mul, mul_pow, ← div_div]

Premises used: neg_eq_neg_one_mul, div_div, mul_pow
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
h :
  1 / HPow.hPow (α := ℂ) (↑n : ℂ) k * HPow.hPow (α := ℂ) (-1) k =
    1 / HPow.hPow (α := ℂ) (-1) k / HPow.hPow (α := ℂ) (↑(↑n : ℤ) : ℂ) k
⊢ HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
        ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) +
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k * HPow.hPow (α := ℂ) (-1) k)
        ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) =
    HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (↑(↑n : ℤ) : ℂ) k)
        ((fourier (↑n : ℤ) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) +
      HMul.hMul (β := ℂ) (1 / HPow.hPow (α := ℂ) (-1) k / HPow.hPow (α := ℂ) (↑(↑n : ℤ) : ℂ) k)
        ((fourier (-(↑n : ℤ)) : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)

Tactic:
congr 2
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
h :
  HPow.hPow (α := ℂ) (-1) k / HPow.hPow (α := ℂ) (↑n : ℂ) k =
    1 / HPow.hPow (α := ℂ) (-1) k / HPow.hPow (α := ℂ) (↑(↑n : ℤ) : ℂ) k
⊢ 1 / HPow.hPow (α := ℂ) (↑n : ℂ) k * HPow.hPow (α := ℂ) (-1) k =
    1 / HPow.hPow (α := ℂ) (-1) k / HPow.hPow (α := ℂ) (↑(↑n : ℤ) : ℂ) k

Tactic:
rw [div_mul_eq_mul_div₀, one_mul]

Premises used: one_mul, div_mul_eq_mul_div₀
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
h : HPow.hPow (α := ℂ) (-1) k = 1 / HPow.hPow (α := ℂ) (-1) k
⊢ HPow.hPow (α := ℂ) (-1) k / HPow.hPow (α := ℂ) (↑n : ℂ) k =
    1 / HPow.hPow (α := ℂ) (-1) k / HPow.hPow (α := ℂ) (↑(↑n : ℤ) : ℂ) k

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
h : HPow.hPow (α := ℂ) (-1) k ≠ 0
⊢ HPow.hPow (α := ℂ) (-1) k = 1 / HPow.hPow (α := ℂ) (-1) k

Tactic:
rw [eq_div_iff, ← mul_pow, ← neg_eq_neg_one_mul, neg_neg, one_pow]

Premises used: one_pow, neg_neg, neg_eq_neg_one_mul, eq_div_iff, mul_pow
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
h : Ne (α := ℂ) (-1) 0
⊢ HPow.hPow (α := ℂ) (-1) k ≠ 0

Tactic:
apply pow_ne_zero

Premises used: pow_ne_zero
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
h : Ne (α := ℂ) 1 0
⊢ Ne (α := ℂ) (-1) 0

Tactic:
rw [neg_ne_zero]

Premises used: neg_ne_zero
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
⊢ Ne (α := ℂ) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
⊢ Ne (α := ℂ) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero