Theorem: HasDerivWithinAt.finset_prod (ForML/FDerivProd.lean)

State before:
𝕜 : 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
x : 𝕜
s t : Set 𝕜
ι : Type u_3
inst✝² : DecidableEq ι
𝔸' : Type u_4
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasDerivWithinAt (f i) (f' i) s x
⊢ HasDerivWithinAt (fun x => ∏ i in u, f i x) (∑ i in u, (∏ j in Finset.erase u i, f j x) • f' i) s x
Tactic:
simpa [ContinuousLinearMap.sum_apply, ContinuousLinearMap.smul_apply] using
  (HasFDerivWithinAt.finset_prod (fun i hi ↦ (hf i hi).hasFDerivWithinAt)).hasDerivWithinAt
State after:
no goals