rw[sub_eq_add_zero_sub]
case h.h.h.h.a
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 g : W → X → Y
hf : HasAdjDiff K fun x => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w : W
x : X
dy : Y
dw : W
⊢ (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy).2 -
      (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy).2 =
    (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w, x)) dy).2 +
      -(semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy).2
case h.h.h.h.a
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 g : W → X → Y
hf : HasAdjDiff K fun x => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w : W
x : X
dy : Y
dw : W
⊢ (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy).2 +
      (0 - (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy).2) =
    (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w, x)) dy).2 +
      -(semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy).2