suffices Tendsto (norm ∘ (fun (s : ℂ) ↦ ↑x ^ s / s - (↑x ^ s / (s + 1) - x⁻¹ / (s + 1))))
    (𝓝[≠] (-1)) (𝓝 (‖x ^ (-1 : ℂ) / -1 - (deriv (fun (s : ℂ) ↦ (x : ℂ) ^ s) (-1))‖)) by
  apply this.congr'
  filter_upwards [diff_mem_nhdsWithin_compl (isOpen_compl_singleton.mem_nhds
    (Set.mem_compl_singleton_iff.mpr (by norm_num : (-1 : ℂ) ≠ 0))) {-1}] with s hs
  rw [Function.comp_apply, Function.comp_apply, keyIdentity _ hs.1 hs.2]
  ring_nf
case hf
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
⊢ Tendsto (Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - -↑x⁻¹ / (s + 1)) (𝓝[≠] (-1)) (𝓝 ?y)

case y
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
⊢ ℝ
case hf
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
⊢ Tendsto (Norm.norm ∘ fun s => ↑x ^ s / s - (↑x ^ s / (s + 1) - ↑x⁻¹ / (s + 1))) (𝓝[≠] (-1))
    (𝓝 ‖↑x ^ (-1) / -1 - deriv (fun s => ↑x ^ s) (-1)‖)