-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
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
⊢ riemannZeta (-(↑k : ℂ)) = HPow.hPow (α := ℂ) (-1) k * (↑(bernoulli (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
have rw₁₄ : HMul.hMul (α := ℂ) (-1) (↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
  HMul.hMul (α := ℂ) (-1) (↑(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]