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