no goals
e : ℂ → ℂ
e' : ℂ
z : ℝ
E : Type ?u.127606
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → ℂ
f' x : ℂ
h : HasDerivAt f f' x
⊢ HasFDerivAt f (f' • 1) x
simpa only [Complex.restrictScalars_one_smulRight] using h.hasFDerivAt.restrictScalars ℝ