-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
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
hu : UniqueDiffOn 𝕜 s
i : ℕ
hi :
  ∀ {x : E} (hx : x ∈ s),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (_root_.iteratedFDerivWithin 𝕜 i (-f) s x) (-_root_.iteratedFDerivWithin 𝕜 i f s x)
x : E
hx : x ∈ s
h : (i : Fin (i + 1)) → E
iteratedFDerivWithin :
  Eq.{uF + 1} (α := F)
    ((((fderivWithin 𝕜 (_root_.iteratedFDerivWithin 𝕜 i (-f) s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
    ((((fderivWithin 𝕜 (-_root_.iteratedFDerivWithin 𝕜 i f s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
iteratedFDerivWithin₁ :
  Eq.{uF + 1} (α := F)
    ((((fderivWithin 𝕜 (-_root_.iteratedFDerivWithin 𝕜 i f s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
    (-(((fderivWithin 𝕜 (_root_.iteratedFDerivWithin 𝕜 i f s) s x :
                  (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
                (h 0) :
              ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
            (a : (i : Fin i) → E) → F)
          (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
iteratedFDerivWithin₂ :
  Eq.{uF + 1} (α := F)
    (-(((fderivWithin 𝕜 (_root_.iteratedFDerivWithin 𝕜 i f s) s x :
                  (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
                (h 0) :
              ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
            (a : (i : Fin i) → E) → F)
          (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
    (-(_root_.iteratedFDerivWithin 𝕜 (i + 1) f s x : (a : (i : Fin (i + 1)) → E) → F) h : F)
⊢ Eq.{uF + 1} (α := F) ((_root_.iteratedFDerivWithin 𝕜 (i + 1) (-f) s x : (a : (i : Fin (i + 1)) → E) → F) h : F)
    ((-_root_.iteratedFDerivWithin 𝕜 (i + 1) f s x : (a : (i : Fin (i + 1)) → E) → F) h : F)

Tactic:
calc
      iteratedFDerivWithin 𝕜 (i + 1) (-f) s x h =
          fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (-f) s) s x (h 0) (Fin.tail h) :=
        iteratedFDerivWithin_succ_apply_left _
      _ = fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x (h 0) (Fin.tail h) := by
        rw [fderivWithin_congr' (@hi) hx, Pi.neg_def]
      _ = -(fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s) x (h 0) (Fin.tail h) := by
        rw [fderivWithin_neg (hu x hx), ContinuousLinearMap.neg_apply,
          ContinuousMultilinearMap.neg_apply]
      _ = -(iteratedFDerivWithin 𝕜 (i + 1) f s) x h := by
        rw [iteratedFDerivWithin_succ_apply_left]

Premises used: iteratedFDerivWithin, iteratedFDerivWithin_succ_apply_left, fderivWithin, HAdd.hAdd, OfNat.ofNat, Fin.tail, DFunLike.coe, Neg.neg