simp at hf hg
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 → K
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => f w x
hg :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => g w x
⊢ (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 dz dw =>
      let dwx := adf.2 ((starRingEnd K) bdg.1 * dz) dw;
      let dwx := bdg.2 ((starRingEnd K) adf.1 * dz) 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 → K
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 dz dw =>
      let dwx := adf.2 ((starRingEnd K) bdg.1 * dz) dw;
      let dwx := bdg.2 ((starRingEnd K) adf.1 * dz) dwx;
      dwx.1)