awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
h1 :
  Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - HDiv.hDiv (α := ℂ) 1 2) * (hurwitzEvenFEPair a).Λ s)
    (𝓝[≠] HDiv.hDiv (α := ℂ) 1 2) (𝓝 1)
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * completedHurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)

Tactic:
(h1.comp <| tendsto_div_two_punctured_nhds 1).congr (fun s ↦ ?_)

Premises used: _private.0.HurwitzZeta.tendsto_div_two_punctured_nhds, Filter.Tendsto.congr, Filter.Tendsto.comp, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
h1 :
  Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - HDiv.hDiv (α := ℂ) 1 2) * (hurwitzEvenFEPair a).Λ s)
    (𝓝[≠] HDiv.hDiv (α := ℂ) 1 2) (𝓝 1)
refine :
  ∀ (s : ℂ),
    ((fun (s : ℂ) ↦ (s - HDiv.hDiv (α := ℂ) 1 2) * (hurwitzEvenFEPair a).Λ s) ∘ fun (s : ℂ) ↦ s / 2) s =
      (s - 1) * completedHurwitzZetaEven a s
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * completedHurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)

Tactic:
refine (h1.comp <| tendsto_div_two_punctured_nhds 1).congr (fun s ↦ ?_)

Premises used: _private.0.HurwitzZeta.tendsto_div_two_punctured_nhds, Filter.Tendsto.congr, Filter.Tendsto.comp, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
h1 :
  Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - HDiv.hDiv (α := ℂ) 1 2) * (hurwitzEvenFEPair a).Λ s)
    (𝓝[≠] HDiv.hDiv (α := ℂ) 1 2) (𝓝 1)
s : ℂ
rw :
  ((fun (s : ℂ) ↦ (s - HDiv.hDiv (α := ℂ) 1 2) * (hurwitzEvenFEPair a).Λ s) ∘ fun (s : ℂ) ↦ s / 2) s =
    (s - 1) * ((hurwitzEvenFEPair a).Λ (s / 2) / 2)
rw₁ :
  (s / 2 - HDiv.hDiv (α := ℂ) 1 2) * (hurwitzEvenFEPair a).Λ (s / 2) = (s - 1) * ((hurwitzEvenFEPair a).Λ (s / 2) / 2)
rw₂ : (s - 1) / 2 * (hurwitzEvenFEPair a).Λ (s / 2) = (s - 1) * ((hurwitzEvenFEPair a).Λ (s / 2) / 2)
rw₃ : (s - 1) * (hurwitzEvenFEPair a).Λ (s / 2) / 2 = (s - 1) * ((hurwitzEvenFEPair a).Λ (s / 2) / 2)
rw₄ rw₅ : (s - 1) * ((hurwitzEvenFEPair a).Λ (s / 2) / 2) = (s - 1) * ((hurwitzEvenFEPair a).Λ (s / 2) / 2)
⊢ ((fun (s : ℂ) ↦ (s - HDiv.hDiv (α := ℂ) 1 2) * (hurwitzEvenFEPair a).Λ s) ∘ fun (s : ℂ) ↦ s / 2) s =
    (s - 1) * completedHurwitzZetaEven a s

Tactic:
rw [completedHurwitzZetaEven, Function.comp_apply, ← sub_div, div_mul_eq_mul_div, mul_div_assoc]

Premises used: mul_div_assoc, sub_div, div_mul_eq_mul_div, HurwitzZeta.completedHurwitzZetaEven, Function.comp_apply
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (-if a = 0 then 1 else 0))

Tactic:
have h1 : Tendsto (fun s : ℂ ↦ s * _) (𝓝[≠] 0)
    (𝓝 (-(if a = 0 then 1 else 0))) := (hurwitzEvenFEPair a).Λ_residue_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
h1 : Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (-if a = 0 then 1 else 0))
pos : a = 0 → Eq (α := ℂ) (-1) (-1)
neg : ¬a = 0 → Eq (α := ℂ) (-0) 0
⊢ Eq (α := ℂ) (-if a = 0 then 1 else 0) (if a = 0 then -1 else 0)

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
h1 : Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (-if a = 0 then 1 else 0))
h : a = 0
⊢ Eq (α := ℂ) (-1) (-1)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
h1 : Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (-if a = 0 then 1 else 0))
h : ¬a = 0
⊢ Eq (α := ℂ) (-0) 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
h1 : Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (-if a = 0 then 1 else 0))
pos : a = 0 → Eq (α := ℂ) (-1) (-1)
neg : ¬a = 0 → Eq (α := ℂ) (-0) 0
pos₁ : a = 0 → Eq (α := ℂ) (-1) (-1)
neg₁ : ¬a = 0 → Eq (α := ℂ) (-0) 0
pos₂ : a = 0 → Eq (α := ℂ) (-1) (-1)
neg₂ : ¬a = 0 → Eq (α := ℂ) (-0) 0
pos₃ : a = 0 → Eq (α := ℂ) (-1) (-1)
neg₃ : ¬a = 0 → Eq (α := ℂ) (-0) 0
⊢ Eq (α := ℂ) (-if a = 0 then 1 else 0) (if a = 0 then -1 else 0)

Tactic:
{ split_ifs <;> simp }
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
h1 : Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (-if a = 0 then 1 else 0))
⊢ Eq (α := ℂ) (-if a = 0 then 1 else 0) (if a = 0 then -1 else 0)

Tactic:
have : -(if a = 0 then (1 : ℂ) else 0) = (if a = 0 then -1 else 0) := by { split_ifs <;> simp }
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
h1 : Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (-if a = 0 then 1 else 0))
this : Eq (α := ℂ) (-if a = 0 then 1 else 0) (if a = 0 then -1 else 0)
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (if a = 0 then -1 else 0))

Tactic:
simp only [this, push_cast] at h1
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
this : Eq (α := ℂ) (-if a = 0 then 1 else 0) (if a = 0 then -1 else 0)
h1 : Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (if a = 0 then -1 else 0))
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * completedHurwitzZetaEven a s) (𝓝[≠] 0) (𝓝 (if a = 0 then -1 else 0))

Tactic:
(h1.comp <| zero_div (2 : ℂ) ▸ (tendsto_div_two_punctured_nhds 0)).congr (fun s ↦ ?_)

Premises used: Filter.Tendsto.congr, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
this : Eq (α := ℂ) (-if a = 0 then 1 else 0) (if a = 0 then -1 else 0)
h1 : Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (if a = 0 then -1 else 0))
refine :
  ∀ (s : ℂ), ((fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).Λ s) ∘ fun (s : ℂ) ↦ s / 2) s = s * completedHurwitzZetaEven a s
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * completedHurwitzZetaEven a s) (𝓝[≠] 0) (𝓝 (if a = 0 then -1 else 0))

Tactic:
refine (h1.comp <| zero_div (2 : ℂ) ▸ (tendsto_div_two_punctured_nhds 0)).congr (fun s ↦ ?_)

Premises used: Filter.Tendsto.congr, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
this : Eq (α := ℂ) (-if a = 0 then 1 else 0) (if a = 0 then -1 else 0)
h1 : Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (if a = 0 then -1 else 0))
s : ℂ
⊢ ((fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).Λ s) ∘ fun (s : ℂ) ↦ s / 2) s = s * completedHurwitzZetaEven a s

Tactic:
simp [completedHurwitzZetaEven, div_mul_eq_mul_div, mul_div_assoc]

Premises used: mul_div_assoc, div_mul_eq_mul_div, HurwitzZeta.completedHurwitzZetaEven
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).symm.Λ s) (𝓝[≠] 0) (𝓝 (-1))

Tactic:
have h1 : Tendsto (fun s : ℂ ↦ s * _) (𝓝[≠] 0)
    (𝓝 (-1)) := (hurwitzEvenFEPair a).symm.Λ_residue_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
h1 : Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).symm.Λ s) (𝓝[≠] 0) (𝓝 (-1))
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * completedCosZeta a s) (𝓝[≠] 0) (𝓝 (-1))

Tactic:
(h1.comp <| zero_div (2 : ℂ) ▸ (tendsto_div_two_punctured_nhds 0)).congr (fun s ↦ ?_)

Premises used: Filter.Tendsto.congr, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
h1 : Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).symm.Λ s) (𝓝[≠] 0) (𝓝 (-1))
refine :
  ∀ (s : ℂ), ((fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).symm.Λ s) ∘ fun (s : ℂ) ↦ s / 2) s = s * completedCosZeta a s
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * completedCosZeta a s) (𝓝[≠] 0) (𝓝 (-1))

Tactic:
refine (h1.comp <| zero_div (2 : ℂ) ▸ (tendsto_div_two_punctured_nhds 0)).congr (fun s ↦ ?_)

Premises used: Filter.Tendsto.congr, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
h1 : Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).symm.Λ s) (𝓝[≠] 0) (𝓝 (-1))
s : ℂ
⊢ ((fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).symm.Λ s) ∘ fun (s : ℂ) ↦ s / 2) s = s * completedCosZeta a s

Tactic:
simp [completedCosZeta, div_mul_eq_mul_div, mul_div_assoc]

Premises used: mul_div_assoc, div_mul_eq_mul_div, HurwitzZeta.completedCosZeta
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
t : ℝ
ht : 0 < t
⊢ HasSum (fun (n : ℤ) ↦ if n = 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
    (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)

Tactic:
((hasSum_int_cosKernel₀ a ht).div_const 2).congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun, HurwitzZeta.hasSum_int_cosKernel₀, HasSum.div_const, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
t : ℝ
ht : 0 < t
refine :
  ∀ (n : ℤ),
    (if n = 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ)) =
      (if n = 0 then 0
        else
          cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
            (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ)) /
        2
⊢ HasSum (fun (n : ℤ) ↦ if n = 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
    (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)

Tactic:
refine ((hasSum_int_cosKernel₀ a ht).div_const 2).congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun, HurwitzZeta.hasSum_int_cosKernel₀, HasSum.div_const, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
t : ℝ
ht : 0 < t
n : ℤ
pos : n = 0 → 0 = 0 / 2
neg :
  ¬n = 0 →
    c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) =
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) /
        2
⊢ (if n = 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ)) =
    (if n = 0 then 0
      else
        cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ)) /
      2

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
t : ℝ
ht : 0 < t
n : ℤ
h : n = 0
⊢ 0 = 0 / 2

Tactic:
simp [c, div_mul_eq_mul_div]

Premises used: div_mul_eq_mul_div
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
t : ℝ
ht : 0 < t
n : ℤ
h : ¬n = 0
⊢ c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) =
    cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) / 2

Tactic:
simp [c, div_mul_eq_mul_div]

Premises used: div_mul_eq_mul_div
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
⊢ ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ if n = 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)

Tactic:
have hF t (ht : 0 < t) : HasSum (fun n : ℤ ↦ if n = 0 then 0 else c n * rexp (-π * n ^ 2 * t))
      ((cosKernel a t - 1) / 2) := by
    refine ((hasSum_int_cosKernel₀ a ht).div_const 2).congr_fun fun n ↦ ?_
    split_ifs <;> simp [c, div_mul_eq_mul_div]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum (fun (n : ℤ) ↦ if n = 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
⊢ ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)

Tactic:
simp only [← Int.cast_eq_zero (α := ℝ)] at hF

Premises used: Int.cast_eq_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
rw :
  (hurwitzEvenFEPair (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)).symm.Λ (s / 2) / 2 =
    HDiv.hDiv (α := ℂ) (mellin (fun (t : ℝ) ↦ (↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) (s / 2)) 2
⊢ completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s =
    mellin (fun (t : ℝ) ↦ ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2) (s / 2)

Tactic:
rw [mellin_div_const, completedCosZeta]

Premises used: mellin_div_const, HurwitzZeta.completedCosZeta
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
e_a :
  (hurwitzEvenFEPair (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)).symm.Λ (s / 2) =
    mellin (fun (t : ℝ) ↦ (↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) (s / 2)
⊢ (hurwitzEvenFEPair (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)).symm.Λ (s / 2) / 2 =
    HDiv.hDiv (α := ℂ) (mellin (fun (t : ℝ) ↦ (↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) (s / 2)) 2

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
⊢ (hurwitzEvenFEPair (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)).symm.Λ (s / 2) =
    mellin (fun (t : ℝ) ↦ (↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) (s / 2)

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

Premises used: QuotientAddGroup.mk, And.right, WeakFEPair.hasMellin, WeakFEPair.symm, Eq.symm, HurwitzZeta.hurwitzEvenFEPair
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
e_a : 1 / 2 < (s / 2).re
⊢ (hurwitzEvenFEPair (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)).symm.Λ (s / 2) =
    mellin (fun (t : ℝ) ↦ (↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) (s / 2)

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

Premises used: QuotientAddGroup.mk, And.right, WeakFEPair.hasMellin, WeakFEPair.symm, Eq.symm, HurwitzZeta.hurwitzEvenFEPair
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
e_a : 1 / 2 < s.re / 2
e_a₁ e_a₂ e_a₃ e_a₄ : 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
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
rw :
  HasSum (α := ℂ)
    (fun (n : ℤ) ↦ s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2)
    (mellin (fun (t : ℝ) ↦ ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2) (s / 2))
⊢ HasSum (fun (n : ℤ) ↦ s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
rw [show completedCosZeta a s = mellin (fun t ↦ (cosKernel a t - 1 : ℂ) / 2) (s / 2) by
    rw [mellin_div_const, completedCosZeta]
    congr 1
    refine ((hurwitzEvenFEPair a).symm.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
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
⊢ HasSum (α := ℂ)
    (fun (n : ℤ) ↦ s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2)
    (mellin (fun (t : ℝ) ↦ ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 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
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
refine_1 : Summable (α := ℝ) fun (i : ℤ) ↦ ‖c i‖ / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re
refine_2 :
  ∀ (n : ℤ),
    s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2 =
      s.Gammaℝ * c n / (↑|(↑n : ℝ)| : ℂ) ^ s
⊢ HasSum (α := ℂ)
    (fun (n : ℤ) ↦ s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2)
    (mellin (fun (t : ℝ) ↦ ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 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
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
refine_1 : ∀ (i : ℤ), ‖‖c i‖ / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re‖ ≤ 1 / |HAdd.hAdd (α := ℝ) (↑i : ℝ) 0| ^ s.re / 2
⊢ Summable (α := ℝ) fun (i : ℤ) ↦ ‖c i‖ / HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re

Tactic:
apply (((summable_one_div_int_add_rpow 0 s.re).mpr hs).div_const 2).of_norm_bounded

Premises used: Iff.mpr, Complex.re, Summable.of_norm_bounded, OfNat.ofNat, Summable.div_const, Real.summable_one_div_int_add_rpow
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
i : ℤ
push_cast : 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑i : ℂ) = 2 * (↑π : ℂ) * (↑a : ℂ) * (↑i : ℂ) * I
⊢ 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑i : ℂ) = (↑(2 * π * a * (↑i : ℝ)) : ℂ) * I

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
i : ℤ
⊢ 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑i : ℂ) = 2 * (↑π : ℂ) * (↑a : ℂ) * (↑i : ℂ) * I

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
i : ℤ
ring ring₁ : 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑i : ℂ) = 2 * (↑π : ℂ) * (↑a : ℂ) * (↑i : ℂ) * I
⊢ 2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑i : ℂ) = (↑(2 * π * a * (↑i : ℝ)) : ℂ) * I

Tactic:
{ push_cast; ring }
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
i : ℤ
⊢ 0 ≤ HPow.hPow (α := ℝ) |(↑i : ℝ)| s.re

Tactic:
positivity
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
hF :
  ∀ (t : ℝ) (ht : 0 < t),
    HasSum
      (fun (n : ℤ) ↦
        if Eq (α := ℝ) (↑n : ℝ) 0 then 0 else c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ))
      (((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2)
n : ℤ
⊢ s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2 =
    s.Gammaℝ * c n / (↑|(↑n : ℝ)| : ℂ) ^ s

Tactic:
simp [c, ← Int.cast_abs, div_right_comm, mul_div_assoc]

Premises used: Int.cast_abs, div_right_comm, mul_div_assoc
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
rw : HPow.hPow (α := ℂ) (↑0 : ℂ) s = 0
rw₁ : HPow.hPow (α := ℂ) 0 s = 0
rw₂ rw₃ : Eq (α := ℂ) 0 0
⊢ HPow.hPow (α := ℂ) (↑|0| : ℂ) s = 0

Tactic:
rw [abs_zero, Int.cast_zero, zero_cpow (ne_zero_of_one_lt_re hs)]

Premises used: Int.cast_zero, Complex.ne_zero_of_one_lt_re, Complex.zero_cpow, abs_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HPow.hPow (α := ℂ) (↑|0| : ℂ) s = 0

Tactic:
have aux : ((|0| : ℤ) : ℂ) ^ s = 0 := by
    rw [abs_zero, Int.cast_zero, zero_cpow (ne_zero_of_one_lt_re hs)]