𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
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 uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m✝ n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : UniqueDiffWithinAt 𝕜 s x
m : Fin 1 → E
⊢ ↑(↑(ContinuousLinearMap.comp
              (↑(ContinuousLinearEquiv.mk
                  (LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)).toLinearEquiv))
              (fderivWithin 𝕜 f s x))
          (m 0))
      (tail m) =
    ↑(fderivWithin 𝕜 f s x) (m 0)
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
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 uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m✝ n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : UniqueDiffWithinAt 𝕜 s x
m : Fin 1 → E
⊢ ↑(iteratedFDerivWithin 𝕜 1 f s x) m = ↑(fderivWithin 𝕜 f s x) (m 0)
simp only [iteratedFDerivWithin_succ_apply_left, iteratedFDerivWithin_zero_eq_comp,
  (continuousMultilinearCurryFin0 𝕜 E F).symm.comp_fderivWithin h]
no goals
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
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 uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m✝ n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : UniqueDiffWithinAt 𝕜 s x
m : Fin 1 → E
⊢ ↑(↑(ContinuousLinearMap.comp
              (↑(ContinuousLinearEquiv.mk
                  (LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)).toLinearEquiv))
              (fderivWithin 𝕜 f s x))
          (m 0))
      (tail m) =
    ↑(fderivWithin 𝕜 f s x) (m 0)
rfl