-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem _root_.HasFDerivWithinAt.multilinear_comp
    [DecidableEq ι] {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
    {g : ∀ i, G → E i} {g' : ∀ i, G →L[𝕜] E i} {s : Set G} {x : G}
    (hg : ∀ i, HasFDerivWithinAt (g i) (g' i) s x) :
    HasFDerivWithinAt (fun x ↦ f (fun i ↦ g i x))
      ((∑ i : ι, (f.toContinuousLinearMap (fun j ↦ g j x) i) ∘L (g' i))) s x

Proof state:
case h.e'_12.h
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
inst✝² : DecidableEq ι
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : (i : ι) → G → E i
g' : (i : ι) → G →L[𝕜] E i
s : Set G
x : G
hg : ∀ (i : ι), HasFDerivWithinAt (g i) (g' i) s x
v : G
⊢ (∑ i : ι, (f.toContinuousLinearMap (fun j => g j x) i).comp (g' i)) v =
    ((f.linearDeriv fun j => g j x).comp (ContinuousLinearMap.pi g')) v

Tactic:
simp [linearDeriv]

Result:
no goals

Proof state:
case h.e'_12
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
inst✝² : DecidableEq ι
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : (i : ι) → G → E i
g' : (i : ι) → G →L[𝕜] E i
s : Set G
x : G
hg : ∀ (i : ι), HasFDerivWithinAt (g i) (g' i) s x
⊢ ∑ i : ι, (f.toContinuousLinearMap (fun j => g j x) i).comp (g' i) =
    (f.linearDeriv fun j => g j x).comp (ContinuousLinearMap.pi g')

Tactic:
ext v

Result:
case h.e'_12.h
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
inst✝² : DecidableEq ι
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : (i : ι) → G → E i
g' : (i : ι) → G →L[𝕜] E i
s : Set G
x : G
hg : ∀ (i : ι), HasFDerivWithinAt (g i) (g' i) s x
v : G
⊢ (∑ i : ι, (f.toContinuousLinearMap (fun j => g j x) i).comp (g' i)) v =
    ((f.linearDeriv fun j => g j x).comp (ContinuousLinearMap.pi g')) v

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
inst✝² : DecidableEq ι
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : (i : ι) → G → E i
g' : (i : ι) → G →L[𝕜] E i
s : Set G
x : G
hg : ∀ (i : ι), HasFDerivWithinAt (g i) (g' i) s x
⊢ HasFDerivWithinAt (fun x => f fun i => g i x) (∑ i : ι, (f.toContinuousLinearMap (fun j => g j x) i).comp (g' i)) s x

Tactic:
convert (f.hasFDerivAt (fun j ↦ g j x)).comp_hasFDerivWithinAt x (hasFDerivWithinAt_pi.2 hg)

Result:
case h.e'_12
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
inst✝² : DecidableEq ι
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : (i : ι) → G → E i
g' : (i : ι) → G →L[𝕜] E i
s : Set G
x : G
hg : ∀ (i : ι), HasFDerivWithinAt (g i) (g' i) s x
⊢ ∑ i : ι, (f.toContinuousLinearMap (fun j => g j x) i).comp (g' i) =
    (f.linearDeriv fun j => g j x).comp (ContinuousLinearMap.pi g')