internlm/Lean-Github huggingface dataset:
Theorem: HMul.hMul.arg_a0a1.revDerivUpdate_rule
Proof 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
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (fun x => (f x * g x, fun dy dx => dx + (revDeriv K (fun x => f x * g x) x).2 dy)) = fun x =>
    (f x * g x, fun dx' dx =>
      dx + (revDeriv K g x).2 ((starRingEnd K) (f x) * dx') + (revDeriv K f x).2 ((starRingEnd K) (g x) * dx'))
Tactic:
fun_trans
Proof 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
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (fun x =>
      (f x * g x, fun dy dx =>
        dx +
          (revDerivUpdate K (fun x => f x) x).2 ((starRingEnd K) (g x) * dy)
            ((revDeriv K (fun x => g x) x).2 ((starRingEnd K) (f x) * dy)))) =
    fun x =>
    (f x * g x, fun dx' dx =>
      dx + (revDeriv K g x).2 ((starRingEnd K) (f x) * dx') + (revDeriv K f x).2 ((starRingEnd K) (g x) * dx'))
Theorem: HMul.hMul.arg_a0a1.revDerivUpdate_rule
Proof 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
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (fun x =>
      (f x * g x, fun dy dx =>
        dx +
          (revDerivUpdate K (fun x => f x) x).2 ((starRingEnd K) (g x) * dy)
            ((revDeriv K (fun x => g x) x).2 ((starRingEnd K) (f x) * dy)))) =
    fun x =>
    (f x * g x, fun dx' dx =>
      dx + (revDeriv K g x).2 ((starRingEnd K) (f x) * dx') + (revDeriv K f x).2 ((starRingEnd K) (g x) * dx'))
Tactic:
simp [smul_push,add_assoc,revDerivUpdate]
Proof state after:
no goals
Theorem: HMul.hMul.arg_a0a1.revDerivProj_rule
Proof 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
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (revDerivProj K Unit fun x => f x * g x) = fun x =>
    let ydf := revDerivUpdate K f x;
    let zdg := revDeriv K g x;
    (ydf.1 * zdg.1, fun x dy =>
      let dy₁ := (starRingEnd K) zdg.1 * dy;
      let dy₂ := (starRingEnd K) ydf.1 * dy;
      let dx := zdg.2 dy₂;
      ydf.2 dy₁ dx)
Tactic:
unfold revDerivProj
Proof 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
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (fun x =>
      let ydf' := revDeriv K (fun x => f x * g x) x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun x =>
    let ydf := revDerivUpdate K f x;
    let zdg := revDeriv K g x;
    (ydf.1 * zdg.1, fun x dy =>
      let dy₁ := (starRingEnd K) zdg.1 * dy;
      let dy₂ := (starRingEnd K) ydf.1 * dy;
      let dx := zdg.2 dy₂;
      ydf.2 dy₁ dx)
Theorem: HMul.hMul.arg_a0a1.revDerivProj_rule
Proof 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
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (fun x =>
      let ydf' := revDeriv K (fun x => f x * g x) x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun x =>
    let ydf := revDerivUpdate K f x;
    let zdg := revDeriv K g x;
    (ydf.1 * zdg.1, fun x dy =>
      let dy₁ := (starRingEnd K) zdg.1 * dy;
      let dy₂ := (starRingEnd K) ydf.1 * dy;
      let dx := zdg.2 dy₂;
      ydf.2 dy₁ dx)
Tactic:
fun_trans
Proof 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
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (fun x =>
      (f x * g x, fun i de =>
        (revDerivUpdate K (fun x => f x) x).2 ((starRingEnd K) (g x) * oneHot i de)
          ((revDeriv K (fun x => g x) x).2 ((starRingEnd K) (f x) * oneHot i de)))) =
    fun x =>
    (f x * g x, fun x_1 dy =>
      (revDerivUpdate K f x).2 ((starRingEnd K) (g x) * dy) ((revDeriv K g x).2 ((starRingEnd K) (f x) * dy)))
Theorem: HMul.hMul.arg_a0a1.revDerivProj_rule
Proof 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
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (fun x =>
      (f x * g x, fun i de =>
        (revDerivUpdate K (fun x => f x) x).2 ((starRingEnd K) (g x) * oneHot i de)
          ((revDeriv K (fun x => g x) x).2 ((starRingEnd K) (f x) * oneHot i de)))) =
    fun x =>
    (f x * g x, fun x_1 dy =>
      (revDerivUpdate K f x).2 ((starRingEnd K) (g x) * dy) ((revDeriv K g x).2 ((starRingEnd K) (f x) * dy)))
Tactic:
simp[oneHot, structMake]
Proof state after:
no goals
Theorem: HMul.hMul.arg_a0a1.revDerivProjUpdate_rule
Proof 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
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (revDerivProjUpdate K Unit fun x => f x * g x) = fun x =>
    let ydf := revDerivUpdate K f x;
    let zdg := revDerivUpdate K g x;
    (ydf.1 * zdg.1, fun x dy dx =>
      let dy₁ := (starRingEnd K) zdg.1 * dy;
      let dy₂ := (starRingEnd K) ydf.1 * dy;
      let dx := zdg.2 dy₂ dx;
      ydf.2 dy₁ dx)
Tactic:
unfold revDerivProjUpdate
Proof 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
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (fun x =>
      let ydf' := revDerivProj K Unit (fun x => f x * g x) x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de)) =
    fun x =>
    let ydf := revDerivUpdate K f x;
    let zdg := revDerivUpdate K g x;
    (ydf.1 * zdg.1, fun x dy dx =>
      let dy₁ := (starRingEnd K) zdg.1 * dy;
      let dy₂ := (starRingEnd K) ydf.1 * dy;
      let dx := zdg.2 dy₂ dx;
      ydf.2 dy₁ dx)
Theorem: HMul.hMul.arg_a0a1.revDerivProjUpdate_rule
Proof 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
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (fun x =>
      let ydf' := revDerivProj K Unit (fun x => f x * g x) x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de)) =
    fun x =>
    let ydf := revDerivUpdate K f x;
    let zdg := revDerivUpdate K g x;
    (ydf.1 * zdg.1, fun x dy dx =>
      let dy₁ := (starRingEnd K) zdg.1 * dy;
      let dy₂ := (starRingEnd K) ydf.1 * dy;
      let dx := zdg.2 dy₂ dx;
      ydf.2 dy₁ dx)
Tactic:
fun_trans
Proof 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
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (fun x =>
      (f x * g x, fun i de dx =>
        dx +
          (revDerivUpdate K (fun x => f x) x).2 ((starRingEnd K) (g x) * de)
            ((revDeriv K (fun x => g x) x).2 ((starRingEnd K) (f x) * de)))) =
    fun x =>
    (f x * g x, fun x_1 dy dx =>
      (revDerivUpdate K f x).2 ((starRingEnd K) (g x) * dy) ((revDerivUpdate K g x).2 ((starRingEnd K) (f x) * dy) dx))
Theorem: HMul.hMul.arg_a0a1.revDerivProjUpdate_rule
Proof 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
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (fun x =>
      (f x * g x, fun i de dx =>
        dx +
          (revDerivUpdate K (fun x => f x) x).2 ((starRingEnd K) (g x) * de)
            ((revDeriv K (fun x => g x) x).2 ((starRingEnd K) (f x) * de)))) =
    fun x =>
    (f x * g x, fun x_1 dy dx =>
      (revDerivUpdate K f x).2 ((starRingEnd K) (g x) * dy) ((revDerivUpdate K g x).2 ((starRingEnd K) (f x) * dy) dx))
Tactic:
simp[revDerivUpdate,add_assoc]
Proof state after:
no goals
Theorem: HSMul.hSMul.arg_a0a1.revDeriv_rule
Proof 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
X' Xi : Type
XI : Xi → Type
inst✝³⁰ : StructType X' Xi XI
inst✝²⁹ : IndexType Xi
inst✝²⁸ : LawfulIndexType Xi
inst✝²⁷ : DecidableEq Xi
Y' Yi✝ : Type
YI✝ : Yi✝ → Type
inst✝²⁶ : StructType Y' Yi✝ YI✝
inst✝²⁵ : IndexType Yi✝
inst✝²⁴ : LawfulIndexType Yi✝
inst✝²³ : DecidableEq Yi✝
Z' Zi : Type
ZI : Zi → Type
inst✝²² : StructType Z' Zi ZI
inst✝²¹ : IndexType Zi
inst✝²⁰ : LawfulIndexType Zi
inst✝¹⁹ : DecidableEq Zi
inst✝¹⁸ : SemiInnerProductSpace K X'
inst✝¹⁷ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹⁶ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹⁵ : SemiInnerProductSpace K Y'
inst✝¹⁴ : (i : Yi✝) → SemiInnerProductSpace K (YI✝ i)
inst✝¹³ : SemiInnerProductSpaceStruct K Y' Yi✝ YI✝
inst✝¹² : SemiInnerProductSpace K Z'
inst✝¹¹ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝¹⁰ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁹ : SemiInnerProductSpace K W
ι : Type
inst✝⁸ : IndexType ι
inst✝⁷ : LawfulIndexType ι
Y Yi : Type
YI : Yi → Type
inst✝⁶ : StructType Y Yi YI
inst✝⁵ : IndexType Yi
inst✝⁴ : LawfulIndexType Yi
inst✝³ : DecidableEq Yi
inst✝² : SemiHilbert K Y
inst✝¹ : (i : Yi) → SemiHilbert K (YI i)
inst✝ : SemiInnerProductSpaceStruct K Y Yi YI
f : X → K
g : X → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (fun x => ((fun x => f x • g x) x, semiAdjoint K (cderiv K (fun x => f x • g x) x))) = fun x =>
    let ydf :=
      let ydf := (f x, semiAdjoint K (cderiv K f x));
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    let zdg := (g x, semiAdjoint K (cderiv K g x));
    (ydf.1 • zdg.1, fun dy' =>
      let dk := ⟪zdg.1, dy'⟫_K;
      let dx := zdg.2 dy';
      let dx := (starRingEnd K) ydf.1 • dx;
      ydf.2 dk dx)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: HSMul.hSMul.arg_a0a1.revDerivUpdate_rule
Proof state before:
case h
K : Type
inst✝³⁴ : RCLike K
X : Type
inst✝³³ : SemiInnerProductSpace K X
Y✝ : Type
inst✝³² : SemiInnerProductSpace K Y✝
Z : Type
inst✝³¹ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝³⁰ : StructType X' Xi XI
inst✝²⁹ : IndexType Xi
inst✝²⁸ : LawfulIndexType Xi
inst✝²⁷ : DecidableEq Xi
Y' Yi✝ : Type
YI✝ : Yi✝ → Type
inst✝²⁶ : StructType Y' Yi✝ YI✝
inst✝²⁵ : IndexType Yi✝
inst✝²⁴ : LawfulIndexType Yi✝
inst✝²³ : DecidableEq Yi✝
Z' Zi : Type
ZI : Zi → Type
inst✝²² : StructType Z' Zi ZI
inst✝²¹ : IndexType Zi
inst✝²⁰ : LawfulIndexType Zi
inst✝¹⁹ : DecidableEq Zi
inst✝¹⁸ : SemiInnerProductSpace K X'
inst✝¹⁷ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹⁶ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹⁵ : SemiInnerProductSpace K Y'
inst✝¹⁴ : (i : Yi✝) → SemiInnerProductSpace K (YI✝ i)
inst✝¹³ : SemiInnerProductSpaceStruct K Y' Yi✝ YI✝
inst✝¹² : SemiInnerProductSpace K Z'
inst✝¹¹ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝¹⁰ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁹ : SemiInnerProductSpace K W
ι : Type
inst✝⁸ : IndexType ι
inst✝⁷ : LawfulIndexType ι
Y Yi : Type
YI : Yi → Type
inst✝⁶ : StructType Y Yi YI
inst✝⁵ : IndexType Yi
inst✝⁴ : LawfulIndexType Yi
inst✝³ : DecidableEq Yi
inst✝² : SemiHilbert K Y
inst✝¹ : (i : Yi) → SemiHilbert K (YI i)
inst✝ : SemiInnerProductSpaceStruct K Y Yi YI
f : X → K
g : X → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : X
⊢ (fun dy dx =>
      dx +
        (revDerivUpdate K (fun x => f x) x).2 (⟪g x, dy⟫_K)
          ((starRingEnd K) (f x) • (revDeriv K (fun x => g x) x).2 dy)) =
    fun dy dx => dx + (revDeriv K g x).2 ((starRingEnd K) (f x) • dy) + (revDeriv K f x).2 ⟪g x, dy⟫_K
Tactic:
simp[mul_assoc,add_assoc,revDerivUpdate,revDeriv,smul_push]
Proof state after:
no goals