-- Mathlib/NumberTheory/ZetaValues.lean
theorem hasSum_one_div_nat_pow_mul_fourier {k : ℕ} (hk : 2 ≤ k) {x : ℝ} (hx : x ∈ Icc (0 : ℝ) 1) :
    HasSum
      (fun n : ℕ =>
        (1 : ℂ) / (n : ℂ) ^ k * (fourier n (x : 𝕌) + (-1 : ℂ) ^ k * fourier (-n) (x : 𝕌)))
      (-(2 * π * I) ^ k / k ! * bernoulliFun k x)

Proof state:
case h.e'_5.h.e_a.e_a.e_a
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ (-1) ^ k = 1 / (-1) ^ k

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

Result:
case h.e'_5.h.e_a.e_a.e_a
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ (-1) ^ k ≠ 0

Proof state:
case h.e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * (fourier ↑n) ↑x + 1 / ↑n ^ k * (-1) ^ k * (fourier (-↑n)) ↑x =
    1 / ↑↑n ^ k * (fourier ↑n) ↑x + 1 / (-↑↑n) ^ k * (fourier (-↑n)) ↑x

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

Result:
case h.e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * (fourier ↑n) ↑x + 1 / ↑n ^ k * (-1) ^ k * (fourier (-↑n)) ↑x =
    1 / ↑↑n ^ k * (fourier ↑n) ↑x + 1 / (-1) ^ k / ↑↑n ^ k * (fourier (-↑n)) ↑x

Proof state:
case h.e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * ((fourier ↑n) ↑x + (-1) ^ k * (fourier (-↑n)) ↑x) =
    1 / ↑↑n ^ k * (fourier ↑n) ↑x + 1 / ↑(-↑n) ^ k * (fourier (-↑n)) ↑x

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

Result:
case h.e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * (fourier ↑n) ↑x + 1 / ↑n ^ k * (-1) ^ k * (fourier (-↑n)) ↑x =
    1 / ↑↑n ^ k * (fourier ↑n) ↑x + 1 / (-↑↑n) ^ k * (fourier (-↑n)) ↑x

Proof state:
case h.e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * (fourier ↑n) ↑x + 1 / ↑n ^ k * (-1) ^ k * (fourier (-↑n)) ↑x =
    1 / ↑↑n ^ k * (fourier ↑n) ↑x + 1 / (-1) ^ k / ↑↑n ^ k * (fourier (-↑n)) ↑x

Tactic:
congr 2

Result:
case h.e'_5.h.e_a.e_a
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * (-1) ^ k = 1 / (-1) ^ k / ↑↑n ^ k

Proof state:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ HasSum (fun n => 1 / ↑n ^ k * ((fourier ↑n) ↑x + (-1) ^ k * (fourier (-↑n)) ↑x))
    (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x))

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

Result:
case h.e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ (fun n => 1 / ↑n ^ k * ((fourier ↑n) ↑x + (-1) ^ k * (fourier (-↑n)) ↑x)) = fun n =>
    1 / ↑↑n ^ k * (fourier ↑n) ↑x + 1 / ↑(-↑n) ^ k * (fourier (-↑n)) ↑x

case h.e'_6
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) =
    -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) + 1 / ↑0 ^ k * (fourier 0) ↑x

Proof state:
case h.e'_5.h.e_a.e_a
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ (-1) ^ k / ↑n ^ k = 1 / (-1) ^ k / ↑↑n ^ k

Tactic:
congr 1

Result:
case h.e'_5.h.e_a.e_a.e_a
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ (-1) ^ k = 1 / (-1) ^ k

Proof state:
case h.e'_5.h.e_a.e_a
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * (-1) ^ k = 1 / (-1) ^ k / ↑↑n ^ k

Tactic:
rw [div_mul_eq_mul_div₀, one_mul]

Result:
case h.e'_5.h.e_a.e_a
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ (-1) ^ k / ↑n ^ k = 1 / (-1) ^ k / ↑↑n ^ k

Proof state:
case h.e'_5.h.e_a.e_a.e_a
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ (-1) ^ k ≠ 0

Tactic:
apply pow_ne_zero

Result:
case h.e'_5.h.e_a.e_a.e_a.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ -1 ≠ 0

Proof state:
case h.e'_5.h.e_a.e_a.e_a.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ -1 ≠ 0

Tactic:
rw [neg_ne_zero]

Result:
case h.e'_5.h.e_a.e_a.e_a.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 ≠ 0

Proof state:
case h.e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ (fun n => 1 / ↑n ^ k * ((fourier ↑n) ↑x + (-1) ^ k * (fourier (-↑n)) ↑x)) = fun n =>
    1 / ↑↑n ^ k * (fourier ↑n) ↑x + 1 / ↑(-↑n) ^ k * (fourier (-↑n)) ↑x

Tactic:
ext1 n

Result:
case h.e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * ((fourier ↑n) ↑x + (-1) ^ k * (fourier (-↑n)) ↑x) =
    1 / ↑↑n ^ k * (fourier ↑n) ↑x + 1 / ↑(-↑n) ^ k * (fourier (-↑n)) ↑x

Proof state:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ k ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case h.e'_6
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) =
    -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) + 1 / ↑0 ^ k * (fourier 0) ↑x

Tactic:
rw [Int.cast_zero, zero_pow (by positivity : k ≠ 0), div_zero, zero_mul, add_zero]

Result:
no goals

Proof state:
case h.e'_5.h.e_a.e_a.e_a.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals