rw [deriv_cexp (hf.smul_const I)]
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
x : ℝ
hf : DifferentiableAt ℝ f x
⊢ deriv (fun x => cexp (f x • I)) x = ↑(deriv f x) * I * cexp (f x • I)
E : Type u_1
inst✝ : TopologicalSpace E
f : ℝ → ℝ
x : ℝ
hf : DifferentiableAt ℝ f x
⊢ cexp (f x • I) * deriv (fun y => f y • I) x = ↑(deriv f x) * I * cexp (f x • I)