𝕜 : 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.266576
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
f : E → F
g : F →ₗᵢ[𝕜] G
hf : ContDiff 𝕜 n f
x : E
i : ℕ
hi : ↑i ≤ n
⊢ ‖iteratedFDerivWithin 𝕜 i (↑g ∘ f) univ x‖ = ‖iteratedFDerivWithin 𝕜 i f univ x‖
𝕜 : 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.266576
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
f : E → F
g : F →ₗᵢ[𝕜] G
hf : ContDiff 𝕜 n f
x : E
i : ℕ
hi : ↑i ≤ n
⊢ ‖iteratedFDeriv 𝕜 i (↑g ∘ f) x‖ = ‖iteratedFDeriv 𝕜 i f x‖
simp only [← iteratedFDerivWithin_univ]
no goals
𝕜 : 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.266576
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
f : E → F
g : F →ₗᵢ[𝕜] G
hf : ContDiff 𝕜 n f
x : E
i : ℕ
hi : ↑i ≤ n
⊢ ‖iteratedFDerivWithin 𝕜 i (↑g ∘ f) univ x‖ = ‖iteratedFDerivWithin 𝕜 i f univ x‖
exact g.norm_iteratedFDerivWithin_comp_left hf.contDiffOn uniqueDiffOn_univ (mem_univ x) hi