convert hasDerivAt_iff_tendsto_slope.mp
  (differentiableAt_id'.const_cpow (.inl hx0)).hasDerivAt using 2
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 / (x_1 + 1) - ↑x⁻¹ / (x_1 + 1)) (𝓝[≠] (-1)) (𝓝 (deriv (fun s => ↑x ^ s) (-1)))
case h.e'_3.h
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
x✝ : ℂ
⊢ ↑x ^ x✝ / (x✝ + 1) - ↑x⁻¹ / (x✝ + 1) = slope (fun x_1 => ↑x ^ x_1) (-1) x✝