no goals
e : ℂ → ℂ
e' : ℂ
z : ℝ
E : Type ?u.137741
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → ℂ
s : Set ℂ
f' x : ℂ
h : HasDerivWithinAt f f' s x
⊢ HasFDerivWithinAt f (f' • 1) s x
simpa only [Complex.restrictScalars_one_smulRight] using h.hasFDerivWithinAt.restrictScalars ℝ