awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
this :
  ∀ (n : ℤ),
    cexp (-((↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 * (↑t : ℂ))) =
      cexp (-((↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑t : ℂ))) *
        jacobiTheta₂_term n ((↑a : ℂ) * I * (↑t : ℂ)) (I * (↑t : ℂ))
⊢ HasSum (fun (x : ℤ) ↦ (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑x : ℝ) + a) 2 * t)) : ℂ))
    (cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑t : ℂ)) *
      jacobiTheta₂ ((↑a : ℂ) * I * (↑t : ℂ)) (I * (↑t : ℂ)))

Tactic:
simpa [this] using (hasSum_jacobiTheta₂_term _ (by simpa)).mul_left _

Premises used: hasSum_jacobiTheta₂_term, HasSum.mul_left
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
rw :
  HasSum
    (fun (n : ℤ) ↦
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
    (jacobiTheta₂ (↑a : ℂ) (I * (↑t : ℂ)))
⊢ HasSum
    (fun (n : ℤ) ↦
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
    (↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)

Tactic:
rw [cosKernel_def a t]

Premises used: HurwitzZeta.cosKernel_def
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
n : ℤ
rw :
  cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) + -((↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ))) =
    cexp
      (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑a : ℂ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑t : ℂ)))
⊢ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
      cexp (-((↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ))) =
    jacobiTheta₂_term n (↑a : ℂ) (I * (↑t : ℂ))

Tactic:
rw [jacobiTheta₂_term, ← Complex.exp_add]

Premises used: Complex.exp_add, jacobiTheta₂_term
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
n : ℤ
ring_nf :
  cexp ((↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) * 2 - (↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ)) =
    cexp
      ((↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) * 2 +
        (↑π : ℂ) * HPow.hPow (β := ℕ) I 2 * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ))
⊢ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) + -((↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ))) =
    cexp
      (2 * (↑π : ℂ) * I * (↑n : ℂ) * (↑a : ℂ) + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑t : ℂ)))

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
n : ℤ
⊢ cexp ((↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) * 2 - (↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ)) =
    cexp
      ((↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ) * 2 +
        (↑π : ℂ) * HPow.hPow (β := ℕ) I 2 * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ))

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
⊢ ∀ (n : ℤ),
    cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
        cexp (-((↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ))) =
      jacobiTheta₂_term n (↑a : ℂ) (I * (↑t : ℂ))

Tactic:
have (n : ℤ) : cexp (2 * π * I * a * n) * cexp (-(π * n ^ 2 * t)) =
      jacobiTheta₂_term n a (I * ↑t) := by
    rw [jacobiTheta₂_term, ← Complex.exp_add]
    ring_nf
    simp [sub_eq_add_neg]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
this :
  ∀ (n : ℤ),
    cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
        cexp (-((↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ))) =
      jacobiTheta₂_term n (↑a : ℂ) (I * (↑t : ℂ))
⊢ 0 < (I * (↑t : ℂ)).im

Tactic:
simpa
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
this :
  ∀ (n : ℤ),
    cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
        cexp (-((↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ))) =
      jacobiTheta₂_term n (↑a : ℂ) (I * (↑t : ℂ))
⊢ HasSum
    (fun (n : ℤ) ↦
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
    (jacobiTheta₂ (↑a : ℂ) (I * (↑t : ℂ)))

Tactic:
simpa [this] using hasSum_jacobiTheta₂_term _ (by simpa)

Premises used: hasSum_jacobiTheta₂_term
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
haveI :
  ∀ (this : (a : Prop) → Decidable a),
    HasSum (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t))
      (evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t -
        if
            Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
              (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
          1
        else 0)
⊢ HasSum (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t))
    (evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t -
      if
          Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
            (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
        1
      else 0)

Tactic:
haveI := Classical.propDecidable
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
simp_rw :
  HasSum (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t))
    (evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - if ∃ (n : ℤ), (↑n : ℝ) = a then 1 else 0)
⊢ HasSum (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t))
    (evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t -
      if
          Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
            (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then
        1
      else 0)

Tactic:
simp_rw [AddCircle.coe_eq_zero_iff, zsmul_one]

Premises used: AddCircle.coe_eq_zero_iff, zsmul_one
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
pos :
  ∀ (h : ∃ (n : ℤ), (↑n : ℝ) = a),
    HasSum (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t))
      (evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - 1)
neg :
  ∀ (h : ¬∃ (n : ℤ), (↑n : ℝ) = a),
    HasSum (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t))
      (evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - 0)
⊢ HasSum (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t))
    (evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - if ∃ (n : ℤ), (↑n : ℝ) = a then 1 else 0)

Tactic:
split_ifs with h
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ∃ (n : ℤ), (↑n : ℝ) = a
pos :
  ∀ (k : ℤ),
    HasSum
      (fun (n : ℤ) ↦
        if HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑k : ℝ) = 0 then 0
        else rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑k : ℝ)) 2 * t))
      (evenKernel (↑(↑k : ℝ) : ℝ ⧸ AddSubgroup.zmultiples 1) t - 1)
⊢ HasSum (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t))
    (evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - 1)

Tactic:
obtain ⟨k, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
k : ℤ
⊢ HasSum
    (fun (n : ℤ) ↦
      if HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑k : ℝ) = 0 then 0
      else rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑k : ℝ)) 2 * t))
    (evenKernel (↑(↑k : ℝ) : ℝ ⧸ AddSubgroup.zmultiples 1) t - 1)

Tactic:
simpa [← Int.cast_add, add_eq_zero_iff_eq_neg]
      using hasSum_ite_sub_hasSum (hasSum_int_evenKernel (k : ℝ) ht) (-k)

Premises used: Int.cast, hasSum_ite_sub_hasSum, Int.cast_add, add_eq_zero_iff_eq_neg, HurwitzZeta.hasSum_int_evenKernel, Neg.neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
this_1 : (a : Prop) → Decidable a
h : ¬∃ (n : ℤ), (↑n : ℝ) = a
this : ∀ (n : ℤ), (↑n : ℝ) + a ≠ 0
⊢ HasSum (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t))
    (evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - 0)

Tactic:
simpa [this] using hasSum_int_evenKernel a ht

Premises used: HurwitzZeta.hasSum_int_evenKernel
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ¬∃ (n : ℤ), (↑n : ℝ) = a
neg : ∀ (n : ℤ), (↑n : ℝ) + a ≠ 0
⊢ HasSum (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t))
    (evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - 0)

Tactic:
suffices ∀ (n : ℤ), n + a ≠ 0 by simpa [this] using hasSum_int_evenKernel a ht
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ¬∃ (n : ℤ), (↑n : ℝ) = a
neg : ∀ (h : ∃ (n : ℤ), (↑n : ℝ) + a = 0), ∃ (n : ℤ), (↑n : ℝ) = a
⊢ ∀ (n : ℤ), (↑n : ℝ) + a ≠ 0

Tactic:
contrapose! h
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ∃ (n : ℤ), (↑n : ℝ) + a = 0
neg : ∀ (n : ℤ) (hn : (↑n : ℝ) + a = 0), ∃ (n : ℤ), (↑n : ℝ) = a
⊢ ∃ (n : ℤ), (↑n : ℝ) = a

Tactic:
let ⟨n, hn⟩ := h
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ∃ (n : ℤ), (↑n : ℝ) + a = 0
n : ℤ
hn : (↑n : ℝ) + a = 0
⊢ (↑(-n) : ℝ) = a

Tactic:
simpa [neg_eq_iff_add_eq_zero]

Premises used: neg_eq_iff_add_eq_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ∃ (n : ℤ), (↑n : ℝ) + a = 0
n : ℤ
hn : (↑n : ℝ) + a = 0
⊢ ∃ (n : ℤ), (↑n : ℝ) = a

Tactic:
exact ⟨-n, by simpa [neg_eq_iff_add_eq_zero]⟩
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
⊢ HasSum
    (fun (n : ℤ) ↦
      if n = 0 then 0
      else
        cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1)

Tactic:
simpa using hasSum_ite_sub_hasSum (hasSum_int_cosKernel a ht) 0

Premises used: hasSum_ite_sub_hasSum, HurwitzZeta.hasSum_int_cosKernel, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
rw :
  HasSum
    (fun (x : ℕ) ↦
      (↑(2 * Real.cos (2 * π * a * HAdd.hAdd (α := ℝ) (↑x : ℝ) 1) *
            rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑x : ℝ) 1) 2 * t)) :
        ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1)
⊢ HasSum
    (fun (n : ℕ) ↦
      2 * Real.cos (2 * π * a * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
        rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) 2 * t))
    (cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - 1)

Tactic:
rw [← hasSum_ofReal, ofReal_sub, ofReal_one]

Premises used: Complex.hasSum_ofReal, Complex.ofReal_one, Complex.ofReal_sub
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
⊢ HasSum
    (fun (n : ℕ) ↦
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
        cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) +
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 2 * t)) : ℂ))

Tactic:
have := (hasSum_int_cosKernel a ht).nat_add_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
        cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) +
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 2 * t)) : ℂ))
⊢ HasSum
    (fun (n : ℕ) ↦
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑(n + 1) : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑(n + 1) : ℤ) : ℝ) 2 * t)) : ℂ) +
        cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑(n + 1) : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑(n + 1) : ℤ)) : ℝ) 2 * t)) : ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) +
        cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 2 * t)) : ℂ) -
      ∑ i ∈ Finset.range 1,
        (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑i : ℤ) : ℂ)) *
            (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑i : ℤ) : ℝ) 2 * t)) : ℂ) +
          cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑i : ℤ)) : ℂ)) *
            (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑i : ℤ)) : ℝ) 2 * t)) : ℂ)))

Tactic:
rw [← hasSum_nat_add_iff' 1] at this

Premises used: hasSum_nat_add_iff', OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑(n + 1) : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑(n + 1) : ℤ) : ℝ) 2 * t)) : ℂ) +
        cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑(n + 1) : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑(n + 1) : ℤ)) : ℝ) 2 * t)) : ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) +
        cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 2 * t)) : ℂ) -
      ∑ i ∈ Finset.range 1,
        (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑i : ℤ) : ℂ)) *
            (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑i : ℤ) : ℝ) 2 * t)) : ℂ) +
          cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑i : ℤ)) : ℂ)) *
            (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑i : ℤ)) : ℝ) 2 * t)) : ℂ)))
⊢ HasSum
    (fun (n : ℕ) ↦
      (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)))) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1) : ℝ) 2 * t)) : ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1)

Tactic:
simp_rw [Finset.sum_range_one, Nat.cast_zero, neg_zero, Int.cast_zero, zero_pow two_ne_zero,
    mul_zero, zero_mul, Complex.exp_zero, Real.exp_zero, ofReal_one, mul_one, Int.cast_neg,
    Int.cast_natCast, neg_sq, ← add_mul, add_sub_assoc, ← sub_sub, sub_self, zero_sub,
    ← sub_eq_add_neg, mul_neg] at this

Premises used: add_sub_assoc, add_mul, Int.cast_neg, Int.cast_natCast, sub_self, Complex.exp_zero, Int.cast_zero, MulZeroClass.zero_mul, sub_eq_add_neg, neg_sq, Finset.sum_range_one, Complex.ofReal_one, MulZeroClass.mul_zero, two_ne_zero, sub_sub, Real.exp_zero, Nat.cast_zero, mul_one, neg_zero, zero_pow, zero_sub, mul_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)))) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1) : ℝ) 2 * t)) : ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1)
⊢ HasSum
    (fun (x : ℕ) ↦
      (↑(2 * Real.cos (2 * π * a * HAdd.hAdd (α := ℝ) (↑x : ℝ) 1) *
            rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑x : ℝ) 1) 2 * t)) :
        ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1)

Tactic:
this.congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)))) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1) : ℝ) 2 * t)) : ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1)
refine :
  ∀ (n : ℕ),
    (↑(2 * Real.cos (2 * π * a * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
            rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) 2 * t)) :
        ℂ) =
      (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)))) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1) : ℝ) 2 * t)) : ℂ)
⊢ HasSum
    (fun (x : ℕ) ↦
      (↑(2 * Real.cos (2 * π * a * HAdd.hAdd (α := ℝ) (↑x : ℝ) 1) *
            rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑x : ℝ) 1) 2 * t)) :
        ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1)

Tactic:
refine this.congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)))) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1) : ℝ) 2 * t)) : ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1)
n : ℕ
push_cast :
  2 * Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) *
      cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * (↑t : ℂ)) =
    (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) +
        cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1))) *
      cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * (↑t : ℂ))
⊢ (↑(2 * Real.cos (2 * π * a * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
          rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) 2 * t)) :
      ℂ) =
    (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)))) *
      (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1) : ℝ) 2 * t)) : ℂ)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)))) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1) : ℝ) 2 * t)) : ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1)
n : ℕ
rw :
  (cexp (2 * (↑π : ℂ) * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * I) +
        cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) * I)) *
      cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * (↑t : ℂ)) =
    (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) +
        cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1))) *
      cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * (↑t : ℂ))
⊢ 2 * Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) *
      cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * (↑t : ℂ)) =
    (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) +
        cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1))) *
      cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * (↑t : ℂ))

Tactic:
rw [Complex.cos, mul_div_cancel₀ _ two_ne_zero]

Premises used: Complex.cos, mul_div_cancel₀, two_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)))) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1) : ℝ) 2 * t)) : ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1)
n : ℕ
e_a :
  2 * (↑π : ℂ) * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * I =
    2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1
e_a₁ :
  -(2 * (↑π : ℂ) * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) * I =
    -(2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
⊢ (cexp (2 * (↑π : ℂ) * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * I) +
        cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) * I)) *
      cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * (↑t : ℂ)) =
    (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) +
        cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1))) *
      cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * (↑t : ℂ))

Tactic:
congr 3
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)))) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1) : ℝ) 2 * t)) : ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1)
n : ℕ
⊢ 2 * (↑π : ℂ) * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * I =
    2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)))) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1) : ℝ) 2 * t)) : ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1)
n : ℕ
⊢ -(2 * (↑π : ℂ) * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) * I =
    -(2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
b : ℝ
H :
  ∀ (p : ℝ) (hp : 0 < p)
    (hp' :
      IsBigO (E := ℝ) (F := ℝ) atTop
        (fun (t : ℝ) ↦
          HurwitzKernelBounds.F_int 0 (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) t -
            if Eq (α := UnitAddCircle) (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then 1 else 0)
        fun (t : ℝ) ↦ rexp (-p * t)),
    ∃ (p : ℝ),
      0 < p ∧
        IsBigO (E := ℝ) (F := ℝ) atTop
          (fun (x : ℝ) ↦
            evenKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) x -
              if Eq (α := UnitAddCircle) (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then 1 else 0)
          fun (x : ℝ) ↦ rexp (-p * x)
⊢ ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop
        (fun (x : ℝ) ↦
          evenKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) x -
            if Eq (α := UnitAddCircle) (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then 1 else 0)
        fun (x : ℝ) ↦ rexp (-p * x)

Tactic:
obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_int_zero_sub b

Premises used: QuotientAddGroup.mk, HurwitzKernelBounds.isBigO_atTop_F_int_zero_sub
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
b p : ℝ
hp : 0 < p
hp' :
  IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (t : ℝ) ↦
      HurwitzKernelBounds.F_int 0 (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) t -
        if Eq (α := UnitAddCircle) (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then 1 else 0)
    fun (t : ℝ) ↦ rexp (-p * t)
⊢ ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop
        (fun (x : ℝ) ↦
          evenKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) x -
            if Eq (α := UnitAddCircle) (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then 1 else 0)
        fun (x : ℝ) ↦ rexp (-p * x)

Tactic:
⟨p, hp, (EventuallyEq.isBigO ?_).trans hp'⟩

Premises used: Filter.EventuallyEq.isBigO, Asymptotics.IsBigO.trans, And.intro, Exists.intro