awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ riemannZeta (-(↑k : ℂ)) = HPow.hPow (α := ℂ) (-1) k * (↑(bernoulli (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
have rw₅ : -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
  HPow.hPow (α := ℂ) (-1) k * (HPow.hPow (α := ℂ) (-1) (k + 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]
-- 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
⊢ 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 =
  HPow.hPow (α := ℂ) (-1) k * (HPow.hPow (α := ℂ) (-1) (k + 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]
-- 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
⊢ 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 =
  HPow.hPow (α := ℂ) (-1) k * HPow.hPow (α := ℂ) (-1) (k + 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]
-- 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
⊢ 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 =
  HPow.hPow (α := ℂ) (-1) k * (HPow.hPow (α := ℂ) (-1) k * -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]
-- 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
⊢ 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 =
  HPow.hPow (α := ℂ) (-1) k * HPow.hPow (α := ℂ) (-1) k * -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]
-- 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
⊢ 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) (-1) ^ k * -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]
-- 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
⊢ 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 =
  HPow.hPow (α := ℂ) (- -1) k * -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]
-- 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
⊢ 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 =
  HPow.hPow (α := ℂ) 1 k * -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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (hypothesis)
Goal:
m n : ℕ
z : ℂ
x : ℝ
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * (z / HPow.hPow (α := ℂ) (↑m : ℂ) (↑x : ℂ)) =
    z / ((↑m : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ (↑x : ℂ)
have Hn : 0 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
Tactic: have Hn : (0 : ℝ) ≤ (n + 1 : ℝ)⁻¹ := by positivity
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * (z / HPow.hPow (α := ℂ) (↑m : ℂ) (↑x : ℂ)) =
    z / ((↑m : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ (↑x : ℂ)
have rw : z * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) / HPow.hPow (α := ℂ) (↑m : ℂ) (↑x : ℂ)) =
  z * (((↑m : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ (↑x : ℂ))⁻¹
Tactic: rw [← mul_div_assoc, mul_comm, div_eq_mul_inv z, mul_div_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
⊢ z * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) / HPow.hPow (α := ℂ) (↑m : ℂ) (↑x : ℂ)) =
    z * (((↑m : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ (↑x : ℂ))⁻¹
have e_a : HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) / HPow.hPow (α := ℂ) (↑m : ℂ) (↑x : ℂ) =
  (((↑m : ℂ) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ (↑x : ℂ))⁻¹
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ)
have norm_cast : n + 1 = n + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
⊢ (↑m : ℂ) = (↑(↑m : ℝ) : ℂ)
have norm_cast : m = m
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ^ (↑x : ℂ) * (HPow.hPow (α := ℂ) (↑m : ℂ) (↑x : ℂ))⁻¹ =
    (((↑m : ℂ) * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹) ^ (↑x : ℂ))⁻¹
have e_a : ((↑(↑m : ℝ) : ℂ) ^ (↑x : ℂ))⁻¹ * (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) =
  ((↑(↑m : ℝ) : ℂ) ^ (↑x : ℂ))⁻¹ * ((↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ : ℂ) ^ (↑x : ℂ))⁻¹
Tactic: rw [show (n + 1 : ℂ)⁻¹ = (n + 1 : ℝ)⁻¹ by simp,
    show (n + 1 : ℂ) = (n + 1 : ℝ) by norm_cast, show (m : ℂ) = (m : ℝ) by norm_cast,
    mul_cpow_ofReal_nonneg m.cast_nonneg Hn, mul_inv, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
⊢ ((↑(↑m : ℝ) : ℂ) ^ (↑x : ℂ))⁻¹ * (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) =
    ((↑(↑m : ℝ) : ℂ) ^ (↑x : ℂ))⁻¹ * ((↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ : ℂ) ^ (↑x : ℂ))⁻¹
have e_a : (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) = ((↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ : ℂ) ^ (↑x : ℂ))⁻¹
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
⊢ (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) = ((↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ : ℂ) ^ (↑x : ℂ))⁻¹
have e_a : (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) = (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ : ℂ) ^ (-(↑x : ℂ))
Tactic: rw [← cpow_neg, show (-x : ℂ) = (-1 : ℝ) * x by simp, cpow_mul_ofReal_nonneg Hn,
    Real.rpow_neg_one, inv_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
e_a : (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) = (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ : ℂ) ^ (-(↑x : ℂ))
⊢ (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) = ((↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ : ℂ) ^ (↑x : ℂ))⁻¹
have e_a₁ : (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) = (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ : ℂ) ^ ((↑(-1) : ℂ) * (↑x : ℂ))
Tactic: rw [← cpow_neg, show (-x : ℂ) = (-1 : ℝ) * x by simp, cpow_mul_ofReal_nonneg Hn,
    Real.rpow_neg_one, inv_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Injectivity (goal)
Goal:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
e_a : (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) = (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ : ℂ) ^ (-(↑x : ℂ))
e_a₁ :
  (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) =
    (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ : ℂ) ^ ((↑(-1) : ℂ) * (↑x : ℂ))
⊢ (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) = ((↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ : ℂ) ^ (↑x : ℂ))⁻¹
have e_a₂ : (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ) ^ (↑x : ℂ) =
  (↑(HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ (-1)) : ℂ) ^ (↑x : ℂ)
Tactic: rw [← cpow_neg, show (-x : ℂ) = (-1 : ℝ) * x by simp, cpow_mul_ofReal_nonneg Hn,
    Real.rpow_neg_one, inv_inv]