ext m
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
ι : Type u_3
inst✝³ : DecidableEq ι
𝔸' : Type u_4
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → E → 𝔸'
f' : ι → E →L[𝕜] 𝔸'
inst✝ : Fintype ι
x : E
hf : ∀ (i : ι), HasFDerivWithinAt (f i) (f' i) s x
⊢ ContinuousLinearMap.comp (∑ i : ι, (∏ j in Finset.erase Finset.univ i, f j x) • proj i) (pi fun i => f' i) =
    ∑ i : ι, (∏ j in Finset.erase Finset.univ i, f j x) • f' i
case h
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
ι : Type u_3
inst✝³ : DecidableEq ι
𝔸' : Type u_4
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → E → 𝔸'
f' : ι → E →L[𝕜] 𝔸'
inst✝ : Fintype ι
x : E
hf : ∀ (i : ι), HasFDerivWithinAt (f i) (f' i) s x
m : E
⊢ (ContinuousLinearMap.comp (∑ i : ι, (∏ j in Finset.erase Finset.univ i, f j x) • proj i) (pi fun i => f' i)) m =
    (∑ i : ι, (∏ j in Finset.erase Finset.univ i, f j x) • f' i) m