rw [(Complex.hasStrictFDerivAt_exp_real (f x)).hasFDerivAt.fderiv]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℂ
x : E
hf : DifferentiableAt ℝ f x
⊢ ContinuousLinearMap.comp (fderiv ℝ Complex.exp (f x)) (fderiv ℝ f x) = Complex.exp (f x) • fderiv ℝ f x
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℂ
x : E
hf : DifferentiableAt ℝ f x
⊢ ContinuousLinearMap.comp (Complex.exp (f x) • 1) (fderiv ℝ f x) = Complex.exp (f x) • fderiv ℝ f x