awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
this : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ) 1
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ℝ
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) 1

Tactic:
apply this.congr_of_eventuallyEq

Premises used: DifferentiableAt.congr_of_eventuallyEq
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
this : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ) 1
h :
  ∀ (x : ℂ) (hx : x ≠ 0),
    hurwitzZetaEven a x - 1 / (x - 1) / x.Gammaℝ = completedHurwitzZetaEven a x / x.Gammaℝ - 1 / (x - 1) / x.Gammaℝ
⊢ 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:
filter_upwards [eventually_ne_nhds one_ne_zero] with x hx

Premises used: eventually_ne_nhds, one_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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ℝ
h₁ h₂ :
  completedHurwitzZetaEven a x / x.Gammaℝ - 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ℝ

Tactic:
rw [hurwitzZetaEven, Function.update_of_ne hx]

Premises used: HurwitzZeta.hurwitzZetaEven, Function.update_of_ne
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
suffices :
  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

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]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
simp_rw : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (completedHurwitzZetaEven a s - 1 / (s - 1)) * s.Gammaℝ⁻¹) 1
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ) 1

Tactic:
simp_rw [← sub_div, div_eq_mul_inv _ (Gammaℝ _)]

Premises used: Complex.Gammaℝ, sub_div, div_eq_mul_inv
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (completedHurwitzZetaEven a s - 1 / (s - 1)) * s.Gammaℝ⁻¹) 1

Tactic:
DifferentiableAt.mul ?_ differentiable_Gammaℝ_inv.differentiableAt

Premises used: DifferentiableAt.mul, Differentiable.differentiableAt, Complex.differentiable_Gammaℝ_inv
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
refine : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s - 1 / (s - 1)) 1
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (completedHurwitzZetaEven a s - 1 / (s - 1)) * s.Gammaℝ⁻¹) 1

Tactic:
refine DifferentiableAt.mul ?_ differentiable_Gammaℝ_inv.differentiableAt

Premises used: DifferentiableAt.mul, Differentiable.differentiableAt, Complex.differentiable_Gammaℝ_inv
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
simp_rw :
  DifferentiableAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦ completedHurwitzZetaEven₀ a s - ((if a = 0 then 1 else 0) / s + (1 / (1 - s) + 1 / (s - 1)))) 1
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven a s - 1 / (s - 1)) 1

Tactic:
simp_rw [completedHurwitzZetaEven_eq, sub_sub, add_assoc]

Premises used: add_assoc, HurwitzZeta.completedHurwitzZetaEven_eq, sub_sub
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
h : ∀ (s : ℂ), (if a = 0 then 1 else 0) / s + (1 / (1 - s) + 1 / (s - 1))
| DifferentiableAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦ completedHurwitzZetaEven₀ a s - ((if a = 0 then 1 else 0) / s + (1 / (1 - s) + 1 / (s - 1)))) 1

Tactic:
enter [2, s, 2]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
h : (if a = 0 then 1 else 0) / s
| (if a = 0 then 1 else 0) / s + (1 / (1 - s) + 1 / (s - 1))

Tactic:
rw [← neg_sub, div_neg, neg_add_cancel, add_zero]

Premises used: neg_sub, neg_add_cancel, div_neg, add_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
h : ∀ (s : ℂ), (if a = 0 then 1 else 0) / s
| DifferentiableAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦ completedHurwitzZetaEven₀ a s - ((if a = 0 then 1 else 0) / s + (1 / (1 - s) + 1 / (s - 1)))) 1

Tactic:
enter [2, s, 2]; rw [← neg_sub, div_neg, neg_add_cancel, add_zero]

Premises used: neg_sub, neg_add_cancel, div_neg, add_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
conv : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s) 1
⊢ DifferentiableAt ℂ (F := ℂ)
    (fun (s : ℂ) ↦ completedHurwitzZetaEven₀ a s - ((if a = 0 then 1 else 0) / s + (1 / (1 - s) + 1 / (s - 1)))) 1

Tactic:
conv => enter [2, s, 2]; rw [← neg_sub, div_neg, neg_add_cancel, add_zero]

Premises used: neg_sub, neg_add_cancel, div_neg, add_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s) 1

Tactic:
(differentiable_completedHurwitzZetaEven₀ a _).sub
    <| (differentiableAt_const _).div differentiableAt_id one_ne_zero

Premises used: DifferentiableAt.div, DifferentiableAt.sub, differentiableAt_const, one_ne_zero, differentiableAt_id, HurwitzZeta.differentiable_completedHurwitzZetaEven₀
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s) 1

Tactic:
exact (differentiable_completedHurwitzZetaEven₀ a _).sub
    <| (differentiableAt_const _).div differentiableAt_id one_ne_zero

Premises used: DifferentiableAt.sub, HurwitzZeta.differentiable_completedHurwitzZetaEven₀
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
⊢ Tendsto (fun (s : ℂ) ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) (𝓝 1) (𝓝 (hurwitzZetaEven a 1))

Tactic:
simpa using (differentiableAt_hurwitzZetaEven_sub_one_div a).continuousAt.tendsto

Premises used: HurwitzZeta.differentiableAt_hurwitzZetaEven_sub_one_div, DifferentiableAt.continuousAt, ContinuousAt.tendsto
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a b : UnitAddCircle
z : ℂ
inl : ∀ (hz : z ≠ 1), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ hurwitzZetaEven a s - hurwitzZetaEven b s) z
inr : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ hurwitzZetaEven a s - hurwitzZetaEven b s) 1
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ hurwitzZetaEven a s - hurwitzZetaEven b s) z

Tactic:
rcases ne_or_eq z 1 with hz | rfl

Premises used: ne_or_eq, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a b : UnitAddCircle
z : ℂ
hz : z ≠ 1
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ hurwitzZetaEven a s - hurwitzZetaEven b s) z

Tactic:
(differentiableAt_hurwitzZetaEven a hz).sub (differentiableAt_hurwitzZetaEven b hz)

Premises used: HurwitzZeta.differentiableAt_hurwitzZetaEven, DifferentiableAt.sub
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a b : UnitAddCircle
z : ℂ
hz : z ≠ 1
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ hurwitzZetaEven a s - hurwitzZetaEven b s) z

Tactic:
exact (differentiableAt_hurwitzZetaEven a hz).sub (differentiableAt_hurwitzZetaEven b hz)

Premises used: HurwitzZeta.differentiableAt_hurwitzZetaEven, DifferentiableAt.sub
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a b : UnitAddCircle
⊢ DifferentiableAt ℂ (F := ℂ)
    (fun (i : ℂ) ↦ hurwitzZetaEven a i - 1 / (i - 1) / i.Gammaℝ - (hurwitzZetaEven b i - 1 / (i - 1) / i.Gammaℝ)) 1

Tactic:
(differentiableAt_hurwitzZetaEven_sub_one_div a).fun_sub
      (differentiableAt_hurwitzZetaEven_sub_one_div b)

Premises used: HurwitzZeta.differentiableAt_hurwitzZetaEven_sub_one_div, DifferentiableAt.fun_sub
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a b : UnitAddCircle
h :
  ∀ (x : ℂ),
    hurwitzZetaEven a x - hurwitzZetaEven b x =
      hurwitzZetaEven a x - 1 / (x - 1) / x.Gammaℝ - (hurwitzZetaEven b x - 1 / (x - 1) / x.Gammaℝ)
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ hurwitzZetaEven a s - hurwitzZetaEven b s) 1

Tactic:
convert!
    (differentiableAt_hurwitzZetaEven_sub_one_div a).fun_sub
      (differentiableAt_hurwitzZetaEven_sub_one_div b) using
    2 with s

Premises used: HurwitzZeta.differentiableAt_hurwitzZetaEven_sub_one_div, DifferentiableAt.fun_sub
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a b : UnitAddCircle
x : ℂ
⊢ hurwitzZetaEven a x - hurwitzZetaEven b x =
    hurwitzZetaEven a x - 1 / (x - 1) / x.Gammaℝ - (hurwitzZetaEven b x - 1 / (x - 1) / x.Gammaℝ)

Tactic:
abel
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
rw :
  HasSum (fun (n : ℤ) ↦ 1 / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2)
    (completedHurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s / s.Gammaℝ)
⊢ HasSum (fun (n : ℤ) ↦ 1 / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2) (hurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
rw [hurwitzZetaEven, Function.update_of_ne (ne_zero_of_one_lt_re hs)]

Premises used: Complex.ne_zero_of_one_lt_re, HurwitzZeta.hurwitzZetaEven, Function.update_of_ne
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ 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)
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum (fun (i : ℤ) ↦ s.Gammaℝ / (↑|(↑i : ℝ) + a| : ℂ) ^ s / 2 / s.Gammaℝ)
    (completedHurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s / s.Gammaℝ)
n : ℤ
⊢ 1 / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 = s.Gammaℝ / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 / s.Gammaℝ

Tactic:
simp only [div_right_comm _ _ (Gammaℝ _),
    div_self (Gammaℝ_ne_zero_of_re_pos (zero_lt_one.trans hs))]

Premises used: div_right_comm, Complex.Gammaℝ, zero_lt_one, Complex.Gammaℝ_ne_zero_of_re_pos, LT.lt.trans, div_self
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum (fun (i : ℤ) ↦ s.Gammaℝ / (↑|(↑i : ℝ) + a| : ℂ) ^ s / 2 / s.Gammaℝ)
    (completedHurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s / s.Gammaℝ)
⊢ HasSum (fun (n : ℤ) ↦ 1 / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2)
    (completedHurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s / s.Gammaℝ)

Tactic:
exact this.congr_fun fun n ↦ by simp only [div_right_comm _ _ (Gammaℝ _),
    div_self (Gammaℝ_ne_zero_of_re_pos (zero_lt_one.trans hs))]

Premises used: HasSum.congr_fun
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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)

Tactic:
(hasSum_int_hurwitzZetaEven a hs).nat_add_neg_add_one.congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun, HasSum.nat_add_neg_add_one, HurwitzZeta.hasSum_int_hurwitzZetaEven
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
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
⊢ HasSum (fun (n : ℕ) ↦ (1 / (↑|(↑n : ℝ) + a| : ℂ) ^ s + 1 / (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s) / 2)
    (hurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
refine (hasSum_int_hurwitzZetaEven a hs).nat_add_neg_add_one.congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun, HasSum.nat_add_neg_add_one, HurwitzZeta.hasSum_int_hurwitzZetaEven
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
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:
simp [← abs_neg (n + 1 - a), -neg_sub, neg_sub', add_div]

Premises used: abs_neg, neg_sub, HSub.hSub, Nat.cast, neg_sub', HAdd.hAdd, OfNat.ofNat, add_div
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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)

Tactic:
(hasSum_nat_hurwitzZetaEven a hs).congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun, HurwitzZeta.hasSum_nat_hurwitzZetaEven
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
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
⊢ HasSum (fun (n : ℕ) ↦ (1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s + 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s) / 2)
    (hurwitzZetaEven (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
refine (hasSum_nat_hurwitzZetaEven a hs).congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun, HurwitzZeta.hasSum_nat_hurwitzZetaEven
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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
e_a₁ : 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s = 1 / (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - 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

Tactic:
congr 2
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
n : ℕ
linarith : (↑n : ℝ) + a < 0 → HSub.hSub (α := ℝ) 0 (↑n : ℝ) + ((↑n : ℝ) + a - 0) + (0 - a) = 0
⊢ 0 ≤ (↑n : ℝ) + a

Tactic:
linarith [ha.1, ha.2]

Premises used: And.right, And.left
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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 / (↑|(↑n : ℝ) + a| : ℂ) ^ s

Tactic:
rw [abs_of_nonneg (by linarith [ha.1, ha.2])]

Premises used: abs_of_nonneg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
n : ℕ
linarith :
  HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a < 0 →
    HSub.hSub (α := ℝ) 0 (↑n : ℝ) + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a - 0) + (a - 1) = 0
⊢ 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a

Tactic:
linarith [ha.1, ha.2]

Premises used: And.right, And.left
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
n : ℕ
e_a : 1 / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - (↑a : ℂ)) ^ s = 1 / (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a) : ℂ) ^ s
⊢ 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])]

Premises used: abs_of_nonneg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / ((↑n : ℂ) + (↑a : ℂ)) ^ s = 1 / (↑((↑n : ℝ) + a) : ℂ) ^ s

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
⊢ cosZeta a 0 = -1 / 2

Tactic:
Function.update_self ..

Premises used: HurwitzZeta.cosZeta, Function.update_self
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
⊢ cosZeta (-a) s = cosZeta a s

Tactic:
simp [cosZeta]

Premises used: HurwitzZeta.cosZeta
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
n : ℕ
this : -2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
rw : -(2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = -HMul.hMul (α := ℂ) 2 (↑(n + 1) : ℂ)
rw₁ rw₂ : -(2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = -(2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
⊢ -2 * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = -HMul.hMul (α := ℂ) 2 (↑(n + 1) : ℂ)

Tactic:
rw [neg_mul, Nat.cast_add_one]

Premises used: neg_mul, Nat.cast_add_one
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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
rw₃ rw₄ : Eq (α := ℂ) 0 0
⊢ cosZeta a (-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]

Premises used: Iff.mpr, Complex.Gammaℝ_eq_zero_iff, HurwitzZeta.cosZeta, HAdd.hAdd, Exists.intro, OfNat.ofNat, div_zero, Function.update_of_ne
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1 ∨ a ≠ 0
inl : ∀ (hs' : s ≠ 1), DifferentiableAt ℂ (cosZeta a) s
inr : ∀ (hs' : Ne (α := ℂ) 1 1 ∨ a ≠ 0), DifferentiableAt ℂ (cosZeta a) 1
⊢ DifferentiableAt ℂ (cosZeta a) s

Tactic:
rcases ne_or_eq s 1 with hs' | rfl

Premises used: ne_or_eq, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs'_1 : s ≠ 1 ∨ a ≠ 0
hs' : s ≠ 1
⊢ DifferentiableAt ℂ (cosZeta a) s

Tactic:
differentiableAt_update_of_residue (fun _ ht ht' ↦
      differentiableAt_completedCosZeta a ht (Or.inl ht')) (completedCosZeta_residue_zero a) s hs'

Premises used: HurwitzZeta.cosZeta, HurwitzZeta.completedCosZeta_residue_zero, HurwitzZeta.differentiableAt_update_of_residue, HurwitzZeta.differentiableAt_completedCosZeta, Or.inl
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
hs'_1 : s ≠ 1 ∨ a ≠ 0
hs' : s ≠ 1
⊢ DifferentiableAt ℂ (cosZeta a) s

Tactic:
exact differentiableAt_update_of_residue (fun _ ht ht' ↦
      differentiableAt_completedCosZeta a ht (Or.inl ht')) (completedCosZeta_residue_zero a) s hs'

Premises used: HurwitzZeta.completedCosZeta_residue_zero, HurwitzZeta.differentiableAt_update_of_residue, HurwitzZeta.differentiableAt_completedCosZeta, Or.inl
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
hs' : Ne (α := ℂ) 1 1 ∨ a ≠ 0
inr : cosZeta a =ᶠ[𝓝 1] fun (i : ℂ) ↦ completedCosZeta a i * i.Gammaℝ⁻¹
⊢ DifferentiableAt ℂ (cosZeta a) 1

Tactic:
apply ((differentiableAt_completedCosZeta a one_ne_zero hs').fun_mul
      (differentiable_Gammaℝ_inv.differentiableAt)).congr_of_eventuallyEq

Premises used: DifferentiableAt.congr_of_eventuallyEq, Differentiable.differentiableAt, Complex.differentiable_Gammaℝ_inv, HurwitzZeta.differentiableAt_completedCosZeta, one_ne_zero, DifferentiableAt.fun_mul
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
hs' : Ne (α := ℂ) 1 1 ∨ a ≠ 0
h : ∀ (x : ℂ) (hx : Membership.mem (γ := Set ℂ) {0}ᶜ x), cosZeta a x = completedCosZeta a x * x.Gammaℝ⁻¹
⊢ cosZeta a =ᶠ[𝓝 1] fun (i : ℂ) ↦ completedCosZeta a i * i.Gammaℝ⁻¹

Tactic:
filter_upwards [isOpen_compl_singleton.mem_nhds one_ne_zero] with x hx

Premises used: isOpen_compl_singleton, IsOpen.mem_nhds, one_ne_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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ℝ⁻¹
h₂ h₃ : completedCosZeta a x * x.Gammaℝ⁻¹ = completedCosZeta a x * x.Gammaℝ⁻¹
⊢ cosZeta a x = completedCosZeta a x * x.Gammaℝ⁻¹

Tactic:
rw [cosZeta, Function.update_of_ne hx, div_eq_mul_inv]

Premises used: HurwitzZeta.cosZeta, div_eq_mul_inv, Function.update_of_ne
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
ha : a ≠ 0
⊢ Differentiable ℂ (cosZeta a)

Tactic:
fun _ ↦ differentiableAt_cosZeta a (Or.inr ha)

Premises used: Differentiable, HurwitzZeta.differentiableAt_cosZeta, Or.inr
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
rw :
  HasSum (fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s / s.Gammaℝ)
⊢ HasSum (fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2)
    (cosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s)

Tactic:
rw [cosZeta, Function.update_of_ne (ne_zero_of_one_lt_re hs)]

Premises used: Complex.ne_zero_of_one_lt_re, HurwitzZeta.cosZeta, Function.update_of_ne
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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ℝ)

Tactic:
((hasSum_int_completedCosZeta a hs).div_const (Gammaℝ s)).congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun, Complex.Gammaℝ, HasSum.div_const, HurwitzZeta.hasSum_int_completedCosZeta
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
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ℝ
⊢ HasSum (fun (n : ℤ) ↦ cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑n : ℂ)) / HPow.hPow (α := ℂ) (↑|n| : ℂ) s / 2)
    (completedCosZeta (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) s / s.Gammaℝ)

Tactic:
refine ((hasSum_int_completedCosZeta a hs).div_const (Gammaℝ s)).congr_fun fun n ↦ ?_

Premises used: HasSum.congr_fun, Complex.Gammaℝ, HasSum.div_const, HurwitzZeta.hasSum_int_completedCosZeta