Theorem: HasFDerivWithinAt.finset_prod_univ (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
ι : 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
⊢ HasFDerivWithinAt (fun x => ∏ i : ι, f i x) (∑ i : ι, (∏ j in Finset.erase Finset.univ i, f j x) • f' i) s x
Tactic:
refine HasFDerivWithinAt.congr_fderiv
  (hasFDerivAt_finset_prod_univ.comp_hasFDerivWithinAt x <| hasFDerivWithinAt_pi.mpr hf) ?_
State after:
𝕜 : 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

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
ι : 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
Tactic:
ext m
State after:
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

State before:
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
Tactic:
simp [comp_apply (R₁ := 𝕜), sum_apply (R₁ := 𝕜), smul_apply]
State after:
no goals