Theorem: SciLean.revDeriv2.let_rule (SciLean/Core/FunctionTransformations/RevDeriv2.lean)

State before:
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)
Tactic:
simp at hf hg
State after:
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)

State before:
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)
Tactic:
unfold revDeriv2
State after:
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
⊢ (fun w x =>
      ((fun w x =>
            let y := g w x;
            f w x y)
          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 =>
                      let y := g w x;
                      f w x y)
                    w x)
              (w, x))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx))) =
    fun w x =>
    let ydg :=
      ((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));
    let zdf :=
      ((fun w xy => f w xy.1 xy.2) w (x, ydg.1), fun dy =>
        match (motive := W × X × Y → W → W × X × Y)
          semiAdjoint K
            (cderiv K
              (fun x =>
                match x with
                | (w, x) => (fun w xy => f w xy.1 xy.2) w x)
              (w, x, ydg.1))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx));
    (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)

State before:
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
⊢ (fun w x =>
      ((fun w x =>
            let y := g w x;
            f w x y)
          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 =>
                      let y := g w x;
                      f w x y)
                    w x)
              (w, x))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx))) =
    fun w x =>
    let ydg :=
      ((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));
    let zdf :=
      ((fun w xy => f w xy.1 xy.2) w (x, ydg.1), fun dy =>
        match (motive := W × X × Y → W → W × X × Y)
          semiAdjoint K
            (cderiv K
              (fun x =>
                match x with
                | (w, x) => (fun w xy => f w xy.1 xy.2) w x)
              (w, x, ydg.1))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx));
    (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)
Tactic:
funext x y
State after:
case h.h
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
x : W
y : X
⊢ ((fun w x =>
          let y := g w x;
          f w x y)
        x y,
      fun dy =>
      match (motive := W × X → W → W × X)
        semiAdjoint K
          (cderiv K
            (fun x =>
              match x with
              | (w, x) =>
                (fun w x =>
                    let y := g w x;
                    f w x y)
                  w x)
            (x, y))
          dy with
      | (dw, dx) => fun dw' => (dw' + dw, dx)) =
    let ydg :=
      ((fun wx x => g wx.1 wx.2) (x, y) (), 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)
              ((x, y), ()))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx));
    let zdf :=
      ((fun w xy => f w xy.1 xy.2) x (y, ydg.1), fun dy =>
        match (motive := W × X × Y → W → W × X × Y)
          semiAdjoint K
            (cderiv K
              (fun x =>
                match x with
                | (w, x) => (fun w xy => f w xy.1 xy.2) w x)
              (x, y, ydg.1))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx));
    (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)

State before:
case h.h
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
x : W
y : X
⊢ ((fun w x =>
          let y := g w x;
          f w x y)
        x y,
      fun dy =>
      match (motive := W × X → W → W × X)
        semiAdjoint K
          (cderiv K
            (fun x =>
              match x with
              | (w, x) =>
                (fun w x =>
                    let y := g w x;
                    f w x y)
                  w x)
            (x, y))
          dy with
      | (dw, dx) => fun dw' => (dw' + dw, dx)) =
    let ydg :=
      ((fun wx x => g wx.1 wx.2) (x, y) (), 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)
              ((x, y), ()))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx));
    let zdf :=
      ((fun w xy => f w xy.1 xy.2) x (y, ydg.1), fun dy =>
        match (motive := W × X × Y → W → W × X × Y)
          semiAdjoint K
            (cderiv K
              (fun x =>
                match x with
                | (w, x) => (fun w xy => f w xy.1 xy.2) w x)
              (x, y, ydg.1))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx));
    (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)
Tactic:
simp (config:={zeta:=false})
State after:
case h.h
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
x : W
y : X
⊢ (let y_1 := g x y;
      f x y y_1,
      fun dy dw' =>
      (dw' +
          (semiAdjoint K
              (cderiv K
                (fun x =>
                  let y := g x.1 x.2;
                  f x.1 x.2 y)
                (x, y))
              dy).1,
        (semiAdjoint K
            (cderiv K
              (fun x =>
                let y := g x.1 x.2;
                f x.1 x.2 y)
              (x, y))
            dy).2)) =
    let ydg :=
      (g x y, fun dy dw' =>
        (dw' + (semiAdjoint K (cderiv K (fun x => g x.1.1 x.1.2) ((x, y), ())) dy).1,
          (semiAdjoint K (cderiv K (fun x => g x.1.1 x.1.2) ((x, y), ())) dy).2));
    let zdf :=
      (f x y ydg.1, fun dy dw' =>
        (dw' + (semiAdjoint K (cderiv K (fun x => f x.1 x.2.1 x.2.2) (x, y, ydg.1)) dy).1,
          (semiAdjoint K (cderiv K (fun x => f x.1 x.2.1 x.2.2) (x, y, ydg.1)) dy).2));
    (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)

State before:
case h.h
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
x : W
y : X
⊢ (let y_1 := g x y;
      f x y y_1,
      fun dy dw' =>
      (dw' +
          (semiAdjoint K
              (cderiv K
                (fun x =>
                  let y := g x.1 x.2;
                  f x.1 x.2 y)
                (x, y))
              dy).1,
        (semiAdjoint K
            (cderiv K
              (fun x =>
                let y := g x.1 x.2;
                f x.1 x.2 y)
              (x, y))
            dy).2)) =
    let ydg :=
      (g x y, fun dy dw' =>
        (dw' + (semiAdjoint K (cderiv K (fun x => g x.1.1 x.1.2) ((x, y), ())) dy).1,
          (semiAdjoint K (cderiv K (fun x => g x.1.1 x.1.2) ((x, y), ())) dy).2));
    let zdf :=
      (f x y ydg.1, fun dy dw' =>
        (dw' + (semiAdjoint K (cderiv K (fun x => f x.1 x.2.1 x.2.2) (x, y, ydg.1)) dy).1,
          (semiAdjoint K (cderiv K (fun x => f x.1 x.2.1 x.2.2) (x, y, ydg.1)) dy).2));
    (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)
Tactic:
conv => lhs; fun_trans
State after:
case h.h
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
x : W
y : X
⊢ (f x y (g x y), fun dy dw' =>
      (dw' +
          ((semiAdjoint K
                (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
                dy).1 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (x, y) x_1)
                (semiAdjoint K
                      (fun dx8 =>
                        cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
                      dy).2.2).1),
        (semiAdjoint K
                (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
                dy).2.1 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (x, y) x_1)
              (semiAdjoint K
                    (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
                    dy).2.2).2)) =
    let ydg :=
      (g x y, fun dy dw' =>
        (dw' + (semiAdjoint K (cderiv K (fun x => g x.1.1 x.1.2) ((x, y), ())) dy).1,
          (semiAdjoint K (cderiv K (fun x => g x.1.1 x.1.2) ((x, y), ())) dy).2));
    let zdf :=
      (f x y ydg.1, fun dy dw' =>
        (dw' + (semiAdjoint K (cderiv K (fun x => f x.1 x.2.1 x.2.2) (x, y, ydg.1)) dy).1,
          (semiAdjoint K (cderiv K (fun x => f x.1 x.2.1 x.2.2) (x, y, ydg.1)) dy).2));
    (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)

State before:
case h.h
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
x : W
y : X
⊢ (f x y (g x y), fun dy dw' =>
      (dw' +
          ((semiAdjoint K
                (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
                dy).1 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (x, y) x_1)
                (semiAdjoint K
                      (fun dx8 =>
                        cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
                      dy).2.2).1),
        (semiAdjoint K
                (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
                dy).2.1 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (x, y) x_1)
              (semiAdjoint K
                    (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
                    dy).2.2).2)) =
    let ydg :=
      (g x y, fun dy dw' =>
        (dw' + (semiAdjoint K (cderiv K (fun x => g x.1.1 x.1.2) ((x, y), ())) dy).1,
          (semiAdjoint K (cderiv K (fun x => g x.1.1 x.1.2) ((x, y), ())) dy).2));
    let zdf :=
      (f x y ydg.1, fun dy dw' =>
        (dw' + (semiAdjoint K (cderiv K (fun x => f x.1 x.2.1 x.2.2) (x, y, ydg.1)) dy).1,
          (semiAdjoint K (cderiv K (fun x => f x.1 x.2.1 x.2.2) (x, y, ydg.1)) dy).2));
    (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)
Tactic:
simp
State after:
case h.h
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
x : W
y : X
⊢ (fun dy dw' =>
      (dw' +
          ((semiAdjoint K
                (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
                dy).1 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (x, y) x_1)
                (semiAdjoint K
                      (fun dx8 =>
                        cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
                      dy).2.2).1),
        (semiAdjoint K
                (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
                dy).2.1 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (x, y) x_1)
              (semiAdjoint K
                    (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
                    dy).2.2).2)) =
    fun dz dx =>
    (dx + (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y)) dz).1,
        (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y)) dz).2.1) +
      (semiAdjoint K (cderiv K (fun x => g x.1.1 x.1.2) ((x, y), ()))
          (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y))
                dz).2.2).1

State before:
case h.h
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
x : W
y : X
⊢ (fun dy dw' =>
      (dw' +
          ((semiAdjoint K
                (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
                dy).1 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (x, y) x_1)
                (semiAdjoint K
                      (fun dx8 =>
                        cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
                      dy).2.2).1),
        (semiAdjoint K
                (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
                dy).2.1 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (x, y) x_1)
              (semiAdjoint K
                    (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
                    dy).2.2).2)) =
    fun dz dx =>
    (dx + (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y)) dz).1,
        (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y)) dz).2.1) +
      (semiAdjoint K (cderiv K (fun x => g x.1.1 x.1.2) ((x, y), ()))
          (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y))
                dz).2.2).1
Tactic:
funext dy dw'
State after:
case h.h.h.h
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
x : W
y : X
dy : Z
dw' : W
⊢ (dw' +
        ((semiAdjoint K
              (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
              dy).1 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (x, y) x_1)
              (semiAdjoint K
                    (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
                    dy).2.2).1),
      (semiAdjoint K
              (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
              dy).2.1 +
        (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (x, y) x_1)
            (semiAdjoint K
                  (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
                  dy).2.2).2) =
    (dw' + (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y)) dy).1,
        (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y)) dy).2.1) +
      (semiAdjoint K (cderiv K (fun x => g x.1.1 x.1.2) ((x, y), ()))
          (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y))
                dy).2.2).1

State before:
case h.h.h.h
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
x : W
y : X
dy : Z
dw' : W
⊢ (dw' +
        ((semiAdjoint K
              (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
              dy).1 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (x, y) x_1)
              (semiAdjoint K
                    (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
                    dy).2.2).1),
      (semiAdjoint K
              (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
              dy).2.1 +
        (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (x, y) x_1)
            (semiAdjoint K
                  (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
                  dy).2.2).2) =
    (dw' + (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y)) dy).1,
        (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y)) dy).2.1) +
      (semiAdjoint K (cderiv K (fun x => g x.1.1 x.1.2) ((x, y), ()))
          (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y))
                dy).2.2).1
Tactic:
sorry_proof
State after:
no goals