case intro.intro.intro
𝕜 : Type ?u.2872501
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.2872922
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_1
inst✝⁴ : IsROrC 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
f' : E' →L[𝕂] F'
x : E'
hf : ContDiffAt 𝕂 n f x
hf' : HasFDerivAt f f' x
hn : 1 ≤ n
u : Set E'
H : u ∈ 𝓝[insert x univ] x
p : E' → FormalMultilinearSeries 𝕂 E' F'
hp : HasFTaylorSeriesUpToOn (↑1) f p u
⊢ HasStrictFDerivAt f f' x
𝕜 : Type ?u.2872501
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.2872922
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_1
inst✝⁴ : IsROrC 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
f' : E' →L[𝕂] F'
x : E'
hf : ContDiffAt 𝕂 n f x
hf' : HasFDerivAt f f' x
hn : 1 ≤ n
⊢ HasStrictFDerivAt f f' x
rcases hf 1 hn with ⟨u, H, p, hp⟩
case intro.intro.intro
𝕜 : Type ?u.2872501
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.2872922
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_1
inst✝⁴ : IsROrC 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
f' : E' →L[𝕂] F'
x : E'
hf : ContDiffAt 𝕂 n f x
hf' : HasFDerivAt f f' x
hn : 1 ≤ n
u : Set E'
p : E' → FormalMultilinearSeries 𝕂 E' F'
hp : HasFTaylorSeriesUpToOn (↑1) f p u
H : u ∈ 𝓝 x
⊢ HasStrictFDerivAt f f' x
case intro.intro.intro
𝕜 : Type ?u.2872501
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.2872922
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_1
inst✝⁴ : IsROrC 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
f' : E' →L[𝕂] F'
x : E'
hf : ContDiffAt 𝕂 n f x
hf' : HasFDerivAt f f' x
hn : 1 ≤ n
u : Set E'
H : u ∈ 𝓝[insert x univ] x
p : E' → FormalMultilinearSeries 𝕂 E' F'
hp : HasFTaylorSeriesUpToOn (↑1) f p u
⊢ HasStrictFDerivAt f f' x
simp only [nhdsWithin_univ, mem_univ, insert_eq_of_mem] at H
case intro.intro.intro
𝕜 : Type ?u.2872501
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.2872922
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_1
inst✝⁴ : IsROrC 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
f' : E' →L[𝕂] F'
x : E'
hf : ContDiffAt 𝕂 n f x
hf' : HasFDerivAt f f' x
hn : 1 ≤ n
u : Set E'
p : E' → FormalMultilinearSeries 𝕂 E' F'
hp : HasFTaylorSeriesUpToOn (↑1) f p u
H : u ∈ 𝓝 x
this : HasStrictFDerivAt f (↑(continuousMultilinearCurryFin1 𝕂 E' F') (p x 1)) x
⊢ HasStrictFDerivAt f f' x
case intro.intro.intro
𝕜 : Type ?u.2872501
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.2872922
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_1
inst✝⁴ : IsROrC 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
f' : E' →L[𝕂] F'
x : E'
hf : ContDiffAt 𝕂 n f x
hf' : HasFDerivAt f f' x
hn : 1 ≤ n
u : Set E'
p : E' → FormalMultilinearSeries 𝕂 E' F'
hp : HasFTaylorSeriesUpToOn (↑1) f p u
H : u ∈ 𝓝 x
⊢ HasStrictFDerivAt f f' x
have := hp.hasStrictFDerivAt le_rfl H
no goals
case intro.intro.intro
𝕜 : Type ?u.2872501
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.2872922
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_1
inst✝⁴ : IsROrC 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
f' : E' →L[𝕂] F'
x : E'
hf : ContDiffAt 𝕂 n f x
hf' : HasFDerivAt f f' x
hn : 1 ≤ n
u : Set E'
p : E' → FormalMultilinearSeries 𝕂 E' F'
hp : HasFTaylorSeriesUpToOn (↑1) f p u
H : u ∈ 𝓝 x
this : HasStrictFDerivAt f (↑(continuousMultilinearCurryFin1 𝕂 E' F') (p x 1)) x
⊢ HasStrictFDerivAt f f' x
rwa [hf'.unique this.hasFDerivAt]