Theorem: Neg.neg.arg_a0.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
⊢ (revDeriv2 K fun w x => -f w x) = fun w x =>
    let ydf := revDeriv2 K f w x;
    (-ydf.1, fun dy dw =>
      let dwx := ydf.2 (-dy) dw;
      dwx)
Tactic:
unfold 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
⊢ (fun w x =>
      ((fun w x => -f w x) 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 => -f w x) w x)
              (w, x))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx))) =
    fun w x =>
    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));
    (-ydf.1, fun dy dw =>
      let dwx := ydf.2 (-dy) dw;
      dwx)

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
⊢ (fun w x =>
      ((fun w x => -f w x) 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 => -f w x) w x)
              (w, x))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx))) =
    fun w x =>
    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));
    (-ydf.1, fun dy dw =>
      let dwx := ydf.2 (-dy) dw;
      dwx)
Tactic:
simp
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
⊢ (fun w x =>
      (-f w x, fun dy dw' =>
        (dw' + (semiAdjoint K (cderiv K (fun x => -f x.1 x.2) (w, x)) dy).1,
          (semiAdjoint K (cderiv K (fun x => -f x.1 x.2) (w, x)) dy).2))) =
    fun w x =>
    (-f w x, fun dy dw =>
      (dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w, x)) (-dy)).1,
        (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w, x)) (-dy)).2))

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
⊢ (fun w x =>
      (-f w x, fun dy dw' =>
        (dw' + (semiAdjoint K (cderiv K (fun x => -f x.1 x.2) (w, x)) dy).1,
          (semiAdjoint K (cderiv K (fun x => -f x.1 x.2) (w, x)) dy).2))) =
    fun w x =>
    (-f w x, fun dy dw =>
      (dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w, x)) (-dy)).1,
        (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w, x)) (-dy)).2))
Tactic:
fun_trans
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
⊢ (fun w x =>
      (-f w x, fun dy dw' =>
        (dw' + -(semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy).1,
          -(semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy).2))) =
    fun w x =>
    (-f w x, fun dy dw =>
      (dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w, x)) (-dy)).1,
        (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w, x)) (-dy)).2))

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
⊢ (fun w x =>
      (-f w x, fun dy dw' =>
        (dw' + -(semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy).1,
          -(semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy).2))) =
    fun w x =>
    (-f w x, fun dy dw =>
      (dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w, x)) (-dy)).1,
        (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w, x)) (-dy)).2))
Tactic:
simp[neg_pull]
State after:
no goals