awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
inl : riemannZeta (-0) = -(↑(bernoulli' (HAdd.hAdd (α := ℕ) 0 1)) : ℂ) / HAdd.hAdd (α := ℂ) 0 1
inl₁ : riemannZeta 0 = -(↑(bernoulli' (HAdd.hAdd (α := ℕ) 0 1)) : ℂ) / HAdd.hAdd (α := ℂ) 0 1
inl₂ : -1 / 2 = -(↑(bernoulli' (HAdd.hAdd (α := ℕ) 0 1)) : ℂ) / HAdd.hAdd (α := ℂ) 0 1
inl₃ : -1 / 2 = -(↑(bernoulli' 1) : ℂ) / HAdd.hAdd (α := ℂ) 0 1
inl₄ : -1 / 2 = HDiv.hDiv (α := ℂ) (-(↑(bernoulli' 1) : ℂ)) 1
inl₅ : -1 / 2 = -(↑(bernoulli' 1) : ℂ)
inl₆ : -1 / 2 = -(↑(1 / 2) : ℂ)
inl₇ : -1 / 2 = -HDiv.hDiv (α := ℂ) (↑1 : ℂ) (↑2 : ℂ)
inl₈ : -1 / 2 = -HDiv.hDiv (α := ℂ) 1 (↑2 : ℂ)
⊢ riemannZeta (-(↑0 : ℂ)) = -(↑(bernoulli' (HAdd.hAdd (α := ℕ) 0 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1
have inl₉ : -1 / 2 = -HDiv.hDiv (α := ℂ) 1 2
Tactic: rw [Nat.cast_zero, neg_zero, riemannZeta_zero, zero_add, zero_add, div_one,
      bernoulli'_one, Rat.cast_div, Rat.cast_one, Rat.cast_ofNat, neg_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
inl : riemannZeta (-0) = -(↑(bernoulli' (HAdd.hAdd (α := ℕ) 0 1)) : ℂ) / HAdd.hAdd (α := ℂ) 0 1
inl₁ : riemannZeta 0 = -(↑(bernoulli' (HAdd.hAdd (α := ℕ) 0 1)) : ℂ) / HAdd.hAdd (α := ℂ) 0 1
inl₂ : -1 / 2 = -(↑(bernoulli' (HAdd.hAdd (α := ℕ) 0 1)) : ℂ) / HAdd.hAdd (α := ℂ) 0 1
inl₃ : -1 / 2 = -(↑(bernoulli' 1) : ℂ) / HAdd.hAdd (α := ℂ) 0 1
inl₄ : -1 / 2 = HDiv.hDiv (α := ℂ) (-(↑(bernoulli' 1) : ℂ)) 1
inl₅ : -1 / 2 = -(↑(bernoulli' 1) : ℂ)
inl₆ : -1 / 2 = -(↑(1 / 2) : ℂ)
inl₇ : -1 / 2 = -HDiv.hDiv (α := ℂ) (↑1 : ℂ) (↑2 : ℂ)
inl₈ : -1 / 2 = -HDiv.hDiv (α := ℂ) 1 (↑2 : ℂ)
inl₉ : -1 / 2 = -HDiv.hDiv (α := ℂ) 1 2
⊢ riemannZeta (-(↑0 : ℂ)) = -(↑(bernoulli' (HAdd.hAdd (α := ℕ) 0 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1
have inl₁₀ : -(1 / 2) = -HDiv.hDiv (α := ℂ) 1 2
Tactic: rw [Nat.cast_zero, neg_zero, riemannZeta_zero, zero_add, zero_add, div_one,
      bernoulli'_one, Rat.cast_div, Rat.cast_one, Rat.cast_ofNat, neg_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
⊢ riemannZeta (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
have inr : hurwitzZeta 0 (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
Tactic: rw [← hurwitzZeta_zero, ← QuotientAddGroup.mk_zero, hurwitzZeta_neg_nat hk
      (left_mem_Icc.mpr zero_le_one), ofReal_zero, Polynomial.eval_zero_map,
      Polynomial.bernoulli_eval_zero, Algebra.algebraMap_eq_smul_one, Rat.smul_one_eq_cast,
      div_mul_eq_mul_div, neg_one_mul, bernoulli_eq_bernoulli'_of_ne_one (by simp [hk])]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
inr : hurwitzZeta 0 (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
⊢ riemannZeta (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
have inr₁ : hurwitzZeta (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) (-(↑k : ℂ)) =
  -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
Tactic: rw [← hurwitzZeta_zero, ← QuotientAddGroup.mk_zero, hurwitzZeta_neg_nat hk
      (left_mem_Icc.mpr zero_le_one), ofReal_zero, Polynomial.eval_zero_map,
      Polynomial.bernoulli_eval_zero, Algebra.algebraMap_eq_smul_one, Rat.smul_one_eq_cast,
      div_mul_eq_mul_div, neg_one_mul, bernoulli_eq_bernoulli'_of_ne_one (by simp [hk])]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
inr : hurwitzZeta 0 (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₁ :
  hurwitzZeta (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) (-(↑k : ℂ)) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
⊢ riemannZeta (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
have inr₂ : -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 *
    Polynomial.eval (↑0 : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1))) =
  -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
Tactic: rw [← hurwitzZeta_zero, ← QuotientAddGroup.mk_zero, hurwitzZeta_neg_nat hk
      (left_mem_Icc.mpr zero_le_one), ofReal_zero, Polynomial.eval_zero_map,
      Polynomial.bernoulli_eval_zero, Algebra.algebraMap_eq_smul_one, Rat.smul_one_eq_cast,
      div_mul_eq_mul_div, neg_one_mul, bernoulli_eq_bernoulli'_of_ne_one (by simp [hk])]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
inr : hurwitzZeta 0 (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₁ :
  hurwitzZeta (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) (-(↑k : ℂ)) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₂ :
  -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 *
      Polynomial.eval (↑0 : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1))) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
⊢ riemannZeta (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
have inr₃ : -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 *
    Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1))) =
  -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
Tactic: rw [← hurwitzZeta_zero, ← QuotientAddGroup.mk_zero, hurwitzZeta_neg_nat hk
      (left_mem_Icc.mpr zero_le_one), ofReal_zero, Polynomial.eval_zero_map,
      Polynomial.bernoulli_eval_zero, Algebra.algebraMap_eq_smul_one, Rat.smul_one_eq_cast,
      div_mul_eq_mul_div, neg_one_mul, bernoulli_eq_bernoulli'_of_ne_one (by simp [hk])]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
inr : hurwitzZeta 0 (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₁ :
  hurwitzZeta (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) (-(↑k : ℂ)) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₂ :
  -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 *
      Polynomial.eval (↑0 : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1))) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₃ :
  -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 *
      Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1))) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
⊢ riemannZeta (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
have inr₄ : HMul.hMul (β := ℂ) (-1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1)
    ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) (Polynomial.eval 0 (Polynomial.bernoulli (k + 1))) : ℂ) =
  -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
Tactic: rw [← hurwitzZeta_zero, ← QuotientAddGroup.mk_zero, hurwitzZeta_neg_nat hk
      (left_mem_Icc.mpr zero_le_one), ofReal_zero, Polynomial.eval_zero_map,
      Polynomial.bernoulli_eval_zero, Algebra.algebraMap_eq_smul_one, Rat.smul_one_eq_cast,
      div_mul_eq_mul_div, neg_one_mul, bernoulli_eq_bernoulli'_of_ne_one (by simp [hk])]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
inr : hurwitzZeta 0 (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₁ :
  hurwitzZeta (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) (-(↑k : ℂ)) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₂ :
  -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 *
      Polynomial.eval (↑0 : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1))) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₃ :
  -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 *
      Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1))) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₄ :
  HMul.hMul (β := ℂ) (-1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1)
      ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) (Polynomial.eval 0 (Polynomial.bernoulli (k + 1))) : ℂ) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
⊢ riemannZeta (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
have inr₅ : HMul.hMul (β := ℂ) (-1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1) ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) (bernoulli (k + 1)) : ℂ) =
  -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
Tactic: rw [← hurwitzZeta_zero, ← QuotientAddGroup.mk_zero, hurwitzZeta_neg_nat hk
      (left_mem_Icc.mpr zero_le_one), ofReal_zero, Polynomial.eval_zero_map,
      Polynomial.bernoulli_eval_zero, Algebra.algebraMap_eq_smul_one, Rat.smul_one_eq_cast,
      div_mul_eq_mul_div, neg_one_mul, bernoulli_eq_bernoulli'_of_ne_one (by simp [hk])]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
inr : hurwitzZeta 0 (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₁ :
  hurwitzZeta (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) (-(↑k : ℂ)) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₂ :
  -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 *
      Polynomial.eval (↑0 : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1))) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₃ :
  -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 *
      Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1))) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₄ :
  HMul.hMul (β := ℂ) (-1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1)
      ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) (Polynomial.eval 0 (Polynomial.bernoulli (k + 1))) : ℂ) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₅ :
  HMul.hMul (β := ℂ) (-1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1) ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) (bernoulli (k + 1)) : ℂ) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
⊢ riemannZeta (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
have inr₆ : -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 * HSMul.hSMul (β := ℂ) (bernoulli (k + 1)) 1 =
  -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
Tactic: rw [← hurwitzZeta_zero, ← QuotientAddGroup.mk_zero, hurwitzZeta_neg_nat hk
      (left_mem_Icc.mpr zero_le_one), ofReal_zero, Polynomial.eval_zero_map,
      Polynomial.bernoulli_eval_zero, Algebra.algebraMap_eq_smul_one, Rat.smul_one_eq_cast,
      div_mul_eq_mul_div, neg_one_mul, bernoulli_eq_bernoulli'_of_ne_one (by simp [hk])]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
inr : hurwitzZeta 0 (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₁ :
  hurwitzZeta (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) (-(↑k : ℂ)) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₂ :
  -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 *
      Polynomial.eval (↑0 : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1))) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₃ :
  -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 *
      Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1))) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₄ :
  HMul.hMul (β := ℂ) (-1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1)
      ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) (Polynomial.eval 0 (Polynomial.bernoulli (k + 1))) : ℂ) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₅ :
  HMul.hMul (β := ℂ) (-1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1) ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) (bernoulli (k + 1)) : ℂ) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₆ :
  -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 * HSMul.hSMul (β := ℂ) (bernoulli (k + 1)) 1 =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
⊢ riemannZeta (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
have inr₇ : -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 * (↑(bernoulli (k + 1)) : ℂ) =
  -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
Tactic: rw [← hurwitzZeta_zero, ← QuotientAddGroup.mk_zero, hurwitzZeta_neg_nat hk
      (left_mem_Icc.mpr zero_le_one), ofReal_zero, Polynomial.eval_zero_map,
      Polynomial.bernoulli_eval_zero, Algebra.algebraMap_eq_smul_one, Rat.smul_one_eq_cast,
      div_mul_eq_mul_div, neg_one_mul, bernoulli_eq_bernoulli'_of_ne_one (by simp [hk])]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
inr : hurwitzZeta 0 (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₁ :
  hurwitzZeta (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) (-(↑k : ℂ)) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₂ :
  -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 *
      Polynomial.eval (↑0 : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1))) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₃ :
  -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 *
      Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1))) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₄ :
  HMul.hMul (β := ℂ) (-1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1)
      ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) (Polynomial.eval 0 (Polynomial.bernoulli (k + 1))) : ℂ) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₅ :
  HMul.hMul (β := ℂ) (-1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1) ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) (bernoulli (k + 1)) : ℂ) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₆ :
  -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 * HSMul.hSMul (β := ℂ) (bernoulli (k + 1)) 1 =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₇ :
  -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 * (↑(bernoulli (k + 1)) : ℂ) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
⊢ riemannZeta (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
have inr₈ : HMul.hMul (α := ℂ) (-1) (↑(bernoulli (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
  -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
Tactic: rw [← hurwitzZeta_zero, ← QuotientAddGroup.mk_zero, hurwitzZeta_neg_nat hk
      (left_mem_Icc.mpr zero_le_one), ofReal_zero, Polynomial.eval_zero_map,
      Polynomial.bernoulli_eval_zero, Algebra.algebraMap_eq_smul_one, Rat.smul_one_eq_cast,
      div_mul_eq_mul_div, neg_one_mul, bernoulli_eq_bernoulli'_of_ne_one (by simp [hk])]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
inr : hurwitzZeta 0 (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₁ :
  hurwitzZeta (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) (-(↑k : ℂ)) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₂ :
  -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 *
      Polynomial.eval (↑0 : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1))) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₃ :
  -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 *
      Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1))) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₄ :
  HMul.hMul (β := ℂ) (-1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1)
      ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) (Polynomial.eval 0 (Polynomial.bernoulli (k + 1))) : ℂ) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₅ :
  HMul.hMul (β := ℂ) (-1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1) ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) (bernoulli (k + 1)) : ℂ) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₆ :
  -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 * HSMul.hSMul (β := ℂ) (bernoulli (k + 1)) 1 =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₇ :
  -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 * (↑(bernoulli (k + 1)) : ℂ) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₈ :
  HMul.hMul (α := ℂ) (-1) (↑(bernoulli (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
⊢ riemannZeta (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
have inr₉ : -(↑(bernoulli (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
  -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
Tactic: rw [← hurwitzZeta_zero, ← QuotientAddGroup.mk_zero, hurwitzZeta_neg_nat hk
      (left_mem_Icc.mpr zero_le_one), ofReal_zero, Polynomial.eval_zero_map,
      Polynomial.bernoulli_eval_zero, Algebra.algebraMap_eq_smul_one, Rat.smul_one_eq_cast,
      div_mul_eq_mul_div, neg_one_mul, bernoulli_eq_bernoulli'_of_ne_one (by simp [hk])]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
inr : hurwitzZeta 0 (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₁ :
  hurwitzZeta (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) (-(↑k : ℂ)) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₂ :
  -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 *
      Polynomial.eval (↑0 : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1))) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₃ :
  -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 *
      Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1))) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₄ :
  HMul.hMul (β := ℂ) (-1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1)
      ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) (Polynomial.eval 0 (Polynomial.bernoulli (k + 1))) : ℂ) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₅ :
  HMul.hMul (β := ℂ) (-1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1) ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) (bernoulli (k + 1)) : ℂ) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₆ :
  -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 * HSMul.hSMul (β := ℂ) (bernoulli (k + 1)) 1 =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₇ :
  -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 * (↑(bernoulli (k + 1)) : ℂ) =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₈ :
  HMul.hMul (α := ℂ) (-1) (↑(bernoulli (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
inr₉ :
  -(↑(bernoulli (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
⊢ riemannZeta (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
have inr₁₀ : -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
  -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
Tactic: rw [← hurwitzZeta_zero, ← QuotientAddGroup.mk_zero, hurwitzZeta_neg_nat hk
      (left_mem_Icc.mpr zero_le_one), ofReal_zero, Polynomial.eval_zero_map,
      Polynomial.bernoulli_eval_zero, Algebra.algebraMap_eq_smul_one, Rat.smul_one_eq_cast,
      div_mul_eq_mul_div, neg_one_mul, bernoulli_eq_bernoulli'_of_ne_one (by simp [hk])]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
⊢ 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 * (↑(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
⊢ 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
⊢ 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 * HMul.hMul (α := ℂ) (↑(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
⊢ 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
⊢ 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]