awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
rw : completedHurwitzZetaEven a (1 - (1 - s)) = completedHurwitzZetaEven a s
⊢ completedCosZeta a (1 - s) = completedHurwitzZetaEven a s
have rw₁ : completedHurwitzZetaEven a s = completedHurwitzZetaEven a s
Tactic: rw [← completedHurwitzZetaEven_one_sub, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
⊢ completedCosZeta₀ a (1 - s) = completedHurwitzZetaEven₀ a s
have rw : completedHurwitzZetaEven₀ a (1 - (1 - s)) = completedHurwitzZetaEven₀ a s
Tactic: rw [← completedHurwitzZetaEven₀_one_sub, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
rw : completedHurwitzZetaEven₀ a (1 - (1 - s)) = completedHurwitzZetaEven₀ a s
⊢ completedCosZeta₀ a (1 - s) = completedHurwitzZetaEven₀ a s
have rw₁ : completedHurwitzZetaEven₀ a s = completedHurwitzZetaEven₀ a s
Tactic: rw [← completedHurwitzZetaEven₀_one_sub, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
⊢ DifferentiableAt ℂ (completedHurwitzZetaEven a) s
have refine_1 : s / 2 ≠ 0 ∨ (hurwitzEvenFEPair a).f₀ = 0
Tactic: refine (((hurwitzEvenFEPair a).differentiableAt_Λ ?_ (Or.inl ?_)).comp s
      (differentiableAt_id.div_const _)).div_const _
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
refine_1 : s / 2 ≠ 0 ∨ (hurwitzEvenFEPair a).f₀ = 0
⊢ DifferentiableAt ℂ (completedHurwitzZetaEven a) s
have refine_2 : s / 2 ≠ (↑(hurwitzEvenFEPair a).k : ℂ)
Tactic: refine (((hurwitzEvenFEPair a).differentiableAt_Λ ?_ (Or.inl ?_)).comp s
      (differentiableAt_id.div_const _)).div_const _
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
⊢ s / 2 ≠ 0 ∨ (hurwitzEvenFEPair a).f₀ = 0
have refine_1 : ∀ (h : s ≠ 0), s / 2 ≠ 0 ∨ (hurwitzEvenFEPair a).f₀ = 0
Tactic: rcases hs with h | h
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
refine_1 : ∀ (h : s ≠ 0), s / 2 ≠ 0 ∨ (hurwitzEvenFEPair a).f₀ = 0
⊢ s / 2 ≠ 0 ∨ (hurwitzEvenFEPair a).f₀ = 0
have refine_1₁ : ∀ (h : a ≠ 0), s / 2 ≠ 0 ∨ (hurwitzEvenFEPair a).f₀ = 0
Tactic: rcases hs with h | h
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
⊢ s / 2 ≠ (↑(1 / 2) : ℂ)
have refine_2 : s / 2 ≠ HDiv.hDiv (α := ℂ) 1 2
Tactic: rw [ofReal_div, ofReal_one, ofReal_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a b : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
    completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
      HSub.hSub (α := ℂ) (if a = 0 then 1 else 0) (if b = 0 then 1 else 0) / s
have simp_rw : completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s - 1 / (1 - s) -
    (completedHurwitzZetaEven₀ b s - (if b = 0 then 1 else 0) / s - 1 / (1 - s)) =
  completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
    ((if a = 0 then 1 else 0) / s - (if b = 0 then 1 else 0) / s)
Tactic: simp_rw [completedHurwitzZetaEven_eq, sub_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a b : UnitAddCircle
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s - completedHurwitzZetaEven b s) 1
have this : ∀ (s : ℂ),
  completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
    completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
      HSub.hSub (α := ℂ) (if a = 0 then 1 else 0) (if b = 0 then 1 else 0) / s
Tactic: have (s : _) : completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
      ((if a = 0 then 1 else 0) - (if b = 0 then 1 else 0)) / s := by
    simp_rw [completedHurwitzZetaEven_eq, sub_div]
    abel
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a b : UnitAddCircle
this :
  ∀ (s : ℂ),
    completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
        HSub.hSub (α := ℂ) (if a = 0 then 1 else 0) (if b = 0 then 1 else 0) / s
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s - completedHurwitzZetaEven b s) 1
have rw : DifferentiableAt ℂ (F := ℂ)
  (fun (x : ℂ) ↦
    completedHurwitzZetaEven₀ a x - completedHurwitzZetaEven₀ b x -
      HSub.hSub (α := ℂ) (if a = 0 then 1 else 0) (if b = 0 then 1 else 0) / x)
  1
Tactic: rw [funext this]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a b : UnitAddCircle
this :
  ∀ (s : ℂ),
    completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
        HSub.hSub (α := ℂ) (if a = 0 then 1 else 0) (if b = 0 then 1 else 0) / s
⊢ DifferentiableAt ℂ (F := ℂ)
    (fun (x : ℂ) ↦
      completedHurwitzZetaEven₀ a x - completedHurwitzZetaEven₀ b x -
        HSub.hSub (α := ℂ) (if a = 0 then 1 else 0) (if b = 0 then 1 else 0) / x)
    1
have refine : DifferentiableAt ℂ (F := ℂ) (fun (x : ℂ) ↦ completedHurwitzZetaEven₀ a x - completedHurwitzZetaEven₀ b x) 1
Tactic: refine .sub ?_ <| (differentiable_const _ _).div (differentiable_id _) one_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a b : UnitAddCircle
this :
  ∀ (s : ℂ),
    completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
        HSub.hSub (α := ℂ) (if a = 0 then 1 else 0) (if b = 0 then 1 else 0) / s
⊢ DifferentiableAt ℂ (F := ℂ) (fun (x : ℂ) ↦ completedHurwitzZetaEven₀ a x - completedHurwitzZetaEven₀ b x) 1
have hf : DifferentiableAt ℂ (completedHurwitzZetaEven₀ a) 1
Tactic: apply DifferentiableAt.sub
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a b : UnitAddCircle
this :
  ∀ (s : ℂ),
    completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
        HSub.hSub (α := ℂ) (if a = 0 then 1 else 0) (if b = 0 then 1 else 0) / s
hf : DifferentiableAt ℂ (completedHurwitzZetaEven₀ a) 1
⊢ DifferentiableAt ℂ (F := ℂ) (fun (x : ℂ) ↦ completedHurwitzZetaEven₀ a x - completedHurwitzZetaEven₀ b x) 1
have hg : DifferentiableAt ℂ (completedHurwitzZetaEven₀ b) 1
Tactic: apply DifferentiableAt.sub
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
⊢ DifferentiableAt ℂ (completedCosZeta a) s
have refine_1 : s / 2 ≠ 0
Tactic: refine (((hurwitzEvenFEPair a).symm.differentiableAt_Λ (Or.inl ?_) ?_).comp s
      (differentiableAt_id.div_const _)).div_const _
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
refine_1 : s / 2 ≠ 0
⊢ DifferentiableAt ℂ (completedCosZeta a) s
have refine_2 : s / 2 ≠ (↑(hurwitzEvenFEPair a).symm.k : ℂ) ∨ (hurwitzEvenFEPair a).symm.g₀ = 0
Tactic: refine (((hurwitzEvenFEPair a).symm.differentiableAt_Λ (Or.inl ?_) ?_).comp s
      (differentiableAt_id.div_const _)).div_const _
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
⊢ s / 2 ≠ (↑(hurwitzEvenFEPair a).symm.k : ℂ) ∨ (hurwitzEvenFEPair a).symm.g₀ = 0
have refine_2 : s / 2 ≠ (↑(1 / 2) : ℂ) ∨ Eq (α := ℂ) (if a = 0 then 1 else 0) 0
Tactic: change s / 2 ≠ ↑(1 / 2 : ℝ) ∨ (if a = 0 then 1 else 0) = 0
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
⊢ s / 2 ≠ (↑(1 / 2) : ℂ) ∨ Eq (α := ℂ) (if a = 0 then 1 else 0) 0
have refine_2 : ∀ (h : s ≠ 1), s / 2 ≠ (↑(1 / 2) : ℂ)
Tactic: refine Or.imp (fun h ↦ ?_) (fun ha ↦ ?_) hs'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
refine_2 : ∀ (h : s ≠ 1), s / 2 ≠ (↑(1 / 2) : ℂ)
⊢ s / 2 ≠ (↑(1 / 2) : ℂ) ∨ Eq (α := ℂ) (if a = 0 then 1 else 0) 0
have refine_2₁ : ∀ (ha : a ≠ 0), Eq (α := ℂ) (if a = 0 then 1 else 0) 0
Tactic: refine Or.imp (fun h ↦ ?_) (fun ha ↦ ?_) hs'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a : UnitAddCircle
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * completedHurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)
have h1 : Tendsto (fun (s : ℂ) ↦ (s - (↑(1 / 2) : ℂ)) * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] (↑(1 / 2) : ℂ))
  (𝓝 (HMul.hMul (α := ℂ) 1 1))
Tactic: have h1 : Tendsto (fun s : ℂ ↦ (s - ↑(1 / 2 : ℝ)) * _) (𝓝[≠] ↑(1 / 2 : ℝ))
    (𝓝 ((1 : ℂ) * (1 : ℂ))) := (hurwitzEvenFEPair a).Λ_residue_k
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a : UnitAddCircle
h1 :
  Tendsto (fun (s : ℂ) ↦ (s - (↑(1 / 2) : ℂ)) * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] (↑(1 / 2) : ℂ))
    (𝓝 (HMul.hMul (α := ℂ) 1 1))
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * completedHurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)
have h1₁ : Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - HDiv.hDiv (α := ℂ) 1 2) * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] HDiv.hDiv (α := ℂ) 1 2)
  (𝓝 1)
Tactic: simp only [push_cast, one_mul] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
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)
have refine : ∀ (s : ℂ),
  ((fun (s : ℂ) ↦ (s - HDiv.hDiv (α := ℂ) 1 2) * (hurwitzEvenFEPair a).Λ s) ∘ fun (s : ℂ) ↦ s / 2) s =
    (s - 1) * completedHurwitzZetaEven a s
Tactic: refine (h1.comp <| tendsto_div_two_punctured_nhds 1).congr (fun s ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
h1 :
  Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - HDiv.hDiv (α := ℂ) 1 2) * (hurwitzEvenFEPair a).Λ s)
    (𝓝[≠] HDiv.hDiv (α := ℂ) 1 2) (𝓝 1)
s : ℂ
⊢ ((fun (s : ℂ) ↦ (s - HDiv.hDiv (α := ℂ) 1 2) * (hurwitzEvenFEPair a).Λ s) ∘ fun (s : ℂ) ↦ s / 2) s =
    (s - 1) * completedHurwitzZetaEven a s
have rw : ((fun (s : ℂ) ↦ (s - HDiv.hDiv (α := ℂ) 1 2) * (hurwitzEvenFEPair a).Λ s) ∘ fun (s : ℂ) ↦ s / 2) s =
  (s - 1) * ((hurwitzEvenFEPair a).Λ (s / 2) / 2)
Tactic: rw [completedHurwitzZetaEven, Function.comp_apply, ← sub_div, div_mul_eq_mul_div, mul_div_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
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)
⊢ ((fun (s : ℂ) ↦ (s - HDiv.hDiv (α := ℂ) 1 2) * (hurwitzEvenFEPair a).Λ s) ∘ fun (s : ℂ) ↦ s / 2) s =
    (s - 1) * completedHurwitzZetaEven a s
have rw₁ : (s / 2 - HDiv.hDiv (α := ℂ) 1 2) * (hurwitzEvenFEPair a).Λ (s / 2) = (s - 1) * ((hurwitzEvenFEPair a).Λ (s / 2) / 2)
Tactic: rw [completedHurwitzZetaEven, Function.comp_apply, ← sub_div, div_mul_eq_mul_div, mul_div_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
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)
⊢ ((fun (s : ℂ) ↦ (s - HDiv.hDiv (α := ℂ) 1 2) * (hurwitzEvenFEPair a).Λ s) ∘ fun (s : ℂ) ↦ s / 2) s =
    (s - 1) * completedHurwitzZetaEven a s
have rw₂ : (s - 1) / 2 * (hurwitzEvenFEPair a).Λ (s / 2) = (s - 1) * ((hurwitzEvenFEPair a).Λ (s / 2) / 2)
Tactic: rw [completedHurwitzZetaEven, Function.comp_apply, ← sub_div, div_mul_eq_mul_div, mul_div_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
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)
⊢ ((fun (s : ℂ) ↦ (s - HDiv.hDiv (α := ℂ) 1 2) * (hurwitzEvenFEPair a).Λ s) ∘ fun (s : ℂ) ↦ s / 2) s =
    (s - 1) * completedHurwitzZetaEven a s
have rw₃ : (s - 1) * (hurwitzEvenFEPair a).Λ (s / 2) / 2 = (s - 1) * ((hurwitzEvenFEPair a).Λ (s / 2) / 2)
Tactic: rw [completedHurwitzZetaEven, Function.comp_apply, ← sub_div, div_mul_eq_mul_div, mul_div_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
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)
⊢ ((fun (s : ℂ) ↦ (s - HDiv.hDiv (α := ℂ) 1 2) * (hurwitzEvenFEPair a).Λ s) ∘ fun (s : ℂ) ↦ s / 2) s =
    (s - 1) * completedHurwitzZetaEven a s
have rw₄ : (s - 1) * ((hurwitzEvenFEPair a).Λ (s / 2) / 2) = (s - 1) * ((hurwitzEvenFEPair a).Λ (s / 2) / 2)
Tactic: rw [completedHurwitzZetaEven, Function.comp_apply, ← sub_div, div_mul_eq_mul_div, mul_div_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a : UnitAddCircle
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * completedHurwitzZetaEven a s) (𝓝[≠] 0) (𝓝 (if a = 0 then -1 else 0))
have h1 : 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
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
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)
have pos : a = 0 → Eq (α := ℂ) (-1) (-1)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
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)
⊢ Eq (α := ℂ) (-if a = 0 then 1 else 0) (if a = 0 then -1 else 0)
have neg : ¬a = 0 → Eq (α := ℂ) (-0) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
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)
have pos : a = 0 → Eq (α := ℂ) (-1) (-1)
Tactic: { split_ifs <;> simp }
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
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)
⊢ Eq (α := ℂ) (-if a = 0 then 1 else 0) (if a = 0 then -1 else 0)
have neg : ¬a = 0 → Eq (α := ℂ) (-0) 0
Tactic: { split_ifs <;> simp }
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a : UnitAddCircle
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))
have this : 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 }
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
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 * completedHurwitzZetaEven a s) (𝓝[≠] 0) (𝓝 (if a = 0 then -1 else 0))
have h1₁ : Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (if a = 0 then -1 else 0))
Tactic: simp only [this, push_cast] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
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))
have refine : ∀ (s : ℂ), ((fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).Λ s) ∘ fun (s : ℂ) ↦ s / 2) s = s * completedHurwitzZetaEven a s
Tactic: refine (h1.comp <| zero_div (2 : ℂ) ▸ (tendsto_div_two_punctured_nhds 0)).congr (fun s ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a : UnitAddCircle
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * completedCosZeta a s) (𝓝[≠] 0) (𝓝 (-1))
have h1 : Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).symm.Λ s) (𝓝[≠] 0) (𝓝 (-1))
Tactic: have h1 : Tendsto (fun s : ℂ ↦ s * _) (𝓝[≠] 0)
    (𝓝 (-1)) := (hurwitzEvenFEPair a).symm.Λ_residue_zero
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
h1 : Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).symm.Λ s) (𝓝[≠] 0) (𝓝 (-1))
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * completedCosZeta a s) (𝓝[≠] 0) (𝓝 (-1))
have refine : ∀ (s : ℂ), ((fun (s : ℂ) ↦ s * (hurwitzEvenFEPair a).symm.Λ s) ∘ fun (s : ℂ) ↦ s / 2) s = s * completedCosZeta a s
Tactic: refine (h1.comp <| zero_div (2 : ℂ) ▸ (tendsto_div_two_punctured_nhds 0)).congr (fun s ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
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)
have 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
Tactic: refine ((hasSum_int_cosKernel₀ a ht).div_const 2).congr_fun fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
t : ℝ
ht : 0 < t
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
have pos : n = 0 → 0 = 0 / 2
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
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
⊢ (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
have neg : ¬n = 0 →
  c n * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) =
    cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * t)) : ℂ) / 2
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
c : (n : ℤ) → ℂ := fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / 2
⊢ HasSum (fun (n : ℤ) ↦ s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
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)
⊢ HasSum (fun (n : ℤ) ↦ s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have 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)
Tactic: simp only [← Int.cast_eq_zero (α := ℝ)] at hF
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
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)
⊢ completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s =
    mellin (fun (t : ℝ) ↦ ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1) / 2) (s / 2)
have 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
Tactic: rw [mellin_div_const, completedCosZeta]