refine (finset_prod_univ fun i : u ↦ hf i i.prop).congr_fderiv ?_
𝕜 : 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[𝕜] 𝔸'
x : E
hf : ∀ i ∈ u, HasFDerivWithinAt (f i) (f' i) s x
⊢ HasFDerivWithinAt (fun x => ∏ i : { x // x ∈ u }, f (↑i) x) (∑ i in u, (∏ j in Finset.erase u i, f j x) • f' i) s x
𝕜 : 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[𝕜] 𝔸'
x : E
hf : ∀ i ∈ u, HasFDerivWithinAt (f i) (f' i) s x
⊢ ∑ i : { x // x ∈ u }, (∏ j in Finset.erase Finset.univ i, f (↑j) x) • f' ↑i =
    ∑ i in u, (∏ j in Finset.erase u i, f j x) • f' i