awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this : hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) = 0
rw :
  hurwitzZetaEven (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) +
      hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    -1 / HMul.hMul (α := ℂ) 2 (↑k : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
rw₁ :
  hurwitzZetaEven (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) + 0 =
    -1 / HMul.hMul (α := ℂ) 2 (↑k : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
rw₂ :
  hurwitzZetaEven (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    -1 / HMul.hMul (α := ℂ) 2 (↑k : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
⊢ hurwitzZeta (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    -1 / HMul.hMul (α := ℂ) 2 (↑k : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
have rw₃ : -1 / HMul.hMul (α := ℂ) 2 (↑k : ℂ) *
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k))) =
  -1 / HMul.hMul (α := ℂ) 2 (↑k : ℂ) *
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
Tactic: rw [hurwitzZeta, this, add_zero, hurwitzZetaEven_one_sub_two_mul_nat hk hx]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ hurwitzZeta (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    -1 / HMul.hMul (α := ℂ) 2 (↑k : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
have suffices : hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) = 0
Tactic: suffices hurwitzZetaOdd x (1 - 2 * k) = 0 by
    rw [hurwitzZeta, this, add_zero, hurwitzZetaEven_one_sub_two_mul_nat hk hx]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) = 0
have obtain : ∀ (k : ℕ) (hk : k.succ ≠ 0),
  hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k.succ : ℂ)) = 0
Tactic: obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hk
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
k : ℕ
hk : k.succ ≠ 0
⊢ hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k.succ : ℂ)) = 0
have rw : hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - 2 * HAdd.hAdd (α := ℂ) (↑k : ℂ) 1) = 0
Tactic: rw [Nat.cast_succ, show (1 : ℂ) - 2 * (k + 1) = -2 * k - 1 by ring,
    hurwitzZetaOdd_neg_two_mul_nat_sub_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
k : ℕ
hk : k.succ ≠ 0
rw : hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - 2 * HAdd.hAdd (α := ℂ) (↑k : ℂ) 1) = 0
⊢ hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k.succ : ℂ)) = 0
have rw₁ : hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (HMul.hMul (α := ℂ) (-2) (↑k : ℂ) - 1) = 0
Tactic: rw [Nat.cast_succ, show (1 : ℂ) - 2 * (k + 1) = -2 * k - 1 by ring,
    hurwitzZetaOdd_neg_two_mul_nat_sub_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
k : ℕ
hk : k.succ ≠ 0
rw : hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - 2 * HAdd.hAdd (α := ℂ) (↑k : ℂ) 1) = 0
rw₁ : hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (HMul.hMul (α := ℂ) (-2) (↑k : ℂ) - 1) = 0
⊢ hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k.succ : ℂ)) = 0
have rw₂ : Eq (α := ℂ) 0 0
Tactic: rw [Nat.cast_succ, show (1 : ℂ) - 2 * (k + 1) = -2 * k - 1 by ring,
    hurwitzZetaOdd_neg_two_mul_nat_sub_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this : hurwitzZetaEven (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) = 0
⊢ hurwitzZeta (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    -1 / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
have rw : hurwitzZetaEven (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) +
    hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
  -1 / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) *
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
Tactic: rw [hurwitzZeta, this, zero_add, hurwitzZetaOdd_neg_two_mul_nat hk hx]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this : hurwitzZetaEven (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) = 0
rw :
  hurwitzZetaEven (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) +
      hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    -1 / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
⊢ hurwitzZeta (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    -1 / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
have rw₁ : 0 + hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
  -1 / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) *
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
Tactic: rw [hurwitzZeta, this, zero_add, hurwitzZetaOdd_neg_two_mul_nat hk hx]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this : hurwitzZetaEven (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) = 0
rw :
  hurwitzZetaEven (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) +
      hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    -1 / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
rw₁ :
  0 + hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    -1 / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
⊢ hurwitzZeta (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    -1 / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
have rw₂ : hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
  -1 / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) *
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
Tactic: rw [hurwitzZeta, this, zero_add, hurwitzZetaOdd_neg_two_mul_nat hk hx]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
this : hurwitzZetaEven (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) = 0
rw :
  hurwitzZetaEven (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) +
      hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    -1 / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
rw₁ :
  0 + hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    -1 / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
rw₂ :
  hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    -1 / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
⊢ hurwitzZeta (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    -1 / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
have rw₃ : -1 / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) *
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1))) =
  -1 / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) *
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
Tactic: rw [hurwitzZeta, this, zero_add, hurwitzZetaOdd_neg_two_mul_nat hk hx]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ hurwitzZeta (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    -1 / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
have suffices : hurwitzZetaEven (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) = 0
Tactic: suffices hurwitzZetaEven x (-(2 * k)) = 0 by
    rw [hurwitzZeta, this, zero_add, hurwitzZetaOdd_neg_two_mul_nat hk hx]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ hurwitzZetaEven (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) = 0
have obtain : ∀ (k : ℕ) (hk : k.succ ≠ 0),
  hurwitzZetaEven (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k.succ : ℂ)) = 0
Tactic: obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hk
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ hurwitzZeta (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-(↑k : ℂ)) =
    -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1)))
have inl : ∀ (n : ℕ) (hk : 2 * n ≠ 0),
  hurwitzZeta (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-(↑(2 * n) : ℂ)) =
    -1 / HAdd.hAdd (α := ℂ) (↑(2 * n) : ℂ) 1 *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * n + 1)))
Tactic: rcases Nat.even_or_odd' k with ⟨n, (rfl | rfl)⟩
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
inl :
  ∀ (n : ℕ) (hk : 2 * n ≠ 0),
    hurwitzZeta (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-(↑(2 * n) : ℂ)) =
      -1 / HAdd.hAdd (α := ℂ) (↑(2 * n) : ℂ) 1 *
        Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * n + 1)))
⊢ hurwitzZeta (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-(↑k : ℂ)) =
    -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1)))
have inr : ∀ (n : ℕ) (hk : 2 * n + 1 ≠ 0),
  hurwitzZeta (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-(↑(2 * n + 1) : ℂ)) =
    -1 / HAdd.hAdd (α := ℂ) (↑(2 * n + 1) : ℂ) 1 *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * n + 1 + 1)))
Tactic: rcases Nat.even_or_odd' k with ⟨n, (rfl | rfl)⟩
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
⊢ riemannZeta (HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    HPow.hPow (α := ℂ) (-1) (k + 1) * HPow.hPow (α := ℂ) 2 (2 * k - 1) * (↑π : ℂ) ^ (2 * k) *
        (↑(bernoulli (2 * k)) : ℂ) /
      (↑(2 * k)! : ℂ)
have h : riemannZeta (HMul.hMul (α := ℂ) 2 (↑k : ℂ)) = (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 * k)) : ℂ)
Tactic: convert! congr_arg ((↑) : ℝ → ℂ) (hasSum_zeta_nat hk).tsum_eq
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
h : riemannZeta (HMul.hMul (α := ℂ) 2 (↑k : ℂ)) = (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 * k)) : ℂ)
⊢ riemannZeta (HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    HPow.hPow (α := ℂ) (-1) (k + 1) * HPow.hPow (α := ℂ) 2 (2 * k - 1) * (↑π : ℂ) ^ (2 * k) *
        (↑(bernoulli (2 * k)) : ℂ) /
      (↑(2 * k)! : ℂ)
have h₁ : HPow.hPow (α := ℂ) (-1) (k + 1) * HPow.hPow (α := ℂ) 2 (2 * k - 1) * (↑π : ℂ) ^ (2 * k) * (↑(bernoulli (2 * k)) : ℂ) /
    (↑(2 * k)! : ℂ) =
  (↑(HPow.hPow (α := ℝ) (-1) (k + 1) * HPow.hPow (α := ℝ) 2 (2 * k - 1) * π ^ (2 * k) * (↑(bernoulli (2 * k)) : ℝ) /
        (↑(2 * k)! : ℝ)) :
    ℂ)
Tactic: convert! congr_arg ((↑) : ℝ → ℂ) (hasSum_zeta_nat hk).tsum_eq
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
⊢ riemannZeta (HMul.hMul (α := ℂ) 2 (↑k : ℂ)) = (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 * k)) : ℂ)
have h : ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k) = (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 * k)) : ℂ)
Tactic: rw [← Nat.cast_two, ← Nat.cast_mul, zeta_nat_eq_tsum_of_gt_one (by lia)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 0
⊢ HPow.hPow (α := ℂ) (-1) (k + 1) * HPow.hPow (α := ℂ) 2 (2 * k - 1) * (↑π : ℂ) ^ (2 * k) * (↑(bernoulli (2 * k)) : ℂ) /
      (↑(2 * k)! : ℂ) =
    (↑(HPow.hPow (α := ℝ) (-1) (k + 1) * HPow.hPow (α := ℝ) 2 (2 * k - 1) * π ^ (2 * k) * (↑(bernoulli (2 * k)) : ℝ) /
          (↑(2 * k)! : ℝ)) :
      ℂ)
have h : (↑(Int.negSucc 0 ^ (k + 1) * (↑(HPow.hPow (α := ℕ) 2 (2 * k - 1)) : ℤ)) : ℝ) * π ^ (2 * k) *
      (↑(bernoulli (2 * k)) : ℝ) /
    (↑(2 * k)! : ℝ) =
  (↑(Int.negSucc 0 ^ (k + 1) * (↑(HPow.hPow (α := ℕ) 2 (2 * k - 1)) : ℤ)) : ℝ) * π ^ (2 * k) *
      (↑(bernoulli (2 * k)) : ℝ) /
    (↑(2 * k)! : ℝ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
⊢ riemannZeta 2 = HPow.hPow (β := ℕ) (↑π : ℂ) 2 / 6
have h : riemannZeta 2 = (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 2) : ℂ)
Tactic: convert! congr_arg ((↑) : ℝ → ℂ) hasSum_zeta_two.tsum_eq
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
h : riemannZeta 2 = (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 2) : ℂ)
⊢ riemannZeta 2 = HPow.hPow (β := ℕ) (↑π : ℂ) 2 / 6
have h₁ : HPow.hPow (β := ℕ) (↑π : ℂ) 2 / 6 = (↑(HPow.hPow (β := ℕ) π 2 / 6) : ℂ)
Tactic: convert! congr_arg ((↑) : ℝ → ℂ) hasSum_zeta_two.tsum_eq
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
⊢ riemannZeta 2 = (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 2) : ℂ)
have h : ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 = (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 2) : ℂ)
Tactic: rw [← Nat.cast_two, zeta_nat_eq_tsum_of_gt_one one_lt_two]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
⊢ HPow.hPow (β := ℕ) (↑π : ℂ) 2 / 6 = (↑(HPow.hPow (β := ℕ) π 2 / 6) : ℂ)
have h : HPow.hPow (β := ℕ) π 2 / 6 = HPow.hPow (β := ℕ) π 2 / 6
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
⊢ riemannZeta 4 = HPow.hPow (β := ℕ) (↑π : ℂ) 4 / 90
have h : riemannZeta 4 = (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 4) : ℂ)
Tactic: convert! congr_arg ((↑) : ℝ → ℂ) hasSum_zeta_four.tsum_eq
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
h : riemannZeta 4 = (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 4) : ℂ)
⊢ riemannZeta 4 = HPow.hPow (β := ℕ) (↑π : ℂ) 4 / 90
have h₁ : HPow.hPow (β := ℕ) (↑π : ℂ) 4 / 90 = (↑(HPow.hPow (β := ℕ) π 4 / 90) : ℂ)
Tactic: convert! congr_arg ((↑) : ℝ → ℂ) hasSum_zeta_four.tsum_eq
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
⊢ riemannZeta 4 = (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 4) : ℂ)
have h : ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 4 =
  (↑(∑' (b : ℕ), (↑1 : ℝ) / HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 4) : ℂ)
Tactic: rw [← Nat.cast_one, show (4 : ℂ) = (4 : ℕ) by simp,
      zeta_nat_eq_tsum_of_gt_one (by simp : 1 < 4)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
⊢ HPow.hPow (β := ℕ) (↑π : ℂ) 4 / 90 = (↑(HPow.hPow (β := ℕ) π 4 / 90) : ℂ)
have h : HPow.hPow (β := ℕ) π 4 / 90 = HPow.hPow (β := ℕ) π 4 / 90
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
⊢ riemannZeta (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
have inl : riemannZeta (-(↑0 : ℂ)) = -(↑(bernoulli' (HAdd.hAdd (α := ℕ) 0 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1
Tactic: rcases eq_or_ne k 0 with rfl | hk
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
inl : riemannZeta (-(↑0 : ℂ)) = -(↑(bernoulli' (HAdd.hAdd (α := ℕ) 0 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1
⊢ riemannZeta (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
have inr : ∀ (hk : k ≠ 0), riemannZeta (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
Tactic: rcases eq_or_ne k 0 with rfl | hk
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
⊢ riemannZeta (-(↑0 : ℂ)) = -(↑(bernoulli' (HAdd.hAdd (α := ℕ) 0 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1
have inl : riemannZeta (-0) = -(↑(bernoulli' (HAdd.hAdd (α := ℕ) 0 1)) : ℂ) / HAdd.hAdd (α := ℂ) 0 1
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
⊢ riemannZeta (-(↑0 : ℂ)) = -(↑(bernoulli' (HAdd.hAdd (α := ℕ) 0 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1
have inl₁ : riemannZeta 0 = -(↑(bernoulli' (HAdd.hAdd (α := ℕ) 0 1)) : ℂ) / HAdd.hAdd (α := ℂ) 0 1
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
⊢ riemannZeta (-(↑0 : ℂ)) = -(↑(bernoulli' (HAdd.hAdd (α := ℕ) 0 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1
have inl₂ : -1 / 2 = -(↑(bernoulli' (HAdd.hAdd (α := ℕ) 0 1)) : ℂ) / HAdd.hAdd (α := ℂ) 0 1
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
⊢ riemannZeta (-(↑0 : ℂ)) = -(↑(bernoulli' (HAdd.hAdd (α := ℕ) 0 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1
have inl₄ : -1 / 2 = HDiv.hDiv (α := ℂ) (-(↑(bernoulli' 1) : ℂ)) 1
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
⊢ riemannZeta (-(↑0 : ℂ)) = -(↑(bernoulli' (HAdd.hAdd (α := ℕ) 0 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1
have inl₅ : -1 / 2 = -(↑(bernoulli' 1) : ℂ)
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) : ℂ)
⊢ riemannZeta (-(↑0 : ℂ)) = -(↑(bernoulli' (HAdd.hAdd (α := ℕ) 0 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1
have inl₆ : -1 / 2 = -(↑(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) : ℂ)
⊢ 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 : ℂ)
⊢ 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]