simp[neg_pull]
K : Type
inst✝⁴ : RCLike K
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
W : Type
inst✝ : SemiInnerProductSpace K W
f : W → X → Y
⊢ (fun w x =>
      (-f w x, fun dy dw' =>
        (dw' + -(semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy).1,
          -(semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy).2))) =
    fun w x =>
    (-f w x, fun dy dw =>
      (dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w, x)) (-dy)).1,
        (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w, x)) (-dy)).2))
no goals