exact HasDerivAt.comp_of_tower x Complex.hasDerivAt_exp_real_smul_I hf
case this
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
f' x : ℝ
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun x => cexp (f x • I)) (f' • (I * cexp (f x • I))) x
no goals