refine (Tendsto.sub ?_ (tendsto_nhdsWithin_of_tendsto_nhds ?_)).norm
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
hx0 : ↑x ≠ 0
⊢ Tendsto (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) (𝓝[≠] 0)
    (𝓝 ‖deriv (fun s => ↑x ^ s) 0 - ↑x ^ 0 / (1 + 0)‖)
case hf.refine_1
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
hx0 : ↑x ≠ 0
⊢ Tendsto (fun x_1 => ↑x ^ x_1 / x_1 - ↑x ^ 0 / x_1) (𝓝[≠] 0) (𝓝 (deriv (fun s => ↑x ^ s) 0))

case hf.refine_2
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
hx0 : ↑x ≠ 0
⊢ Tendsto (fun x_1 => ↑x ^ x_1 / (1 + x_1)) (𝓝 0) (𝓝 (↑x ^ 0 / (1 + 0)))