have := (Complex.analyticAt_iff_eventually_differentiableAt (c := x) (f := ζ)).mpr ?_
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
⊢ DifferentiableAt ℂ (deriv ζ) x
case refine_2
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
this : AnalyticAt ℂ ζ x
⊢ DifferentiableAt ℂ (deriv ζ) x

case refine_1
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
⊢ ∀ᶠ (z : ℂ) in 𝓝 x, DifferentiableAt ℂ ζ z