-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
lemma differentiableAt_hurwitzZetaEven_sub_one_div (a : UnitAddCircle) :
    DifferentiableAt ℂ (fun s ↦ hurwitzZetaEven a s - 1 / (s - 1) / Gammaℝ s) 1

Proof state:
a : UnitAddCircle
⊢ DifferentiableAt ℂ
    (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]

Result:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s => completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s) 1

Proof state:
a : UnitAddCircle
this : DifferentiableAt ℂ (fun s => completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ) 1
⊢ DifferentiableAt ℂ (fun s => hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) 1

Tactic:
apply this.congr_of_eventuallyEq

Result:
a : UnitAddCircle
this : DifferentiableAt ℂ (fun s => completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ) 1
⊢ (fun s => hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) =ᶠ[𝓝 1] fun s =>
    completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ

Proof state:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s => completedHurwitzZetaEven a s - 1 / (s - 1)) 1

Tactic:
simp_rw [completedHurwitzZetaEven_eq, sub_sub, add_assoc]

Result:
a : UnitAddCircle
⊢ DifferentiableAt ℂ
    (fun s => completedHurwitzZetaEven₀ a s - ((if a = 0 then 1 else 0) / s + (1 / (1 - s) + 1 / (s - 1)))) 1

Proof state:
case h
a : UnitAddCircle
this : DifferentiableAt ℂ (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ℝ

Tactic:
rw [hurwitzZetaEven, Function.update_of_ne hx]

Result:
no goals

Proof state:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (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

Result:
no goals

Proof state:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s => (completedHurwitzZetaEven a s - 1 / (s - 1)) * s.Gammaℝ⁻¹) 1

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

Result:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s => completedHurwitzZetaEven a s - 1 / (s - 1)) 1

Proof state:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s => completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ) 1

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

Result:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s => (completedHurwitzZetaEven a s - 1 / (s - 1)) * s.Gammaℝ⁻¹) 1

Proof state:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (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]

Result:
a : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s => completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ) 1

Proof state:
a : UnitAddCircle
this : DifferentiableAt ℂ (fun s => completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ) 1
⊢ (fun s => hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) =ᶠ[𝓝 1] fun s =>
    completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ

Tactic:
filter_upwards [eventually_ne_nhds one_ne_zero] with x hx

Result:
case h
a : UnitAddCircle
this : DifferentiableAt ℂ (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ℝ