awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a t : ℝ
ht : 0 < t
⊢ HasSum
    (fun (n : ℕ) ↦
      -I * (↑(↑n : ℤ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
        -I * (↑(-(↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ))
    ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) +
      -I * (↑0 : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 2 * t)) : ℂ))

Tactic:
have := (hasSum_int_sinKernel a ht).nat_add_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(↑n : ℤ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
        -I * (↑(-(↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ))
    ((↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) +
      -I * (↑0 : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 2 * t)) : ℂ))
⊢ HasSum
    (fun (n : ℕ) ↦
      -I * (↑(↑n : ℤ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
        -I * (↑(-(↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ))
    (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)

Tactic:
simp only [Int.cast_zero, zero_mul, mul_zero, add_zero] at this

Premises used: Int.cast_zero, MulZeroClass.zero_mul, MulZeroClass.mul_zero, add_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(↑n : ℤ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
        -I * (↑(-(↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ))
    (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)
⊢ HasSum
    (fun (x : ℕ) ↦
      (↑(HMul.hMul (α := ℝ) 2 (↑x : ℝ) * Real.sin (2 * π * a * (↑x : ℝ)) *
            rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑x : ℝ) 2 * t)) :
        ℂ))
    (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)

Tactic:
this.congr_fun fun n ↦ ?_

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

Tactic:
refine this.congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(↑n : ℤ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
        -I * (↑(-(↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ))
    (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)
n : ℕ
simp_rw :
  HMul.hMul (α := ℂ) 2 (↑n : ℂ) *
        ((cexp (-(↑(2 * π * a * (↑n : ℝ)) : ℂ) * I) - cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)) * I / 2) *
      (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) =
    (-I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) +
        -(-I * (↑n : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)))) *
      (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ)
⊢ (↑(HMul.hMul (α := ℝ) 2 (↑n : ℝ) * Real.sin (2 * π * a * (↑n : ℝ)) *
          rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) :
      ℂ) =
    -I * (↑(↑n : ℤ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
      -I * (↑(-(↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ)

Tactic:
simp_rw [Int.cast_neg, neg_sq, mul_neg, ofReal_mul, Int.cast_natCast, ofReal_natCast,
      ofReal_ofNat, ← add_mul, ofReal_sin, Complex.sin]

Premises used: add_mul, Int.cast_neg, Int.cast_natCast, Complex.sin, neg_sq, Complex.ofReal_natCast, Complex.ofReal_sin, Complex.ofReal_ofNat, Complex.ofReal_mul, mul_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(↑n : ℤ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
        -I * (↑(-(↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ))
    (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)
n : ℕ
push_cast :
  HMul.hMul (α := ℂ) 2 (↑n : ℂ) *
        ((cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I) - cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) * I / 2) *
      cexp (-(↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ)) =
    (-I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) +
        -(-I * (↑n : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)))) *
      cexp (-(↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ))
⊢ HMul.hMul (α := ℂ) 2 (↑n : ℂ) *
        ((cexp (-(↑(2 * π * a * (↑n : ℝ)) : ℂ) * I) - cexp ((↑(2 * π * a * (↑n : ℝ)) : ℂ) * I)) * I / 2) *
      (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) =
    (-I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) +
        -(-I * (↑n : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)))) *
      (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(↑n : ℤ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
        -I * (↑(-(↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ))
    (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)
n : ℕ
e_a :
  HMul.hMul (α := ℂ) 2 (↑n : ℂ) *
      ((cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I) - cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) * I / 2) =
    -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) +
      -(-I * (↑n : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)))
⊢ HMul.hMul (α := ℂ) 2 (↑n : ℂ) *
        ((cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I) - cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) * I / 2) *
      cexp (-(↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ)) =
    (-I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) +
        -(-I * (↑n : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)))) *
      cexp (-(↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (↑t : ℂ))

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(↑n : ℤ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
        -I * (↑(-(↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ))
    (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)
n : ℕ
e_a :
  I * (↑n : ℂ) * cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) -
      I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I) =
    I * (↑n : ℂ) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) -
      I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))
⊢ HMul.hMul (α := ℂ) 2 (↑n : ℂ) *
      ((cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ)) * I) - cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) * I / 2) =
    -I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) +
      -(-I * (↑n : ℂ)) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)))

Tactic:
rw [← mul_div_assoc, ← div_mul_eq_mul_div, ← div_mul_eq_mul_div, div_self two_ne_zero, one_mul,
    neg_mul, neg_mul, neg_neg, mul_comm _ I, ← mul_assoc, mul_comm _ I, neg_mul,
    ← sub_eq_neg_add, mul_sub]

Premises used: mul_sub, sub_eq_neg_add, mul_assoc, mul_div_assoc, neg_neg, div_mul_eq_mul_div, two_ne_zero, mul_comm, neg_mul, one_mul, div_self, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      -I * (↑(↑n : ℤ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
        -I * (↑(-(↑n : ℤ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ))
    (↑(sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ)
n : ℕ
e_a : -(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I) = -(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))
e_a₁ : 2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I = 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)
⊢ I * (↑n : ℂ) * cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I)) -
      I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I) =
    I * (↑n : ℂ) * cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))) -
      I * (↑n : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ))

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

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

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
b : ℝ
H :
  ∀ (p : ℝ) (hp : 0 < p)
    (hp' :
      IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_int 1 (↑b : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (t : ℝ) ↦
        rexp (-p * t)),
    ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (oddKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (x : ℝ) ↦ rexp (-p * x)
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (oddKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (x : ℝ) ↦ rexp (-p * x)

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

Premises used: HurwitzKernelBounds.isBigO_atTop_F_int_one, QuotientAddGroup.mk
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
b p : ℝ
hp : 0 < p
hp' :
  IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_int 1 (↑b : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (t : ℝ) ↦ rexp (-p * t)
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (oddKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (x : ℝ) ↦ rexp (-p * x)

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

Premises used: Asymptotics.IsBigO.trans, Filter.Eventually.isBigO, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
b p : ℝ
hp : 0 < p
hp' :
  IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_int 1 (↑b : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (t : ℝ) ↦ rexp (-p * t)
H :
  ∀ᶠ (x : ℝ) in atTop,
    ‖oddKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) x‖ ≤
      HurwitzKernelBounds.F_int 1 (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) x
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (oddKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (x : ℝ) ↦ rexp (-p * x)

Tactic:
refine ⟨p, hp, (Eventually.isBigO ?_).trans hp'⟩
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
b p : ℝ
hp : 0 < p
hp' :
  IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_int 1 (↑b : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (t : ℝ) ↦ rexp (-p * t)
h :
  ∀ (t : ℝ) (ht : 0 < t),
    ‖oddKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) t‖ ≤
      HurwitzKernelBounds.F_int 1 (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) t
⊢ ∀ᶠ (x : ℝ) in atTop,
    ‖oddKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) x‖ ≤
      HurwitzKernelBounds.F_int 1 (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) x

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
b p : ℝ
hp : 0 < p
hp' :
  IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_int 1 (↑b : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (t : ℝ) ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ ‖oddKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) t‖ ≤ HurwitzKernelBounds.F_int 1 (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) t

Tactic:
simpa [← (hasSum_int_oddKernel b ht).tsum_eq, HurwitzKernelBounds.F_int,
    HurwitzKernelBounds.f_int, abs_of_nonneg (exp_pos _).le] using
    norm_tsum_le_tsum_norm (hasSum_int_oddKernel b ht).summable.norm

Premises used: HurwitzKernelBounds.f_int, LT.lt.le, HasSum.summable, HasSum.tsum_eq, norm_tsum_le_tsum_norm, HurwitzZeta.hasSum_int_oddKernel, abs_of_nonneg, Summable.norm, HurwitzKernelBounds.F_int, Real.exp_pos
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
H :
  ∀ (b : ℝ),
    ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (oddKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (x : ℝ) ↦ rexp (-p * x)
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (oddKernel a) fun (x : ℝ) ↦ rexp (-p * x)

Tactic:
induction a using QuotientAddGroup.induction_on with | H b =>
  obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_int_one b
  refine ⟨p, hp, (Eventually.isBigO ?_).trans hp'⟩
  filter_upwards [eventually_gt_atTop 0] with t ht
  simpa [← (hasSum_int_oddKernel b ht).tsum_eq, HurwitzKernelBounds.F_int,
    HurwitzKernelBounds.f_int, abs_of_nonneg (exp_pos _).le] using
    norm_tsum_le_tsum_norm (hasSum_int_oddKernel b ht).summable.norm

Premises used: HurwitzKernelBounds.f_int, LT.lt.le, abs_of_nonneg, OfNat.ofNat, HurwitzKernelBounds.F_int, Real.exp_pos, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : ℝ
H :
  ∀ (p : ℝ) (hp : 0 < p) (hp' : IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_nat 1 0) fun (t : ℝ) ↦ rexp (-p * t)),
    ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (x : ℝ) ↦ rexp (-p * x)
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (x : ℝ) ↦ rexp (-p * x)

Tactic:
obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_nat_one (le_refl 0)

Premises used: le_refl, HurwitzKernelBounds.isBigO_atTop_F_nat_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_nat 1 0) fun (t : ℝ) ↦ rexp (-p * t)
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (x : ℝ) ↦ rexp (-p * x)

Tactic:
⟨p, hp, (Eventually.isBigO ?_).trans (hp'.const_mul_left 2)⟩

Premises used: Asymptotics.IsBigO.const_mul_left, Asymptotics.IsBigO.trans, Filter.Eventually.isBigO, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_nat 1 0) fun (t : ℝ) ↦ rexp (-p * t)
H : ∀ᶠ (x : ℝ) in atTop, ‖sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x‖ ≤ 2 * HurwitzKernelBounds.F_nat 1 0 x
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (x : ℝ) ↦ rexp (-p * x)

Tactic:
refine ⟨p, hp, (Eventually.isBigO ?_).trans (hp'.const_mul_left 2)⟩
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_nat 1 0) fun (t : ℝ) ↦ rexp (-p * t)
h : ∀ (t : ℝ) (ht : 0 < t), ‖sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t‖ ≤ 2 * HurwitzKernelBounds.F_nat 1 0 t
⊢ ∀ᶠ (x : ℝ) in atTop, ‖sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x‖ ≤ 2 * HurwitzKernelBounds.F_nat 1 0 x

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_nat 1 0) fun (t : ℝ) ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
h :
  Norm.norm (E := ℝ)
      (∑' (b : ℕ),
        HMul.hMul (α := ℝ) 2 (↑b : ℝ) * Real.sin (2 * π * a * (↑b : ℝ)) *
          rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 2 * t)) ≤
    HMul.hMul (α := ℝ) 2 (∑' (n : ℕ), HurwitzKernelBounds.f_nat 1 0 t n)
⊢ ‖sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t‖ ≤ 2 * HurwitzKernelBounds.F_nat 1 0 t

Tactic:
rw [HurwitzKernelBounds.F_nat, ← (hasSum_nat_sinKernel a ht).tsum_eq]

Premises used: HurwitzZeta.hasSum_nat_sinKernel, HasSum.tsum_eq, HurwitzKernelBounds.F_nat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_nat 1 0) fun (t : ℝ) ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
h :
  HasSum (fun (n : ℕ) ↦ 2 * HurwitzKernelBounds.f_nat 1 0 t n)
    (HMul.hMul (α := ℝ) 2 (∑' (n : ℕ), HurwitzKernelBounds.f_nat 1 0 t n))
h₁ :
  ∀ (i : ℕ),
    ‖HMul.hMul (α := ℝ) 2 (↑i : ℝ) * Real.sin (2 * π * a * (↑i : ℝ)) *
          rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 * t)‖ ≤
      2 * HurwitzKernelBounds.f_nat 1 0 t i
⊢ Norm.norm (E := ℝ)
      (∑' (b : ℕ),
        HMul.hMul (α := ℝ) 2 (↑b : ℝ) * Real.sin (2 * π * a * (↑b : ℝ)) *
          rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 2 * t)) ≤
    HMul.hMul (α := ℝ) 2 (∑' (n : ℕ), HurwitzKernelBounds.f_nat 1 0 t n)

Tactic:
apply tsum_of_norm_bounded (g := fun n ↦ 2 * HurwitzKernelBounds.f_nat 1 0 t n)

Premises used: tsum_of_norm_bounded
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_nat 1 0) fun (t : ℝ) ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ HasSum (fun (n : ℕ) ↦ 2 * HurwitzKernelBounds.f_nat 1 0 t n)
    (HMul.hMul (α := ℝ) 2 (∑' (n : ℕ), HurwitzKernelBounds.f_nat 1 0 t n))

Tactic:
(HurwitzKernelBounds.summable_f_nat 1 0 ht).hasSum.mul_left _

Premises used: HasSum.mul_left, HurwitzKernelBounds.summable_f_nat, Summable.hasSum, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_nat 1 0) fun (t : ℝ) ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ HasSum (fun (n : ℕ) ↦ 2 * HurwitzKernelBounds.f_nat 1 0 t n)
    (HMul.hMul (α := ℝ) 2 (∑' (n : ℕ), HurwitzKernelBounds.f_nat 1 0 t n))

Tactic:
exact (HurwitzKernelBounds.summable_f_nat 1 0 ht).hasSum.mul_left _

Premises used: HasSum.mul_left, HurwitzKernelBounds.summable_f_nat, Summable.hasSum, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_nat 1 0) fun (t : ℝ) ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
h : (↑n : ℝ) * ‖Real.sin (2 * π * a * (↑n : ℝ))‖ ≤ (↑n : ℝ)
⊢ ‖HMul.hMul (α := ℝ) 2 (↑n : ℝ) * Real.sin (2 * π * a * (↑n : ℝ)) *
        rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)‖ ≤
    2 * HurwitzKernelBounds.f_nat 1 0 t n

Tactic:
rw [norm_mul, norm_mul, norm_mul, norm_two, mul_assoc, mul_assoc,
      mul_le_mul_iff_of_pos_left two_pos, HurwitzKernelBounds.f_nat, pow_one, add_zero,
      norm_of_nonneg (exp_pos _).le, Real.norm_eq_abs, Nat.abs_cast, ← mul_assoc,
      mul_le_mul_iff_of_pos_right (exp_pos _)]

Premises used: Real.norm_two, mul_le_mul_iff_of_pos_right, Nat.abs_cast, mul_assoc, two_pos, mul_le_mul_iff_of_pos_left, LT.lt.le, norm_mul, pow_one, HurwitzKernelBounds.f_nat, add_zero, Real.norm_eq_abs, Real.norm_of_nonneg, Real.exp_pos
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_nat 1 0) fun (t : ℝ) ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ (↑n : ℝ) * ‖Real.sin (2 * π * a * (↑n : ℝ))‖ ≤ (↑n : ℝ)

Tactic:
mul_le_of_le_one_right (Nat.cast_nonneg _) (abs_sin_le_one _)

Premises used: Nat.cast_nonneg, mul_le_of_le_one_right, Real.abs_sin_le_one
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (HurwitzKernelBounds.F_nat 1 0) fun (t : ℝ) ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ (↑n : ℝ) * ‖Real.sin (2 * π * a * (↑n : ℝ))‖ ≤ (↑n : ℝ)

Tactic:
exact mul_le_of_le_one_right (Nat.cast_nonneg _) (abs_sin_le_one _)

Premises used: Nat.cast_nonneg, mul_le_of_le_one_right, Real.abs_sin_le_one
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
Goal:
a : UnitAddCircle
H :
  ∀ (a : ℝ),
    ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (sinKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (x : ℝ) ↦ rexp (-p * x)
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (sinKernel a) fun (x : ℝ) ↦ rexp (-p * x)

Tactic:
induction a using QuotientAddGroup.induction_on with | H a =>
  obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_nat_one (le_refl 0)
  refine ⟨p, hp, (Eventually.isBigO ?_).trans (hp'.const_mul_left 2)⟩
  filter_upwards [eventually_gt_atTop 0] with t ht
  rw [HurwitzKernelBounds.F_nat, ← (hasSum_nat_sinKernel a ht).tsum_eq]
  apply tsum_of_norm_bounded (g := fun n ↦ 2 * HurwitzKernelBounds.f_nat 1 0 t n)
  · exact (HurwitzKernelBounds.summable_f_nat 1 0 ht).hasSum.mul_left _
  · intro n
    rw [norm_mul, norm_mul, norm_mul, norm_two, mul_assoc, mul_assoc,
      mul_le_mul_iff_of_pos_left two_pos, HurwitzKernelBounds.f_nat, pow_one, add_zero,
      norm_of_nonneg (exp_pos _).le, Real.norm_eq_abs, Nat.abs_cast, ← mul_assoc,
      mul_le_mul_iff_of_pos_right (exp_pos _)]
    exact mul_le_of_le_one_right (Nat.cast_nonneg _) (abs_sin_le_one _)

Premises used: le_refl, Real.norm_two, mul_le_mul_iff_of_pos_right, Nat.abs_cast, Nat.cast_nonneg, mul_assoc, two_pos, mul_le_mul_iff_of_pos_left, HurwitzKernelBounds.isBigO_atTop_F_nat_one, mul_le_of_le_one_right, LT.lt.le, norm_mul, pow_one, HurwitzKernelBounds.f_nat, Real.abs_sin_le_one, add_zero, OfNat.ofNat, HurwitzKernelBounds.F_nat, Real.norm_eq_abs, Real.norm_of_nonneg, Real.exp_pos, Filter.eventually_gt_atTop