funext w x
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
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
⊢ (fun w x =>
      ((g w x, f w x), fun dy dw' =>
        (dw' +
            ((semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy.1).1 +
              (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy.2).1),
          (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy.1).2 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy.2).2))) =
    fun w x =>
    ((g w x, f w x), fun dyz dw =>
      (dw + (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) dyz.1).1,
          (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) dyz.1).2) +
        (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) dyz.2).1)
case h.h
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
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
w : W
x : X
⊢ ((g w x, f w x), fun dy dw' =>
      (dw' +
          ((semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy.1).1 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy.2).1),
        (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy.1).2 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy.2).2)) =
    ((g w x, f w x), fun dyz dw =>
      (dw + (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) dyz.1).1,
          (semiAdjoint K (cderiv K (fun x => g x.1 x.2) (w, x)) dyz.1).2) +
        (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((w, x), ())) dyz.2).1)