Theorem: Prod.snd.arg_self.revDeriv2_rule (SciLean/Core/FunctionTransformations/RevDeriv2.lean)

State before:
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 : W → X → Y × Z
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => f w x
⊢ (revDeriv2 K fun x y => (f x y).2) = fun w x =>
    let zdf := revDeriv2Proj K (Unit ⊕ Unit) f w x (Sum.inr ());
    zdf
Tactic:
unfold revDeriv2Proj revDeriv2
State after:
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 : W → X → Y × Z
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => f w x
⊢ (fun w x =>
      ((fun x y => (f x y).2) w x, fun dy =>
        match (motive := W × X → W → W × X)
          semiAdjoint K
            (cderiv K
              (fun x =>
                match x with
                | (w, x) => (fun x y => (f x y).2) w x)
              (w, x))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx))) =
    fun w x =>
    let zdf :=
      let ydf :=
        (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));
      (structProj ydf.1 (Sum.inr ()), fun dyi => ydf.2 (oneHot (Sum.inr ()) dyi));
    zdf

State before:
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 : W → X → Y × Z
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => f w x
⊢ (fun w x =>
      ((fun x y => (f x y).2) w x, fun dy =>
        match (motive := W × X → W → W × X)
          semiAdjoint K
            (cderiv K
              (fun x =>
                match x with
                | (w, x) => (fun x y => (f x y).2) w x)
              (w, x))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx))) =
    fun w x =>
    let zdf :=
      let ydf :=
        (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));
      (structProj ydf.1 (Sum.inr ()), fun dyi => ydf.2 (oneHot (Sum.inr ()) dyi));
    zdf
Tactic:
fun_trans
State after:
no goals