𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type ?u.68719
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ ↑(↑(ContinuousLinearMap.comp
              (↑(ContinuousLinearEquiv.mk (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).toLinearEquiv))
              (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x))
          1)
      (Fin.tail fun x => 1) =
    ↑(fderivWithin 𝕜 (iteratedDerivWithin n f s) s x) 1
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type ?u.68719
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x
rw [iteratedDerivWithin_eq_iteratedFDerivWithin, iteratedFDerivWithin_succ_apply_left,
  iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_fderivWithin _ hxs, derivWithin]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type ?u.68719
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ (↑(ContinuousMultilinearMap.mkPiField 𝕜 (Fin n) (↑(fderivWithin 𝕜 (iteratedDerivWithin n f s) s x) 1)) fun i => 1) =
    ↑(fderivWithin 𝕜 (iteratedDerivWithin n f s) s x) 1
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type ?u.68719
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ ↑(↑(ContinuousLinearMap.comp
              (↑(ContinuousLinearEquiv.mk (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).toLinearEquiv))
              (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x))
          1)
      (Fin.tail fun x => 1) =
    ↑(fderivWithin 𝕜 (iteratedDerivWithin n f s) s x) 1
change ((ContinuousMultilinearMap.mkPiField 𝕜 (Fin n) ((fderivWithin 𝕜
  (iteratedDerivWithin n f s) s x : 𝕜 → F) 1) : (Fin n → 𝕜) → F) fun i : Fin n => 1) =
  (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x : 𝕜 → F) 1
no goals
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type ?u.68719
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x✝ x : 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ (↑(ContinuousMultilinearMap.mkPiField 𝕜 (Fin n) (↑(fderivWithin 𝕜 (iteratedDerivWithin n f s) s x) 1)) fun i => 1) =
    ↑(fderivWithin 𝕜 (iteratedDerivWithin n f s) s x) 1
simp