-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
/-- The difference of two completed even Hurwitz zeta functions is differentiable at `s = 1`. -/
lemma differentiableAt_one_completedHurwitzZetaEven_sub_completedHurwitzZetaEven
    (a b : UnitAddCircle) :
    DifferentiableAt ℂ (fun s ↦ completedHurwitzZetaEven a s - completedHurwitzZetaEven b s) 1

Proof state:
a b : UnitAddCircle
s : ℂ
⊢ 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:
abel

Result:
no goals

Proof state:
a b : UnitAddCircle
this :
  ∀ (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
⊢ DifferentiableAt ℂ
    (fun x =>
      completedHurwitzZetaEven₀ a x - completedHurwitzZetaEven₀ b x -
        ((if a = 0 then 1 else 0) - if b = 0 then 1 else 0) / x)
    1

Tactic:
refine .sub ?_ <| (differentiable_const _ _).div (differentiable_id _) one_ne_zero

Result:
a b : UnitAddCircle
this :
  ∀ (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
⊢ DifferentiableAt ℂ (fun x => completedHurwitzZetaEven₀ a x - completedHurwitzZetaEven₀ b x) 1

Proof state:
a b : UnitAddCircle
this :
  ∀ (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
⊢ DifferentiableAt ℂ (fun s => completedHurwitzZetaEven a s - completedHurwitzZetaEven b s) 1

Tactic:
rw [funext this]

Result:
a b : UnitAddCircle
this :
  ∀ (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
⊢ DifferentiableAt ℂ
    (fun x =>
      completedHurwitzZetaEven₀ a x - completedHurwitzZetaEven₀ b x -
        ((if a = 0 then 1 else 0) - if b = 0 then 1 else 0) / x)
    1

Proof state:
a b : UnitAddCircle
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

Tactic:
simp_rw [completedHurwitzZetaEven_eq, sub_div]

Result:
a b : UnitAddCircle
s : ℂ
⊢ 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)

Proof state:
a b : UnitAddCircle
this :
  ∀ (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
⊢ DifferentiableAt ℂ (fun x => completedHurwitzZetaEven₀ a x - completedHurwitzZetaEven₀ b x) 1

Tactic:
apply DifferentiableAt.sub <;> apply differentiable_completedHurwitzZetaEven₀

Result:
no goals

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

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

Result:
a b : UnitAddCircle
this :
  ∀ (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
⊢ DifferentiableAt ℂ (fun s => completedHurwitzZetaEven a s - completedHurwitzZetaEven b s) 1