no goals
E : Type ?u.21873
inst✝ : NormedAddCommGroup E
c : ℂ
R θ : ℝ
⊢ HasDerivAt (circleMap c R) (circleMap 0 R θ * I) θ
simpa only [mul_assoc, one_mul, ofRealClm_apply, circleMap, ofReal_one, zero_add]
  using (((ofRealClm.hasDerivAt (x := θ)).mul_const I).cexp.const_mul (R : ℂ)).const_add c