Theorem: HSub.hSub.arg_a0a1.revDerivUpdate_rule (SciLean/Core/FunctionTransformations/RevDeriv.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
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 → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (revDerivUpdate K fun x => f x - g x) = fun x =>
    let ydf := revDerivUpdate K f x;
    let ydg := revDerivUpdate K g x;
    (ydf.1 - ydg.1, fun dy dx =>
      let dx := ydf.2 dy dx;
      let dy' := -dy;
      ydg.2 dy' dx)
Tactic:
unfold revDerivUpdate
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 → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (fun x =>
      let ydf := revDeriv K (fun x => f x - g x) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    fun x =>
    let ydf :=
      let ydf := revDeriv K f x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    let ydg :=
      let ydf := revDeriv K g x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    (ydf.1 - ydg.1, fun dy dx =>
      let dx := ydf.2 dy dx;
      let dy' := -dy;
      ydg.2 dy' dx)

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 → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (fun x =>
      let ydf := revDeriv K (fun x => f x - g x) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    fun x =>
    let ydf :=
      let ydf := revDeriv K f x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    let ydg :=
      let ydf := revDeriv K g x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    (ydf.1 - ydg.1, fun dy dx =>
      let dx := ydf.2 dy dx;
      let dy' := -dy;
      ydg.2 dy' dx)
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
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 → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (fun x =>
      (f x - g x, fun dy dx => dx + (revDerivUpdate K (fun x => g x) x).2 (-dy) ((revDeriv K (fun x => f x) x).2 dy))) =
    fun x => (f x - g x, fun dy dx => dx + (revDeriv K f x).2 dy + (revDeriv K g x).2 (-dy))

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 → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (fun x =>
      (f x - g x, fun dy dx => dx + (revDerivUpdate K (fun x => g x) x).2 (-dy) ((revDeriv K (fun x => f x) x).2 dy))) =
    fun x => (f x - g x, fun dy dx => dx + (revDeriv K f x).2 dy + (revDeriv K g x).2 (-dy))
Tactic:
funext x
State after:
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 ι
f g : X → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : X
⊢ (f x - g x, fun dy dx => dx + (revDerivUpdate K (fun x => g x) x).2 (-dy) ((revDeriv K (fun x => f x) x).2 dy)) =
    (f x - g x, fun dy dx => dx + (revDeriv K f x).2 dy + (revDeriv K g x).2 (-dy))

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 ι
f g : X → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : X
⊢ (f x - g x, fun dy dx => dx + (revDerivUpdate K (fun x => g x) x).2 (-dy) ((revDeriv K (fun x => f x) x).2 dy)) =
    (f x - g x, fun dy dx => dx + (revDeriv K f x).2 dy + (revDeriv K g x).2 (-dy))
Tactic:
simp[add_assoc,revDerivUpdate]
State after:
no goals