-- Mathlib/NumberTheory/ZetaValues.lean
theorem bernoulliFourierCoeff_eq {k : ℕ} (hk : k ≠ 0) (n : ℤ) :
    bernoulliFourierCoeff k n = -k ! / (2 * π * I * n) ^ k

Proof state:
case inr.refine_2
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
⊢ 1 / (-2 * ↑π * I * ↑n) * ((if k + 1 = 1 then 1 else 0) - ↑(k + 1) * bernoulliFourierCoeff k n) =
    -↑(k + 1)! / (2 * ↑π * I * ↑n) ^ (k + 1)

Tactic:
split_ifs with h

Result:
case pos
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
h : k + 1 = 1
⊢ 1 / (-2 * ↑π * I * ↑n) * (1 - ↑(k + 1) * bernoulliFourierCoeff k n) = -↑(k + 1)! / (2 * ↑π * I * ↑n) ^ (k + 1)

case neg
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
h : ¬k + 1 = 1
⊢ 1 / (-2 * ↑π * I * ↑n) * (0 - ↑(k + 1) * bernoulliFourierCoeff k n) = -↑(k + 1)! / (2 * ↑π * I * ↑n) ^ (k + 1)

Proof state:
case neg
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
h : ¬k + 1 = 1
⊢ 1 / (-2 * ↑π * I * ↑n) * (0 - ↑(k + 1) * bernoulliFourierCoeff k n) = -↑(k + 1)! / (2 * ↑π * I * ↑n) ^ (k + 1)

Tactic:
rw [h'k, Nat.factorial_succ, zero_sub, Nat.cast_mul, pow_add, pow_one, neg_div, mul_neg,
  mul_neg, mul_neg, neg_neg, neg_mul, neg_mul, neg_mul, div_neg]

Result:
case neg
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
h : ¬k + 1 = 1
⊢ -(1 / (2 * ↑π * I * ↑n)) * (↑(k + 1) * (↑k ! / (2 * ↑π * I * ↑n) ^ k)) =
    -(↑(k + 1) * ↑k !) / ((2 * ↑π * I * ↑n) ^ k * (2 * ↑π * I * ↑n))

Proof state:
case pos
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
h : k + 1 = 1
⊢ 1 / (-2 * ↑π * I * ↑n) * (1 - ↑(k + 1) * bernoulliFourierCoeff k n) = -↑(k + 1)! / (2 * ↑π * I * ↑n) ^ (k + 1)

Tactic:
exfalso

Result:
case pos
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
h : k + 1 = 1
⊢ False

Proof state:
case inr.refine_1
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 / -(2 * ↑π * I * ↑n) * (1 - bernoulliFourierCoeff 0 n) = -1 / (2 * ↑π * I * ↑n)

Tactic:
rw [bernoulli_zero_fourier_coeff hn, sub_zero, mul_one, div_neg, neg_div]

Result:
no goals

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

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Result:
case inl
k : ℕ
hk : k ≠ 0
⊢ bernoulliFourierCoeff k 0 = -↑k ! / (2 * ↑π * I * ↑0) ^ k

case inr
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k

Proof state:
case inl
k : ℕ
hk : k ≠ 0
⊢ bernoulliFourierCoeff k 0 = -↑k ! / (2 * ↑π * I * ↑0) ^ k

Tactic:
rw [bernoulliFourierCoeff_zero hk, Int.cast_zero, mul_zero, zero_pow hk,
  div_zero]

Result:
no goals

Proof state:
case inr
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k

Tactic:
refine Nat.le_induction ?_ (fun k hk h'k => ?_) k (Nat.one_le_iff_ne_zero.mpr hk)

Result:
case inr.refine_1
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff 1 n = -↑1! / (2 * ↑π * I * ↑n) ^ 1

case inr.refine_2
k✝ : ℕ
hk✝ : k✝ ≠ 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)

Proof state:
case inr.refine_1
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff 1 n = -↑1! / (2 * ↑π * I * ↑n) ^ 1

Tactic:
rw [bernoulliFourierCoeff_recurrence 1 hn]

Result:
case inr.refine_1
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) * ((if 1 = 1 then 1 else 0) - ↑1 * bernoulliFourierCoeff (1 - 1) n) =
    -↑1! / (2 * ↑π * I * ↑n) ^ 1

Proof state:
case inr.refine_1
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) * ((if 1 = 1 then 1 else 0) - ↑1 * bernoulliFourierCoeff (1 - 1) n) =
    -↑1! / (2 * ↑π * I * ↑n) ^ 1

Tactic:
simp only [Nat.cast_one, tsub_self, neg_mul, one_mul, eq_self_iff_true, if_true,
  Nat.factorial_one, pow_one, inv_I, mul_neg]

Result:
case inr.refine_1
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 / -(2 * ↑π * I * ↑n) * (1 - bernoulliFourierCoeff 0 n) = -1 / (2 * ↑π * I * ↑n)

Proof state:
case pos
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
h : k + 1 = 1
⊢ False

Tactic:
exact (ne_of_gt (Nat.lt_succ_iff.mpr hk)) h

Result:
no goals

Proof state:
case neg
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
h : ¬k + 1 = 1
⊢ -(1 / (2 * ↑π * I * ↑n)) * (↑(k + 1) * (↑k ! / (2 * ↑π * I * ↑n) ^ k)) =
    -(↑(k + 1) * ↑k !) / ((2 * ↑π * I * ↑n) ^ k * (2 * ↑π * I * ↑n))

Tactic:
field_simp [Int.cast_ne_zero.mpr hn, I_ne_zero]

Result:
case neg
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
h : ¬k + 1 = 1
⊢ -((↑k + 1) * ↑k !) / (2 * ↑π * I * ↑n * (2 * ↑π * I * ↑n) ^ k) =
    -((↑k + 1) * ↑k !) / ((2 * ↑π * I * ↑n) ^ k * (2 * ↑π * I * ↑n))

Proof state:
case inr.refine_2
k✝ : ℕ
hk✝ : k✝ ≠ 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)

Tactic:
rw [bernoulliFourierCoeff_recurrence (k + 1) hn, Nat.add_sub_cancel k 1]

Result:
case inr.refine_2
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
⊢ 1 / (-2 * ↑π * I * ↑n) * ((if k + 1 = 1 then 1 else 0) - ↑(k + 1) * bernoulliFourierCoeff k n) =
    -↑(k + 1)! / (2 * ↑π * I * ↑n) ^ (k + 1)

Proof state:
case neg
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
h : ¬k + 1 = 1
⊢ -((↑k + 1) * ↑k !) / (2 * ↑π * I * ↑n * (2 * ↑π * I * ↑n) ^ k) =
    -((↑k + 1) * ↑k !) / ((2 * ↑π * I * ↑n) ^ k * (2 * ↑π * I * ↑n))

Tactic:
ring_nf

Result:
no goals