-- Mathlib/NumberTheory/ZetaValues.lean
theorem bernoulliFourierCoeff_recurrence (k : ℕ) {n : ℤ} (hn : n ≠ 0) :
    bernoulliFourierCoeff k n =
      1 / (-2 * π * I * n) * (ite (k = 1) 1 0 - k * bernoulliFourierCoeff (k - 1) n)

Proof state:
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) * (↑(if k = 1 then 1 else 0) - fourierCoeffOn ⋯ (fun x => ↑(↑k * bernoulliFun (k - 1) x)) n) =
    1 / (-2 * ↑π * I * ↑n) *
      ((if k = 1 then 1 else 0) -
        ↑k * fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun (k - 1) x)) n)

Tactic:
congr 2

Result:
case e_a.e_a
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ ↑(if k = 1 then 1 else 0) = if k = 1 then 1 else 0

case e_a.e_a
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ fourierCoeffOn ⋯ (fun x => ↑(↑k * bernoulliFun (k - 1) x)) n =
    ↑k * fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun (k - 1) x)) n

Proof state:
case e_a.e_a
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ ↑(if k = 1 then 1 else 0) = if k = 1 then 1 else 0

Tactic:
split_ifs <;> simp only [ofReal_one, ofReal_zero, one_mul]

Result:
no goals

Proof state:
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun k x)) n =
    1 / (-2 * ↑π * I * ↑n) *
      ((if k = 1 then 1 else 0) -
        ↑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
      _ _)]

Result:
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) *
      ((fourier (-n)) ↑0 * (↑(bernoulliFun k 1) - ↑(bernoulliFun k 0)) -
        (↑1 - ↑0) * fourierCoeffOn ⋯ (fun x => ↑(↑k * bernoulliFun (k - 1) x)) n) =
    1 / (-2 * ↑π * I * ↑n) *
      ((if k = 1 then 1 else 0) -
        ↑k * fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun (k - 1) x)) n)

Proof state:
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) *
      ((fourier (-n)) ↑0 * (↑(bernoulliFun k 1) - ↑(bernoulliFun k 0)) -
        fourierCoeffOn ⋯ (fun x => ↑(↑k * bernoulliFun (k - 1) x)) n) =
    1 / (-2 * ↑π * I * ↑n) *
      ((if k = 1 then 1 else 0) -
        ↑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]

Result:
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) * (↑(if k = 1 then 1 else 0) - fourierCoeffOn ⋯ (fun x => ↑(↑k * bernoulliFun (k - 1) x)) n) =
    1 / (-2 * ↑π * I * ↑n) *
      ((if k = 1 then 1 else 0) -
        ↑k * fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun (k - 1) x)) n)

Proof state:
case e_a.e_a
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ fourierCoeffOn ⋯ (fun x => ↑(↑k * bernoulliFun (k - 1) x)) n =
    ↑k * fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun (k - 1) x)) n

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

Result:
no goals

Proof state:
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) *
      ((fourier (-n)) ↑0 * (↑(bernoulliFun k 1) - ↑(bernoulliFun k 0)) -
        (↑1 - ↑0) * fourierCoeffOn ⋯ (fun x => ↑(↑k * bernoulliFun (k - 1) x)) n) =
    1 / (-2 * ↑π * I * ↑n) *
      ((if k = 1 then 1 else 0) -
        ↑k * fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun (k - 1) x)) n)

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

Result:
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) *
      ((fourier (-n)) ↑0 * (↑(bernoulliFun k 1) - ↑(bernoulliFun k 0)) -
        fourierCoeffOn ⋯ (fun x => ↑(↑k * bernoulliFun (k - 1) x)) n) =
    1 / (-2 * ↑π * I * ↑n) *
      ((if k = 1 then 1 else 0) -
        ↑k * fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun (k - 1) x)) n)

Proof state:
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff k n = 1 / (-2 * ↑π * I * ↑n) * ((if k = 1 then 1 else 0) - ↑k * bernoulliFourierCoeff (k - 1) n)

Tactic:
unfold bernoulliFourierCoeff

Result:
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun k x)) n =
    1 / (-2 * ↑π * I * ↑n) *
      ((if k = 1 then 1 else 0) -
        ↑k * fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun (k - 1) x)) n)