no goals
f g : ℂ → ℂ
s : Set ℂ
f' g' x c : ℂ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h0 : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasDerivWithinAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') s x
simpa only [aux] using (hf.hasFDerivWithinAt.cpow hg h0).hasDerivWithinAt