Theorem: SciLean.revDeriv2Proj.let_rule
Proof 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
⊢ (fun w x i =>
      let ydf :=
        ((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));
      (structProj ydf.1 i, fun dyi => ydf.2 (oneHot i dyi))) =
    fun w x i =>
    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 :=
      let ydf :=
        ((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));
      (structProj ydf.1 i, fun dyi => ydf.2 (oneHot i dyi));
    (zdf.1, fun dz dw =>
      let dwxy := zdf.2 dz dw;
      let dxy := ydg.2 dwxy.2.2 (dwxy.1, dwxy.2.1);
      dxy.1)
Tactic:
conv =>
  lhs; fun_trans
Proof 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 =>
    match x with
    | (w, x, y) => f w x y
hg :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => g w x
⊢ (fun w x i =>
      (structProj (f w x (g w x)) i, fun dyi dw' =>
        (dw' +
            ((semiAdjoint K
                  (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x) dx8)
                  (oneHot i dyi)).1 +
              (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1)
                  (semiAdjoint K
                        (fun dx8 =>
                          cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x) dx8)
                        (oneHot i dyi)).2.2).1),
          (semiAdjoint K
                  (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x) dx8)
                  (oneHot i dyi)).2.1 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1)
                (semiAdjoint K
                      (fun dx8 =>
                        cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x) dx8)
                      (oneHot i dyi)).2.2).2))) =
    fun w x i =>
    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 :=
      let ydf :=
        ((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));
      (structProj ydf.1 i, fun dyi => ydf.2 (oneHot i dyi));
    (zdf.1, fun dz dw =>
      let dwxy := zdf.2 dz dw;
      let dxy := ydg.2 dwxy.2.2 (dwxy.1, dwxy.2.1);
      dxy.1)