have (x : (i : ι) → E i) := (g.hasFDerivAt (fun i ↦ f i (x i))).hasFDerivAtFilter (le_refl _)
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
⊢ HasFDerivAt (fun f => compContinuousLinearMap g f)
    (∑ i : ι, ContinuousLinearMap.comp (compContinuousLinearMapUpdate g i f) (ContinuousLinearMap.proj i)) f
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
this :
  ∀ (x : (i : ι) → E i),
    HasFDerivAtFilter (⇑g) (linearDeriv g fun i => (f i) (x i)) (fun i => (f i) (x i)) (nhds fun i => (f i) (x i))
⊢ HasFDerivAt (fun f => compContinuousLinearMap g f)
    (∑ i : ι, ContinuousLinearMap.comp (compContinuousLinearMapUpdate g i f) (ContinuousLinearMap.proj i)) f