Theorem: hasStrictFDerivAt_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 : ι → 𝔸'
⊢ HasStrictFDerivAt (fun x => ∏ i : ι, x i) (∑ i : ι, (∏ j in Finset.erase Finset.univ i, x j) • proj i) x
Tactic:
generalize (Finset.univ : Finset ι) = 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[𝕜] 𝔸'
inst✝ : Fintype ι
x : ι → 𝔸'
u : Finset ι
⊢ HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x

State before:
case empty
𝕜 : 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 : ι → 𝔸'
⊢ HasStrictFDerivAt (fun x => ∏ i in ∅, x i) (∑ i in ∅, (∏ j in Finset.erase ∅ i, x j) • proj i) x
Tactic:
simp [hasStrictFDerivAt_const]
State after:
no goals

State before:
case insert
𝕜 : 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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
⊢ HasStrictFDerivAt (fun x => ∏ i in insert i u, x i)
    (∑ i_1 in insert i u, (∏ j in Finset.erase (insert i u) i_1, x j) • proj i_1) x
Tactic:
simp only [Finset.prod_insert hi]
State after:
case insert
𝕜 : 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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
⊢ HasStrictFDerivAt (fun x => x i * ∏ i in u, x i)
    (∑ x_1 in insert i u, (∏ j in Finset.erase (insert i u) x_1, x j) • proj x_1) x

State before:
case insert
𝕜 : 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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
⊢ HasStrictFDerivAt (fun x => x i * ∏ i in u, x i)
    (∑ x_1 in insert i u, (∏ j in Finset.erase (insert i u) x_1, x j) • proj x_1) x
Tactic:
refine ((proj i).hasStrictFDerivAt.mul' IH).congr_fderiv ?_
State after:
case insert
𝕜 : 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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
⊢ (proj i) x • ∑ i in u, (∏ j in Finset.erase u i, x j) • proj i + smulRight (proj i) (∏ i in u, x i) =
    ∑ x_1 in insert i u, (∏ j in Finset.erase (insert i u) x_1, x j) • proj x_1

State before:
case insert
𝕜 : 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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
⊢ (proj i) x • ∑ i in u, (∏ j in Finset.erase u i, x j) • proj i + smulRight (proj i) (∏ i in u, x i) =
    ∑ x_1 in insert i u, (∏ j in Finset.erase (insert i u) x_1, x j) • proj x_1
Tactic:
simp only [Finset.sum_insert hi, Finset.erase_insert hi]
State after:
case insert
𝕜 : 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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
⊢ (proj i) x • ∑ x_1 in u, (∏ j in Finset.erase u x_1, x j) • proj x_1 + smulRight (proj i) (∏ j in u, x j) =
    (∏ j in u, x j) • proj i + ∑ x_1 in u, (∏ j in Finset.erase (insert i u) x_1, x j) • proj x_1

State before:
case insert
𝕜 : 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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
⊢ (proj i) x • ∑ x_1 in u, (∏ j in Finset.erase u x_1, x j) • proj x_1 + smulRight (proj i) (∏ j in u, x j) =
    (∏ j in u, x j) • proj i + ∑ x_1 in u, (∏ j in Finset.erase (insert i u) x_1, x j) • proj x_1
Tactic:
rw [add_comm]
State after:
case insert
𝕜 : 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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
⊢ smulRight (proj i) (∏ j in u, x j) + (proj i) x • ∑ x_1 in u, (∏ j in Finset.erase u x_1, x j) • proj x_1 =
    (∏ j in u, x j) • proj i + ∑ x_1 in u, (∏ j in Finset.erase (insert i u) x_1, x j) • proj x_1

State before:
case insert
𝕜 : 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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
⊢ smulRight (proj i) (∏ j in u, x j) + (proj i) x • ∑ x_1 in u, (∏ j in Finset.erase u x_1, x j) • proj x_1 =
    (∏ j in u, x j) • proj i + ∑ x_1 in u, (∏ j in Finset.erase (insert i u) x_1, x j) • proj x_1
Tactic:
refine congrArg₂ _ ?_ ?_
State after:
case insert.refine_1
𝕜 : 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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
⊢ smulRight (proj i) (∏ j in u, x j) = (∏ j in u, x j) • proj i

case insert.refine_2
𝕜 : 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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
⊢ (proj i) x • ∑ x_1 in u, (∏ j in Finset.erase u x_1, x j) • proj x_1 =
    ∑ x_1 in u, (∏ j in Finset.erase (insert i u) x_1, x j) • proj x_1

State before:
case insert.refine_1
𝕜 : 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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
⊢ smulRight (proj i) (∏ j in u, x j) = (∏ j in u, x j) • proj i
Tactic:
ext m
State after:
case insert.refine_1.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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
m : ι → 𝔸'
⊢ (smulRight (proj i) (∏ j in u, x j)) m = ((∏ j in u, x j) • proj i) m

State before:
case insert.refine_1.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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
m : ι → 𝔸'
⊢ (smulRight (proj i) (∏ j in u, x j)) m = ((∏ j in u, x j) • proj i) m
Tactic:
simp only [smulRight_apply (R := 𝕜), smul_apply, smul_eq_mul]
State after:
case insert.refine_1.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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
m : ι → 𝔸'
⊢ (proj i) m * ∏ j in u, x j = (∏ j in u, x j) * (proj i) m

State before:
case insert.refine_1.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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
m : ι → 𝔸'
⊢ (proj i) m * ∏ j in u, x j = (∏ j in u, x j) * (proj i) m
Tactic:
exact mul_comm _ _
State after:
no goals

State before:
case insert.refine_2
𝕜 : 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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
⊢ (proj i) x • ∑ x_1 in u, (∏ j in Finset.erase u x_1, x j) • proj x_1 =
    ∑ x_1 in u, (∏ j in Finset.erase (insert i u) x_1, x j) • proj x_1
Tactic:
ext m
State after:
case insert.refine_2.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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
m : ι → 𝔸'
⊢ ((proj i) x • ∑ x_1 in u, (∏ j in Finset.erase u x_1, x j) • proj x_1) m =
    (∑ x_1 in u, (∏ j in Finset.erase (insert i u) x_1, x j) • proj x_1) m

State before:
case insert.refine_2.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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
m : ι → 𝔸'
⊢ ((proj i) x • ∑ x_1 in u, (∏ j in Finset.erase u x_1, x j) • proj x_1) m =
    (∑ x_1 in u, (∏ j in Finset.erase (insert i u) x_1, x j) • proj x_1) m
Tactic:
simp only [smul_apply (R₁ := 𝕜), sum_apply (R₁ := 𝕜), Finset.smul_sum, smul_smul, proj_apply]
State after:
case insert.refine_2.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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
m : ι → 𝔸'
⊢ ∑ x_1 in u, (x i * ∏ j in Finset.erase u x_1, x j) • m x_1 =
    ∑ x_1 in u, (∏ j in Finset.erase (insert i u) x_1, x j) • m x_1

State before:
case insert.refine_2.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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
m : ι → 𝔸'
⊢ ∑ x_1 in u, (x i * ∏ j in Finset.erase u x_1, x j) • m x_1 =
    ∑ x_1 in u, (∏ j in Finset.erase (insert i u) x_1, x j) • m x_1
Tactic:
refine Finset.sum_congr rfl ?_
State after:
case insert.refine_2.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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
m : ι → 𝔸'
⊢ ∀ x_1 ∈ u, (x i * ∏ j in Finset.erase u x_1, x j) • m x_1 = (∏ j in Finset.erase (insert i u) x_1, x j) • m x_1

State before:
case insert.refine_2.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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
m : ι → 𝔸'
⊢ ∀ x_1 ∈ u, (x i * ∏ j in Finset.erase u x_1, x j) • m x_1 = (∏ j in Finset.erase (insert i u) x_1, x j) • m x_1
Tactic:
intro k hk
State after:
case insert.refine_2.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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
m : ι → 𝔸'
k : ι
hk : k ∈ u
⊢ (x i * ∏ j in Finset.erase u k, x j) • m k = (∏ j in Finset.erase (insert i u) k, x j) • m k

State before:
case insert.refine_2.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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
m : ι → 𝔸'
k : ι
hk : k ∈ u
⊢ (x i * ∏ j in Finset.erase u k, x j) • m k = (∏ j in Finset.erase (insert i u) k, x j) • m k
Tactic:
rw [Finset.erase_insert_of_ne fun hik ↦ hi <| by simpa [hik]]
State after:
case insert.refine_2.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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
m : ι → 𝔸'
k : ι
hk : k ∈ u
⊢ (x i * ∏ j in Finset.erase u k, x j) • m k = (∏ j in insert i (Finset.erase u k), x j) • m k

State before:
case insert.refine_2.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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
m : ι → 𝔸'
k : ι
hk : k ∈ u
⊢ (x i * ∏ j in Finset.erase u k, x j) • m k = (∏ j in insert i (Finset.erase u k), x j) • m k
Tactic:
rw [Finset.prod_insert <| by simp [hi]]
State after:
no goals

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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
m : ι → 𝔸'
k : ι
hk : k ∈ u
hik : i = k
⊢ i ∈ u
Tactic:
simpa [hik]
State after:
no goals

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 : ι → 𝔸'
i : ι
u : Finset ι
hi : i ∉ u
IH : HasStrictFDerivAt (fun x => ∏ i in u, x i) (∑ i in u, (∏ j in Finset.erase u i, x j) • proj i) x
m : ι → 𝔸'
k : ι
hk : k ∈ u
⊢ i ∉ Finset.erase u k
Tactic:
simp [hi]
State after:
no goals