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
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
e_a₂ : Complex.cos ((↑π : ℂ) * (↑(↑k : ℝ) : ℂ)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₃ : Complex.cos (↑(π * (↑k : ℝ)) : ℂ) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₄ : (↑(Real.cos (π * (↑k : ℝ))) : ℂ) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₅ : (↑(Real.cos ((↑k : ℝ) * π)) : ℂ) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₆ : (↑(Real.cos ((↑k : ℝ) * π - 0)) : ℂ) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₇ : (↑(HPow.hPow (α := ℝ) (-1) k * Real.cos 0) : ℂ) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₈ : (↑(HPow.hPow (α := ℝ) (-1) k * 1) : ℂ) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₉ : (↑(HPow.hPow (α := ℝ) (-1) k) : ℂ) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₁₀ : (↑(-1) : ℂ) ^ k * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₁₁ : (-(↑1 : ℂ)) ^ k * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₁₂ : HPow.hPow (α := ℂ) (-1) k * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₁₃ : HPow.hPow (α := ℂ) (-1) k * (HPow.hPow (α := ℂ) (-1) k * -1) = -1
e_a₁₄ : HPow.hPow (α := ℂ) (-1) k * -HPow.hPow (α := ℂ) (-1) k = -1
e_a₁₅ : -(HPow.hPow (α := ℂ) (-1) k * HPow.hPow (α := ℂ) (-1) k) = -1
e_a₁₆ : -HMul.hMul (α := ℂ) (-1) (-1) ^ k = -1
e_a₁₇ : -HPow.hPow (α := ℂ) (- -1) k = -1
⊢ Complex.cos ((↑π : ℂ) * HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
have e_a₁₈ : -HPow.hPow (α := ℂ) 1 k = -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
e_a₂ : Complex.cos ((↑π : ℂ) * (↑(↑k : ℝ) : ℂ)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₃ : Complex.cos (↑(π * (↑k : ℝ)) : ℂ) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₄ : (↑(Real.cos (π * (↑k : ℝ))) : ℂ) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₅ : (↑(Real.cos ((↑k : ℝ) * π)) : ℂ) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₆ : (↑(Real.cos ((↑k : ℝ) * π - 0)) : ℂ) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₇ : (↑(HPow.hPow (α := ℝ) (-1) k * Real.cos 0) : ℂ) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₈ : (↑(HPow.hPow (α := ℝ) (-1) k * 1) : ℂ) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₉ : (↑(HPow.hPow (α := ℝ) (-1) k) : ℂ) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₁₀ : (↑(-1) : ℂ) ^ k * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₁₁ : (-(↑1 : ℂ)) ^ k * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₁₂ : HPow.hPow (α := ℂ) (-1) k * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₁₃ : HPow.hPow (α := ℂ) (-1) k * (HPow.hPow (α := ℂ) (-1) k * -1) = -1
e_a₁₄ : HPow.hPow (α := ℂ) (-1) k * -HPow.hPow (α := ℂ) (-1) k = -1
e_a₁₅ : -(HPow.hPow (α := ℂ) (-1) k * HPow.hPow (α := ℂ) (-1) k) = -1
e_a₁₆ : -HMul.hMul (α := ℂ) (-1) (-1) ^ k = -1
e_a₁₇ : -HPow.hPow (α := ℂ) (- -1) k = -1
e_a₁₈ : -HPow.hPow (α := ℂ) 1 k = -1
⊢ Complex.cos ((↑π : ℂ) * HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
have e_a₁₉ : Eq (α := ℂ) (-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
n : ℕ
⊢ HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1 ≠ -(↑n : ℂ)
have rw : HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1 ≠ -(↑n : ℤ)
Tactic: rw [← Int.cast_ofNat, ← Int.cast_natCast, ← Int.cast_mul, ← Int.cast_natCast n, ← Int.cast_neg,
      ← Int.cast_one, ← Int.cast_add, 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 : ℤ) + 1 ≠ -(↑n : ℤ)
have refine : 0 < HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1
Tactic: refine ne_of_gt ((neg_nonpos_of_nonneg n.cast_nonneg).trans_lt ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaValues (hypothesis)
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ 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)))
have h1 : ∀ (n : ℕ), HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1 ≠ -(↑n : ℂ)
Tactic: have h1 (n : ℕ) : (2 * k + 1 : ℂ) ≠ -n := by
    rw [← Int.cast_ofNat, ← Int.cast_natCast, ← Int.cast_mul, ← Int.cast_natCast n, ← Int.cast_neg,
      ← Int.cast_one, ← Int.cast_add, Ne, Int.cast_inj, ← Ne]
    refine ne_of_gt ((neg_nonpos_of_nonneg n.cast_nonneg).trans_lt ?_)
    positivity
-- 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 : ℂ) + 1 ≠ -(↑n : ℂ)
⊢ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).Gammaℂ ≠ 0
have refine : (2 * (↑π : ℂ)) ^ (-(HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1)) ≠ 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 : ℂ) + 1 ≠ -(↑n : ℂ)
⊢ 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)))
have h3 : (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]
-- 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 : ℂ) + 1 ≠ -(↑n : ℂ)
h3 : (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).Gammaℂ ≠ 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)))
have 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)))
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]
-- 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 : ℂ) + 1 ≠ -(↑n : ℂ)
h3 : (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).Gammaℂ ≠ 0
⊢ 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)))
have e_a : Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 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 : ℂ) + 1 ≠ -(↑n : ℂ)
h3 : (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1).Gammaℂ ≠ 0
⊢ Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
have e_a : Complex.sin ((↑π : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
Tactic: rw [mul_div_assoc, add_div, mul_div_cancel_left₀ _ two_ne_zero, ← ofReal_natCast,
    ← ofReal_one, ← ofReal_ofNat, ← ofReal_div, ← ofReal_add, ← ofReal_mul,
    ← ofReal_sin, mul_comm π, add_mul, mul_comm (1 / 2), mul_one_div, Real.sin_add_pi_div_two,
    ← 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 : ℂ) + 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) = -1
have e_a₁ : Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2 + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
Tactic: rw [mul_div_assoc, add_div, mul_div_cancel_left₀ _ two_ne_zero, ← ofReal_natCast,
    ← ofReal_one, ← ofReal_ofNat, ← ofReal_div, ← ofReal_add, ← ofReal_mul,
    ← ofReal_sin, mul_comm π, add_mul, mul_comm (1 / 2), mul_one_div, Real.sin_add_pi_div_two,
    ← 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 : ℂ) + 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
e_a₁ : Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2 + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
⊢ Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
have e_a₂ : Complex.sin ((↑π : ℂ) * ((↑k : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
Tactic: rw [mul_div_assoc, add_div, mul_div_cancel_left₀ _ two_ne_zero, ← ofReal_natCast,
    ← ofReal_one, ← ofReal_ofNat, ← ofReal_div, ← ofReal_add, ← ofReal_mul,
    ← ofReal_sin, mul_comm π, add_mul, mul_comm (1 / 2), mul_one_div, Real.sin_add_pi_div_two,
    ← 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 : ℂ) + 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
e_a₁ : Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2 + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₂ : Complex.sin ((↑π : ℂ) * ((↑k : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
⊢ Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
have e_a₃ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
Tactic: rw [mul_div_assoc, add_div, mul_div_cancel_left₀ _ two_ne_zero, ← ofReal_natCast,
    ← ofReal_one, ← ofReal_ofNat, ← ofReal_div, ← ofReal_add, ← ofReal_mul,
    ← ofReal_sin, mul_comm π, add_mul, mul_comm (1 / 2), mul_one_div, Real.sin_add_pi_div_two,
    ← 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 : ℂ) + 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
e_a₁ : Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2 + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₂ : Complex.sin ((↑π : ℂ) * ((↑k : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₃ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
⊢ Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
have e_a₄ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / 2)) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
Tactic: rw [mul_div_assoc, add_div, mul_div_cancel_left₀ _ two_ne_zero, ← ofReal_natCast,
    ← ofReal_one, ← ofReal_ofNat, ← ofReal_div, ← ofReal_add, ← ofReal_mul,
    ← ofReal_sin, mul_comm π, add_mul, mul_comm (1 / 2), mul_one_div, Real.sin_add_pi_div_two,
    ← 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 : ℂ) + 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
e_a₁ : Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2 + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₂ : Complex.sin ((↑π : ℂ) * ((↑k : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₃ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₄ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / 2)) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
⊢ Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
have e_a₅ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / (↑2 : ℂ))) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
Tactic: rw [mul_div_assoc, add_div, mul_div_cancel_left₀ _ two_ne_zero, ← ofReal_natCast,
    ← ofReal_one, ← ofReal_ofNat, ← ofReal_div, ← ofReal_add, ← ofReal_mul,
    ← ofReal_sin, mul_comm π, add_mul, mul_comm (1 / 2), mul_one_div, Real.sin_add_pi_div_two,
    ← 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 : ℂ) + 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
e_a₁ : Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2 + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₂ : Complex.sin ((↑π : ℂ) * ((↑k : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₃ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₄ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / 2)) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₅ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / (↑2 : ℂ))) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
⊢ Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
have e_a₆ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑(HDiv.hDiv (α := ℝ) 1 2) : ℂ))) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
Tactic: rw [mul_div_assoc, add_div, mul_div_cancel_left₀ _ two_ne_zero, ← ofReal_natCast,
    ← ofReal_one, ← ofReal_ofNat, ← ofReal_div, ← ofReal_add, ← ofReal_mul,
    ← ofReal_sin, mul_comm π, add_mul, mul_comm (1 / 2), mul_one_div, Real.sin_add_pi_div_two,
    ← 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 : ℂ) + 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
e_a₁ : Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2 + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₂ : Complex.sin ((↑π : ℂ) * ((↑k : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₃ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₄ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / 2)) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₅ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / (↑2 : ℂ))) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₆ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑(HDiv.hDiv (α := ℝ) 1 2) : ℂ))) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
⊢ Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
have e_a₇ : Complex.sin ((↑π : ℂ) * (↑((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2) : ℂ)) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
Tactic: rw [mul_div_assoc, add_div, mul_div_cancel_left₀ _ two_ne_zero, ← ofReal_natCast,
    ← ofReal_one, ← ofReal_ofNat, ← ofReal_div, ← ofReal_add, ← ofReal_mul,
    ← ofReal_sin, mul_comm π, add_mul, mul_comm (1 / 2), mul_one_div, Real.sin_add_pi_div_two,
    ← 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 : ℂ) + 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
e_a₁ : Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2 + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₂ : Complex.sin ((↑π : ℂ) * ((↑k : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₃ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₄ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / 2)) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₅ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / (↑2 : ℂ))) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₆ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑(HDiv.hDiv (α := ℝ) 1 2) : ℂ))) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₇ : Complex.sin ((↑π : ℂ) * (↑((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2) : ℂ)) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
⊢ Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
have e_a₈ : Complex.sin (↑(π * ((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
Tactic: rw [mul_div_assoc, add_div, mul_div_cancel_left₀ _ two_ne_zero, ← ofReal_natCast,
    ← ofReal_one, ← ofReal_ofNat, ← ofReal_div, ← ofReal_add, ← ofReal_mul,
    ← ofReal_sin, mul_comm π, add_mul, mul_comm (1 / 2), mul_one_div, Real.sin_add_pi_div_two,
    ← 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 : ℂ) + 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
e_a₁ : Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) / 2 + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₂ : Complex.sin ((↑π : ℂ) * ((↑k : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₃ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + 1 / 2)) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
e_a₄ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / 2)) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₅ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑1 : ℂ) / (↑2 : ℂ))) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₆ : Complex.sin ((↑π : ℂ) * ((↑(↑k : ℝ) : ℂ) + (↑(HDiv.hDiv (α := ℝ) 1 2) : ℂ))) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₇ : Complex.sin ((↑π : ℂ) * (↑((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2) : ℂ)) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
e_a₈ : Complex.sin (↑(π * ((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2)) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
⊢ Complex.sin ((↑π : ℂ) * (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) / 2) * HPow.hPow (α := ℂ) (-1) (k + 1) = -1
have e_a₉ : (↑(Real.sin (π * ((↑k : ℝ) + HDiv.hDiv (α := ℝ) 1 2))) : ℂ) * (-(↑1 : ℂ)) ^ (k + 1) = -(↑1 : ℂ)
Tactic: rw [mul_div_assoc, add_div, mul_div_cancel_left₀ _ two_ne_zero, ← ofReal_natCast,
    ← ofReal_one, ← ofReal_ofNat, ← ofReal_div, ← ofReal_add, ← ofReal_mul,
    ← ofReal_sin, mul_comm π, add_mul, mul_comm (1 / 2), mul_one_div, Real.sin_add_pi_div_two,
    ← 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]