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