awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1 ≠ -(↑n : ℂ)
refine : (2 * (↑π : ℂ)) ^ (-(HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1)) ≠ 0
⊢ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).Gammaℂ ≠ 0

Tactic:
refine mul_ne_zero (mul_ne_zero two_ne_zero ?_) (Gamma_ne_zero h1)

Premises used: two_ne_zero, mul_ne_zero, Complex.Gamma_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1 ≠ -(↑n : ℂ)
⊢ (2 * (↑π : ℂ)) ^ (-(HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1)) ≠ 0

Tactic:
simp [pi_ne_zero]

Premises used: Real.pi_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1 ≠ -(↑n : ℂ)
⊢ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).Gammaℂ ≠ 0

Tactic:
have h3 : Gammaℂ (2 * k + 1) ≠ 0 := by
    refine mul_ne_zero (mul_ne_zero two_ne_zero ?_) (Gamma_ne_zero h1)
    simp [pi_ne_zero]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1 ≠ -(↑n : ℂ)
h3 : (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).Gammaℂ ≠ 0
⊢ -HMul.hMul (α := ℂ) 2 (↑k : ℂ) = 1 - (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1 ≠ -(↑n : ℂ)
h3 : (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).Gammaℂ ≠ 0
rw :
  Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2) * HPow.hPow (α := ℂ) (-1) (k + 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)))
⊢ 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 [(by simp : -(2 * k : ℂ) = 1 - (2 * k + 1)),
    hurwitzZetaOdd_one_sub _ h1, ← Gammaℂ, sinZeta_two_mul_nat_add_one' hk hx, ← mul_assoc,
    ← mul_div_assoc, mul_assoc, mul_div_cancel_left₀ _ h3, ← mul_div_assoc]

Premises used: Complex.Gammaℂ, mul_assoc, mul_div_assoc, mul_div_cancel_left₀, HurwitzZeta.sinZeta_two_mul_nat_add_one', HurwitzZeta.hurwitzZetaOdd_one_sub
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1 ≠ -(↑n : ℂ)
h3 : (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).Gammaℂ ≠ 0
e_a : Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
⊢ Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2) * HPow.hPow (α := ℂ) (-1) (k + 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:
congr 2
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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)))
rw₃ 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)))
⊢ 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)))

Tactic:
rw [hurwitzZeta, this, add_zero, hurwitzZetaEven_one_sub_two_mul_nat hk hx]

Premises used: HurwitzZeta.hurwitzZetaEven_one_sub_two_mul_nat, HurwitzZeta.hurwitzZeta, add_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
suffices : hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) = 0
⊢ 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)))

Tactic:
suffices hurwitzZetaOdd x (1 - 2 * k) = 0 by
    rw [hurwitzZeta, this, add_zero, hurwitzZetaEven_one_sub_two_mul_nat hk hx]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
obtain :
  ∀ (k : ℕ) (hk : k.succ ≠ 0),
    hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k.succ : ℂ)) = 0
⊢ hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k : ℂ)) = 0

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hk

Premises used: Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
k : ℕ
hk : k.succ ≠ 0
⊢ 1 - 2 * HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 = HMul.hMul (α := ℂ) (-2) (↑k : ℂ) - 1

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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
rw₂ rw₃ : Eq (α := ℂ) 0 0
⊢ hurwitzZetaOdd (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (1 - HMul.hMul (α := ℂ) 2 (↑k.succ : ℂ)) = 0

Tactic:
rw [Nat.cast_succ, show (1 : ℂ) - 2 * (k + 1) = -2 * k - 1 by ring,
    hurwitzZetaOdd_neg_two_mul_nat_sub_one]

Premises used: Nat.cast_succ, HurwitzZeta.hurwitzZetaOdd_neg_two_mul_nat_sub_one
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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)))
rw₃ 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)))
⊢ 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)))

Tactic:
rw [hurwitzZeta, this, zero_add, hurwitzZetaOdd_neg_two_mul_nat hk hx]

Premises used: HurwitzZeta.hurwitzZetaOdd_neg_two_mul_nat, zero_add, HurwitzZeta.hurwitzZeta
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
suffices : 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)))

Tactic:
suffices hurwitzZetaEven x (-(2 * k)) = 0 by
    rw [hurwitzZeta, this, zero_add, hurwitzZetaOdd_neg_two_mul_nat hk hx]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
obtain :
  ∀ (k : ℕ) (hk : k.succ ≠ 0),
    hurwitzZetaEven (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k.succ : ℂ)) = 0
⊢ hurwitzZetaEven (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) = 0

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hk

Premises used: Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
k : ℕ
hk : k.succ ≠ 0
⊢ hurwitzZetaEven (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-HMul.hMul (α := ℂ) 2 (↑k.succ : ℂ)) = 0

Tactic:
simpa using hurwitzZetaEven_neg_two_mul_nat_add_one x k

Premises used: HurwitzZeta.hurwitzZetaEven_neg_two_mul_nat_add_one, QuotientAddGroup.mk
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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)))
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)))
⊢ hurwitzZeta (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (-(↑k : ℂ)) =
    -1 / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1)))

Tactic:
rcases Nat.even_or_odd' k with ⟨n, (rfl | rfl)⟩

Premises used: Nat.even_or_odd', rfl
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
hk : 2 * n ≠ 0
⊢ n ≠ 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
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:
exact_mod_cast hurwitzZeta_neg_two_mul_nat (by lia : n ≠ 0) hx

Premises used: _private.0.HurwitzZeta.hurwitzZeta_neg_two_mul_nat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
hk : 2 * n + 1 ≠ 0
⊢ n + 1 ≠ 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
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:
exact_mod_cast hurwitzZeta_one_sub_two_mul_nat (by lia : n + 1 ≠ 0) hx

Premises used: _private.0.HurwitzZeta.hurwitzZeta_one_sub_two_mul_nat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
hk : k ≠ 0
⊢ (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 * k)) : ℂ) =
    (↑(HPow.hPow (α := ℝ) (-1) (k + 1) * HPow.hPow (α := ℝ) 2 (2 * k - 1) * π ^ (2 * k) * (↑(bernoulli (2 * k)) : ℝ) /
          (↑(2 * k)! : ℝ)) :
      ℂ)

Tactic:
congr_arg ((↑) : ℝ → ℂ) (hasSum_zeta_nat hk).tsum_eq

Premises used: Complex.ofReal, congr_arg, HasSum.tsum_eq, hasSum_zeta_nat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
hk : k ≠ 0
h : riemannZeta (HMul.hMul (α := ℂ) 2 (↑k : ℂ)) = (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 * k)) : ℂ)
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)! : ℝ)) :
      ℂ)
⊢ riemannZeta (HMul.hMul (α := ℂ) 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

Premises used: Complex.ofReal, congr_arg, HasSum.tsum_eq, hasSum_zeta_nat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
hk : k ≠ 0
⊢ 1 < 2 * k

Tactic:
lia
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
hk : k ≠ 0
h : ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k) = (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 * k)) : ℂ)
⊢ riemannZeta (HMul.hMul (α := ℂ) 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)]

Premises used: Nat.cast_mul, zeta_nat_eq_tsum_of_gt_one, Nat.cast_two
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
hk : k ≠ 0
⊢ ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (↑n : ℂ) (2 * k) = (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 * k)) : ℂ)

Tactic:
simp [push_cast]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
hk : k ≠ 0
h h₁ h₂ 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)! : ℝ)
⊢ 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:
norm_cast
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
⊢ (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 2) : ℂ) = (↑(HPow.hPow (β := ℕ) π 2 / 6) : ℂ)

Tactic:
congr_arg ((↑) : ℝ → ℂ) hasSum_zeta_two.tsum_eq

Premises used: Complex.ofReal, congr_arg, HasSum.tsum_eq, hasSum_zeta_two
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
h : riemannZeta 2 = (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 2) : ℂ)
h₁ : HPow.hPow (β := ℕ) (↑π : ℂ) 2 / 6 = (↑(HPow.hPow (β := ℕ) π 2 / 6) : ℂ)
⊢ riemannZeta 2 = HPow.hPow (β := ℕ) (↑π : ℂ) 2 / 6

Tactic:
convert! congr_arg ((↑) : ℝ → ℂ) hasSum_zeta_two.tsum_eq

Premises used: Complex.ofReal, congr_arg, HasSum.tsum_eq, hasSum_zeta_two
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
h :
  ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 =
    (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 2) : ℂ)
⊢ riemannZeta 2 = (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 2) : ℂ)

Tactic:
rw [← Nat.cast_two, zeta_nat_eq_tsum_of_gt_one one_lt_two]

Premises used: one_lt_two, zeta_nat_eq_tsum_of_gt_one, Nat.cast_two
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
⊢ ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 =
    (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 2) : ℂ)

Tactic:
simp [push_cast]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
h h₁ h₂ h₃ : HPow.hPow (β := ℕ) π 2 / 6 = HPow.hPow (β := ℕ) π 2 / 6
⊢ HPow.hPow (β := ℕ) (↑π : ℂ) 2 / 6 = (↑(HPow.hPow (β := ℕ) π 2 / 6) : ℂ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
⊢ (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 4) : ℂ) = (↑(HPow.hPow (β := ℕ) π 4 / 90) : ℂ)

Tactic:
congr_arg ((↑) : ℝ → ℂ) hasSum_zeta_four.tsum_eq

Premises used: hasSum_zeta_four, Complex.ofReal, congr_arg, HasSum.tsum_eq
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
h : riemannZeta 4 = (↑(∑' (b : ℕ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 4) : ℂ)
h₁ : HPow.hPow (β := ℕ) (↑π : ℂ) 4 / 90 = (↑(HPow.hPow (β := ℕ) π 4 / 90) : ℂ)
⊢ riemannZeta 4 = HPow.hPow (β := ℕ) (↑π : ℂ) 4 / 90

Tactic:
convert! congr_arg ((↑) : ℝ → ℂ) hasSum_zeta_four.tsum_eq

Premises used: hasSum_zeta_four, Complex.ofReal, congr_arg, HasSum.tsum_eq
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
⊢ Eq (α := ℂ) 4 (↑4 : ℂ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
⊢ LT.lt (α := ℕ) 1 4

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
h :
  ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 4 =
    (↑(∑' (b : ℕ), (↑1 : ℝ) / HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 4) : ℂ)
⊢ riemannZeta 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)]

Premises used: zeta_nat_eq_tsum_of_gt_one, Nat.cast_one
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
⊢ ∑' (n : ℕ), 1 / HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 4 =
    (↑(∑' (b : ℕ), (↑1 : ℝ) / HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 4) : ℂ)

Tactic:
simp only [push_cast]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
h h₁ h₂ h₃ : HPow.hPow (β := ℕ) π 4 / 90 = HPow.hPow (β := ℕ) π 4 / 90
⊢ HPow.hPow (β := ℕ) (↑π : ℂ) 4 / 90 = (↑(HPow.hPow (β := ℕ) π 4 / 90) : ℂ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
inl : riemannZeta (-(↑0 : ℂ)) = -(↑(bernoulli' (HAdd.hAdd (α := ℕ) 0 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1
inr : ∀ (hk : k ≠ 0), riemannZeta (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
⊢ riemannZeta (-(↑k : ℂ)) = -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1

Tactic:
rcases eq_or_ne k 0 with rfl | hk

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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
inl₁₀ inl₁₁ : -(1 / 2) = -HDiv.hDiv (α := ℂ) 1 2
⊢ 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]

Premises used: neg_div, riemannZeta_zero, Rat.cast_div, zero_add, Rat.cast_ofNat, bernoulli'_one, Nat.cast_zero, neg_zero, div_one, Rat.cast_one
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
hk : k ≠ 0
⊢ k + 1 ≠ 1

Tactic:
simp [hk]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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
inr₁₀ inr₁₁ :
  -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1 =
    -(↑(bernoulli' (k + 1)) : ℂ) / HAdd.hAdd (α := ℂ) (↑k : ℂ) 1
⊢ riemannZeta (-(↑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])]

Premises used: Iff.mpr, Polynomial.bernoulli_eval_zero, neg_one_mul, HurwitzZeta.hurwitzZeta_neg_nat, div_mul_eq_mul_div, zero_le_one, Algebra.algebraMap_eq_smul_one, Complex.ofReal_zero, QuotientAddGroup.mk_zero, Polynomial.eval_zero_map, Set.left_mem_Icc, Rat.smul_one_eq_cast, HurwitzZeta.hurwitzZeta_zero, bernoulli_eq_bernoulli'_of_ne_one
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
⊢ abscissaOfAbsConv (f + g) ≤ max (abscissaOfAbsConv f) (abscissaOfAbsConv g)

Tactic:
abscissaOfAbsConv_binop_le LSeriesSummable.add f g

Premises used: LSeries.abscissaOfAbsConv_binop_le, LSeriesSummable.add
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
f g : ℕ → ℂ
⊢ abscissaOfAbsConv (f - g) ≤ max (abscissaOfAbsConv f) (abscissaOfAbsConv g)

Tactic:
abscissaOfAbsConv_binop_le LSeriesSummable.sub f g

Premises used: LSeries.abscissaOfAbsConv_binop_le, LSeriesSummable.sub
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
m n : ℕ
z : ℂ
x : ℝ
⊢ 0 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹

Tactic:
positivity
-- Module: Mathlib.NumberTheory.LSeries.Injectivity
Goal:
m n : ℕ
z : ℂ
x : ℝ
⊢ 0 ≤ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹

Tactic:
have Hn : (0 : ℝ) ≤ (n + 1 : ℝ)⁻¹ := by positivity