awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
n : ℕ
this : -2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
rw :
  Eq (α := ℂ)
    (Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0
        (if a = 0 then -1 / 2 else 0) (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) :
      ℂ)
    (0 : ℂ)
rw₁ : completedHurwitzZetaEven a (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) / (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1).Gammaℝ = 0
⊢ hurwitzZetaEven a (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = 0
have rw₂ : completedHurwitzZetaEven a (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) / 0 = 0
Tactic: rw [hurwitzZetaEven, Function.update_of_ne this, Gammaℝ_eq_zero_iff.mpr ⟨n + 1, by simp⟩,
    div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
n : ℕ
this : -2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
rw :
  Eq (α := ℂ)
    (Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0
        (if a = 0 then -1 / 2 else 0) (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) :
      ℂ)
    (0 : ℂ)
rw₁ : completedHurwitzZetaEven a (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) / (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1).Gammaℝ = 0
rw₂ : completedHurwitzZetaEven a (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) / 0 = 0
⊢ hurwitzZetaEven a (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = 0
have rw₃ : Eq (α := ℂ) 0 0
Tactic: rw [hurwitzZetaEven, Function.update_of_ne this, Gammaℝ_eq_zero_iff.mpr ⟨n + 1, by simp⟩,
    div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
⊢ DifferentiableAt ℂ (hurwitzZetaEven a) s
have this : DifferentiableAt ℂ (F := ℂ)
  (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0
    (HDiv.hDiv (α := ℂ) (if a = 0 then -1 else 0) 2))
  s
Tactic: have := differentiableAt_update_of_residue
    (fun t ht ht' ↦ differentiableAt_completedHurwitzZetaEven a (Or.inl ht) ht')
    (completedHurwitzZetaEven_residue_zero a) s hs'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
this :
  DifferentiableAt ℂ (F := ℂ)
    (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0
      (HDiv.hDiv (α := ℂ) (if a = 0 then -1 else 0) 2))
    s
⊢ DifferentiableAt ℂ (hurwitzZetaEven a) s
have this₁ : DifferentiableAt ℂ (F := ℂ)
  (Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0
    (if a = 0 then -1 / 2 else 0))
  s
Tactic: simp_rw [div_eq_mul_inv, ite_mul, zero_mul, ← div_eq_mul_inv] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a : UnitAddCircle
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * hurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)
have this : Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) (𝓝[≠] 1) (𝓝 1)
Tactic: have : Tendsto (fun s ↦ (s - 1) * completedHurwitzZetaEven a s / Gammaℝ s) (𝓝[≠] 1) (𝓝 1) := by
    simpa only [Gammaℝ_one, inv_one, mul_one] using (completedHurwitzZetaEven_residue_one a).mul
      <| (differentiable_Gammaℝ_inv.continuous.tendsto _).mono_left nhdsWithin_le_nhds
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
this : Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) (𝓝[≠] 1) (𝓝 1)
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * hurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)
have refine : EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (s : ℂ) ↦ (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) fun (s : ℂ) ↦
  (s - 1) * hurwitzZetaEven a s
Tactic: refine this.congr' ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
this : Tendsto (β := ℂ) (fun (s : ℂ) ↦ (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) (𝓝[≠] 1) (𝓝 1)
⊢ EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (s : ℂ) ↦ (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) fun (s : ℂ) ↦
    (s - 1) * hurwitzZetaEven a s
have h : ∀ (s : ℂ) (hs : s ≠ 0), (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ = (s - 1) * hurwitzZetaEven a s
Tactic: filter_upwards [eventually_ne_nhdsWithin one_ne_zero] with s hs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
this : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ) 1
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) 1
have apply : EventuallyEq (β := ℂ) (𝓝 1) (fun (s : ℂ) ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) fun (s : ℂ) ↦
  completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ
Tactic: apply this.congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
this : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ) 1
⊢ EventuallyEq (β := ℂ) (𝓝 1) (fun (s : ℂ) ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) fun (s : ℂ) ↦
    completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ
have h : ∀ (x : ℂ) (hx : x ≠ 0),
  hurwitzZetaEven a x - 1 / (x - 1) / x.Gammaℝ = completedHurwitzZetaEven a x / x.Gammaℝ - 1 / (x - 1) / x.Gammaℝ
Tactic: filter_upwards [eventually_ne_nhds one_ne_zero] with x hx
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
this : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ) 1
x : ℂ
hx : x ≠ 0
⊢ hurwitzZetaEven a x - 1 / (x - 1) / x.Gammaℝ = completedHurwitzZetaEven a x / x.Gammaℝ - 1 / (x - 1) / x.Gammaℝ
have h : HSub.hSub (α := ℂ)
    (Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0
        (if a = 0 then -1 / 2 else 0) x :
      ℂ)
    (1 / (x - 1) / x.Gammaℝ) =
  completedHurwitzZetaEven a x / x.Gammaℝ - 1 / (x - 1) / x.Gammaℝ
Tactic: rw [hurwitzZetaEven, Function.update_of_ne hx]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
this : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ) 1
x : ℂ
hx : x ≠ 0
h :
  HSub.hSub (α := ℂ)
      (Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0
          (if a = 0 then -1 / 2 else 0) x :
        ℂ)
      (1 / (x - 1) / x.Gammaℝ) =
    completedHurwitzZetaEven a x / x.Gammaℝ - 1 / (x - 1) / x.Gammaℝ
⊢ hurwitzZetaEven a x - 1 / (x - 1) / x.Gammaℝ = completedHurwitzZetaEven a x / x.Gammaℝ - 1 / (x - 1) / x.Gammaℝ
have h₁ : completedHurwitzZetaEven a x / x.Gammaℝ - 1 / (x - 1) / x.Gammaℝ =
  completedHurwitzZetaEven a x / x.Gammaℝ - 1 / (x - 1) / x.Gammaℝ
Tactic: rw [hurwitzZetaEven, Function.update_of_ne hx]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) 1
have suffices : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ) 1
Tactic: suffices DifferentiableAt ℂ
      (fun s ↦ completedHurwitzZetaEven a s / Gammaℝ s - 1 / (s - 1) / Gammaℝ s) 1 by
    apply this.congr_of_eventuallyEq
    filter_upwards [eventually_ne_nhds one_ne_zero] with x hx
    rw [hurwitzZetaEven, Function.update_of_ne hx]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ) 1
have simp_rw : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (completedHurwitzZetaEven a s - 1 / (s - 1)) * s.Gammaℝ⁻¹) 1
Tactic: simp_rw [← sub_div, div_eq_mul_inv _ (Gammaℝ _)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (completedHurwitzZetaEven a s - 1 / (s - 1)) * s.Gammaℝ⁻¹) 1
have refine : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s - 1 / (s - 1)) 1
Tactic: refine DifferentiableAt.mul ?_ differentiable_Gammaℝ_inv.differentiableAt
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s - 1 / (s - 1)) 1
have simp_rw : DifferentiableAt ℂ (F := ℂ)
  (fun (s : ℂ) ↦ completedHurwitzZetaEven₀ a s - ((if a = 0 then 1 else 0) / s + (1 / (1 - s) + 1 / (s - 1)))) 1
Tactic: simp_rw [completedHurwitzZetaEven_eq, sub_sub, add_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
| DifferentiableAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦ completedHurwitzZetaEven₀ a s - ((if a = 0 then 1 else 0) / s + (1 / (1 - s) + 1 / (s - 1)))) 1
have h : ∀ (s : ℂ), (if a = 0 then 1 else 0) / s + (1 / (1 - s) + 1 / (s - 1))
Tactic: enter [2, s, 2]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
| (if a = 0 then 1 else 0) / s + (1 / (1 - s) + 1 / (s - 1))
have h : (if a = 0 then 1 else 0) / s
Tactic: rw [← neg_sub, div_neg, neg_add_cancel, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
| DifferentiableAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦ completedHurwitzZetaEven₀ a s - ((if a = 0 then 1 else 0) / s + (1 / (1 - s) + 1 / (s - 1)))) 1
have h : ∀ (s : ℂ), (if a = 0 then 1 else 0) / s
Tactic: enter [2, s, 2]; rw [← neg_sub, div_neg, neg_add_cancel, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦ completedHurwitzZetaEven₀ a s - ((if a = 0 then 1 else 0) / s + (1 / (1 - s) + 1 / (s - 1)))) 1
have conv : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s) 1
Tactic: conv => enter [2, s, 2]; rw [← neg_sub, div_neg, neg_add_cancel, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a b : UnitAddCircle
z : ℂ
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ hurwitzZetaEven a s - hurwitzZetaEven b s) z
have inl : ∀ (hz : z ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ hurwitzZetaEven a s - hurwitzZetaEven b s) z
Tactic: rcases ne_or_eq z 1 with hz | rfl
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a b : UnitAddCircle
z : ℂ
inl : ∀ (hz : z ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ hurwitzZetaEven a s - hurwitzZetaEven b s) z
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ hurwitzZetaEven a s - hurwitzZetaEven b s) z
have inr : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ hurwitzZetaEven a s - hurwitzZetaEven b s) 1
Tactic: rcases ne_or_eq z 1 with hz | rfl
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a b : UnitAddCircle
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ hurwitzZetaEven a s - hurwitzZetaEven b s) 1
have h : ∀ (x : ℂ),
  hurwitzZetaEven a x - hurwitzZetaEven b x =
    hurwitzZetaEven a x - 1 / (x - 1) / x.Gammaℝ - (hurwitzZetaEven b x - 1 / (x - 1) / x.Gammaℝ)
Tactic: convert!
    (differentiableAt_hurwitzZetaEven_sub_one_div a).fun_sub
      (differentiableAt_hurwitzZetaEven_sub_one_div b) using
    2 with s
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun (n : ℤ) ↦ 1 / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2) (hurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have rw : HasSum (fun (n : ℤ) ↦ 1 / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2)
  (completedHurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s / s.Gammaℝ)
Tactic: rw [hurwitzZetaEven, Function.update_of_ne (ne_zero_of_one_lt_re hs)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun (n : ℤ) ↦ 1 / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2)
    (completedHurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s / s.Gammaℝ)
have this : HasSum (fun (i : ℤ) ↦ s.Gammaℝ / (↑|(↑i : ℝ) + a| : ℂ) ^ s / 2 / s.Gammaℝ)
  (completedHurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s / s.Gammaℝ)
Tactic: have := (hasSum_int_completedHurwitzZetaEven a hs).div_const (Gammaℝ s)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun (n : ℕ) ↦ (1 / (↑|(↑n : ℝ) + a| : ℂ) ^ s + 1 / (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s) / 2)
    (hurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have refine : ∀ (n : ℕ),
  (1 / (↑|(↑n : ℝ) + a| : ℂ) ^ s + 1 / (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s) / 2 =
    1 / (↑|(↑(↑n : ℤ) : ℝ) + a| : ℂ) ^ s / 2 + 1 / (↑|(↑(-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℝ) + a| : ℂ) ^ s / 2
Tactic: refine (hasSum_int_hurwitzZetaEven a hs).nat_add_neg_add_one.congr_fun fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun (n : ℕ) ↦ (1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s + 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s) / 2)
    (hurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have refine : ∀ (n : ℕ),
  (1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s + 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s) / 2 =
    (1 / (↑|(↑n : ℝ) + a| : ℂ) ^ s + 1 / (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s) / 2
Tactic: refine (hasSum_nat_hurwitzZetaEven a hs).congr_fun fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ (1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s + 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s) / 2 =
    (1 / (↑|(↑n : ℝ) + a| : ℂ) ^ s + 1 / (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s) / 2
have e_a : 1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s = 1 / (↑|(↑n : ℝ) + a| : ℂ) ^ s
Tactic: congr 2
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
n : ℕ
e_a : 1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s = 1 / (↑|(↑n : ℝ) + a| : ℂ) ^ s
⊢ (1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s + 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s) / 2 =
    (1 / (↑|(↑n : ℝ) + a| : ℂ) ^ s + 1 / (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s) / 2
have e_a₁ : 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s = 1 / (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s
Tactic: congr 2
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 0 ≤ (↑n : ℝ) + a
have linarith : (↑n : ℝ) + a < 0 → HSub.hSub (α := ℝ) 0 (↑n : ℝ) + ((↑n : ℝ) + a - 0) + (0 - a) = 0
Tactic: linarith [ha.1, ha.2]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s = 1 / (↑|(↑n : ℝ) + a| : ℂ) ^ s
have e_a : 1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s = 1 / (↑((↑n : ℝ) + a) : ℂ) ^ s
Tactic: rw [abs_of_nonneg (by linarith [ha.1, ha.2])]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a
have linarith : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a < 0 →
  HSub.hSub (α := ℝ) 0 (↑n : ℝ) + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a - 0) + (a - 1) = 0
Tactic: linarith [ha.1, ha.2]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s = 1 / (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s
have e_a : 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s = 1 / (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a) : ℂ) ^ s
Tactic: rw [abs_of_nonneg (by linarith [ha.1, ha.2])]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a : UnitAddCircle
n : ℕ
⊢ cosZeta a (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = 0
have this : -2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
Tactic: have : (-2 : ℂ) * (n + 1) ≠ 0 :=
    mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (Nat.cast_add_one_ne_zero n)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
n : ℕ
this : -2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
⊢ -2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = -HMul.hMul (α := ℂ) 2 (↑(n + 1) : ℂ)
have rw : -(2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = -HMul.hMul (α := ℂ) 2 (↑(n + 1) : ℂ)
Tactic: rw [neg_mul, Nat.cast_add_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
n : ℕ
this : -2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
rw : -(2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = -HMul.hMul (α := ℂ) 2 (↑(n + 1) : ℂ)
⊢ -2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = -HMul.hMul (α := ℂ) 2 (↑(n + 1) : ℂ)
have rw₁ : -(2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = -(2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
Tactic: rw [neg_mul, Nat.cast_add_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
n : ℕ
this : -2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
⊢ cosZeta a (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = 0
have rw : Eq (α := ℂ)
  (Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedCosZeta a s / s.Gammaℝ) 0 (-1 / 2)
      (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) :
    ℂ)
  (0 : ℂ)
Tactic: rw [cosZeta, Function.update_of_ne this,
    Gammaℝ_eq_zero_iff.mpr ⟨n + 1, by rw [neg_mul, Nat.cast_add_one]⟩, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
n : ℕ
this : -2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
rw :
  Eq (α := ℂ)
    (Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedCosZeta a s / s.Gammaℝ) 0 (-1 / 2)
        (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) :
      ℂ)
    (0 : ℂ)
⊢ cosZeta a (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = 0
have rw₁ : completedCosZeta a (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) / (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1).Gammaℝ = 0
Tactic: rw [cosZeta, Function.update_of_ne this,
    Gammaℝ_eq_zero_iff.mpr ⟨n + 1, by rw [neg_mul, Nat.cast_add_one]⟩, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
n : ℕ
this : -2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
rw :
  Eq (α := ℂ)
    (Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedCosZeta a s / s.Gammaℝ) 0 (-1 / 2)
        (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) :
      ℂ)
    (0 : ℂ)
rw₁ : completedCosZeta a (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) / (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1).Gammaℝ = 0
⊢ cosZeta a (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = 0
have rw₂ : completedCosZeta a (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) / 0 = 0
Tactic: rw [cosZeta, Function.update_of_ne this,
    Gammaℝ_eq_zero_iff.mpr ⟨n + 1, by rw [neg_mul, Nat.cast_add_one]⟩, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
n : ℕ
this : -2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
rw :
  Eq (α := ℂ)
    (Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedCosZeta a s / s.Gammaℝ) 0 (-1 / 2)
        (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) :
      ℂ)
    (0 : ℂ)
rw₁ : completedCosZeta a (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) / (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1).Gammaℝ = 0
rw₂ : completedCosZeta a (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) / 0 = 0
⊢ cosZeta a (-2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = 0
have rw₃ : Eq (α := ℂ) 0 0
Tactic: rw [cosZeta, Function.update_of_ne this,
    Gammaℝ_eq_zero_iff.mpr ⟨n + 1, by rw [neg_mul, Nat.cast_add_one]⟩, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1 ∨ a ≠ 0
⊢ DifferentiableAt ℂ (cosZeta a) s
have inl : ∀ (hs' : s ≠ 1), DifferentiableAt ℂ (cosZeta a) s
Tactic: rcases ne_or_eq s 1 with hs' | rfl
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1 ∨ a ≠ 0
inl : ∀ (hs' : s ≠ 1), DifferentiableAt ℂ (cosZeta a) s
⊢ DifferentiableAt ℂ (cosZeta a) s
have inr : ∀ (hs' : Ne (α := ℂ) 1 1 ∨ a ≠ 0), DifferentiableAt ℂ (cosZeta a) 1
Tactic: rcases ne_or_eq s 1 with hs' | rfl
Cleared hypotheses: s, hs'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
hs' : Ne (α := ℂ) 1 1 ∨ a ≠ 0
⊢ DifferentiableAt ℂ (cosZeta a) 1
have inr : cosZeta a =ᶠ[𝓝 1] fun (i : ℂ) ↦ completedCosZeta a i * i.Gammaℝ⁻¹
Tactic: apply ((differentiableAt_completedCosZeta a one_ne_zero hs').fun_mul
      (differentiable_Gammaℝ_inv.differentiableAt)).congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
hs' : Ne (α := ℂ) 1 1 ∨ a ≠ 0
⊢ cosZeta a =ᶠ[𝓝 1] fun (i : ℂ) ↦ completedCosZeta a i * i.Gammaℝ⁻¹
have h : ∀ (x : ℂ) (hx : Membership.mem (γ := Set ℂ) {0}ᶜ x), cosZeta a x = completedCosZeta a x * x.Gammaℝ⁻¹
Tactic: filter_upwards [isOpen_compl_singleton.mem_nhds one_ne_zero] with x hx
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
hs' : Ne (α := ℂ) 1 1 ∨ a ≠ 0
x : ℂ
hx : Membership.mem (γ := Set ℂ) {0}ᶜ x
⊢ cosZeta a x = completedCosZeta a x * x.Gammaℝ⁻¹
have h : Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedCosZeta a s / s.Gammaℝ) 0 (-1 / 2) x =
  completedCosZeta a x * x.Gammaℝ⁻¹
Tactic: rw [cosZeta, Function.update_of_ne hx, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
hs' : Ne (α := ℂ) 1 1 ∨ a ≠ 0
x : ℂ
hx : Membership.mem (γ := Set ℂ) {0}ᶜ x
h :
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedCosZeta a s / s.Gammaℝ) 0 (-1 / 2) x =
    completedCosZeta a x * x.Gammaℝ⁻¹
⊢ cosZeta a x = completedCosZeta a x * x.Gammaℝ⁻¹
have h₁ : completedCosZeta a x / x.Gammaℝ = completedCosZeta a x * x.Gammaℝ⁻¹
Tactic: rw [cosZeta, Function.update_of_ne hx, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
hs' : Ne (α := ℂ) 1 1 ∨ a ≠ 0
x : ℂ
hx : Membership.mem (γ := Set ℂ) {0}ᶜ x
h :
  Function.update (β := fun (s : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ completedCosZeta a s / s.Gammaℝ) 0 (-1 / 2) x =
    completedCosZeta a x * x.Gammaℝ⁻¹
h₁ : completedCosZeta a x / x.Gammaℝ = completedCosZeta a x * x.Gammaℝ⁻¹
⊢ cosZeta a x = completedCosZeta a x * x.Gammaℝ⁻¹
have h₂ : completedCosZeta a x * x.Gammaℝ⁻¹ = completedCosZeta a x * x.Gammaℝ⁻¹
Tactic: rw [cosZeta, Function.update_of_ne hx, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2)
    (cosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)
have rw : HasSum (fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2)
  (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s / s.Gammaℝ)
Tactic: rw [cosZeta, Function.update_of_ne (ne_zero_of_one_lt_re hs)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s / s.Gammaℝ)
have refine : ∀ (n : ℤ),
  cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2 =
    s.Gammaℝ * cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2 / s.Gammaℝ
Tactic: refine ((hasSum_int_completedCosZeta a hs).div_const (Gammaℝ s)).congr_fun fun n ↦ ?_