𝕜 : 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.4345403
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
g : F → G
f : E → F
n : ℕ
N : ℕ∞
hg : ContDiff 𝕜 N g
hf : ContDiff 𝕜 N f
hn : ↑n ≤ N
x : E
C D : ℝ
hC : ∀ (i : ℕ), i ≤ n → ‖iteratedFDerivWithin 𝕜 i g univ (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f univ x‖ ≤ D ^ i
⊢ ‖iteratedFDerivWithin 𝕜 n (g ∘ f) univ x‖ ≤ ↑n ! * C * D ^ n
𝕜 : 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.4345403
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
g : F → G
f : E → F
n : ℕ
N : ℕ∞
hg : ContDiff 𝕜 N g
hf : ContDiff 𝕜 N f
hn : ↑n ≤ N
x : E
C D : ℝ
hC : ∀ (i : ℕ), i ≤ n → ‖iteratedFDeriv 𝕜 i g (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv 𝕜 i f x‖ ≤ D ^ i
⊢ ‖iteratedFDeriv 𝕜 n (g ∘ f) x‖ ≤ ↑n ! * C * D ^ n
simp_rw [← iteratedFDerivWithin_univ] at hC hD ⊢
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.4345403
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
g : F → G
f : E → F
n : ℕ
N : ℕ∞
hg : ContDiff 𝕜 N g
hf : ContDiff 𝕜 N f
hn : ↑n ≤ N
x : E
C D : ℝ
hC : ∀ (i : ℕ), i ≤ n → ‖iteratedFDerivWithin 𝕜 i g univ (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f univ x‖ ≤ D ^ i
⊢ ‖iteratedFDerivWithin 𝕜 n (g ∘ f) univ x‖ ≤ ↑n ! * C * D ^ n
exact norm_iteratedFDerivWithin_comp_le hg.contDiffOn hf.contDiffOn hn uniqueDiffOn_univ
  uniqueDiffOn_univ (mapsTo_univ _ _) (mem_univ x) hC hD