have := HasDerivAt.cpow_const (c := s) (hasDerivAt_id (x : ℂ)) (Or.inl hx)
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s✝ : ℂ
hs✝ : s✝ ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
s : ℂ
hs : s ≠ 0
x : ℝ
hx : x ∈ Ioi 0
⊢ deriv g x = ↑x ^ (s - 1)
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s✝ : ℂ
hs✝ : s✝ ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
s : ℂ
hs : s ≠ 0
x : ℝ
hx : x ∈ Ioi 0
this : HasDerivAt (fun x => id x ^ s) (s * id ↑x ^ (s - 1) * 1) ↑x
⊢ deriv g x = ↑x ^ (s - 1)