no goals
x✝ y z a x : ℝ
ha : a < 0
⊢ HasStrictDerivAt (fun x => a ^ x) (a ^ x * log a - exp (log a * x) * sin (x * π) * π) x
simpa using (hasStrictFDerivAt_rpow_of_neg (a, x) ha).comp_hasStrictDerivAt x
  ((hasStrictDerivAt_const _ _).prod (hasStrictDerivAt_id _))