Real DifferentiableAt of cpow?

Stream: Is there code for X?

[Alex Kontorovich]

We have docs#Real.differentiableAt_rpow_const_of_ne but we seem not to have something like this, is that right?

import Mathlib

theorem Real.differentiableAt_cpow_const_of_ne (s : ℂ) {x : ℝ} (hx : x ≠ 0) :
    DifferentiableAt ℝ (fun (x : ℝ) => (x : ℂ) ^ s) x := by
  sorry

[Floris van Doorn]

docs#hasDerivAt_ofReal_cpow is close, but it is formulated in an inconvenient way.