awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
aux : HPow.hPow (α := ℂ) (↑|0| : ℂ) s = 0
⊢ HasSum
    (fun (n : ℕ) ↦
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
        s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s /
          2)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s +
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) / HPow.hPow (α := ℂ) (↑|0| : ℂ) s / 2)

Tactic:
have hint := (hasSum_int_completedCosZeta a hs).nat_add_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
aux : HPow.hPow (α := ℂ) (↑|0| : ℂ) s = 0
hint :
  HasSum
    (fun (n : ℕ) ↦
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
        s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s /
          2)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s +
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) / HPow.hPow (α := ℂ) (↑|0| : ℂ) s / 2)
⊢ HasSum
    (fun (n : ℕ) ↦
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
        s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s /
          2)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
rw [aux, div_zero, zero_div, add_zero] at hint

Premises used: zero_div, add_zero, div_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
aux : HPow.hPow (α := ℂ) (↑|0| : ℂ) s = 0
hint :
  HasSum
    (fun (n : ℕ) ↦
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
        s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s /
          2)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
⊢ HasSum
    (fun (n : ℕ) ↦
      if n = 0 then 0 else s.Gammaℝ * (↑(Real.cos (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
hint.congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
aux : HPow.hPow (α := ℂ) (↑|0| : ℂ) s = 0
hint :
  HasSum
    (fun (n : ℕ) ↦
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
        s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s /
          2)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
refine :
  ∀ (n : ℕ),
    (if n = 0 then 0 else s.Gammaℝ * (↑(Real.cos (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s) =
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
        s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s /
          2
⊢ HasSum
    (fun (n : ℕ) ↦
      if n = 0 then 0 else s.Gammaℝ * (↑(Real.cos (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
refine hint.congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
aux : HPow.hPow (α := ℂ) (↑|0| : ℂ) s = 0
hint :
  HasSum
    (fun (n : ℕ) ↦
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
        s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s /
          2)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
n : ℕ
pos :
  ∀ (h : n = 0),
    0 =
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
        s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s /
          2
neg :
  ∀ (h : ¬n = 0),
    s.Gammaℝ * (↑(Real.cos (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
        s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s /
          2
⊢ (if n = 0 then 0 else s.Gammaℝ * (↑(Real.cos (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s) =
    s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s / 2

Tactic:
split_ifs with h
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
aux : HPow.hPow (α := ℂ) (↑|0| : ℂ) s = 0
hint :
  HasSum
    (fun (n : ℕ) ↦
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
        s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s /
          2)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
n : ℕ
h : n = 0
⊢ 0 =
    s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s / 2

Tactic:
simp only [h, Nat.cast_zero, aux, div_zero, zero_div, neg_zero, zero_add]

Premises used: zero_div, zero_add, Nat.cast_zero, neg_zero, div_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
aux : HPow.hPow (α := ℂ) (↑|0| : ℂ) s = 0
hint :
  HasSum
    (fun (n : ℕ) ↦
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
        s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s /
          2)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
n : ℕ
h : ¬n = 0
⊢ 2 * (↑π : ℂ) * (↑a : ℂ) * (↑n : ℂ) * I = 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
aux : HPow.hPow (α := ℂ) (↑|0| : ℂ) s = 0
hint :
  HasSum
    (fun (n : ℕ) ↦
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
        s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s /
          2)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
n : ℕ
h : ¬n = 0
⊢ s.Gammaℝ * (↑(Real.cos (2 * π * a * (↑n : ℝ))) : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) / HPow.hPow (α := ℂ) (↑|(↑n : ℤ)| : ℂ) s / 2 +
      s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) / HPow.hPow (α := ℂ) (↑|(-(↑n : ℤ))| : ℂ) s / 2

Tactic:
simp only [ofReal_cos, ofReal_mul, ofReal_ofNat, ofReal_natCast, Complex.cos,
      show 2 * π * a * n * I = 2 * π * I * a * n by ring, neg_mul, mul_div_assoc,
      div_right_comm _ (2 : ℂ), Int.cast_natCast, Nat.abs_cast, Int.cast_neg, mul_neg, abs_neg, ←
      mul_add, ← add_div]

Premises used: Int.cast_neg, Int.cast_natCast, abs_neg, div_right_comm, Complex.cos, Nat.abs_cast, mul_div_assoc, Complex.ofReal_natCast, Complex.ofReal_cos, mul_add, neg_mul, Complex.ofReal_ofNat, OfNat.ofNat, Complex.ofReal_mul, mul_neg, add_div
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
t : ℝ
ht : 0 < t
refine :
  ∀ (n : ℤ),
    (if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ)) =
      (↑(if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) / 2
⊢ HasSum
    (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(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) :
          ℂ)) /
      2)

Tactic:
refine (ofReal_sub .. ▸ (hasSum_ofReal.mpr (hasSum_int_evenKernel₀ a ht)).div_const
      2).congr_fun fun n ↦ ?_
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
t : ℝ
ht : 0 < t
n : ℤ
pos : (↑n : ℝ) + a = 0 → 0 = (↑0 : ℂ) / 2
neg :
  ¬(↑n : ℝ) + a = 0 →
    1 / 2 * (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) =
      (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) / 2
⊢ (if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ)) =
    (↑(if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) / 2

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
t : ℝ
ht : 0 < t
n : ℤ
h : (↑n : ℝ) + a = 0
pos : 0 = 0 / 2
pos₁ pos₂ : Eq (α := ℂ) 0 0
⊢ 0 = (↑0 : ℂ) / 2

Tactic:
rw [ofReal_zero, zero_div]

Premises used: zero_div, Complex.ofReal_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
t : ℝ
ht : 0 < t
n : ℤ
h : ¬(↑n : ℝ) + a = 0
neg :
  (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) * (1 / 2) =
    (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) / 2
neg₁ neg₂ :
  (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) / 2 =
    (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) / 2
⊢ 1 / 2 * (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) =
    (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) : ℂ) / 2

Tactic:
rw [mul_comm, mul_one_div]

Premises used: mul_one_div, mul_comm
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(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) :
            ℂ)) /
        2)

Tactic:
have hF (t : ℝ) (ht : 0 < t) : HasSum (fun n : ℤ ↦ if n + a = 0 then 0
      else (1 / 2 : ℂ) * rexp (-π * (n + a) ^ 2 * t))
      ((evenKernel a t - (if (a : UnitAddCircle) = 0 then 1 else 0 : ℝ)) / 2) := by
    refine (ofReal_sub .. ▸ (hasSum_ofReal.mpr (hasSum_int_evenKernel₀ a ht)).div_const
      2).congr_fun fun n ↦ ?_
    split_ifs
    · rw [ofReal_zero, zero_div]
    · rw [mul_comm, mul_one_div]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(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) :
            ℂ)) /
        2)
simp_rw :
  completedHurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s =
    HDiv.hDiv (α := ℂ)
      (mellin
        (fun (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)
        (s / 2))
      2
⊢ completedHurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s =
    mellin
      (fun (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) :
              ℂ)) /
          2)
      (s / 2)

Tactic:
simp_rw [mellin_div_const, apply_ite ofReal, ofReal_one, ofReal_zero]

Premises used: mellin_div_const, apply_ite, Complex.ofReal_one, Complex.ofReal, Complex.ofReal_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(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) :
            ℂ)) /
        2)
⊢ completedHurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s =
    HDiv.hDiv (α := ℂ)
      (mellin
        (fun (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)
        (s / 2))
      2

Tactic:
congr_arg (· / 2) ((hurwitzEvenFEPair a).hasMellin (?_ : 1 / 2 < (s / 2).re)).2.symm

Premises used: QuotientAddGroup.mk, HDiv.hDiv, congr_arg, And.right, HurwitzZeta.completedHurwitzZetaEven, WeakFEPair.hasMellin, OfNat.ofNat, Eq.symm, HurwitzZeta.hurwitzEvenFEPair
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(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) :
            ℂ)) /
        2)
refine : 1 / 2 < (s / 2).re
⊢ completedHurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s =
    HDiv.hDiv (α := ℂ)
      (mellin
        (fun (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)
        (s / 2))
      2

Tactic:
refine congr_arg (· / 2) ((hurwitzEvenFEPair a).hasMellin (?_ : 1 / 2 < (s / 2).re)).2.symm

Premises used: QuotientAddGroup.mk, HDiv.hDiv, congr_arg, And.right, WeakFEPair.hasMellin, OfNat.ofNat, Eq.symm, HurwitzZeta.hurwitzEvenFEPair
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(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) :
            ℂ)) /
        2)
rwa : 1 / 2 < s.re / 2
rwa₁ rwa₂ rwa₃ rwa₄ : 1 < s.re
⊢ 1 / 2 < (s / 2).re

Tactic:
rwa [div_ofNat_re, div_lt_div_iff_of_pos_right two_pos]

Premises used: div_lt_div_iff_of_pos_right, Complex.div_ofNat_re
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(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) :
            ℂ)) /
        2)
rw :
  HasSum (α := ℂ) (fun (n : ℤ) ↦ s.Gammaℝ / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2)
    (mellin
      (fun (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) :
              ℂ)) /
          2)
      (s / 2))
⊢ HasSum (fun (n : ℤ) ↦ s.Gammaℝ / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2)
    (completedHurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
rw [show completedHurwitzZetaEven a s = mellin (fun t ↦ ((evenKernel (↑a) t : ℂ) -
        ↑(if (a : UnitAddCircle) = 0 then 1 else 0 : ℝ)) / 2) (s / 2) by
    simp_rw [mellin_div_const, apply_ite ofReal, ofReal_one, ofReal_zero]
    refine congr_arg (· / 2) ((hurwitzEvenFEPair a).hasMellin (?_ : 1 / 2 < (s / 2).re)).2.symm
    rwa [div_ofNat_re, div_lt_div_iff_of_pos_right two_pos]]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(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) :
            ℂ)) /
        2)
⊢ HasSum (α := ℂ) (fun (n : ℤ) ↦ s.Gammaℝ / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2)
    (mellin
      (fun (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) :
              ℂ)) /
          2)
      (s / 2))

Tactic:
(hasSum_mellin_pi_mul_sq (zero_lt_one.trans hs) hF ?_).congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun, zero_lt_one, LT.lt.trans, hasSum_mellin_pi_mul_sq
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(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) :
            ℂ)) /
        2)
refine_1 : Summable (α := ℝ) fun (i : ℤ) ↦ ‖1 / 2‖ / |(↑i : ℝ) + a| ^ s.re
refine_2 : ∀ (n : ℤ), s.Gammaℝ / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 = s.Gammaℝ * (1 / 2) / (↑|(↑n : ℝ) + a| : ℂ) ^ s
⊢ HasSum (α := ℂ) (fun (n : ℤ) ↦ s.Gammaℝ / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2)
    (mellin
      (fun (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) :
              ℂ)) /
          2)
      (s / 2))

Tactic:
refine (hasSum_mellin_pi_mul_sq (zero_lt_one.trans hs) hF ?_).congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun, zero_lt_one, LT.lt.trans, hasSum_mellin_pi_mul_sq
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(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) :
            ℂ)) /
        2)
refine_1 : Summable (α := ℝ) fun (i : ℤ) ↦ ‖1 / 2‖ * (1 / |(↑i : ℝ) + a| ^ s.re)
⊢ Summable (α := ℝ) fun (i : ℤ) ↦ ‖1 / 2‖ / |(↑i : ℝ) + a| ^ s.re

Tactic:
simp_rw [← mul_one_div ‖_‖]

Premises used: Norm.norm, mul_one_div
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(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) :
            ℂ)) /
        2)
refine_1 : Summable (α := ℝ) fun (i : ℤ) ↦ 1 / |(↑i : ℝ) + a| ^ s.re
⊢ Summable (α := ℝ) fun (i : ℤ) ↦ ‖1 / 2‖ * (1 / |(↑i : ℝ) + a| ^ s.re)

Tactic:
apply Summable.mul_left

Premises used: Summable.mul_left
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if (↑n : ℝ) + a = 0 then 0 else 1 / 2 * (↑(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) :
            ℂ)) /
        2)
n : ℤ
refine_2 : s.Gammaℝ / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 = s.Gammaℝ / 2 / (↑|(↑n : ℝ) + a| : ℂ) ^ s
refine_2₁ refine_2₂ : s.Gammaℝ / 2 / (↑|(↑n : ℝ) + a| : ℂ) ^ s = s.Gammaℝ / 2 / (↑|(↑n : ℝ) + a| : ℂ) ^ s
⊢ s.Gammaℝ / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 = s.Gammaℝ * (1 / 2) / (↑|(↑n : ℝ) + a| : ℂ) ^ s

Tactic:
rw [mul_one_div, div_right_comm]

Premises used: div_right_comm, mul_one_div
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun (s : ℂ) ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
⊢ ∀ (t : ℂ) (ht : t ≠ 0) (ht' : t ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (u : ℂ) ↦ Λ u / u.Gammaℝ) t

Tactic:
have claim (t) (ht : t ≠ 0) (ht' : t ≠ 1) : DifferentiableAt ℂ (fun u : ℂ ↦ Λ u / Gammaℝ u) t :=
    (hf t ht ht').mul differentiable_Gammaℝ_inv.differentiableAt
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun (s : ℂ) ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
claim : ∀ (t : ℂ) (ht : t ≠ 0) (ht' : t ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (u : ℂ) ↦ Λ u / u.Gammaℝ) t
⊢ Tendsto (fun (s : ℂ) ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))

Tactic:
Tendsto.congr' ?_ (h_lim.div Gammaℝ_residue_zero two_ne_zero)

Premises used: Filter.Tendsto.div, two_ne_zero, Complex.Gammaℝ_residue_zero, Filter.Tendsto.congr'