-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem _root_.HasFDerivWithinAt.linear_multilinear_comp
    [DecidableEq ι] {a : H → E} {a' : H →L[𝕜] E}
    {b : ∀ i, H → G i} {b' : ∀ i, H →L[𝕜] G i} {s : Set H} {x : H}
    (ha : HasFDerivWithinAt a a' s x) (hb : ∀ i, HasFDerivWithinAt (b i) (b' i) s x)
    (f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F) :
    HasFDerivWithinAt (fun y ↦ f (a y) (fun i ↦ b i y))
      ((f.flipMultilinear (fun i ↦ b i x)) ∘L a' +
        ∑ i, ((f (a x)).toContinuousLinearMap (fun j ↦ b j x) i) ∘L (b' i)) s x

Proof state:
case h.e'_12.h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type v
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
ι : Type u_2
G : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (G i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (G i)
inst✝³ : Fintype ι
H : Type u_4
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : DecidableEq ι
a : H → E
a' : H →L[𝕜] E
b : (i : ι) → H → G i
b' : (i : ι) → H →L[𝕜] G i
s : Set H
x : H
ha : HasFDerivWithinAt a a' s x
hb : ∀ (i : ι), HasFDerivWithinAt (b i) (b' i) s x
f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F
v : H
⊢ ((f.flipMultilinear fun i => b i x).comp a' +
        ∑ i : ι, ((f (a x)).toContinuousLinearMap (fun j => b j x) i).comp (b' i))
      v =
    (((f.flipMultilinear (a x, fun i => b i x).2).comp (fst 𝕜 E ((i : ι) → G i)) +
            ∑ i : ι,
              ((f (a x, fun i => b i x).1).toContinuousLinearMap (a x, fun i => b i x).2 i).comp
                ((proj i).comp (snd 𝕜 E ((i : ι) → G i)))).comp
        (a'.prod (pi b')))
      v

Tactic:
simp

Result:
no goals

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

Tactic:
convert (hasFDerivAt_uncurry_of_multilinear f (a x, fun i ↦ b i x)).comp_hasFDerivWithinAt x
  (ha.prod (hasFDerivWithinAt_pi.mpr hb))

Result:
case h.e'_12
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type v
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
ι : Type u_2
G : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (G i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (G i)
inst✝³ : Fintype ι
H : Type u_4
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : DecidableEq ι
a : H → E
a' : H →L[𝕜] E
b : (i : ι) → H → G i
b' : (i : ι) → H →L[𝕜] G i
s : Set H
x : H
ha : HasFDerivWithinAt a a' s x
hb : ∀ (i : ι), HasFDerivWithinAt (b i) (b' i) s x
f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F
⊢ (f.flipMultilinear fun i => b i x).comp a' +
      ∑ i : ι, ((f (a x)).toContinuousLinearMap (fun j => b j x) i).comp (b' i) =
    ((f.flipMultilinear (a x, fun i => b i x).2).comp (fst 𝕜 E ((i : ι) → G i)) +
          ∑ i : ι,
            ((f (a x, fun i => b i x).1).toContinuousLinearMap (a x, fun i => b i x).2 i).comp
              ((proj i).comp (snd 𝕜 E ((i : ι) → G i)))).comp
      (a'.prod (pi b'))

Proof state:
case h.e'_12
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type v
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
ι : Type u_2
G : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (G i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (G i)
inst✝³ : Fintype ι
H : Type u_4
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : DecidableEq ι
a : H → E
a' : H →L[𝕜] E
b : (i : ι) → H → G i
b' : (i : ι) → H →L[𝕜] G i
s : Set H
x : H
ha : HasFDerivWithinAt a a' s x
hb : ∀ (i : ι), HasFDerivWithinAt (b i) (b' i) s x
f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F
⊢ (f.flipMultilinear fun i => b i x).comp a' +
      ∑ i : ι, ((f (a x)).toContinuousLinearMap (fun j => b j x) i).comp (b' i) =
    ((f.flipMultilinear (a x, fun i => b i x).2).comp (fst 𝕜 E ((i : ι) → G i)) +
          ∑ i : ι,
            ((f (a x, fun i => b i x).1).toContinuousLinearMap (a x, fun i => b i x).2 i).comp
              ((proj i).comp (snd 𝕜 E ((i : ι) → G i)))).comp
      (a'.prod (pi b'))

Tactic:
ext v

Result:
case h.e'_12.h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type v
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
ι : Type u_2
G : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (G i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (G i)
inst✝³ : Fintype ι
H : Type u_4
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : DecidableEq ι
a : H → E
a' : H →L[𝕜] E
b : (i : ι) → H → G i
b' : (i : ι) → H →L[𝕜] G i
s : Set H
x : H
ha : HasFDerivWithinAt a a' s x
hb : ∀ (i : ι), HasFDerivWithinAt (b i) (b' i) s x
f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F
v : H
⊢ ((f.flipMultilinear fun i => b i x).comp a' +
        ∑ i : ι, ((f (a x)).toContinuousLinearMap (fun j => b j x) i).comp (b' i))
      v =
    (((f.flipMultilinear (a x, fun i => b i x).2).comp (fst 𝕜 E ((i : ι) → G i)) +
            ∑ i : ι,
              ((f (a x, fun i => b i x).1).toContinuousLinearMap (a x, fun i => b i x).2 i).comp
                ((proj i).comp (snd 𝕜 E ((i : ι) → G i)))).comp
        (a'.prod (pi b')))
      v