simp at hf hg
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
f : W → X → Y → Z
g : W → X → Y
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x, y) => f w x y
hg :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => g w x
⊢ (revDeriv2 K fun w x =>
      let y := g w x;
      f w x y) =
    fun w x =>
    let ydg := revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ();
    let zdf := revDeriv2 K (fun w xy => f w xy.1 xy.2) w (x, ydg.1);
    (zdf.1, fun dz dx =>
      let dxyz := zdf.2 dz dx;
      let dxy := ydg.2 dxyz.2.2 (dxyz.1, dxyz.2.1);
      dxy.1)
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
f : W → X → Y → Z
g : W → X → Y
hf : HasAdjDiff K fun x => f x.1 x.2.1 x.2.2
hg : HasAdjDiff K fun x => g x.1 x.2
⊢ (revDeriv2 K fun w x =>
      let y := g w x;
      f w x y) =
    fun w x =>
    let ydg := revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ();
    let zdf := revDeriv2 K (fun w xy => f w xy.1 xy.2) w (x, ydg.1);
    (zdf.1, fun dz dx =>
      let dxyz := zdf.2 dz dx;
      let dxy := ydg.2 dxyz.2.2 (dxyz.1, dxyz.2.1);
      dxy.1)