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
⊢ 1 < 2 * k + 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
rw :
  HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / 2 / (↑(2 * k)! : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k))) =
    HPow.hPow (α := ℂ) (-1) (k + 1) / HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (HMul.hMul (α := ℂ) 2 (↑k : ℂ)).Gammaℂ *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
⊢ cosZeta (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) (HMul.hMul (α := ℂ) 2 (↑k : ℂ)) =
    HPow.hPow (α := ℂ) (-1) (k + 1) / HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (HMul.hMul (α := ℂ) 2 (↑k : ℂ)).Gammaℂ *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Tactic:
rw [cosZeta_two_mul_nat hk hx]

Premises used: HurwitzZeta.cosZeta_two_mul_nat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
e_a :
  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ℂ
⊢ HPow.hPow (α := ℂ) (-1) (k + 1) * (2 * (↑π : ℂ)) ^ (2 * k) / 2 / (↑(2 * k)! : ℂ) *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k))) =
    HPow.hPow (α := ℂ) (-1) (k + 1) / HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (HMul.hMul (α := ℂ) 2 (↑k : ℂ)).Gammaℂ *
      Polynomial.eval (↑x : ℂ) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
norm_cast : 2 * k = 2 * k - 1 + 1
⊢ HMul.hMul (α := ℂ) 2 (↑k : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ 2 * k = 2 * k - 1 + 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
lia lia₁ lia₂ lia₃ lia₄ lia₅ : 2 * k = 2 * k - 1 + 1
⊢ HMul.hMul (α := ℂ) 2 (↑k : ℂ) = HAdd.hAdd (α := ℂ) (↑(2 * k - 1) : ℂ) 1

Tactic:
{ norm_cast; lia }
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ 1 ≤ 2 * k

Tactic:
lia
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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)! : ℂ)
rw₆ rw₇ : Eq (α := ℂ) (↑(2 * k)! : ℂ) (↑(2 * k)! : ℂ)
⊢ (↑(2 * k)! : ℂ) = HMul.hMul (α := ℂ) 2 (↑k : ℂ) * Complex.Gamma (HMul.hMul (α := ℂ) 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)]

Premises used: Complex.Gamma_nat_eq_factorial, Nat.factorial_succ, Nat.cast_mul, Nat.sub_add_cancel, Nat.cast_add_one
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ (↑(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)]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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 : ℂ))
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 : ℂ)))
⊢ 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ℂ

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 : ℂ)]

Premises used: Complex.Gammaℂ, Complex.cpow_neg, div_mul_eq_mul_div, Nat.cast, mul_right_comm, div_inv_eq_mul, div_div, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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 : ℂ))
e_a e_a₁ e_a₂ 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) : ℂ))
⊢ 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:
norm_cast
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
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)))
⊢ 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)))

Tactic:
rw [sinZeta_two_mul_nat_add_one hk hx]

Premises used: HurwitzZeta.sinZeta_two_mul_nat_add_one
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
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ℂ
⊢ 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:
congr 1
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ Complex.Gamma (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) = Complex.Gamma (HAdd.hAdd (α := ℂ) (↑(2 * k) : ℂ) 1)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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)!) : ℂ)
rw₇ rw₈ : Eq (α := ℂ) (↑(2 * k + 1)! : ℂ) (↑(2 * k + 1)! : ℂ)
⊢ (↑(2 * k + 1)! : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * Complex.Gamma (HMul.hMul (α := ℂ) 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]

Premises used: Nat.cast_ofNat, Complex.Gamma_nat_eq_factorial, Nat.factorial_succ, Nat.cast_mul, Nat.cast_add_one
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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)

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]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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)
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))
⊢ 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:
simp_rw [this, Gammaℂ, cpow_neg, ← div_div, div_inv_eq_mul, div_mul_eq_mul_div, div_div]

Premises used: Complex.Gammaℂ, Complex.cpow_neg, div_mul_eq_mul_div, div_inv_eq_mul, div_div
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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)
⊢ HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1 = (↑(2 * k + 1) : ℂ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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)
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) : ℂ))
⊢ 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:
rw [(by simp : 2 * (k : ℂ) + 1 = ↑(2 * k + 1)), cpow_natCast]

Premises used: Complex.cpow_natCast
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
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) /
      (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:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
rw : HMul.hMul (α := ℤ) 2 (↑k : ℤ) ≠ -(↑n : ℤ)
⊢ 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]

Premises used: Int.cast_neg, Int.cast_natCast, Int.cast_inj, Ne, Int.cast_ofNat, Int.cast_mul
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
⊢ HMul.hMul (α := ℤ) 2 (↑k : ℤ) ≠ -(↑n : ℤ)

Tactic:
ne_of_gt ((neg_nonpos_of_nonneg n.cast_nonneg).trans_lt (mul_pos two_pos ?_))

Premises used: two_pos, ne_of_gt, neg_nonpos_of_nonneg, mul_pos, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
refine : LT.lt (α := ℤ) 0 (↑k : ℤ)
⊢ HMul.hMul (α := ℤ) 2 (↑k : ℤ) ≠ -(↑n : ℤ)

Tactic:
refine ne_of_gt ((neg_nonpos_of_nonneg n.cast_nonneg).trans_lt (mul_pos two_pos ?_))

Premises used: ne_of_gt, neg_nonpos_of_nonneg, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
⊢ LT.lt (α := ℤ) 0 (↑k : ℤ)

Tactic:
Nat.cast_pos.mpr (Nat.pos_of_ne_zero hk)

Premises used: Iff.mpr, Nat.cast_pos, Nat.pos_of_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
⊢ LT.lt (α := ℤ) 0 (↑k : ℤ)

Tactic:
exact Nat.cast_pos.mpr (Nat.pos_of_ne_zero hk)

Premises used: Iff.mpr, Nat.cast_pos, Nat.pos_of_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ ∀ (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)
-- 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 : ℂ) ≠ -(↑n : ℂ)
norm_cast : ¬2 * k = 1
⊢ HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ 1

Tactic:
norm_cast
-- 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 : ℂ) ≠ -(↑n : ℂ)
⊢ ¬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 : ℂ) ≠ -(↑n : ℂ)
⊢ HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ 1

Tactic:
have h2 : (2 * k : ℂ) ≠ 1 := by norm_cast; 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 : ℂ) ≠ -(↑n : ℂ)
h2 : HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ 1
⊢ (HMul.hMul (α := ℂ) 2 (↑k : ℂ)).Gammaℂ ≠ 0

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

Premises used: Complex.Gammaℂ, 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 : ℂ) ≠ -(↑n : ℂ)
h2 : HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ 1
refine : (2 * (↑π : ℂ)) ^ (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) ≠ 0
⊢ (HMul.hMul (α := ℂ) 2 (↑k : ℂ)).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 : ℂ) ≠ -(↑n : ℂ)
h2 : HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ 1
⊢ (2 * (↑π : ℂ)) ^ (-HMul.hMul (α := ℂ) 2 (↑k : ℂ)) ≠ 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 : ℂ) ≠ -(↑n : ℂ)
h2 : HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ 1
⊢ (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]
-- 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 : ℂ) ≠ -(↑n : ℂ)
h2 : HMul.hMul (α := ℂ) 2 (↑k : ℂ) ≠ 1
h3 : (HMul.hMul (α := ℂ) 2 (↑k : ℂ)).Gammaℂ ≠ 0
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)))
⊢ 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)))

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]

Premises used: HurwitzZeta.cosZeta_two_mul_nat', Complex.Gammaℂ, mul_assoc, mul_div_assoc, mul_div_cancel_left₀, HurwitzZeta.hurwitzZetaEven_one_sub, Or.inr
-- 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 : ℂ) ≠ -(↑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) /
        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:
congr 2
-- 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 : ℂ) ≠ -(↑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
e_a₁₉ e_a₂₀ : Eq (α := ℂ) (-1) (-1)
⊢ 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]

Premises used: one_pow, Real.pi, HMul.hMul, sub_zero, pow_succ, mul_div_assoc, Complex.ofReal_neg, neg_one_mul, mul_div_cancel_left₀, neg_neg, Complex.ofReal_one, Nat.cast, two_ne_zero, Real.cos_nat_mul_pi_sub, Complex.ofReal_natCast, Complex.ofReal_cos, mul_comm, mul_neg_one, mul_one, Real.cos_zero, mul_pow, Complex.ofReal_pow, Complex.ofReal_mul, mul_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
rw : HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1 ≠ -(↑n : ℤ)
⊢ 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]

Premises used: Int.cast_neg, Int.cast_natCast, Int.cast_inj, Int.cast_add, Ne, Int.cast_ofNat, Int.cast_mul, Int.cast_one
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
⊢ HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1 ≠ -(↑n : ℤ)

Tactic:
ne_of_gt ((neg_nonpos_of_nonneg n.cast_nonneg).trans_lt ?_)

Premises used: ne_of_gt, neg_nonpos_of_nonneg, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
refine : 0 < HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1
⊢ HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1 ≠ -(↑n : ℤ)

Tactic:
refine ne_of_gt ((neg_nonpos_of_nonneg n.cast_nonneg).trans_lt ?_)

Premises used: ne_of_gt, neg_nonpos_of_nonneg, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
n : ℕ
⊢ 0 < HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1

Tactic:
positivity
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues
Goal:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ ∀ (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
-- 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:
mul_ne_zero (mul_ne_zero two_ne_zero ?_) (Gamma_ne_zero h1)

Premises used: Complex.Gammaℂ, two_ne_zero, mul_ne_zero, Complex.Gamma_ne_zero