-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
/-- Technical lemma which will give us differentiability of Hurwitz zeta at `s = 0`. -/
lemma differentiableAt_update_of_residue
    {Λ : ℂ → ℂ} (hf : ∀ (s : ℂ) (_ : s ≠ 0) (_ : s ≠ 1), DifferentiableAt ℂ Λ s)
    {L : ℂ} (h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)) (s : ℂ) (hs' : s ≠ 1) :
    DifferentiableAt ℂ (Function.update (fun s ↦ Λ s / Gammaℝ s) 0 (L / 2)) s

Proof state:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s => s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u => Λ u / u.Gammaℝ) t
⊢ Tendsto (fun s => Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))

Tactic:
refine Tendsto.congr' ?_ (h_lim.div Gammaℝ_residue_zero two_ne_zero)

Result:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s => s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u => Λ u / u.Gammaℝ) t
⊢ ((fun s => s * Λ s) / fun s => s * s.Gammaℝ) =ᶠ[𝓝[≠] 0] fun s => Λ s / s.Gammaℝ

Proof state:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s => s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u => Λ u / u.Gammaℝ) t
⊢ DifferentiableAt ℂ (Function.update (fun s => Λ s / s.Gammaℝ) 0 (L / 2)) s

Tactic:
have claim2 : Tendsto (fun s : ℂ ↦ Λ s / Gammaℝ s) (𝓝[≠] 0) (𝓝 <| L / 2) := by
  refine Tendsto.congr' ?_ (h_lim.div Gammaℝ_residue_zero two_ne_zero)
  filter_upwards [self_mem_nhdsWithin] with s (hs : s ≠ 0)
  rw [Pi.div_apply, ← div_div, mul_div_cancel_left₀ _ hs]

Result:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s => s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u => Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun s => Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
⊢ DifferentiableAt ℂ (Function.update (fun s => Λ s / s.Gammaℝ) 0 (L / 2)) s

Proof state:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s => s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u => Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun s => Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
⊢ DifferentiableAt ℂ (Function.update (fun s => Λ s / s.Gammaℝ) 0 (L / 2)) s

Tactic:
rcases ne_or_eq s 0 with hs | rfl

Result:
case inl
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s => s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u => Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun s => Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs : s ≠ 0
⊢ DifferentiableAt ℂ (Function.update (fun s => Λ s / s.Gammaℝ) 0 (L / 2)) s

case inr
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s => s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u => Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun s => Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : 0 ≠ 1
⊢ DifferentiableAt ℂ (Function.update (fun s => Λ s / s.Gammaℝ) 0 (L / 2)) 0

Proof state:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s => s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
⊢ DifferentiableAt ℂ (Function.update (fun s => Λ s / s.Gammaℝ) 0 (L / 2)) s

Tactic:
have claim (t) (ht : t ≠ 0) (ht' : t ≠ 1) : DifferentiableAt ℂ (fun u : ℂ ↦ Λ u / Gammaℝ u) t :=
  (hf t ht ht').mul differentiable_Gammaℝ_inv.differentiableAt

Result:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s => s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u => Λ u / u.Gammaℝ) t
⊢ DifferentiableAt ℂ (Function.update (fun s => Λ s / s.Gammaℝ) 0 (L / 2)) s

Proof state:
case inr
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s => s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u => Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun s => Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : 0 ≠ 1
S_nhds : {1}ᶜ ∈ 𝓝 0
⊢ DifferentiableAt ℂ (Function.update (fun s => Λ s / s.Gammaℝ) 0 (limUnder (𝓝[≠] 0) fun s => Λ s / s.Gammaℝ)) 0

Tactic:
refine ((Complex.differentiableOn_update_limUnder_of_isLittleO S_nhds
  (fun t ht ↦ (claim t ht.2 ht.1).differentiableWithinAt) ?_) 0 hs').differentiableAt S_nhds

Result:
case inr
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s => s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u => Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun s => Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : 0 ≠ 1
S_nhds : {1}ᶜ ∈ 𝓝 0
⊢ (fun z => Λ z / z.Gammaℝ - Λ 0 / Gammaℝ 0) =o[𝓝[≠] 0] fun z => (z - 0)⁻¹

Proof state:
case h
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s => s * Λ s) (𝓝[≠] 0) (𝓝 L)
s✝ : ℂ
hs' : s✝ ≠ 1
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u => Λ u / u.Gammaℝ) t
s : ℂ
hs : s ≠ 0
⊢ ((fun s => s * Λ s) / fun s => s * s.Gammaℝ) s = Λ s / s.Gammaℝ

Tactic:
rw [Pi.div_apply, ← div_div, mul_div_cancel_left₀ _ hs]

Result:
no goals

Proof state:
case inr
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s => s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u => Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun s => Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : 0 ≠ 1
S_nhds : {1}ᶜ ∈ 𝓝 0
⊢ (fun z => Λ z / (↑π ^ (-z / 2) * Complex.Gamma (z / 2))) =o[𝓝[≠] 0] fun z => z⁻¹

Tactic:
refine (isBigO_const_of_tendsto claim2 <| one_ne_zero' ℂ).trans_isLittleO ?_

Result:
case inr
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s => s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u => Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun s => Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : 0 ≠ 1
S_nhds : {1}ᶜ ∈ 𝓝 0
⊢ (fun _x => 1) =o[𝓝[≠] 0] fun z => z⁻¹

Proof state:
case inl
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s => s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u => Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun s => Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs : s ≠ 0
⊢ Function.update (fun s => Λ s / s.Gammaℝ) 0 (L / 2) =ᶠ[𝓝 s] fun u => Λ u / u.Gammaℝ

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

Result:
case h
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s => s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u => Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun s => Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs : s ≠ 0
x : ℂ
hx : x ∈ {0}ᶜ
⊢ Function.update (fun s => Λ s / s.Gammaℝ) 0 (L / 2) x = Λ x / x.Gammaℝ