-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
rw :
  -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
    HPow.hPow (α := ℂ) (-1) k * (↑(bernoulli (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
rw₁ :
  -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
    HPow.hPow (α := ℂ) (-1) k * (↑(HPow.hPow (α := ℚ) (-1) (k + 1) * bernoulli' (k + 1)) : ℂ) /
      HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
rw₂ :
  -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
    HPow.hPow (α := ℂ) (-1) k *
        HMul.hMul (α := ℂ) (↑(HPow.hPow (α := ℚ) (-1) (k + 1)) : ℂ) (↑(bernoulli' (k + 1)) : ℂ) /
      HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
rw₃ :
  -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
    HPow.hPow (α := ℂ) (-1) k * (HPow.hPow (α := ℂ) (↑(-1) : ℂ) (k + 1) * (↑(bernoulli' (k + 1)) : ℂ)) /
      HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
rw₄ :
  -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
    HPow.hPow (α := ℂ) (-1) k * (HPow.hPow (α := ℂ) (-(↑1 : ℂ)) (k + 1) * (↑(bernoulli' (k + 1)) : ℂ)) /
      HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
rw₅ :
  -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
    HPow.hPow (α := ℂ) (-1) k * (HPow.hPow (α := ℂ) (-1) (k + 1) * (↑(bernoulli' (k + 1)) : ℂ)) /
      HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
rw₆ :
  HMul.hMul (α := ℂ) (-1) (↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
    HPow.hPow (α := ℂ) (-1) k * (HPow.hPow (α := ℂ) (-1) (k + 1) * (↑(bernoulli' (k + 1)) : ℂ)) /
      HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
rw₇ :
  HMul.hMul (α := ℂ) (-1) (↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
    HPow.hPow (α := ℂ) (-1) k * HPow.hPow (α := ℂ) (-1) (k + 1) * (↑(bernoulli' (k + 1)) : ℂ) /
      HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
rw₈ :
  HMul.hMul (α := ℂ) (-1) (↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
    HPow.hPow (α := ℂ) (-1) k * (HPow.hPow (α := ℂ) (-1) k * -1) * (↑(bernoulli' (k + 1)) : ℂ) /
      HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
rw₉ :
  HMul.hMul (α := ℂ) (-1) (↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
    HPow.hPow (α := ℂ) (-1) k * HPow.hPow (α := ℂ) (-1) k * -1 * (↑(bernoulli' (k + 1)) : ℂ) /
      HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
rw₁₀ :
  HMul.hMul (α := ℂ) (-1) (↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
    HMul.hMul (α := ℂ) (-1) (-1) ^ k * -1 * (↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
rw₁₁ :
  HMul.hMul (α := ℂ) (-1) (↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
    HPow.hPow (α := ℂ) (- -1) k * -1 * (↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
rw₁₂ :
  HMul.hMul (α := ℂ) (-1) (↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
    HPow.hPow (α := ℂ) 1 k * -1 * (↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
rw₁₃ :
  HMul.hMul (α := ℂ) (-1) (↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
    HMul.hMul (α := ℂ) 1 (-1) * (↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
rw₁₄ rw₁₅ :
  HMul.hMul (α := ℂ) (-1) (↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
    HMul.hMul (α := ℂ) (-1) (↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
⊢ riemannZeta (-(↑k : ℂ)) = HPow.hPow (α := ℂ) (-1) k * (↑(bernoulli (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1

Tactic:
rw [riemannZeta_neg_nat_eq_bernoulli', bernoulli, Rat.cast_mul, Rat.cast_pow, Rat.cast_neg,
    Rat.cast_one, ← neg_one_mul, ← mul_assoc, pow_succ, ← mul_assoc, ← mul_pow, neg_one_mul (-1),
    neg_neg, one_pow, one_mul]

Premises used: one_pow, Rat.cast_mul, pow_succ, bernoulli, mul_assoc, neg_one_mul, neg_neg, riemannZeta_neg_nat_eq_bernoulli', OfNat.ofNat, Rat.cast_neg, mul_pow, Rat.cast_pow, Neg.neg, one_mul, Rat.cast_one