rw [Function.comp_apply, Function.comp_apply, keyIdentity _ hs.1 hs.2]
case h
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
this :
  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)‖)
s : ℂ
hs : s ∈ {0}ᶜ \ {-1}
⊢ (Norm.norm ∘ fun s => ↑x ^ s / s - (↑x ^ s / (s + 1) - ↑x⁻¹ / (s + 1))) s =
    (Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - -↑x⁻¹ / (s + 1)) s
case h
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
this :
  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)‖)
s : ℂ
hs : s ∈ {0}ᶜ \ {-1}
⊢ ‖↑x ^ s / s - (↑x ^ s / (s + 1) - ↑x⁻¹ / (s + 1))‖ = ‖↑x ^ s / s - ↑x ^ s / (s + 1) - -↑x⁻¹ / (s + 1)‖