𝕜 : 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.273156
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
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
this :
  iteratedFDerivWithin 𝕜 i (↑g ∘ f) s x =
    ContinuousLinearMap.compContinuousMultilinearMap (↑(ContinuousLinearEquiv.mk g.toLinearEquiv))
      (iteratedFDerivWithin 𝕜 i f s x)
⊢ ‖iteratedFDerivWithin 𝕜 i (↑g ∘ f) s x‖ = ‖iteratedFDerivWithin 𝕜 i f s 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.273156
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
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
⊢ ‖iteratedFDerivWithin 𝕜 i (↑g ∘ f) s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖
have :
  iteratedFDerivWithin 𝕜 i (g ∘ f) s x =
    (g : F →L[𝕜] G).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x) :=
  g.toContinuousLinearEquiv.iteratedFDerivWithin_comp_left f hs hx i
𝕜 : 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.273156
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
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
this :
  iteratedFDerivWithin 𝕜 i (↑g ∘ f) s x =
    ContinuousLinearMap.compContinuousMultilinearMap (↑(ContinuousLinearEquiv.mk g.toLinearEquiv))
      (iteratedFDerivWithin 𝕜 i f s x)
⊢ ‖ContinuousLinearMap.compContinuousMultilinearMap (↑(ContinuousLinearEquiv.mk g.toLinearEquiv))
        (iteratedFDerivWithin 𝕜 i f s x)‖ =
    ‖iteratedFDerivWithin 𝕜 i f s 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.273156
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
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
this :
  iteratedFDerivWithin 𝕜 i (↑g ∘ f) s x =
    ContinuousLinearMap.compContinuousMultilinearMap (↑(ContinuousLinearEquiv.mk g.toLinearEquiv))
      (iteratedFDerivWithin 𝕜 i f s x)
⊢ ‖iteratedFDerivWithin 𝕜 i (↑g ∘ f) s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖
rw [this]
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.273156
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
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
this :
  iteratedFDerivWithin 𝕜 i (↑g ∘ f) s x =
    ContinuousLinearMap.compContinuousMultilinearMap (↑(ContinuousLinearEquiv.mk g.toLinearEquiv))
      (iteratedFDerivWithin 𝕜 i f s x)
⊢ ‖ContinuousLinearMap.compContinuousMultilinearMap (↑(ContinuousLinearEquiv.mk g.toLinearEquiv))
        (iteratedFDerivWithin 𝕜 i f s x)‖ =
    ‖iteratedFDerivWithin 𝕜 i f s x‖
apply LinearIsometry.norm_compContinuousMultilinearMap g.toLinearIsometry