Theorem: HMul.hMul.arg_a0a1.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 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
⊢ (revDeriv2 K fun w x => f w x * g w x) = fun w x =>
    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 at 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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
⊢ (revDeriv2 K fun w x => f w x * g w x) = fun w x =>
    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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
⊢ (revDeriv2 K fun w x => f w x * g w x) = fun w x =>
    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 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 g : W → X → K
hf : HasAdjDiff K fun x => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
⊢ (fun w x =>
      ((fun w x => f w x * g 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 * g w x) w x)
              (w, x))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx))) =
    fun w x =>
    let adf :=
      (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));
    let bdg :=
      ((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));
    (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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
⊢ (fun w x =>
      ((fun w x => f w x * g 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 * g w x) w x)
              (w, x))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx))) =
    fun w x =>
    let adf :=
      (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));
    let bdg :=
      ((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));
    (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:
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 g : W → X → K
hf : HasAdjDiff K fun x => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
⊢ (fun w x =>
      (f w x * g w x, fun dy dw' =>
        (dw' +
            ((starRingEnd K) (f w x) • (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy).1 +
              (starRingEnd K) (g w x) • (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy).1),
          (starRingEnd K) (f w x) • (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy).2 +
            (starRingEnd K) (g w x) • (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 * g w x, fun dz dw =>
      (dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w, x)) ((starRingEnd K) (g w x) * dz)).1,
          (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w, x)) ((starRingEnd K) (g w x) * dz)).2) +
        semiAdjoint K (fun dx8 => cderiv K (fun x => g x.1 x.2) (w, x) dx8) ((starRingEnd K) (f w x) * dz))

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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
⊢ (fun w x =>
      (f w x * g w x, fun dy dw' =>
        (dw' +
            ((starRingEnd K) (f w x) • (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy).1 +
              (starRingEnd K) (g w x) • (semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2) (w, x) x_1) dy).1),
          (starRingEnd K) (f w x) • (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1) dy).2 +
            (starRingEnd K) (g w x) • (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 * g w x, fun dz dw =>
      (dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w, x)) ((starRingEnd K) (g w x) * dz)).1,
          (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w, x)) ((starRingEnd K) (g w x) * dz)).2) +
        semiAdjoint K (fun dx8 => cderiv K (fun x => g x.1 x.2) (w, x) dx8) ((starRingEnd K) (f w x) * dz))
Tactic:
funext w w
State after:
case 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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
⊢ (f w✝ w * g w✝ w, fun dy dw' =>
      (dw' +
          ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dy).1 +
            (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dy).1),
        (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dy).2 +
          (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dy).2)) =
    (f w✝ w * g w✝ w, fun dz dw =>
      (dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) ((starRingEnd K) (g w✝ w) * dz)).1,
          (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) ((starRingEnd K) (g w✝ w) * dz)).2) +
        semiAdjoint K (fun dx8 => cderiv K (fun x => g x.1 x.2) (w✝, w) dx8) ((starRingEnd K) (f w✝ w) * dz))

State before:
case 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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
⊢ (f w✝ w * g w✝ w, fun dy dw' =>
      (dw' +
          ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dy).1 +
            (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dy).1),
        (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dy).2 +
          (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dy).2)) =
    (f w✝ w * g w✝ w, fun dz dw =>
      (dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) ((starRingEnd K) (g w✝ w) * dz)).1,
          (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) ((starRingEnd K) (g w✝ w) * dz)).2) +
        semiAdjoint K (fun dx8 => cderiv K (fun x => g x.1 x.2) (w✝, w) dx8) ((starRingEnd K) (f w✝ w) * dz))
Tactic:
simp
State after:
case 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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
⊢ (fun dy dw' =>
      (dw' +
          ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dy).1 +
            (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dy).1),
        (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dy).2 +
          (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dy).2)) =
    fun dz dw =>
    (dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) ((starRingEnd K) (g w✝ w) * dz)).1,
        (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) ((starRingEnd K) (g w✝ w) * dz)).2) +
      semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) ((starRingEnd K) (f w✝ w) * dz)

State before:
case 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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
⊢ (fun dy dw' =>
      (dw' +
          ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dy).1 +
            (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dy).1),
        (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dy).2 +
          (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dy).2)) =
    fun dz dw =>
    (dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) ((starRingEnd K) (g w✝ w) * dz)).1,
        (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) ((starRingEnd K) (g w✝ w) * dz)).2) +
      semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) ((starRingEnd K) (f w✝ w) * dz)
Tactic:
funext dx dw
State after:
case h.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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ (dw +
        ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).1 +
          (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).1),
      (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).2 +
        (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).2) =
    (dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) ((starRingEnd K) (g w✝ w) * dx)).1,
        (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) ((starRingEnd K) (g w✝ w) * dx)).2) +
      semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) ((starRingEnd K) (f w✝ w) * dx)

State before:
case h.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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ (dw +
        ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).1 +
          (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).1),
      (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).2 +
        (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).2) =
    (dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) ((starRingEnd K) (g w✝ w) * dx)).1,
        (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) ((starRingEnd K) (g w✝ w) * dx)).2) +
      semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) ((starRingEnd K) (f w✝ w) * dx)
Tactic:
simp[mul_assoc,mul_comm,smul_push,add_assoc]
State after:
case h.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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ (dw +
        ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).1 +
          (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).1),
      (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).2 +
        (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).2) =
    (dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).1,
        (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).2) +
      semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) (dx * (starRingEnd K) (f w✝ w))

State before:
case h.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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ (dw +
        ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).1 +
          (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).1),
      (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).2 +
        (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).2) =
    (dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).1,
        (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).2) +
      semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) (dx * (starRingEnd K) (f w✝ w))
Tactic:
ext
State after:
case h.h.h.h.a
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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ (dw +
          ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).1 +
            (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).1),
        (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).2 +
          (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).2).1 =
    ((dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).1,
          (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).2) +
        semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) (dx * (starRingEnd K) (f w✝ w))).1

case h.h.h.h.a
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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ (dw +
          ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).1 +
            (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).1),
        (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).2 +
          (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).2).2 =
    ((dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).1,
          (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).2) +
        semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) (dx * (starRingEnd K) (f w✝ w))).2

State before:
case h.h.h.h.a
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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ (dw +
          ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).1 +
            (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).1),
        (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).2 +
          (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).2).1 =
    ((dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).1,
          (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).2) +
        semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) (dx * (starRingEnd K) (f w✝ w))).1

case h.h.h.h.a
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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ (dw +
          ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).1 +
            (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).1),
        (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).2 +
          (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).2).2 =
    ((dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).1,
          (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).2) +
        semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) (dx * (starRingEnd K) (f w✝ w))).2
Tactic:
. simp[smul_push]; sorry_proof
State after:
case h.h.h.h.a
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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ (dw +
          ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).1 +
            (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).1),
        (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).2 +
          (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).2).2 =
    ((dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).1,
          (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).2) +
        semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) (dx * (starRingEnd K) (f w✝ w))).2

State before:
case h.h.h.h.a
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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ (dw +
          ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).1 +
            (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).1),
        (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).2 +
          (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).2).2 =
    ((dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).1,
          (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).2) +
        semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) (dx * (starRingEnd K) (f w✝ w))).2
Tactic:
. simp[smul_push]; sorry_proof
State after:
no goals

State before:
case h.h.h.h.a
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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ (dw +
          ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).1 +
            (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).1),
        (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).2 +
          (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).2).1 =
    ((dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).1,
          (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).2) +
        semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) (dx * (starRingEnd K) (f w✝ w))).1
Tactic:
simp[smul_push]
State after:
case h.h.h.h.a
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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ dw +
      ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).1 +
        (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).1) =
    dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).1 +
      (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) (dx * (starRingEnd K) (f w✝ w))).1

State before:
case h.h.h.h.a
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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ dw +
      ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).1 +
        (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).1) =
    dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).1 +
      (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) (dx * (starRingEnd K) (f w✝ w))).1
Tactic:
sorry_proof
State after:
no goals

State before:
case h.h.h.h.a
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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ (dw +
          ((starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).1 +
            (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).1),
        (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).2 +
          (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).2).2 =
    ((dw + (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).1,
          (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).2) +
        semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) (dx * (starRingEnd K) (f w✝ w))).2
Tactic:
simp[smul_push]
State after:
case h.h.h.h.a
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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).2 +
      (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).2 =
    (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).2 +
      (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) (dx * (starRingEnd K) (f w✝ w))).2

State before:
case h.h.h.h.a
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 => f x.1 x.2
hg : HasAdjDiff K fun x => g x.1 x.2
w✝ : W
w : X
dx : K
dw : W
⊢ (starRingEnd K) (f w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) dx).2 +
      (starRingEnd K) (g w✝ w) • (semiAdjoint K (fun x => cderiv K (fun x => f x.1 x.2) (w✝, w) x) dx).2 =
    (semiAdjoint K (cderiv K (fun x => f x.1 x.2) (w✝, w)) (dx * (starRingEnd K) (g w✝ w))).2 +
      (semiAdjoint K (fun x => cderiv K (fun x => g x.1 x.2) (w✝, w) x) (dx * (starRingEnd K) (f w✝ w))).2
Tactic:
sorry_proof
State after:
no goals