-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
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) (iteratedFDerivWithin 𝕜 i (-f) s x)
      (-iteratedFDerivWithin 𝕜 i f s x)
x : E
hx : x ∈ s
h : (i : Fin (i + 1)) → E
rw :
  Eq.{uF + 1} (α := F)
    ((((-fderivWithin 𝕜 (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 𝕜 (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)
rw₁ :
  Eq.{uF + 1} (α := F)
    (((-(fderivWithin 𝕜 (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 𝕜 (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)
⊢ Eq.{uF + 1} (α := F)
    ((((fderivWithin 𝕜 (-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 𝕜 (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)
have rw₂ : Eq.{uF + 1} (α := F)
  (-(((fderivWithin 𝕜 (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 𝕜 (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)
Tactic: rw [fderivWithin_neg (hu x hx), ContinuousLinearMap.neg_apply,
          ContinuousMultilinearMap.neg_apply]