no goals
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
A' : ι → F
h : ∀ (i : ι), i ∈ u → HasStrictDerivAt (A i) (A' i) x
⊢ HasStrictDerivAt (fun y => ∑ i in u, A i y) (∑ i in u, A' i) x
simpa [ContinuousLinearMap.sum_apply] using (HasStrictFDerivAt.sum h).hasStrictDerivAt