awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : Ne (α := ℝ) (↑m : ℝ) 0
f : (k : ℕ) → (x : ℝ) → ℝ :=
  fun (k : ℕ) (x : ℝ) ↦
    bernoulliFun k ((↑m : ℝ) * x) -
      HPow.hPow (α := ℝ) (↑m : ℝ) k / (↑m : ℝ) *
        ∑ i ∈ Finset.range m, bernoulliFun k (x + HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑m : ℝ))
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ Eq (α := ℝ)
    (∫ (x : ℝ) in HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑m : ℝ)..HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑m : ℝ), bernoulliFun (k + 1) x) 0

Tactic:
simp [div_self m0', integral_bernoulliFun_eq_zero]

Premises used: integral_bernoulliFun_eq_zero, div_self
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : Ne (α := ℝ) (↑m : ℝ) 0
f : (k : ℕ) → (x : ℝ) → ℝ :=
  fun (k : ℕ) (x : ℝ) ↦
    bernoulliFun k ((↑m : ℝ) * x) -
      HPow.hPow (α := ℝ) (↑m : ℝ) k / (↑m : ℝ) *
        ∑ i ∈ Finset.range m, bernoulliFun k (x + HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑m : ℝ))
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
k_1 : ℕ
h_1 : k_1 < m
⊢ Continuous (bernoulliFun (k + 1))

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : Ne (α := ℝ) (↑m : ℝ) 0
f : (k : ℕ) → (x : ℝ) → ℝ :=
  fun (k : ℕ) (x : ℝ) ↦
    bernoulliFun k ((↑m : ℝ) * x) -
      HPow.hPow (α := ℝ) (↑m : ℝ) k / (↑m : ℝ) *
        ∑ i ∈ Finset.range m, bernoulliFun k (x + HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑m : ℝ))
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
k_1 : ℕ
h_1 : k_1 < m
⊢ IntervalIntegrable (bernoulliFun (k + 1)) volume (HDiv.hDiv (α := ℝ) (↑k_1 : ℝ) (↑m : ℝ))
    (HDiv.hDiv (α := ℝ) (↑(k_1 + 1) : ℝ) (↑m : ℝ))

Tactic:
exact Continuous.intervalIntegrable (by fun_prop) _ _

Premises used: Continuous.intervalIntegrable
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : Ne (α := ℝ) (↑m : ℝ) 0
f : (k : ℕ) → (x : ℝ) → ℝ :=
  fun (k : ℕ) (x : ℝ) ↦
    bernoulliFun k ((↑m : ℝ) * x) -
      HPow.hPow (α := ℝ) (↑m : ℝ) k / (↑m : ℝ) *
        ∑ i ∈ Finset.range m, bernoulliFun k (x + HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑m : ℝ))
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
i : ℕ
h_1 : i ∈ Finset.range m
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ bernoulliFun (k + 1) (x + HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑m : ℝ))

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : Ne (α := ℝ) (↑m : ℝ) 0
f : (k : ℕ) → (x : ℝ) → ℝ :=
  fun (k : ℕ) (x : ℝ) ↦
    bernoulliFun k ((↑m : ℝ) * x) -
      HPow.hPow (α := ℝ) (↑m : ℝ) k / (↑m : ℝ) *
        ∑ i ∈ Finset.range m, bernoulliFun k (x + HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑m : ℝ))
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
i : ℕ
h_1 : i ∈ Finset.range m
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ bernoulliFun (k + 1) (x + HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑m : ℝ))) volume 0
    (↑m : ℝ)⁻¹

Tactic:
exact Continuous.intervalIntegrable (by fun_prop) _ _

Premises used: Continuous.intervalIntegrable
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : Ne (α := ℝ) (↑m : ℝ) 0
f : (k : ℕ) → (x : ℝ) → ℝ :=
  fun (k : ℕ) (x : ℝ) ↦
    bernoulliFun k ((↑m : ℝ) * x) -
      HPow.hPow (α := ℝ) (↑m : ℝ) k / (↑m : ℝ) *
        ∑ i ∈ Finset.range m, bernoulliFun k (x + HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑m : ℝ))
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ bernoulliFun (k + 1) ((↑m : ℝ) * x)

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : Ne (α := ℝ) (↑m : ℝ) 0
f : (k : ℕ) → (x : ℝ) → ℝ :=
  fun (k : ℕ) (x : ℝ) ↦
    bernoulliFun k ((↑m : ℝ) * x) -
      HPow.hPow (α := ℝ) (↑m : ℝ) k / (↑m : ℝ) *
        ∑ i ∈ Finset.range m, bernoulliFun k (x + HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑m : ℝ))
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ bernoulliFun (k + 1) ((↑m : ℝ) * x)) volume 0 (↑m : ℝ)⁻¹

Tactic:
exact Continuous.intervalIntegrable (by fun_prop) _ _

Premises used: Continuous.intervalIntegrable
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : Ne (α := ℝ) (↑m : ℝ) 0
f : (k : ℕ) → (x : ℝ) → ℝ :=
  fun (k : ℕ) (x : ℝ) ↦
    bernoulliFun k ((↑m : ℝ) * x) -
      HPow.hPow (α := ℝ) (↑m : ℝ) k / (↑m : ℝ) *
        ∑ i ∈ Finset.range m, bernoulliFun k (x + HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑m : ℝ))
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦
    HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1) / (↑m : ℝ) *
      ∑ i ∈ Finset.range m, bernoulliFun (k + 1) (x + HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑m : ℝ))

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : Ne (α := ℝ) (↑m : ℝ) 0
f : (k : ℕ) → (x : ℝ) → ℝ :=
  fun (k : ℕ) (x : ℝ) ↦
    bernoulliFun k ((↑m : ℝ) * x) -
      HPow.hPow (α := ℝ) (↑m : ℝ) k / (↑m : ℝ) *
        ∑ i ∈ Finset.range m, bernoulliFun k (x + HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑m : ℝ))
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ IntervalIntegrable (ε := ℝ)
    (fun (x : ℝ) ↦
      HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1) / (↑m : ℝ) *
        ∑ i ∈ Finset.range m, bernoulliFun (k + 1) (x + HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑m : ℝ)))
    volume 0 (↑m : ℝ)⁻¹

Tactic:
exact Continuous.intervalIntegrable (by fun_prop) _ _

Premises used: Continuous.intervalIntegrable
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : Ne (α := ℝ) (↑m : ℝ) 0
f : (k : ℕ) → (x : ℝ) → ℝ :=
  fun (k : ℕ) (x : ℝ) ↦
    bernoulliFun k ((↑m : ℝ) * x) -
      HPow.hPow (α := ℝ) (↑m : ℝ) k / (↑m : ℝ) *
        ∑ i ∈ Finset.range m, bernoulliFun k (x + HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑m : ℝ))
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..(↑m : ℝ)⁻¹, f (k + 1) x) 0

Tactic:
have i : ∫ x in (0 : ℝ)..m⁻¹, f (k + 1) x = 0 := by
      simp only [f]
      rw [intervalIntegral.integral_sub, intervalIntegral.integral_comp_mul_left _ m0', mul_zero,
        mul_inv_cancel₀ m0', integral_bernoulliFun_eq_zero (by lia), smul_zero, sub_eq_zero,
        intervalIntegral.integral_const_mul, eq_comm (a := 0), mul_eq_zero]
      · right
        rw [intervalIntegral.integral_finsetSum]
        · simp only [intervalIntegral.integral_comp_add_right, zero_add, ← one_div, ← add_div,
            add_comm (1 : ℝ), ← Nat.cast_add_one]
          rw [intervalIntegral.sum_integral_adjacent_intervals]
          · simp [div_self m0', integral_bernoulliFun_eq_zero]
          · intros; exact Continuous.intervalIntegrable (by fun_prop) _ _
        · intros; exact Continuous.intervalIntegrable (by fun_prop) _ _
      · exact Continuous.intervalIntegrable (by fun_prop) _ _
      · exact Continuous.intervalIntegrable (by fun_prop) _ _
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : Ne (α := ℝ) (↑m : ℝ) 0
f : (k : ℕ) → (x : ℝ) → ℝ :=
  fun (k : ℕ) (x : ℝ) ↦
    bernoulliFun k ((↑m : ℝ) * x) -
      HPow.hPow (α := ℝ) (↑m : ℝ) k / (↑m : ℝ) *
        ∑ i ∈ Finset.range m, bernoulliFun k (x + HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑m : ℝ))
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
i : Eq (α := ℝ) (∫ (x : ℝ) in 0..(↑m : ℝ)⁻¹, f (k + 1) x) 0
⊢ c = 0

Tactic:
simp only [fc, intervalIntegral.integral_const, sub_zero, smul_eq_mul, mul_eq_zero, inv_eq_zero,
      Nat.cast_eq_zero, m0, false_or] at i

Premises used: inv_eq_zero, sub_zero, false_or, mul_eq_zero, Nat.cast_eq_zero, smul_eq_mul, intervalIntegral.integral_const
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : Ne (α := ℝ) (↑m : ℝ) 0
f : (k : ℕ) → (x : ℝ) → ℝ :=
  fun (k : ℕ) (x : ℝ) ↦
    bernoulliFun k ((↑m : ℝ) * x) -
      HPow.hPow (α := ℝ) (↑m : ℝ) k / (↑m : ℝ) *
        ∑ i ∈ Finset.range m, bernoulliFun k (x + HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑m : ℝ))
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
i : c = 0
⊢ ∀ (x : ℝ), f (k + 1) x = 0

Tactic:
simpa only [i] using fc
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : Ne (α := ℝ) (↑m : ℝ) 0
f : (k : ℕ) → (x : ℝ) → ℝ :=
  fun (k : ℕ) (x : ℝ) ↦
    bernoulliFun k ((↑m : ℝ) * x) -
      HPow.hPow (α := ℝ) (↑m : ℝ) k / (↑m : ℝ) *
        ∑ i ∈ Finset.range m, bernoulliFun k (x + HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑m : ℝ))
zero : ∀ (x : ℝ), f 0 x = 0
succ : ∀ (k : ℕ) (h : ∀ (x : ℝ), f k x = 0) (x : ℝ), f (k + 1) x = 0
⊢ ∀ (x : ℝ), f k x = 0

Tactic:
induction k with
  | zero =>
    intro x
    simp only [f, bernoulliFun_zero, pow_zero, one_div, Finset.sum_const, Finset.card_range,
      nsmul_eq_mul, mul_one, sub_eq_zero]
    rw [inv_mul_cancel₀ (Nat.cast_ne_zero.mpr m0)]
  | succ k h =>
    have d (x) : HasDerivAt (f (k + 1)) (m * (k + 1) * f k x) x := by
      simp only [f, mul_sub, Finset.mul_sum, pow_succ, mul_div_cancel_right₀ _ m0',
        ← mul_assoc, mul_comm _ (_ / _), div_mul_cancel₀ _ m0']
      apply HasDerivAt.sub
      · rw [mul_assoc, mul_comm (m : ℝ) _, ← Nat.cast_add_one]
        exact (hasDerivAt_bernoulliFun _ _).comp _ (hasDerivAt_const_mul ..)
      · refine HasDerivAt.fun_sum fun i _ ↦ ?_
        simp only [mul_assoc, ← Nat.cast_add_one]
        apply HasDerivAt.const_mul
        rw [← mul_one (_ * _)]
        exact (hasDerivAt_bernoulliFun _ _).comp _ ((hasDerivAt_id' _).add_const _)
    simp only [h, mul_zero] at d
    have fc (x) : f (k + 1) x = f (k + 1) 0 :=
      is_const_of_deriv_eq_zero (fun _ ↦ (d _).differentiableAt) (fun _ ↦ (d _).deriv) x 0
    generalize f (k + 1) 0 = c at fc
    have i : ∫ x in (0 : ℝ)..m⁻¹, f (k + 1) x = 0 := by
      simp only [f]
      rw [intervalIntegral.integral_sub, intervalIntegral.integral_comp_mul_left _ m0', mul_zero,
        mul_inv_cancel₀ m0', integral_bernoulliFun_eq_zero (by lia), smul_zero, sub_eq_zero,
        intervalIntegral.integral_const_mul, eq_comm (a := 0), mul_eq_zero]
      · right
        rw [intervalIntegral.integral_finsetSum]
        · simp only [intervalIntegral.integral_comp_add_right, zero_add, ← one_div, ← add_div,
            add_comm (1 : ℝ), ← Nat.cast_add_one]
          rw [intervalIntegral.sum_integral_adjacent_intervals]
          · simp [div_self m0', integral_bernoulliFun_eq_zero]
          · intros; exact Continuous.intervalIntegrable (by fun_prop) _ _
        · intros; exact Continuous.intervalIntegrable (by fun_prop) _ _
      · exact Continuous.intervalIntegrable (by fun_prop) _ _
      · exact Continuous.intervalIntegrable (by fun_prop) _ _
    simp only [fc, intervalIntegral.integral_const, sub_zero, smul_eq_mul, mul_eq_zero, inv_eq_zero,
      Nat.cast_eq_zero, m0, false_or] at i
    simpa only [i] using fc

Premises used: inv_eq_zero, sub_eq_zero, sub_zero, Finset.card_range, false_or, mul_eq_zero, pow_zero, MulZeroClass.mul_zero, bernoulliFun_zero, Nat.cast_eq_zero, HAdd.hAdd, one_div, nsmul_eq_mul, smul_eq_mul, mul_one, OfNat.ofNat, inv_mul_cancel₀, intervalIntegral.integral_const, Finset.sum_const
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
⊢ bernoulliFun (2 * k + 1) (HSub.hSub (α := ℝ) 1 2⁻¹) =
    HPow.hPow (α := ℝ) (-1) (2 * k + 1) * bernoulliFun (2 * k + 1) 2⁻¹

Tactic:
have h := bernoulliFun_eval_one_sub (k := 2 * k + 1) (x := 2⁻¹)
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
h :
  bernoulliFun (2 * k + 1) (HSub.hSub (α := ℝ) 1 2⁻¹) =
    HPow.hPow (α := ℝ) (-1) (2 * k + 1) * bernoulliFun (2 * k + 1) 2⁻¹
⊢ bernoulliFun (2 * k + 1) (1 / 2) = -bernoulliFun (2 * k + 1) (1 / 2)

Tactic:
simp only [pow_succ, even_two, Even.mul_right, Even.neg_pow, one_pow, mul_neg, mul_one, neg_mul,
    one_mul, ← one_div, (sub_eq_of_eq_add (add_halves (1 : ℝ)).symm)] at h

Premises used: one_pow, add_halves, even_two, pow_succ, Even.neg_pow, Even.mul_right, one_div, neg_mul, sub_eq_of_eq_add, mul_one, OfNat.ofNat, Eq.symm, one_mul, mul_neg
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
h : bernoulliFun (2 * k + 1) (1 / 2) = -bernoulliFun (2 * k + 1) (1 / 2)
linarith :
  bernoulliFun (2 * k + 1) 2⁻¹ < 0 →
    -(1 * bernoulliFun (2 * k + 1) (1 / 2) - -(1 * bernoulliFun (2 * k + 1) (1 / 2))) +
        2 * (1 * bernoulliFun (2 * k + 1) (1 / 2) - HMul.hMul (α := ℝ) 1 0) =
      0
linarith₁ : bernoulliFun (2 * k + 1) 2⁻¹ < 0 → GT.gt (α := ℝ) 2 0
linarith₂ :
  0 < bernoulliFun (2 * k + 1) 2⁻¹ →
    1 * bernoulliFun (2 * k + 1) (1 / 2) - -(1 * bernoulliFun (2 * k + 1) (1 / 2)) +
        2 * (HMul.hMul (α := ℝ) 1 0 - 1 * bernoulliFun (2 * k + 1) (1 / 2)) =
      0
linarith₃ : 0 < bernoulliFun (2 * k + 1) 2⁻¹ → GT.gt (α := ℝ) 2 0
⊢ bernoulliFun (2 * k + 1) 2⁻¹ = 0

Tactic:
linarith
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
pos : ∀ (k1 : k = 1), bernoulliFun k 2⁻¹ = (2 / HPow.hPow (α := ℝ) 2 k - 1) * (↑(bernoulli k) : ℝ)
neg : ∀ (k1 : ¬k = 1), bernoulliFun k 2⁻¹ = (2 / HPow.hPow (α := ℝ) 2 k - 1) * (↑(bernoulli k) : ℝ)
⊢ bernoulliFun k 2⁻¹ = (2 / HPow.hPow (α := ℝ) 2 k - 1) * (↑(bernoulli k) : ℝ)

Tactic:
by_cases k1 : k = 1
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
k1 : k = 1
⊢ bernoulliFun k 2⁻¹ = (2 / HPow.hPow (α := ℝ) 2 k - 1) * (↑(bernoulli k) : ℝ)

Tactic:
simp [k1]
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
k1 : ¬k = 1
⊢ bernoulliFun k (HMul.hMul (α := ℝ) (↑2 : ℝ) 2⁻¹) =
    HPow.hPow (α := ℝ) (↑2 : ℝ) k / (↑2 : ℝ) *
      ∑ i ∈ Finset.range 2, bernoulliFun k (2⁻¹ + HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑2 : ℝ))

Tactic:
have m := bernoulliFun_mul k two_ne_zero 2⁻¹
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
k1 : ¬k = 1
m :
  bernoulliFun k (HMul.hMul (α := ℝ) (↑2 : ℝ) 2⁻¹) =
    HPow.hPow (α := ℝ) (↑2 : ℝ) k / (↑2 : ℝ) *
      ∑ i ∈ Finset.range 2, bernoulliFun k (2⁻¹ + HDiv.hDiv (α := ℝ) (↑i : ℝ) (↑2 : ℝ))
⊢ (↑(bernoulli k) : ℝ) = HPow.hPow (α := ℝ) 2 k / 2 * (bernoulliFun k (1 / 2) + (↑(bernoulli k) : ℝ))

Tactic:
simp_rw [Nat.cast_ofNat, mul_inv_cancel₀ (two_ne_zero' ℝ), Finset.sum_range_succ,
      Finset.sum_range_zero, Nat.cast_zero, Nat.cast_one, ← one_div, add_halves,
      bernoulliFun_eval_one, if_neg k1, bernoulliFun_eval_zero, zero_div, add_zero, zero_add] at m

Premises used: Nat.cast_ofNat, Real, mul_inv_cancel₀, add_halves, bernoulliFun_eval_one, zero_div, Finset.sum_range_zero, zero_add, bernoulliFun_eval_zero, two_ne_zero', one_div, Nat.cast_zero, add_zero, if_neg, Nat.cast_one, Finset.sum_range_succ
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
k1 : ¬k = 1
m : (↑(bernoulli k) : ℝ) = HPow.hPow (α := ℝ) 2 k / 2 * (bernoulliFun k (1 / 2) + (↑(bernoulli k) : ℝ))
⊢ HPow.hPow (α := ℝ) 2 k / 2 ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
k1 : ¬k = 1
m : (↑(bernoulli k) : ℝ) = HPow.hPow (α := ℝ) 2 k / 2 * (bernoulliFun k (1 / 2) + (↑(bernoulli k) : ℝ))
⊢ (2 / HPow.hPow (α := ℝ) 2 k - 1) * (↑(bernoulli k) : ℝ) = bernoulliFun k (1 / 2)

Tactic:
rw [← inv_mul_eq_iff_eq_mul₀ (by positivity), ← sub_eq_iff_eq_add, ← sub_one_mul, inv_div] at m

Premises used: inv_mul_eq_iff_eq_mul₀, sub_eq_iff_eq_add, inv_div, sub_one_mul
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
k1 : ¬k = 1
m : (2 / HPow.hPow (α := ℝ) 2 k - 1) * (↑(bernoulli k) : ℝ) = bernoulliFun k (1 / 2)
neg : bernoulliFun k 2⁻¹ = bernoulliFun k (1 / 2)
neg₁ neg₂ : bernoulliFun k 2⁻¹ = bernoulliFun k 2⁻¹
⊢ bernoulliFun k 2⁻¹ = (2 / HPow.hPow (α := ℝ) 2 k - 1) * (↑(bernoulli k) : ℝ)

Tactic:
rw [m, one_div]

Premises used: one_div
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
n : ℤ
hn : n ≠ 0
rw :
  1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      (HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (1 - 0)) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples (1 - 0)) : ℂ)
          ((↑(bernoulliFun k 1) : ℂ) - (↑(bernoulliFun k 0) : ℂ)) -
        ((↑1 : ℂ) - (↑0 : ℂ)) *
          fourierCoeffOn (a := 0) (b := 1) ⋯ (fun (x : ℝ) ↦ (↑((↑k : ℝ) * bernoulliFun (k - 1) x) : ℂ)) n) =
    1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      ((if k = 1 then 1 else 0) -
        HMul.hMul (α := ℂ) (↑k : ℂ)
          (fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun (x : ℝ) ↦ (↑(bernoulliFun (k - 1) x) : ℂ)) n))
⊢ fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun (x : ℝ) ↦ (↑(bernoulliFun k x) : ℂ)) n =
    1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      ((if k = 1 then 1 else 0) -
        HMul.hMul (α := ℂ) (↑k : ℂ)
          (fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun (x : ℝ) ↦ (↑(bernoulliFun (k - 1) x) : ℂ)) n))

Tactic:
rw [fourierCoeffOn_of_hasDerivAt zero_lt_one hn
      (fun x _ => (hasDerivAt_bernoulliFun k x).ofReal_comp)
      ((continuous_ofReal.comp <|
            continuous_const.mul <| Polynomial.continuous _).intervalIntegrable
        _ _)]

Premises used: hasDerivAt_bernoulliFun, Polynomial.continuous, Continuous.comp, continuous_const, Continuous.intervalIntegrable, Continuous.mul, zero_lt_one, HasDerivAt.ofReal_comp, Complex.continuous_ofReal, fourierCoeffOn_of_hasDerivAt
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
n : ℤ
hn : n ≠ 0
simp_rw :
  1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      (HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (1 - 0)) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples (1 - 0)) : ℂ)
          ((↑(bernoulliFun k 1) : ℂ) - (↑(bernoulliFun k 0) : ℂ)) -
        fourierCoeffOn (a := 0) (b := 1) ⋯ (fun (x : ℝ) ↦ (↑((↑k : ℝ) * bernoulliFun (k - 1) x) : ℂ)) n) =
    1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      ((if k = 1 then 1 else 0) -
        HMul.hMul (α := ℂ) (↑k : ℂ)
          (fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun (x : ℝ) ↦ (↑(bernoulliFun (k - 1) x) : ℂ)) n))
⊢ 1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      (HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (1 - 0)) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples (1 - 0)) : ℂ)
          ((↑(bernoulliFun k 1) : ℂ) - (↑(bernoulliFun k 0) : ℂ)) -
        ((↑1 : ℂ) - (↑0 : ℂ)) *
          fourierCoeffOn (a := 0) (b := 1) ⋯ (fun (x : ℝ) ↦ (↑((↑k : ℝ) * bernoulliFun (k - 1) x) : ℂ)) n) =
    1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      ((if k = 1 then 1 else 0) -
        HMul.hMul (α := ℂ) (↑k : ℂ)
          (fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun (x : ℝ) ↦ (↑(bernoulliFun (k - 1) x) : ℂ)) n))

Tactic:
simp_rw [ofReal_one, ofReal_zero, sub_zero, one_mul]

Premises used: sub_zero, Complex.ofReal_one, Complex.ofReal_zero, one_mul
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
n : ℤ
hn : n ≠ 0
rw :
  1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      ((↑(if k = 1 then 1 else 0) : ℂ) -
        fourierCoeffOn (a := 0) (b := 1) ⋯ (fun (x : ℝ) ↦ (↑((↑k : ℝ) * bernoulliFun (k - 1) x) : ℂ)) n) =
    1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      ((if k = 1 then 1 else 0) -
        HMul.hMul (α := ℂ) (↑k : ℂ)
          (fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun (x : ℝ) ↦ (↑(bernoulliFun (k - 1) x) : ℂ)) n))
⊢ 1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      (HMul.hMul (α := ℂ) ((fourier (-n) : (a : AddCircle (1 - 0)) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples (1 - 0)) : ℂ)
          ((↑(bernoulliFun k 1) : ℂ) - (↑(bernoulliFun k 0) : ℂ)) -
        fourierCoeffOn (a := 0) (b := 1) ⋯ (fun (x : ℝ) ↦ (↑((↑k : ℝ) * bernoulliFun (k - 1) x) : ℂ)) n) =
    1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      ((if k = 1 then 1 else 0) -
        HMul.hMul (α := ℂ) (↑k : ℂ)
          (fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun (x : ℝ) ↦ (↑(bernoulliFun (k - 1) x) : ℂ)) n))

Tactic:
rw [QuotientAddGroup.mk_zero, fourier_eval_zero, one_mul, ← ofReal_sub, bernoulliFun_eval_one,
    add_sub_cancel_left]

Premises used: add_sub_cancel_left, bernoulliFun_eval_one, fourier_eval_zero, QuotientAddGroup.mk_zero, Complex.ofReal_sub, one_mul
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
n : ℤ
hn : n ≠ 0
e_a : (↑(if k = 1 then 1 else 0) : ℂ) = if k = 1 then 1 else 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)
⊢ 1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      ((↑(if k = 1 then 1 else 0) : ℂ) -
        fourierCoeffOn (a := 0) (b := 1) ⋯ (fun (x : ℝ) ↦ (↑((↑k : ℝ) * bernoulliFun (k - 1) x) : ℂ)) n) =
    1 / (-2 * (↑π : ℂ) * I * (↑n : ℂ)) *
      ((if k = 1 then 1 else 0) -
        HMul.hMul (α := ℂ) (↑k : ℂ)
          (fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun (x : ℝ) ↦ (↑(bernoulliFun (k - 1) x) : ℂ)) n))

Tactic:
congr 2
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
n : ℤ
hn : n ≠ 0
pos : k = 1 → (↑1 : ℂ) = 1
neg : ¬k = 1 → (↑0 : ℂ) = 0
⊢ (↑(if k = 1 then 1 else 0) : ℂ) = if k = 1 then 1 else 0

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
n : ℤ
hn : n ≠ 0
h : k = 1
⊢ (↑1 : ℂ) = 1

Tactic:
simp only [ofReal_one, ofReal_zero]

Premises used: Complex.ofReal_one, Complex.ofReal_zero
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
n : ℤ
hn : n ≠ 0
h : ¬k = 1
⊢ (↑0 : ℂ) = 0

Tactic:
simp only [ofReal_one, ofReal_zero]

Premises used: Complex.ofReal_one, Complex.ofReal_zero
-- Module: Mathlib.NumberTheory.ZetaValues
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)
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)

Tactic:
simp_rw [ofReal_mul, ofReal_natCast, fourierCoeffOn.const_mul]

Premises used: fourierCoeffOn.const_mul, Complex.ofReal_natCast, Complex.ofReal_mul
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff 0 n = 0

Tactic:
simpa using bernoulliFourierCoeff_recurrence 0 hn

Premises used: bernoulliFourierCoeff_recurrence, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ZetaValues
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
simp_rw₈ : (↑0 : ℂ) = 0
⊢ bernoulliFourierCoeff k 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]

Premises used: intervalIntegral.integral_ofReal, sub_zero, integral_bernoulliFun_eq_zero, fourier_zero, one_smul, bernoulliFourierCoeff, Complex.ofReal_zero, fourierCoeffOn_eq_integral, neg_zero, div_one