no goals
𝕂 : Type u_1
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : CompleteSpace 𝕂
inst✝ : CharZero 𝕂
x : 𝕂
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝕂))
⊢ HasStrictDerivAt (exp 𝕂) (exp 𝕂 x) x
simpa using (hasStrictFDerivAt_exp_of_mem_ball hx).hasStrictDerivAt