-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : UniqueDiffOn 𝕜 s
n : ℕ
IH :
  ∀ {x : E} (hx : x ∈ s) (m : Fin (n + 1) → E),
    Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 (n + 1) f s x : (a : (i : Fin (n + 1)) → E) → F) m : F)
      ((((iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s x : (a : (i : Fin n) → E) → E →L[𝕜] F)
                (init (α := fun (i : Fin (n + 1)) ↦ E) m) :
              E →L[𝕜] F) :
            (a : E) → F)
          (m (last n)) :
        F)
x : E
hx : x ∈ s
m : Fin (n + 1 + 1) → E
I : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F) ≃ₗᵢ[𝕜]
  ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F :=
  LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n E F)
A :
  ∀ y ∈ s,
    Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F)
      (iteratedFDerivWithin 𝕜 n.succ f s y)
      (comp (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
        ((⇑I :
            (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
              ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F) :
          (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
            ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F)
        (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s :
          E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
        y)
𝕜₁ :
  Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 (n + 2) f s x : (a : (i : Fin (n + 2)) → E) → F) m : F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n.succ f s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n.succ) ↦ E) F)
              (m 0) :
            ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F) :
          (a : (i : Fin n.succ) → E) → F)
        (tail (α := fun (i : Fin (n + 1 + 1)) ↦ E) m) :
      F)
𝕜₂ :
  Eq.{uF + 1} (α := F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n.succ f s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n.succ) ↦ E) F)
              (m 0) :
            ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F) :
          (a : (i : Fin n.succ) → E) → F)
        (tail (α := fun (i : Fin (n + 1 + 1)) ↦ E) m) :
      F)
    ((((fderivWithin 𝕜
                  (comp (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
                    ((⇑I :
                        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
                          ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F) :
                      (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
                        ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F)
                    (iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s :
                      E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)))
                  s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n.succ) ↦ E) F)
              (m 0) :
            ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F) :
          (a : (i : Fin n.succ) → E) → F)
        (tail (α := fun (i : Fin (n + 1 + 1)) ↦ E) m) :
      F)
𝕜₃ :
  Eq.{uF + 1} (α := F)
    ((((fderivWithin 𝕜
                  (comp (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
                    ((⇑I :
                        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
                          ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F) :
                      (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
                        ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F)
                    (iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s :
                      E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)))
                  s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n.succ) ↦ E) F)
              (m 0) :
            ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F) :
          (a : (i : Fin n.succ) → E) → F)
        (tail (α := fun (i : Fin (n + 1 + 1)) ↦ E) m) :
      F)
    ((comp (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
            (⇑I :
              (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
                ContinuousMultilinearMap 𝕜 (fun (i : Fin n.succ) ↦ E) F)
            (⇑(fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s) s x) :
              (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
            (m 0) :
          (a : (i : Fin (n + 1)) → E) → F)
        (tail (α := fun (i : Fin (n + 1 + 1)) ↦ E) m) :
      F)
𝕜₄ :
  Eq.{uF + 1} (α := F)
    ((comp (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
            (⇑I :
              (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
                ContinuousMultilinearMap 𝕜 (fun (i : Fin n.succ) ↦ E) F)
            (⇑(fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s) s x) :
              (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
            (m 0) :
          (a : (i : Fin (n + 1)) → E) → F)
        (tail (α := fun (i : Fin (n + 1 + 1)) ↦ E) m) :
      F)
    ((((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s) s x :
                      (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
                    (m 0) :
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) :
                (a : (i : Fin n) → E) → E →L[𝕜] F)
              (init (α := fun (i : Fin (n + 1)) ↦ E) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ E) m)) :
            E →L[𝕜] F) :
          (a : E) → F)
        (tail (α := fun (i : Fin (n + 1 + 1)) ↦ E) m (last n)) :
      F)
𝕜₅ :
  Eq.{uF + 1} (α := F)
    ((((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s) s x :
                      (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
                    (m 0) :
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) :
                (a : (i : Fin n) → E) → E →L[𝕜] F)
              (init (α := fun (i : Fin (n + 1)) ↦ E) (tail (α := fun (i : Fin (n + 1 + 1)) ↦ E) m)) :
            E →L[𝕜] F) :
          (a : E) → F)
        (tail (α := fun (i : Fin (n + 1 + 1)) ↦ E) m (last n)) :
      F)
    ((((iteratedFDerivWithin 𝕜 n.succ (fun (y : E) ↦ fderivWithin 𝕜 f s y) s x : (a : (i : Fin n.succ) → E) → E →L[𝕜] F)
              (init (α := fun (i : Fin (n + 1 + 1)) ↦ E) m) :
            E →L[𝕜] F) :
          (a : E) → F)
        (m (last (n + 1))) :
      F)
⊢ Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 (n + 1 + 1) f s x : (a : (i : Fin (n + 1 + 1)) → E) → F) m : F)
    ((((iteratedFDerivWithin 𝕜 (n + 1) (fun (y : E) ↦ fderivWithin 𝕜 f s y) s x :
                (a : (i : Fin (n + 1)) → E) → E →L[𝕜] F)
              (init (α := fun (i : Fin (n + 1 + 1)) ↦ E) m) :
            E →L[𝕜] F) :
          (a : E) → F)
        (m (last (n + 1))) :
      F)

Tactic:
calc
      (iteratedFDerivWithin 𝕜 (n + 2) f s x : (Fin (n + 2) → E) → F) m =
          (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n.succ f s) s x : E → E [×n + 1]→L[𝕜] F) (m 0)
            (tail m) := by
        simp [iteratedFDerivWithin_succ_eq_comp_left]
      _ = (fderivWithin 𝕜 (I ∘ iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s) s x :
              E → E [×n + 1]→L[𝕜] F) (m 0) (tail m) := by
        rw [fderivWithin_congr A (A x hx)]
      _ = (I ∘ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s) s x :
              E → E [×n + 1]→L[𝕜] F) (m 0) (tail m) := by
        simp [LinearIsometryEquiv.comp_fderivWithin _ (hs x hx)]
      _ = (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s) s x :
              E → E [×n]→L[𝕜] E →L[𝕜] F) (m 0) (init (tail m)) ((tail m) (last n)) := by
        simp [I]
      _ = iteratedFDerivWithin 𝕜 (Nat.succ n) (fun y => fderivWithin 𝕜 f s y) s x (init m)
            (m (last (n + 1))) := by
        rw [iteratedFDerivWithin_succ_apply_left, tail_init_eq_init_tail]
        simp [init, tail]

Premises used: Function.comp, iteratedFDerivWithin, Fin.init, fderivWithin, HAdd.hAdd, Fin.last, OfNat.ofNat, Nat.succ, Fin.tail, DFunLike.coe