𝕜 : 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.537850
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 : G ≃ₗᵢ[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : G
hx : ↑g x ∈ s
i : ℕ
this :
  iteratedFDerivWithin 𝕜 i (f ∘ ↑g) (↑g ⁻¹' s) x =
    ContinuousMultilinearMap.compContinuousLinearMap (iteratedFDerivWithin 𝕜 i f s (↑g x)) fun x =>
      ↑(ContinuousLinearEquiv.mk g.toLinearEquiv)
⊢ ‖iteratedFDerivWithin 𝕜 i (f ∘ ↑g) (↑g ⁻¹' s) x‖ = ‖iteratedFDerivWithin 𝕜 i f s (↑g 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.537850
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 : G ≃ₗᵢ[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : G
hx : ↑g x ∈ s
i : ℕ
⊢ ‖iteratedFDerivWithin 𝕜 i (f ∘ ↑g) (↑g ⁻¹' s) x‖ = ‖iteratedFDerivWithin 𝕜 i f s (↑g x)‖
have : iteratedFDerivWithin 𝕜 i (f ∘ g) (g ⁻¹' s) x =
    (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun _ => g :=
  g.toContinuousLinearEquiv.iteratedFDerivWithin_comp_right f hs hx i
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.537850
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 : G ≃ₗᵢ[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : G
hx : ↑g x ∈ s
i : ℕ
this :
  iteratedFDerivWithin 𝕜 i (f ∘ ↑g) (↑g ⁻¹' s) x =
    ContinuousMultilinearMap.compContinuousLinearMap (iteratedFDerivWithin 𝕜 i f s (↑g x)) fun x =>
      ↑(ContinuousLinearEquiv.mk g.toLinearEquiv)
⊢ ‖iteratedFDerivWithin 𝕜 i (f ∘ ↑g) (↑g ⁻¹' s) x‖ = ‖iteratedFDerivWithin 𝕜 i f s (↑g x)‖
rw [this, ContinuousMultilinearMap.norm_compContinuous_linearIsometryEquiv]