𝕜 : Type u_3
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.85620
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f✝ f₀ f₁ g✝ : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x✝ : E
s✝ t✝ : Set E
L L₁ L₂ : Filter E
g : F → G
f : E → F
x : E
s : Set E
t : Set F
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
v : E
hg : DifferentiableWithinAt 𝕜 g t (f x)
⊢ ↑(fderivWithin 𝕜 g t (f x)) (↑(fderivWithin 𝕜 f s x) v) = ↑(fderivWithin 𝕜 (g ∘ f) s x) v
𝕜 : Type u_3
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.85620
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f✝ f₀ f₁ g✝ : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x✝ : E
s✝ t✝ : Set E
L L₁ L₂ : Filter E
g : F → G
f : E → F
x : E
y : F
s : Set E
t : Set F
hg : DifferentiableWithinAt 𝕜 g t y
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
hy : f x = y
v : E
⊢ ↑(fderivWithin 𝕜 g t y) (↑(fderivWithin 𝕜 f s x) v) = ↑(fderivWithin 𝕜 (g ∘ f) s x) v
subst y
𝕜 : Type u_3
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.85620
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f✝ f₀ f₁ g✝ : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x✝ : E
s✝ t✝ : Set E
L L₁ L₂ : Filter E
g : F → G
f : E → F
x : E
s : Set E
t : Set F
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
v : E
hg : DifferentiableWithinAt 𝕜 g t (f x)
⊢ ↑(fderivWithin 𝕜 g t (f x)) (↑(fderivWithin 𝕜 f s x) v) = ↑(comp (fderivWithin 𝕜 g t (f x)) (fderivWithin 𝕜 f s x)) v
𝕜 : Type u_3
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.85620
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f✝ f₀ f₁ g✝ : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x✝ : E
s✝ t✝ : Set E
L L₁ L₂ : Filter E
g : F → G
f : E → F
x : E
s : Set E
t : Set F
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
v : E
hg : DifferentiableWithinAt 𝕜 g t (f x)
⊢ ↑(fderivWithin 𝕜 g t (f x)) (↑(fderivWithin 𝕜 f s x) v) = ↑(fderivWithin 𝕜 (g ∘ f) s x) v
rw [fderivWithin.comp x hg hf h hxs]
no goals
𝕜 : Type u_3
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.85620
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f✝ f₀ f₁ g✝ : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x✝ : E
s✝ t✝ : Set E
L L₁ L₂ : Filter E
g : F → G
f : E → F
x : E
s : Set E
t : Set F
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
v : E
hg : DifferentiableWithinAt 𝕜 g t (f x)
⊢ ↑(fderivWithin 𝕜 g t (f x)) (↑(fderivWithin 𝕜 f s x) v) = ↑(comp (fderivWithin 𝕜 g t (f x)) (fderivWithin 𝕜 f s x)) v
rfl