Theorem: HasFDerivAt.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
ι : Type u_3
inst✝² : DecidableEq ι
𝔸' : Type u_4
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → E → 𝔸'
f' : ι → E →L[𝕜] 𝔸'
x : E
hf : ∀ i ∈ u, HasFDerivAt (f i) (f' i) x
⊢ HasFDerivAt (fun x => ∏ i in u, f i x) (∑ i in u, (∏ j in Finset.erase u i, f j x) • f' i) x
Tactic:
simp only [← Finset.prod_coe_sort u]
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[𝕜] 𝔸'
x : E
hf : ∀ i ∈ u, HasFDerivAt (f i) (f' i) x
⊢ HasFDerivAt (fun x => ∏ i : { x // x ∈ u }, f (↑i) x) (∑ i in u, (∏ j in Finset.erase u i, f j x) • f' i) x

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

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[𝕜] 𝔸'
x : E
hf : ∀ i ∈ u, HasFDerivAt (f i) (f' i) 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
Tactic:
rw [← Finset.sum_attach u, Finset.univ_eq_attach]
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[𝕜] 𝔸'
x : E
hf : ∀ i ∈ u, HasFDerivAt (f i) (f' i) x
⊢ ∑ i in Finset.attach u, (∏ j in Finset.erase (Finset.attach u) i, f (↑j) x) • f' ↑i =
    ∑ x_1 in Finset.attach u, (∏ j in Finset.erase u ↑x_1, f j x) • f' ↑x_1