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