no goals
e : ℂ → ℂ
e' : ℂ
z : ℝ
E : Type ?u.149374
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt f u z
⊢ HasDerivAt (fun y => ↑(f y)) (↑u) z
simpa only [ofRealClm_apply, ofReal_one, real_smul, mul_one] using
  ofRealClm.hasDerivAt.scomp z hf