-- Mathlib/NumberTheory/ZetaValues.lean
theorem summable_bernoulli_fourier {k : ℕ} (hk : 2 ≤ k) :
    Summable (fun n => -k ! / (2 * π * I * n) ^ k : ℤ → ℂ)

Proof state:
k : ℕ
hk : 2 ≤ k
this✝ : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
this : (fun x => ‖1 / ↑x ^ k‖) = fun x => |1 / ↑x ^ k|
⊢ Summable fun x => |1 / ↑x ^ k|

Tactic:
rwa [summable_abs_iff, Real.summable_one_div_int_pow]

Result:
no goals

Proof state:
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
⊢ Summable fun n => -↑k ! / (2 * ↑π * I * ↑n) ^ k

Tactic:
simp_rw [this]

Result:
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
⊢ Summable fun n => -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)

Proof state:
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
⊢ Summable fun a => ‖1 / ↑a ^ 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]

Result:
k : ℕ
hk : 2 ≤ k
this✝ : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
this : (fun x => ‖1 / ↑x ^ k‖) = fun x => |1 / ↑x ^ k|
⊢ Summable fun a => ‖1 / ↑a ^ k‖

Proof state:
case h
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
x : ℤ
⊢ ‖1 / ↑x ^ k‖ = |1 / ↑x ^ k|

Tactic:
simp only [one_div, norm_inv, norm_pow, norm_intCast, pow_abs, abs_inv]

Result:
no goals

Proof state:
k : ℕ
hk : 2 ≤ k
this✝ : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
this : (fun x => ‖1 / ↑x ^ k‖) = fun x => |1 / ↑x ^ k|
⊢ Summable fun a => ‖1 / ↑a ^ k‖

Tactic:
simp_rw [this]

Result:
k : ℕ
hk : 2 ≤ k
this✝ : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
this : (fun x => ‖1 / ↑x ^ k‖) = fun x => |1 / ↑x ^ k|
⊢ Summable fun x => |1 / ↑x ^ k|

Proof state:
k : ℕ
hk : 2 ≤ k
n : ℤ
⊢ -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)

Tactic:
rw [mul_one_div, div_div, ← mul_pow]

Result:
no goals

Proof state:
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
⊢ Summable fun n => -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)

Tactic:
refine Summable.mul_left _ <| .of_norm ?_

Result:
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
⊢ Summable fun a => ‖1 / ↑a ^ k‖

Proof state:
k : ℕ
hk : 2 ≤ k
⊢ ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)

Tactic:
intro n

Result:
k : ℕ
hk : 2 ≤ k
n : ℤ
⊢ -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)

Proof state:
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
⊢ (fun x => ‖1 / ↑x ^ k‖) = fun x => |1 / ↑x ^ k|

Tactic:
ext1 x

Result:
case h
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
x : ℤ
⊢ ‖1 / ↑x ^ k‖ = |1 / ↑x ^ k|

Proof state:
k : ℕ
hk : 2 ≤ k
⊢ Summable fun n => -↑k ! / (2 * ↑π * I * ↑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]

Result:
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
⊢ Summable fun n => -↑k ! / (2 * ↑π * I * ↑n) ^ k