internlm/Lean-Github huggingface dataset:
Theorem: iteratedFDerivWithin_sum_apply
Proof 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 ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffOn 𝕜 (↑i) (f j) s) →
    iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) s x = ∑ j in u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ∀ j ∈ insert a u, ContDiffOn 𝕜 (↑i) (f j) s
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j in insert a u, f j x) s x =
    ∑ j in insert a u, iteratedFDerivWithin 𝕜 i (f j) s x
Tactic:
simp only [Finset.mem_insert] at h
Proof 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 ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffOn 𝕜 (↑i) (f j) s) →
    iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) s x = ∑ j in u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ∀ (j : ι), j = a ∨ j ∈ u → ContDiffOn 𝕜 (↑i) (f j) s
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j in insert a u, f j x) s x =
    ∑ j in insert a u, iteratedFDerivWithin 𝕜 i (f j) s x
Theorem: iteratedFDerivWithin_sum_apply
Proof 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 ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffOn 𝕜 (↑i) (f j) s) →
    iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) s x = ∑ j in u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ∀ (j : ι), j = a ∨ j ∈ u → ContDiffOn 𝕜 (↑i) (f j) s
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j in insert a u, f j x) s x =
    ∑ j in insert a u, iteratedFDerivWithin 𝕜 i (f j) s x
Tactic:
simp only [Finset.mem_insert, forall_eq_or_imp] at h
Proof 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 ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffOn 𝕜 (↑i) (f j) s) →
    iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) s x = ∑ j in u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ContDiffOn 𝕜 (↑i) (f a) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 (↑i) (f a) s
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j in insert a u, f j x) s x =
    ∑ j in insert a u, iteratedFDerivWithin 𝕜 i (f j) s x
Theorem: iteratedFDerivWithin_sum_apply
Proof 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 ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffOn 𝕜 (↑i) (f j) s) →
    iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) s x = ∑ j in u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ContDiffOn 𝕜 (↑i) (f a) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 (↑i) (f a) s
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j in insert a u, f j x) s x =
    ∑ j in insert a u, iteratedFDerivWithin 𝕜 i (f j) s x
Tactic:
simp only [Finset.sum_insert ha]
Proof 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 ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffOn 𝕜 (↑i) (f j) s) →
    iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) s x = ∑ j in u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ContDiffOn 𝕜 (↑i) (f a) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 (↑i) (f a) s
⊢ iteratedFDerivWithin 𝕜 i (fun x => f a x + ∑ j in u, f j x) s x =
    iteratedFDerivWithin 𝕜 i (f a) s x + ∑ j in u, iteratedFDerivWithin 𝕜 i (f j) s x
Theorem: iteratedFDerivWithin_sum_apply
Proof 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 ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffOn 𝕜 (↑i) (f j) s) →
    iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) s x = ∑ j in u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ContDiffOn 𝕜 (↑i) (f a) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 (↑i) (f a) s
⊢ iteratedFDerivWithin 𝕜 i (fun x => f a x + ∑ j in u, f j x) s x =
    iteratedFDerivWithin 𝕜 i (f a) s x + ∑ j in u, iteratedFDerivWithin 𝕜 i (f j) s x
Tactic:
rw [iteratedFDerivWithin_add_apply' h.1 (ContDiffOn.sum h.2) hs hx, IH h.2]
Proof state after:
no goals
Theorem: iteratedFDeriv_sum
Proof 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 ι
f : ι → E → F
u : Finset ι
i : ℕ
h : ∀ j ∈ u, ContDiff 𝕜 (↑i) (f j)
⊢ (iteratedFDeriv 𝕜 i fun x => ∑ j in u, f j x) = ∑ j in u, iteratedFDeriv 𝕜 i (f j)
Tactic:
simp only [← iteratedFDerivWithin_univ]
Proof 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 ι
f : ι → E → F
u : Finset ι
i : ℕ
h : ∀ j ∈ u, ContDiff 𝕜 (↑i) (f j)
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) Set.univ = ∑ x in u, iteratedFDerivWithin 𝕜 i (f x) Set.univ
Theorem: iteratedFDeriv_sum
Proof 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 ι
f : ι → E → F
u : Finset ι
i : ℕ
h : ∀ j ∈ u, ContDiff 𝕜 (↑i) (f j)
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) Set.univ = ∑ x in u, iteratedFDerivWithin 𝕜 i (f x) Set.univ
Tactic:
funext x
Proof 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 ι
f : ι → E → F
u : Finset ι
i : ℕ
h : ∀ j ∈ u, ContDiff 𝕜 (↑i) (f j)
x : E
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) Set.univ x =
    Finset.sum u (fun x => iteratedFDerivWithin 𝕜 i (f x) Set.univ) x
Theorem: iteratedFDeriv_sum
Proof 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 ι
f : ι → E → F
u : Finset ι
i : ℕ
h : ∀ j ∈ u, ContDiff 𝕜 (↑i) (f j)
x : E
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) Set.univ x =
    Finset.sum u (fun x => iteratedFDerivWithin 𝕜 i (f x) Set.univ) x
Tactic:
rw [Finset.sum_apply]
Proof 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 ι
f : ι → E → F
u : Finset ι
i : ℕ
h : ∀ j ∈ u, ContDiff 𝕜 (↑i) (f j)
x : E
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) Set.univ x = ∑ c in u, iteratedFDerivWithin 𝕜 i (f c) Set.univ x
Theorem: iteratedFDeriv_sum
Proof 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 ι
f : ι → E → F
u : Finset ι
i : ℕ
h : ∀ j ∈ u, ContDiff 𝕜 (↑i) (f j)
x : E
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) Set.univ x = ∑ c in u, iteratedFDerivWithin 𝕜 i (f c) Set.univ x
Tactic:
exact iteratedFDerivWithin_sum_apply uniqueDiffOn_univ trivial fun j hj ↦ (h j hj).contDiffOn
Proof state after:
no goals
Theorem: hasStrictFDerivAt_finset_prod_univ
Proof 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
Proof 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
Theorem: hasStrictFDerivAt_finset_prod_univ
Proof 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]
Proof state after:
no goals
Theorem: hasStrictFDerivAt_finset_prod_univ
Proof 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]
Proof 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
Theorem: hasStrictFDerivAt_finset_prod_univ
Proof 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 ?_
Proof 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
Theorem: hasStrictFDerivAt_finset_prod_univ
Proof 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]
Proof 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
Theorem: hasStrictFDerivAt_finset_prod_univ
Proof 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]
Proof 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