no goals
f g : ℂ → ℂ
s : Set ℂ
f' g' x c : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ HasStrictDerivAt (fun z => z ^ c) (c * x ^ (c - 1)) x
simpa only [MulZeroClass.mul_zero, add_zero, mul_one] using
  (hasStrictDerivAt_id x).cpow (hasStrictDerivAt_const x c) h