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
rw : HMul.hMul (α := ℂ) 2 (↑k : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1
rw₁ :
  (↑(2 * k)! : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1 * Complex.Gamma (HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1)
rw₂ : (↑(2 * k)! : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1 * (↑(2 * k - 1)! : ℂ)
rw₃ : (↑(2 * k)! : ℂ) = HMul.hMul (α := ℂ) (↑(2 * k - 1 + 1) : ℂ) (↑(2 * k - 1)! : ℂ)
rw₄ : Eq (α := ℂ) (↑(2 * k)! : ℂ) (↑((2 * k - 1 + 1) * (2 * k - 1)!) : ℂ)
rw₅ : Eq (α := ℂ) (↑(2 * k)! : ℂ) (↑(2 * k - 1 + 1)! : ℂ)
⊢ (↑(2 * k)! : ℂ) = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ))
have rw₆ : Eq (α := ℂ) (↑(2 * k)! : ℂ) (↑(2 * k)! : ℂ)
Tactic: rw [(by { norm_cast; lia } : 2 * (k : ℂ) = ↑(2 * k - 1) + 1), Complex.Gamma_nat_eq_factorial,
      ← Nat.cast_add_one, ← Nat.cast_mul, ← Nat.factorial_succ, Nat.sub_add_cancel (by lia)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (hypothesis)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / 2 / (↑(2 * k)! : ℂ) =
    HPow.hPow (α := ℂ) (-1) (k + 1) / HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (HMul.hMul (α := ℂ) 2 (↑k : ℂ)).Gammaℂ
have this : (↑(2 * k)! : ℂ) = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ))
Tactic: have : (2 * k)! = (2 * k) * Complex.Gamma (2 * k) := by
    rw [(by { norm_cast; lia } : 2 * (k : ℂ) = ↑(2 * k - 1) + 1), Complex.Gamma_nat_eq_factorial,
      ← Nat.cast_add_one, ← Nat.cast_mul, ← Nat.factorial_succ, Nat.sub_add_cancel (by lia)]
-- 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 : (↑(2 * k)! : ℂ) = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ))
⊢ HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / 2 / (↑(2 * k)! : ℂ) =
    HPow.hPow (α := ℂ) (-1) (k + 1) / HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (HMul.hMul (α := ℂ) 2 (↑k : ℂ)).Gammaℂ
have e_a : HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) /
    (HMul.hMul (α := ℂ) 2 2 * (↑k : ℂ) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ))) =
  HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ HMul.hMul (α := ℂ) 2 (↑k : ℂ) /
    (HMul.hMul (α := ℂ) 2 2 * (↑k : ℂ) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ)))
Tactic: simp_rw [this, Gammaℂ, cpow_neg, ← div_div, div_inv_eq_mul, div_mul_eq_mul_div, div_div,
    mul_right_comm (2 : ℂ) (k : ℂ)]
-- 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 : (↑(2 * k)! : ℂ) = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ))
⊢ HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) /
      (HMul.hMul (α := ℂ) 2 2 * (↑k : ℂ) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ))) =
    HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ HMul.hMul (α := ℂ) 2 (↑k : ℂ) /
      (HMul.hMul (α := ℂ) 2 2 * (↑k : ℂ) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ)))
have e_a : (↑((↑(Int.negSucc 0 ^ (k + 1)) : ℝ) * (2 * π) ^ (2 * k)) : ℂ) /
    ((↑(HMul.hMul (α := ℕ) 2 2 * k) : ℂ) * Complex.Gamma (↑(2 * k) : ℂ)) =
  (↑((↑(Int.negSucc 0 ^ (k + 1)) : ℝ) * (2 * π) ^ (2 * k)) : ℂ) /
    ((↑(HMul.hMul (α := ℕ) 2 2 * k) : ℂ) * Complex.Gamma (↑(2 * k) : ℂ))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ sinZeta (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) =
    HPow.hPow (α := ℂ) (-1) (k + 1) / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).Gammaℂ *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
have rw : HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k + 1) / 2 / (↑(2 * k + 1)! : ℂ) *
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1))) =
  HPow.hPow (α := ℂ) (-1) (k + 1) / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).Gammaℂ *
    Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
Tactic: rw [sinZeta_two_mul_nat_add_one 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
⊢ HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k + 1) / 2 / (↑(2 * k + 1)! : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1))) =
    HPow.hPow (α := ℂ) (-1) (k + 1) / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).Gammaℂ *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
have e_a : HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k + 1) / 2 / (↑(2 * k + 1)! : ℂ) =
  HPow.hPow (α := ℂ) (-1) (k + 1) / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).Gammaℂ
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1)
have rw : Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) = Complex.Gamma (HAdd.hAdd (α := ℂ) (↑(2 * k) : ℂ) 1)
Tactic: rw [(by simp : Complex.Gamma (2 * k + 1) = Complex.Gamma (↑(2 * k) + 1)),
       Complex.Gamma_nat_eq_factorial, ← Nat.cast_ofNat (R := ℂ), ← Nat.cast_mul,
      ← Nat.cast_add_one, ← Nat.cast_mul, ← Nat.factorial_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
rw : Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) = Complex.Gamma (HAdd.hAdd (α := ℂ) (↑(2 * k) : ℂ) 1)
⊢ (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1)
have rw₁ : (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * Complex.Gamma (HAdd.hAdd (α := ℂ) (↑(2 * k) : ℂ) 1)
Tactic: rw [(by simp : Complex.Gamma (2 * k + 1) = Complex.Gamma (↑(2 * k) + 1)),
       Complex.Gamma_nat_eq_factorial, ← Nat.cast_ofNat (R := ℂ), ← Nat.cast_mul,
      ← Nat.cast_add_one, ← Nat.cast_mul, ← Nat.factorial_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
rw : Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) = Complex.Gamma (HAdd.hAdd (α := ℂ) (↑(2 * k) : ℂ) 1)
rw₁ : (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * Complex.Gamma (HAdd.hAdd (α := ℂ) (↑(2 * k) : ℂ) 1)
⊢ (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1)
have rw₂ : (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑(2 * k)! : ℂ)
Tactic: rw [(by simp : Complex.Gamma (2 * k + 1) = Complex.Gamma (↑(2 * k) + 1)),
       Complex.Gamma_nat_eq_factorial, ← Nat.cast_ofNat (R := ℂ), ← Nat.cast_mul,
      ← Nat.cast_add_one, ← Nat.cast_mul, ← Nat.factorial_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
rw : Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) = Complex.Gamma (HAdd.hAdd (α := ℂ) (↑(2 * k) : ℂ) 1)
rw₁ : (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * Complex.Gamma (HAdd.hAdd (α := ℂ) (↑(2 * k) : ℂ) 1)
rw₂ : (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑(2 * k)! : ℂ)
⊢ (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1)
have rw₃ : (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) (↑2 : ℂ) (↑k : ℂ) + 1) * (↑(2 * k)! : ℂ)
Tactic: rw [(by simp : Complex.Gamma (2 * k + 1) = Complex.Gamma (↑(2 * k) + 1)),
       Complex.Gamma_nat_eq_factorial, ← Nat.cast_ofNat (R := ℂ), ← Nat.cast_mul,
      ← Nat.cast_add_one, ← Nat.cast_mul, ← Nat.factorial_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
rw : Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) = Complex.Gamma (HAdd.hAdd (α := ℂ) (↑(2 * k) : ℂ) 1)
rw₁ : (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * Complex.Gamma (HAdd.hAdd (α := ℂ) (↑(2 * k) : ℂ) 1)
rw₂ : (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑(2 * k)! : ℂ)
rw₃ : (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) (↑2 : ℂ) (↑k : ℂ) + 1) * (↑(2 * k)! : ℂ)
⊢ (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1)
have rw₄ : (↑(2 * k + 1)! : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k) : ℂ) 1 * (↑(2 * k)! : ℂ)
Tactic: rw [(by simp : Complex.Gamma (2 * k + 1) = Complex.Gamma (↑(2 * k) + 1)),
       Complex.Gamma_nat_eq_factorial, ← Nat.cast_ofNat (R := ℂ), ← Nat.cast_mul,
      ← Nat.cast_add_one, ← Nat.cast_mul, ← Nat.factorial_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
rw : Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) = Complex.Gamma (HAdd.hAdd (α := ℂ) (↑(2 * k) : ℂ) 1)
rw₁ : (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * Complex.Gamma (HAdd.hAdd (α := ℂ) (↑(2 * k) : ℂ) 1)
rw₂ : (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑(2 * k)! : ℂ)
rw₃ : (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) (↑2 : ℂ) (↑k : ℂ) + 1) * (↑(2 * k)! : ℂ)
rw₄ : (↑(2 * k + 1)! : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k) : ℂ) 1 * (↑(2 * k)! : ℂ)
⊢ (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1)
have rw₅ : (↑(2 * k + 1)! : ℂ) = HMul.hMul (α := ℂ) (↑(2 * k + 1) : ℂ) (↑(2 * k)! : ℂ)
Tactic: rw [(by simp : Complex.Gamma (2 * k + 1) = Complex.Gamma (↑(2 * k) + 1)),
       Complex.Gamma_nat_eq_factorial, ← Nat.cast_ofNat (R := ℂ), ← Nat.cast_mul,
      ← Nat.cast_add_one, ← Nat.cast_mul, ← Nat.factorial_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
rw : Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) = Complex.Gamma (HAdd.hAdd (α := ℂ) (↑(2 * k) : ℂ) 1)
rw₁ : (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * Complex.Gamma (HAdd.hAdd (α := ℂ) (↑(2 * k) : ℂ) 1)
rw₂ : (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑(2 * k)! : ℂ)
rw₃ : (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) (↑2 : ℂ) (↑k : ℂ) + 1) * (↑(2 * k)! : ℂ)
rw₄ : (↑(2 * k + 1)! : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k) : ℂ) 1 * (↑(2 * k)! : ℂ)
rw₅ : (↑(2 * k + 1)! : ℂ) = HMul.hMul (α := ℂ) (↑(2 * k + 1) : ℂ) (↑(2 * k)! : ℂ)
⊢ (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1)
have rw₆ : Eq (α := ℂ) (↑(2 * k + 1)! : ℂ) (↑((2 * k + 1) * (2 * k)!) : ℂ)
Tactic: rw [(by simp : Complex.Gamma (2 * k + 1) = Complex.Gamma (↑(2 * k) + 1)),
       Complex.Gamma_nat_eq_factorial, ← Nat.cast_ofNat (R := ℂ), ← Nat.cast_mul,
      ← Nat.cast_add_one, ← Nat.cast_mul, ← Nat.factorial_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
rw : Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) = Complex.Gamma (HAdd.hAdd (α := ℂ) (↑(2 * k) : ℂ) 1)
rw₁ : (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * Complex.Gamma (HAdd.hAdd (α := ℂ) (↑(2 * k) : ℂ) 1)
rw₂ : (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑(2 * k)! : ℂ)
rw₃ : (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) (↑2 : ℂ) (↑k : ℂ) + 1) * (↑(2 * k)! : ℂ)
rw₄ : (↑(2 * k + 1)! : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k) : ℂ) 1 * (↑(2 * k)! : ℂ)
rw₅ : (↑(2 * k + 1)! : ℂ) = HMul.hMul (α := ℂ) (↑(2 * k + 1) : ℂ) (↑(2 * k)! : ℂ)
rw₆ : Eq (α := ℂ) (↑(2 * k + 1)! : ℂ) (↑((2 * k + 1) * (2 * k)!) : ℂ)
⊢ (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1)
have rw₇ : Eq (α := ℂ) (↑(2 * k + 1)! : ℂ) (↑(2 * k + 1)! : ℂ)
Tactic: rw [(by simp : Complex.Gamma (2 * k + 1) = Complex.Gamma (↑(2 * k) + 1)),
       Complex.Gamma_nat_eq_factorial, ← Nat.cast_ofNat (R := ℂ), ← Nat.cast_mul,
      ← Nat.cast_add_one, ← Nat.cast_mul, ← Nat.factorial_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (hypothesis)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k + 1) / 2 / (↑(2 * k + 1)! : ℂ) =
    HPow.hPow (α := ℂ) (-1) (k + 1) / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).Gammaℂ
have this : (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1)
Tactic: have : (2 * k + 1)! = (2 * k + 1) * Complex.Gamma (2 * k + 1) := by
    rw [(by simp : Complex.Gamma (2 * k + 1) = Complex.Gamma (↑(2 * k) + 1)),
       Complex.Gamma_nat_eq_factorial, ← Nat.cast_ofNat (R := ℂ), ← Nat.cast_mul,
      ← Nat.cast_add_one, ← Nat.cast_mul, ← Nat.factorial_succ]
-- 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 : (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1)
⊢ HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k + 1) / 2 / (↑(2 * k + 1)! : ℂ) =
    HPow.hPow (α := ℂ) (-1) (k + 1) / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).Gammaℂ
have e_a : HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k + 1) /
    (2 * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1)) =
  HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) /
    ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * 2 * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1))
Tactic: simp_rw [this, Gammaℂ, cpow_neg, ← div_div, div_inv_eq_mul, div_mul_eq_mul_div, div_div]
-- 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 : (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1)
⊢ HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k + 1) /
      (2 * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1)) =
    HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) /
      ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * 2 * Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1))
have e_a : HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k + 1) /
    (HMul.hMul (α := ℂ) 2 (↑(2 * k + 1) : ℂ) * Complex.Gamma (↑(2 * k + 1) : ℂ)) =
  HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k + 1) /
    (HMul.hMul (α := ℂ) (↑(2 * k + 1) : ℂ) 2 * Complex.Gamma (↑(2 * k + 1) : ℂ))
Tactic: rw [(by simp : 2 * (k : ℂ) + 1 = ↑(2 * k + 1)), cpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
⊢ HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ -(↑n : ℂ)
have rw : HMul.hMul (α := ℤ) 2 (↑k : ℤ) ≠ -(↑n : ℤ)
Tactic: rw [← Int.cast_ofNat, ← Int.cast_natCast, ← Int.cast_mul, ← Int.cast_natCast n, ← Int.cast_neg,
      Ne, Int.cast_inj, ← Ne]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
⊢ HMul.hMul (α := ℤ) 2 (↑k : ℤ) ≠ -(↑n : ℤ)
have refine : LT.lt (α := ℤ) 0 (↑k : ℤ)
Tactic: refine ne_of_gt ((neg_nonpos_of_nonneg n.cast_nonneg).trans_lt (mul_pos two_pos ?_))
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (hypothesis)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ 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)))
have h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ -(↑n : ℂ)
Tactic: have h1 (n : ℕ) : (2 * k : ℂ) ≠ -n := by
    rw [← Int.cast_ofNat, ← Int.cast_natCast, ← Int.cast_mul, ← Int.cast_natCast n, ← Int.cast_neg,
      Ne, Int.cast_inj, ← Ne]
    refine ne_of_gt ((neg_nonpos_of_nonneg n.cast_nonneg).trans_lt (mul_pos two_pos ?_))
    exact Nat.cast_pos.mpr (Nat.pos_of_ne_zero 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
h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ -(↑n : ℂ)
⊢ HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ 1
have norm_cast : ¬2 * k = 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (hypothesis)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ -(↑n : ℂ)
⊢ 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)))
have h2 : HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ 1
Tactic: have h2 : (2 * k : ℂ) ≠ 1 := by norm_cast; simp
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ -(↑n : ℂ)
h2 : HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ 1
⊢ (HMul.hMul (α := ℂ) 2 (↑k : ℂ)).Gammaℂ ≠ 0
have refine : (2 * (↑π : ℂ)) ^ (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) ≠ 0
Tactic: refine mul_ne_zero (mul_ne_zero two_ne_zero ?_) (Gamma_ne_zero h1)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (hypothesis)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ -(↑n : ℂ)
h2 : HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ 1
⊢ 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)))
have h3 : (HMul.hMul (α := ℂ) 2 (↑k : ℂ)).Gammaℂ ≠ 0
Tactic: have h3 : Gammaℂ (2 * k) ≠ 0 := by
    refine mul_ne_zero (mul_ne_zero two_ne_zero ?_) (Gamma_ne_zero h1)
    simp [pi_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ -(↑n : ℂ)
h2 : HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ 1
h3 : (HMul.hMul (α := ℂ) 2 (↑k : ℂ)).Gammaℂ ≠ 0
⊢ 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)))
have rw : Complex.cos ((↑π : ℂ) * HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2) * HPow.hPow (α := ℂ) (-1) (k + 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 [hurwitzZetaEven_one_sub _ h1 (Or.inr h2), ← Gammaℂ, cosZeta_two_mul_nat' hk hx, ← mul_assoc,
    ← mul_div_assoc, mul_assoc, mul_div_cancel_left₀ _ h3, ← mul_div_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ -(↑n : ℂ)
h2 : HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ 1
h3 : (HMul.hMul (α := ℂ) 2 (↑k : ℂ)).Gammaℂ ≠ 0
⊢ Complex.cos ((↑π : ℂ) * HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2) * HPow.hPow (α := ℂ) (-1) (k + 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)))
have e_a : Complex.cos ((↑π : ℂ) * HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
Tactic: congr 2
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ -(↑n : ℂ)
h2 : HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ 1
h3 : (HMul.hMul (α := ℂ) 2 (↑k : ℂ)).Gammaℂ ≠ 0
⊢ Complex.cos ((↑π : ℂ) * HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
have e_a : Complex.cos ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
Tactic: rw [mul_div_assoc, mul_div_cancel_left₀ _ two_ne_zero, ← ofReal_natCast, ← ofReal_mul,
    ← ofReal_cos, mul_comm π, ← sub_zero (k * π), cos_nat_mul_pi_sub, Real.cos_zero, mul_one,
    ofReal_pow, ofReal_neg, ofReal_one, pow_succ, mul_neg_one, mul_neg, ← mul_pow, neg_one_mul,
    neg_neg, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ -(↑n : ℂ)
h2 : HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ 1
h3 : (HMul.hMul (α := ℂ) 2 (↑k : ℂ)).Gammaℂ ≠ 0
e_a : Complex.cos ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
⊢ Complex.cos ((↑π : ℂ) * HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
have e_a₁ : Complex.cos ((↑π : ℂ) * (↑k : ℂ)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
Tactic: rw [mul_div_assoc, mul_div_cancel_left₀ _ two_ne_zero, ← ofReal_natCast, ← ofReal_mul,
    ← ofReal_cos, mul_comm π, ← sub_zero (k * π), cos_nat_mul_pi_sub, Real.cos_zero, mul_one,
    ofReal_pow, ofReal_neg, ofReal_one, pow_succ, mul_neg_one, mul_neg, ← mul_pow, neg_one_mul,
    neg_neg, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (goal)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ -(↑n : ℂ)
h2 : HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ 1
h3 : (HMul.hMul (α := ℂ) 2 (↑k : ℂ)).Gammaℂ ≠ 0
e_a : Complex.cos ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₁ : Complex.cos ((↑π : ℂ) * (↑k : ℂ)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
⊢ Complex.cos ((↑π : ℂ) * HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
have e_a₂ : Complex.cos ((↑π : ℂ) * (↑(↑k : ℝ) : ℂ)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
Tactic: rw [mul_div_assoc, mul_div_cancel_left₀ _ two_ne_zero, ← ofReal_natCast, ← ofReal_mul,
    ← ofReal_cos, mul_comm π, ← sub_zero (k * π), cos_nat_mul_pi_sub, Real.cos_zero, mul_one,
    ofReal_pow, ofReal_neg, ofReal_one, pow_succ, mul_neg_one, mul_neg, ← mul_pow, neg_one_mul,
    neg_neg, one_pow]