awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
n : ℤ
hn : n ≠ 0
pos : k = 1 → (↑1 : ℂ) = 1
⊢ (↑(if k = 1 then 1 else 0) : ℂ) = if k = 1 then 1 else 0
have neg : ¬k = 1 → (↑0 : ℂ) = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ fourierCoeffOn (a := 0) (b := 1) ⋯ (fun (x : ℝ) ↦ (↑((↑k : ℝ) * bernoulliFun (k - 1) x) : ℂ)) n =
    HMul.hMul (α := ℂ) (↑k : ℂ)
      (fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun (x : ℝ) ↦ (↑(bernoulliFun (k - 1) x) : ℂ)) n)
have e_a : fourierCoeffOn (a := 0) (b := 1) sorry (fun (x : ℝ) ↦ (↑(↑k : ℝ) : ℂ) * (↑(bernoulliFun (k - 1) x) : ℂ)) n =
  HMul.hMul (α := ℂ) (↑k : ℂ)
    (fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun (x : ℝ) ↦ (↑(bernoulliFun (k - 1) x) : ℂ)) n)
Tactic: simp_rw [ofReal_mul, ofReal_natCast, fourierCoeffOn.const_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
n : ℤ
hn : n ≠ 0
e_a :
  fourierCoeffOn (a := 0) (b := 1) ⋯ (fun (x : ℝ) ↦ (↑(↑k : ℝ) : ℂ) * (↑(bernoulliFun (k - 1) x) : ℂ)) n =
    HMul.hMul (α := ℂ) (↑k : ℂ)
      (fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun (x : ℝ) ↦ (↑(bernoulliFun (k - 1) x) : ℂ)) n)
⊢ fourierCoeffOn (a := 0) (b := 1) ⋯ (fun (x : ℝ) ↦ (↑((↑k : ℝ) * bernoulliFun (k - 1) x) : ℂ)) n =
    HMul.hMul (α := ℂ) (↑k : ℂ)
      (fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun (x : ℝ) ↦ (↑(bernoulliFun (k - 1) x) : ℂ)) n)
have e_a₁ : fourierCoeffOn (a := 0) (b := 1) sorry (fun (x : ℝ) ↦ (↑k : ℂ) * (↑(bernoulliFun (k - 1) x) : ℂ)) n =
  HMul.hMul (α := ℂ) (↑k : ℂ)
    (fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun (x : ℝ) ↦ (↑(bernoulliFun (k - 1) x) : ℂ)) n)
Tactic: simp_rw [ofReal_mul, ofReal_natCast, fourierCoeffOn.const_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
⊢ bernoulliFourierCoeff k 0 = 0
have simp_rw : Eq (α := ℂ) (fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun (x : ℝ) ↦ (↑(bernoulliFun k x) : ℂ)) 0) 0
Tactic: simp_rw [bernoulliFourierCoeff, fourierCoeffOn_eq_integral, neg_zero, fourier_zero, sub_zero,
    div_one, one_smul, intervalIntegral.integral_ofReal, integral_bernoulliFun_eq_zero hk,
    ofReal_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
simp_rw : Eq (α := ℂ) (fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun (x : ℝ) ↦ (↑(bernoulliFun k x) : ℂ)) 0) 0
⊢ bernoulliFourierCoeff k 0 = 0
have simp_rw₁ : HSMul.hSMul (β := ℂ) (1 / HSub.hSub (α := ℝ) 1 0)
    (∫ (x : ℝ) in 0..1,
      HSMul.hSMul (α := ℂ) ((fourier (-0) : (a : AddCircle (1 - 0)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (1 - 0)) : ℂ)
        (↑(bernoulliFun k x) : ℂ)) =
  0
Tactic: simp_rw [bernoulliFourierCoeff, fourierCoeffOn_eq_integral, neg_zero, fourier_zero, sub_zero,
    div_one, one_smul, intervalIntegral.integral_ofReal, integral_bernoulliFun_eq_zero hk,
    ofReal_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
simp_rw : Eq (α := ℂ) (fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun (x : ℝ) ↦ (↑(bernoulliFun k x) : ℂ)) 0) 0
simp_rw₁ :
  HSMul.hSMul (β := ℂ) (1 / HSub.hSub (α := ℝ) 1 0)
      (∫ (x : ℝ) in 0..1,
        HSMul.hSMul (α := ℂ)
          ((fourier (-0) : (a : AddCircle (1 - 0)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (1 - 0)) : ℂ)
          (↑(bernoulliFun k x) : ℂ)) =
    0
⊢ bernoulliFourierCoeff k 0 = 0
have simp_rw₂ : HSMul.hSMul (β := ℂ) (1 / HSub.hSub (α := ℝ) 1 0)
    (∫ (x : ℝ) in 0..1,
      HSMul.hSMul (α := ℂ) ((fourier 0 : (a : AddCircle (1 - 0)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (1 - 0)) : ℂ)
        (↑(bernoulliFun k x) : ℂ)) =
  0
Tactic: simp_rw [bernoulliFourierCoeff, fourierCoeffOn_eq_integral, neg_zero, fourier_zero, sub_zero,
    div_one, one_smul, intervalIntegral.integral_ofReal, integral_bernoulliFun_eq_zero hk,
    ofReal_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
simp_rw : Eq (α := ℂ) (fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun (x : ℝ) ↦ (↑(bernoulliFun k x) : ℂ)) 0) 0
simp_rw₁ :
  HSMul.hSMul (β := ℂ) (1 / HSub.hSub (α := ℝ) 1 0)
      (∫ (x : ℝ) in 0..1,
        HSMul.hSMul (α := ℂ)
          ((fourier (-0) : (a : AddCircle (1 - 0)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (1 - 0)) : ℂ)
          (↑(bernoulliFun k x) : ℂ)) =
    0
simp_rw₂ :
  HSMul.hSMul (β := ℂ) (1 / HSub.hSub (α := ℝ) 1 0)
      (∫ (x : ℝ) in 0..1,
        HSMul.hSMul (α := ℂ) ((fourier 0 : (a : AddCircle (1 - 0)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (1 - 0)) : ℂ)
          (↑(bernoulliFun k x) : ℂ)) =
    0
⊢ bernoulliFourierCoeff k 0 = 0
have simp_rw₃ : HSMul.hSMul (β := ℂ) (1 / HSub.hSub (α := ℝ) 1 0)
    (∫ (x : ℝ) in 0..1, HSMul.hSMul (α := ℂ) 1 (↑(bernoulliFun k x) : ℂ)) =
  0
Tactic: simp_rw [bernoulliFourierCoeff, fourierCoeffOn_eq_integral, neg_zero, fourier_zero, sub_zero,
    div_one, one_smul, intervalIntegral.integral_ofReal, integral_bernoulliFun_eq_zero hk,
    ofReal_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
simp_rw : Eq (α := ℂ) (fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun (x : ℝ) ↦ (↑(bernoulliFun k x) : ℂ)) 0) 0
simp_rw₁ :
  HSMul.hSMul (β := ℂ) (1 / HSub.hSub (α := ℝ) 1 0)
      (∫ (x : ℝ) in 0..1,
        HSMul.hSMul (α := ℂ)
          ((fourier (-0) : (a : AddCircle (1 - 0)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (1 - 0)) : ℂ)
          (↑(bernoulliFun k x) : ℂ)) =
    0
simp_rw₂ :
  HSMul.hSMul (β := ℂ) (1 / HSub.hSub (α := ℝ) 1 0)
      (∫ (x : ℝ) in 0..1,
        HSMul.hSMul (α := ℂ) ((fourier 0 : (a : AddCircle (1 - 0)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (1 - 0)) : ℂ)
          (↑(bernoulliFun k x) : ℂ)) =
    0
simp_rw₃ :
  HSMul.hSMul (β := ℂ) (1 / HSub.hSub (α := ℝ) 1 0)
      (∫ (x : ℝ) in 0..1, HSMul.hSMul (α := ℂ) 1 (↑(bernoulliFun k x) : ℂ)) =
    0
⊢ bernoulliFourierCoeff k 0 = 0
have simp_rw₄ : HSMul.hSMul (β := ℂ) (1 / 1) (∫ (x : ℝ) in 0..1, HSMul.hSMul (α := ℂ) 1 (↑(bernoulliFun k x) : ℂ)) = 0
Tactic: simp_rw [bernoulliFourierCoeff, fourierCoeffOn_eq_integral, neg_zero, fourier_zero, sub_zero,
    div_one, one_smul, intervalIntegral.integral_ofReal, integral_bernoulliFun_eq_zero hk,
    ofReal_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
simp_rw : Eq (α := ℂ) (fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun (x : ℝ) ↦ (↑(bernoulliFun k x) : ℂ)) 0) 0
simp_rw₁ :
  HSMul.hSMul (β := ℂ) (1 / HSub.hSub (α := ℝ) 1 0)
      (∫ (x : ℝ) in 0..1,
        HSMul.hSMul (α := ℂ)
          ((fourier (-0) : (a : AddCircle (1 - 0)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (1 - 0)) : ℂ)
          (↑(bernoulliFun k x) : ℂ)) =
    0
simp_rw₂ :
  HSMul.hSMul (β := ℂ) (1 / HSub.hSub (α := ℝ) 1 0)
      (∫ (x : ℝ) in 0..1,
        HSMul.hSMul (α := ℂ) ((fourier 0 : (a : AddCircle (1 - 0)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (1 - 0)) : ℂ)
          (↑(bernoulliFun k x) : ℂ)) =
    0
simp_rw₃ :
  HSMul.hSMul (β := ℂ) (1 / HSub.hSub (α := ℝ) 1 0)
      (∫ (x : ℝ) in 0..1, HSMul.hSMul (α := ℂ) 1 (↑(bernoulliFun k x) : ℂ)) =
    0
simp_rw₄ : HSMul.hSMul (β := ℂ) (1 / 1) (∫ (x : ℝ) in 0..1, HSMul.hSMul (α := ℂ) 1 (↑(bernoulliFun k x) : ℂ)) = 0
⊢ bernoulliFourierCoeff k 0 = 0
have simp_rw₅ : HSMul.hSMul (α := ℝ) (β := ℂ) 1 (∫ (x : ℝ) in 0..1, HSMul.hSMul (α := ℂ) 1 (↑(bernoulliFun k x) : ℂ)) = 0
Tactic: simp_rw [bernoulliFourierCoeff, fourierCoeffOn_eq_integral, neg_zero, fourier_zero, sub_zero,
    div_one, one_smul, intervalIntegral.integral_ofReal, integral_bernoulliFun_eq_zero hk,
    ofReal_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
simp_rw : Eq (α := ℂ) (fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun (x : ℝ) ↦ (↑(bernoulliFun k x) : ℂ)) 0) 0
simp_rw₁ :
  HSMul.hSMul (β := ℂ) (1 / HSub.hSub (α := ℝ) 1 0)
      (∫ (x : ℝ) in 0..1,
        HSMul.hSMul (α := ℂ)
          ((fourier (-0) : (a : AddCircle (1 - 0)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (1 - 0)) : ℂ)
          (↑(bernoulliFun k x) : ℂ)) =
    0
simp_rw₂ :
  HSMul.hSMul (β := ℂ) (1 / HSub.hSub (α := ℝ) 1 0)
      (∫ (x : ℝ) in 0..1,
        HSMul.hSMul (α := ℂ) ((fourier 0 : (a : AddCircle (1 - 0)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (1 - 0)) : ℂ)
          (↑(bernoulliFun k x) : ℂ)) =
    0
simp_rw₃ :
  HSMul.hSMul (β := ℂ) (1 / HSub.hSub (α := ℝ) 1 0)
      (∫ (x : ℝ) in 0..1, HSMul.hSMul (α := ℂ) 1 (↑(bernoulliFun k x) : ℂ)) =
    0
simp_rw₄ : HSMul.hSMul (β := ℂ) (1 / 1) (∫ (x : ℝ) in 0..1, HSMul.hSMul (α := ℂ) 1 (↑(bernoulliFun k x) : ℂ)) = 0
simp_rw₅ : HSMul.hSMul (α := ℝ) (β := ℂ) 1 (∫ (x : ℝ) in 0..1, HSMul.hSMul (α := ℂ) 1 (↑(bernoulliFun k x) : ℂ)) = 0
⊢ bernoulliFourierCoeff k 0 = 0
have simp_rw₆ : Eq (α := ℂ) (∫ (x : ℝ) in 0..1, (↑(bernoulliFun k x) : ℂ)) 0
Tactic: simp_rw [bernoulliFourierCoeff, fourierCoeffOn_eq_integral, neg_zero, fourier_zero, sub_zero,
    div_one, one_smul, intervalIntegral.integral_ofReal, integral_bernoulliFun_eq_zero hk,
    ofReal_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
simp_rw : Eq (α := ℂ) (fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun (x : ℝ) ↦ (↑(bernoulliFun k x) : ℂ)) 0) 0
simp_rw₁ :
  HSMul.hSMul (β := ℂ) (1 / HSub.hSub (α := ℝ) 1 0)
      (∫ (x : ℝ) in 0..1,
        HSMul.hSMul (α := ℂ)
          ((fourier (-0) : (a : AddCircle (1 - 0)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (1 - 0)) : ℂ)
          (↑(bernoulliFun k x) : ℂ)) =
    0
simp_rw₂ :
  HSMul.hSMul (β := ℂ) (1 / HSub.hSub (α := ℝ) 1 0)
      (∫ (x : ℝ) in 0..1,
        HSMul.hSMul (α := ℂ) ((fourier 0 : (a : AddCircle (1 - 0)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (1 - 0)) : ℂ)
          (↑(bernoulliFun k x) : ℂ)) =
    0
simp_rw₃ :
  HSMul.hSMul (β := ℂ) (1 / HSub.hSub (α := ℝ) 1 0)
      (∫ (x : ℝ) in 0..1, HSMul.hSMul (α := ℂ) 1 (↑(bernoulliFun k x) : ℂ)) =
    0
simp_rw₄ : HSMul.hSMul (β := ℂ) (1 / 1) (∫ (x : ℝ) in 0..1, HSMul.hSMul (α := ℂ) 1 (↑(bernoulliFun k x) : ℂ)) = 0
simp_rw₅ : HSMul.hSMul (α := ℝ) (β := ℂ) 1 (∫ (x : ℝ) in 0..1, HSMul.hSMul (α := ℂ) 1 (↑(bernoulliFun k x) : ℂ)) = 0
simp_rw₆ : Eq (α := ℂ) (∫ (x : ℝ) in 0..1, (↑(bernoulliFun k x) : ℂ)) 0
⊢ bernoulliFourierCoeff k 0 = 0
have simp_rw₇ : (↑(∫ (x : ℝ) in 0..1, bernoulliFun k x) : ℂ) = 0
Tactic: simp_rw [bernoulliFourierCoeff, fourierCoeffOn_eq_integral, neg_zero, fourier_zero, sub_zero,
    div_one, one_smul, intervalIntegral.integral_ofReal, integral_bernoulliFun_eq_zero hk,
    ofReal_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
simp_rw : Eq (α := ℂ) (fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun (x : ℝ) ↦ (↑(bernoulliFun k x) : ℂ)) 0) 0
simp_rw₁ :
  HSMul.hSMul (β := ℂ) (1 / HSub.hSub (α := ℝ) 1 0)
      (∫ (x : ℝ) in 0..1,
        HSMul.hSMul (α := ℂ)
          ((fourier (-0) : (a : AddCircle (1 - 0)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (1 - 0)) : ℂ)
          (↑(bernoulliFun k x) : ℂ)) =
    0
simp_rw₂ :
  HSMul.hSMul (β := ℂ) (1 / HSub.hSub (α := ℝ) 1 0)
      (∫ (x : ℝ) in 0..1,
        HSMul.hSMul (α := ℂ) ((fourier 0 : (a : AddCircle (1 - 0)) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples (1 - 0)) : ℂ)
          (↑(bernoulliFun k x) : ℂ)) =
    0
simp_rw₃ :
  HSMul.hSMul (β := ℂ) (1 / HSub.hSub (α := ℝ) 1 0)
      (∫ (x : ℝ) in 0..1, HSMul.hSMul (α := ℂ) 1 (↑(bernoulliFun k x) : ℂ)) =
    0
simp_rw₄ : HSMul.hSMul (β := ℂ) (1 / 1) (∫ (x : ℝ) in 0..1, HSMul.hSMul (α := ℂ) 1 (↑(bernoulliFun k x) : ℂ)) = 0
simp_rw₅ : HSMul.hSMul (α := ℝ) (β := ℂ) 1 (∫ (x : ℝ) in 0..1, HSMul.hSMul (α := ℂ) 1 (↑(bernoulliFun k x) : ℂ)) = 0
simp_rw₆ : Eq (α := ℂ) (∫ (x : ℝ) in 0..1, (↑(bernoulliFun k x) : ℂ)) 0
simp_rw₇ : (↑(∫ (x : ℝ) in 0..1, bernoulliFun k x) : ℂ) = 0
⊢ bernoulliFourierCoeff k 0 = 0
have simp_rw₈ : (↑0 : ℂ) = 0
Tactic: simp_rw [bernoulliFourierCoeff, fourierCoeffOn_eq_integral, neg_zero, fourier_zero, sub_zero,
    div_one, one_smul, intervalIntegral.integral_ofReal, integral_bernoulliFun_eq_zero hk,
    ofReal_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
⊢ bernoulliFourierCoeff k n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
have inl : bernoulliFourierCoeff k 0 = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑0 : ℂ)) ^ k
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
inl : bernoulliFourierCoeff k 0 = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑0 : ℂ)) ^ k
⊢ bernoulliFourierCoeff k n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
have inr : ∀ (hn : n ≠ 0), bernoulliFourierCoeff k n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
⊢ bernoulliFourierCoeff k 0 = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑0 : ℂ)) ^ k
have inl : 0 = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑0 : ℂ)) ^ k
Tactic: rw [bernoulliFourierCoeff_zero hk, Int.cast_zero, mul_zero, zero_pow hk,
      div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
inl : 0 = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑0 : ℂ)) ^ k
⊢ bernoulliFourierCoeff k 0 = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑0 : ℂ)) ^ k
have inl₁ : 0 = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * 0) ^ k
Tactic: rw [bernoulliFourierCoeff_zero hk, Int.cast_zero, mul_zero, zero_pow hk,
      div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
inl : 0 = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑0 : ℂ)) ^ k
inl₁ : 0 = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * 0) ^ k
⊢ bernoulliFourierCoeff k 0 = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑0 : ℂ)) ^ k
have inl₂ : 0 = -(↑k ! : ℂ) / HPow.hPow (α := ℂ) 0 k
Tactic: rw [bernoulliFourierCoeff_zero hk, Int.cast_zero, mul_zero, zero_pow hk,
      div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
inl : 0 = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑0 : ℂ)) ^ k
inl₁ : 0 = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * 0) ^ k
inl₂ : 0 = -(↑k ! : ℂ) / HPow.hPow (α := ℂ) 0 k
⊢ bernoulliFourierCoeff k 0 = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑0 : ℂ)) ^ k
have inl₃ : 0 = HDiv.hDiv (α := ℂ) (-(↑k ! : ℂ)) 0
Tactic: rw [bernoulliFourierCoeff_zero hk, Int.cast_zero, mul_zero, zero_pow hk,
      div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
inl : 0 = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑0 : ℂ)) ^ k
inl₁ : 0 = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * 0) ^ k
inl₂ : 0 = -(↑k ! : ℂ) / HPow.hPow (α := ℂ) 0 k
inl₃ : 0 = HDiv.hDiv (α := ℂ) (-(↑k ! : ℂ)) 0
⊢ bernoulliFourierCoeff k 0 = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑0 : ℂ)) ^ k
have inl₄ : Eq (α := ℂ) 0 0
Tactic: rw [bernoulliFourierCoeff_zero hk, Int.cast_zero, mul_zero, zero_pow hk,
      div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff k n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
have inr : bernoulliFourierCoeff 1 n = -(↑1! : ℂ) / HPow.hPow (β := ℕ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) 1
Tactic: refine Nat.le_induction ?_ (fun k hk h'k => ?_) k (Nat.one_le_iff_ne_zero.mpr hk)
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
inr : bernoulliFourierCoeff 1 n = -(↑1! : ℂ) / HPow.hPow (β := ℕ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) 1
⊢ bernoulliFourierCoeff k n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
have inr₁ : ∀ (k : ℕ) (hk : 1 ≤ k) (h'k : bernoulliFourierCoeff k n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k),
  bernoulliFourierCoeff (k + 1) n = -(↑(k + 1)! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ (k + 1)
Tactic: refine Nat.le_induction ?_ (fun k hk h'k => ?_) k (Nat.one_le_iff_ne_zero.mpr hk)
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff 1 n = -(↑1! : ℂ) / HPow.hPow (β := ℕ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) 1
have inr : 1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
    ((if Eq (α := ℕ) 1 1 then 1 else 0) - (↑1 : ℂ) * bernoulliFourierCoeff (HSub.hSub (α := ℕ) 1 1) n) =
  -(↑1! : ℂ) / HPow.hPow (β := ℕ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) 1
Tactic: rw [bernoulliFourierCoeff_recurrence 1 hn]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      ((if Eq (α := ℕ) 1 1 then 1 else 0) - (↑1 : ℂ) * bernoulliFourierCoeff (HSub.hSub (α := ℕ) 1 1) n) =
    -(↑1! : ℂ) / HPow.hPow (β := ℕ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) 1
have inr : 1 / -(2 * (↑π : ℂ) * I * (↑n : ℂ)) * (1 - bernoulliFourierCoeff 0 n) = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
Tactic: simp only [Nat.cast_one, tsub_self, neg_mul, one_mul, if_true,
      Nat.factorial_one, pow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 / -(2 * (↑π : ℂ) * I * (↑n : ℂ)) * (1 - bernoulliFourierCoeff 0 n) = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
have inr : 1 / -(2 * (↑π : ℂ) * I * (↑n : ℂ)) * HSub.hSub (α := ℂ) 1 0 = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
Tactic: rw [bernoulli_zero_fourier_coeff hn, sub_zero, mul_one, div_neg, neg_div]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
inr : 1 / -(2 * (↑π : ℂ) * I * (↑n : ℂ)) * HSub.hSub (α := ℂ) 1 0 = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
⊢ 1 / -(2 * (↑π : ℂ) * I * (↑n : ℂ)) * (1 - bernoulliFourierCoeff 0 n) = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
have inr₁ : 1 / -(2 * (↑π : ℂ) * I * (↑n : ℂ)) * 1 = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
Tactic: rw [bernoulli_zero_fourier_coeff hn, sub_zero, mul_one, div_neg, neg_div]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
inr : 1 / -(2 * (↑π : ℂ) * I * (↑n : ℂ)) * HSub.hSub (α := ℂ) 1 0 = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
inr₁ : 1 / -(2 * (↑π : ℂ) * I * (↑n : ℂ)) * 1 = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
⊢ 1 / -(2 * (↑π : ℂ) * I * (↑n : ℂ)) * (1 - bernoulliFourierCoeff 0 n) = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
have inr₂ : 1 / -(2 * (↑π : ℂ) * I * (↑n : ℂ)) = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
Tactic: rw [bernoulli_zero_fourier_coeff hn, sub_zero, mul_one, div_neg, neg_div]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
inr : 1 / -(2 * (↑π : ℂ) * I * (↑n : ℂ)) * HSub.hSub (α := ℂ) 1 0 = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
inr₁ : 1 / -(2 * (↑π : ℂ) * I * (↑n : ℂ)) * 1 = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
inr₂ : 1 / -(2 * (↑π : ℂ) * I * (↑n : ℂ)) = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
⊢ 1 / -(2 * (↑π : ℂ) * I * (↑n : ℂ)) * (1 - bernoulliFourierCoeff 0 n) = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
have inr₃ : -(1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))) = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
Tactic: rw [bernoulli_zero_fourier_coeff hn, sub_zero, mul_one, div_neg, neg_div]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
inr : 1 / -(2 * (↑π : ℂ) * I * (↑n : ℂ)) * HSub.hSub (α := ℂ) 1 0 = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
inr₁ : 1 / -(2 * (↑π : ℂ) * I * (↑n : ℂ)) * 1 = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
inr₂ : 1 / -(2 * (↑π : ℂ) * I * (↑n : ℂ)) = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
inr₃ : -(1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))) = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
⊢ 1 / -(2 * (↑π : ℂ) * I * (↑n : ℂ)) * (1 - bernoulliFourierCoeff 0 n) = -1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))
have inr₄ : -(1 / (2 * (↑π : ℂ) * I * (↑n : ℂ))) = -(1 / (2 * (↑π : ℂ) * I * (↑n : ℂ)))
Tactic: rw [bernoulli_zero_fourier_coeff hn, sub_zero, mul_one, div_neg, neg_div]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k_1 : ℕ
hk_1 : k_1 ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
⊢ bernoulliFourierCoeff (k + 1) n = -(↑(k + 1)! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ (k + 1)
have inr : 1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) * -((↑(k + 1) : ℂ) * (-(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k)) =
  -HMul.hMul (α := ℂ) (↑(k + 1) : ℂ) (↑k ! : ℂ) /
    ((2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k * HPow.hPow (β := ℕ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) 1)
Tactic: rw [bernoulliFourierCoeff_recurrence (k + 1) hn, if_neg (by grind), Nat.add_sub_cancel k 1, h'k,
      Nat.factorial_succ, zero_sub, Nat.cast_mul, pow_add]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
⊢ ofReal ∘ periodizedBernoulli k = AddCircle.liftIco 1 0 (ofReal ∘ bernoulliFun k)
have h : ∀ (x : 𝕌), (ofReal ∘ periodizedBernoulli k) x = AddCircle.liftIco 1 0 (ofReal ∘ bernoulliFun k) x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (hypothesis)
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
⊢ fourierCoeff (ofReal ∘ periodizedBernoulli k) n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
have this : ofReal ∘ periodizedBernoulli k = AddCircle.liftIco 1 0 (ofReal ∘ bernoulliFun k)
Tactic: have : ((↑) ∘ periodizedBernoulli k : 𝕌 → ℂ) = AddCircle.liftIco 1 0 ((↑) ∘ bernoulliFun k) := by
    ext1 x; rfl
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
n : ℤ
this : ofReal ∘ periodizedBernoulli k = AddCircle.liftIco 1 0 (ofReal ∘ bernoulliFun k)
⊢ fourierCoeff (ofReal ∘ periodizedBernoulli k) n = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
have rw : fourierCoeffOn (a := 0) (b := HAdd.hAdd (α := ℝ) 0 1) sorry (ofReal ∘ bernoulliFun k) n =
  -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
Tactic: rw [this, fourierCoeff_liftIco_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : 2 ≤ k
n : ℤ
⊢ -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k =
    -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
have rw : -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k / HPow.hPow (α := ℂ) (↑n : ℂ) k
Tactic: rw [mul_one_div, div_div, ← mul_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : 2 ≤ k
n : ℤ
rw :
  -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k / HPow.hPow (α := ℂ) (↑n : ℂ) k
⊢ -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k =
    -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
have rw₁ : -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k = -(↑k ! : ℂ) / ((2 * (↑π : ℂ) * I) ^ k * HPow.hPow (α := ℂ) (↑n : ℂ) k)
Tactic: rw [mul_one_div, div_div, ← mul_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : 2 ≤ k
n : ℤ
rw :
  -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k / HPow.hPow (α := ℂ) (↑n : ℂ) k
rw₁ :
  -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k =
    -(↑k ! : ℂ) / ((2 * (↑π : ℂ) * I) ^ k * HPow.hPow (α := ℂ) (↑n : ℂ) k)
⊢ -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k =
    -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
have rw₂ : -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k = -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
Tactic: rw [mul_one_div, div_div, ← mul_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (hypothesis)
Goal:
k : ℕ
hk : 2 ≤ k
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k
have this : ∀ (n : ℤ),
  -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I * (↑n : ℂ)) ^ k =
    -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
Tactic: have :
      ∀ n : ℤ, -(k ! : ℂ) / (2 * π * I * n) ^ k = -k ! / (2 * π * I) ^ k * (1 / (n : ℂ) ^ k) := by
    intro n; rw [mul_one_div, div_div, ← mul_pow]
-- 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 * (↑n : ℂ)) ^ k
have simp_rw : Summable (α := ℂ) fun (n : ℤ) ↦ -(↑k ! : ℂ) / (2 * (↑π : ℂ) * I) ^ k * (1 / HPow.hPow (α := ℂ) (↑n : ℂ) k)
Tactic: simp_rw [this]