unfold revDeriv2
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
⊢ (revDeriv2 K fun w x => f w x + g w x) = fun w x =>
    let adf := revDeriv2 K f w x;
    let bdg := revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ();
    (adf.1 + bdg.1, fun dy dw =>
      let dwx := adf.2 dy dw;
      let dwx := bdg.2 dy dwx;
      dwx.1)
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
⊢ (fun w x =>
      ((fun w x => f w x + g w x) w x, fun dy =>
        match (motive := W × X → W → W × X)
          semiAdjoint K
            (cderiv K
              (fun x =>
                match x with
                | (w, x) => (fun w x => f w x + g w x) w x)
              (w, x))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx))) =
    fun w x =>
    let adf :=
      (f w x, fun dy =>
        match (motive := W × X → W → W × X)
          semiAdjoint K
            (cderiv K
              (fun x =>
                match x with
                | (w, x) => f w x)
              (w, x))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx));
    let bdg :=
      ((fun wx x => g wx.1 wx.2) (w, x) (), fun dy =>
        match (motive := (W × X) × Unit → W × X → (W × X) × Unit)
          semiAdjoint K
            (cderiv K
              (fun x =>
                match x with
                | (w, x) => (fun wx x => g wx.1 wx.2) w x)
              ((w, x), ()))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx));
    (adf.1 + bdg.1, fun dy dw =>
      let dwx := adf.2 dy dw;
      let dwx := bdg.2 dy dwx;
      dwx.1)