simpa using hf
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
⊢ HasFDerivAt f f' (Function.update x i (x i))
no goals