Theorem: HMul.hMul.arg_a0a1.revDeriv2Proj_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 g : W → X → K
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => f w x
hg :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => g w x
⊢ (revDeriv2Proj K Unit fun w x => f w x * g w x) = fun w x x_1 =>
    let adf := revDeriv2 K f w x;
    let bdg := revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ();
    (adf.1 * bdg.1, fun dz dw =>
      let dwx := adf.2 ((starRingEnd K) bdg.1 * dz) dw;
      let dwx := bdg.2 ((starRingEnd K) adf.1 * dz) dwx;
      dwx.1)
Tactic:
unfold revDeriv2Proj
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 g : W → X → K
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => f w x
hg :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => g w x
⊢ (fun w x i =>
      let ydf := revDeriv2 K (fun w x => f w x * g w x) w x;
      (structProj ydf.1 i, fun dyi => ydf.2 (oneHot i dyi))) =
    fun w x x_1 =>
    let adf := revDeriv2 K f w x;
    let bdg := revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ();
    (adf.1 * bdg.1, fun dz dw =>
      let dwx := adf.2 ((starRingEnd K) bdg.1 * dz) dw;
      let dwx := bdg.2 ((starRingEnd K) adf.1 * dz) dwx;
      dwx.1)

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 g : W → X → K
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => f w x
hg :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => g w x
⊢ (fun w x i =>
      let ydf := revDeriv2 K (fun w x => f w x * g w x) w x;
      (structProj ydf.1 i, fun dyi => ydf.2 (oneHot i dyi))) =
    fun w x x_1 =>
    let adf := revDeriv2 K f w x;
    let bdg := revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ();
    (adf.1 * bdg.1, fun dz dw =>
      let dwx := adf.2 ((starRingEnd K) bdg.1 * dz) dw;
      let dwx := bdg.2 ((starRingEnd K) adf.1 * dz) dwx;
      dwx.1)
Tactic:
simp only [HMul.hMul.arg_a0a1.revDeriv2_rule _ _ hf hg]
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 g : W → X → K
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => f w x
hg :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => g w x
⊢ (fun w x i =>
      (structProj ((revDeriv2 K f w x).1 * (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1) i, fun dyi dw =>
        ((revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).2 ((starRingEnd K) (revDeriv2 K f w x).1 * oneHot i dyi)
            ((revDeriv2 K f w x).2 ((starRingEnd K) (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1 * oneHot i dyi)
              dw)).1)) =
    fun w x x_1 =>
    ((revDeriv2 K f w x).1 * (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1, fun dz dw =>
      ((revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).2 ((starRingEnd K) (revDeriv2 K f w x).1 * dz)
          ((revDeriv2 K f w x).2 ((starRingEnd K) (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1 * dz) dw)).1)

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 g : W → X → K
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => f w x
hg :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => g w x
⊢ (fun w x i =>
      (structProj ((revDeriv2 K f w x).1 * (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1) i, fun dyi dw =>
        ((revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).2 ((starRingEnd K) (revDeriv2 K f w x).1 * oneHot i dyi)
            ((revDeriv2 K f w x).2 ((starRingEnd K) (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1 * oneHot i dyi)
              dw)).1)) =
    fun w x x_1 =>
    ((revDeriv2 K f w x).1 * (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1, fun dz dw =>
      ((revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).2 ((starRingEnd K) (revDeriv2 K f w x).1 * dz)
          ((revDeriv2 K f w x).2 ((starRingEnd K) (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1 * dz) dw)).1)
Tactic:
funext w x i
State after:
case h.h.h
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 g : W → X → K
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => f w x
hg :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => g w x
w : W
x : X
i : Unit
⊢ (structProj ((revDeriv2 K f w x).1 * (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1) i, fun dyi dw =>
      ((revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).2 ((starRingEnd K) (revDeriv2 K f w x).1 * oneHot i dyi)
          ((revDeriv2 K f w x).2 ((starRingEnd K) (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1 * oneHot i dyi)
            dw)).1) =
    ((revDeriv2 K f w x).1 * (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1, fun dz dw =>
      ((revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).2 ((starRingEnd K) (revDeriv2 K f w x).1 * dz)
          ((revDeriv2 K f w x).2 ((starRingEnd K) (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1 * dz) dw)).1)

State before:
case h.h.h
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 g : W → X → K
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => f w x
hg :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => g w x
w : W
x : X
i : Unit
⊢ (structProj ((revDeriv2 K f w x).1 * (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1) i, fun dyi dw =>
      ((revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).2 ((starRingEnd K) (revDeriv2 K f w x).1 * oneHot i dyi)
          ((revDeriv2 K f w x).2 ((starRingEnd K) (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1 * oneHot i dyi)
            dw)).1) =
    ((revDeriv2 K f w x).1 * (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1, fun dz dw =>
      ((revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).2 ((starRingEnd K) (revDeriv2 K f w x).1 * dz)
          ((revDeriv2 K f w x).2 ((starRingEnd K) (revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ()).1 * dz) dw)).1)
Tactic:
simp[revDeriv2, oneHot]
State after:
no goals