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