-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
/-- The residue of `completedHurwitzZetaEven a s` at `s = 0` is equal to `-1` if `a = 0`, and `0`
otherwise. -/
lemma completedHurwitzZetaEven_residue_zero (a : UnitAddCircle) :
    Tendsto (fun s ↦ s * completedHurwitzZetaEven a s) (𝓝[≠] 0) (𝓝 (if a = 0 then -1 else 0))

Proof state:
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))

Tactic:
have : -(if a = 0 then (1 : ℂ) else 0) = (if a = 0 then -1 else 0) := by { split_ifs <;> simp }

Result:
a : UnitAddCircle
h1 : Tendsto (fun s => s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (-if a = 0 then 1 else 0))
this : (-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))

Proof state:
a : UnitAddCircle
⊢ Tendsto (fun s => s * completedHurwitzZetaEven 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

Result:
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))

Proof state:
a : UnitAddCircle
h1 : Tendsto (fun s => s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (-if a = 0 then 1 else 0))
this : (-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))

Tactic:
simp only [this, push_cast, one_mul] at h1

Result:
a : UnitAddCircle
this : (-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))

Proof state:
a : UnitAddCircle
h1 : Tendsto (fun s => s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (-if a = 0 then 1 else 0))
⊢ (-if a = 0 then 1 else 0) = if a = 0 then -1 else 0

Tactic:
split_ifs <;> simp

Result:
no goals

Proof state:
a : UnitAddCircle
this : (-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))
s : ℂ
⊢ ((fun s => s * (hurwitzEvenFEPair a).Λ s) ∘ fun s => s / 2) s = s * completedHurwitzZetaEven a s

Tactic:
simp [completedHurwitzZetaEven, div_mul_eq_mul_div, mul_div_assoc]

Result:
no goals

Proof state:
a : UnitAddCircle
this : (-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))

Tactic:
refine (h1.comp <| zero_div (2 : ℂ) ▸ (tendsto_div_two_punctured_nhds 0)).congr (fun s ↦ ?_)

Result:
a : UnitAddCircle
this : (-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))
s : ℂ
⊢ ((fun s => s * (hurwitzEvenFEPair a).Λ s) ∘ fun s => s / 2) s = s * completedHurwitzZetaEven a s