Theorem: HMul.hMul.arg_a0a1.revDeriv2_rule
Proof 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
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