∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ] {f : 𝕜 → ℂ} {f' : ℂ} {x : 𝕜}
  {s : Set 𝕜}, HasDerivWithinAt f f' s x → HasDerivWithinAt (fun x => Complex.exp (f x)) (Complex.exp (f x) * f') s x