no goals
e : ℂ → ℂ
e' : ℂ
z : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
s : Set ℂ
x : ℂ
f' : E
h : HasDerivWithinAt f f' s x
⊢ HasFDerivWithinAt f (ContinuousLinearMap.smulRight reClm f' + I • ContinuousLinearMap.smulRight imClm f') s x
simpa only [Complex.restrictScalars_one_smulRight'] using
  h.hasFDerivWithinAt.restrictScalars ℝ