Theorem: IndexType.sum.arg_f.revDerivProj_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 ι✝
ι : Type
inst✝² : IndexType ι
inst✝¹ : LawfulIndexType ι
inst✝ : DecidableEq ι
f : X → ι → Y'
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
⊢ (revDerivProj K Yi fun x =>  ∑ i, f x i) = fun x =>
    let ydf := revDerivProjUpdate K (ι × Yi) f x;
    ( ∑ i, ydf.1 i, fun j dy => fold (IndexType.univ ι) (fun dx i => ydf.2 (i, j) dy dx) 0)
Tactic:
unfold revDerivProj
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 ι✝
ι : Type
inst✝² : IndexType ι
inst✝¹ : LawfulIndexType ι
inst✝ : DecidableEq ι
f : X → ι → Y'
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
⊢ (fun x =>
      let ydf' := revDeriv K (fun x =>  ∑ i, f x i) x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun x =>
    let ydf := revDerivProjUpdate K (ι × Yi) f x;
    ( ∑ i, ydf.1 i, fun j dy => fold (IndexType.univ ι) (fun dx i => ydf.2 (i, j) dy dx) 0)

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 ι✝
ι : Type
inst✝² : IndexType ι
inst✝¹ : LawfulIndexType ι
inst✝ : DecidableEq ι
f : X → ι → Y'
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
⊢ (fun x =>
      let ydf' := revDeriv K (fun x =>  ∑ i, f x i) x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun x =>
    let ydf := revDerivProjUpdate K (ι × Yi) f x;
    ( ∑ i, ydf.1 i, fun j dy => fold (IndexType.univ ι) (fun dx i => ydf.2 (i, j) dy dx) 0)
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 ι✝
ι : Type
inst✝² : IndexType ι
inst✝¹ : LawfulIndexType ι
inst✝ : DecidableEq ι
f : X → ι → Y'
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
⊢ (fun x => ( ∑ i, f x i, fun i de => (revDeriv K (fun x i => f x i) x).2 fun x => oneHot i de)) = fun x =>
    ( ∑ i, f x i, fun j dy =>
      fold (IndexType.univ ι) (fun dx i => (revDerivProjUpdate K (ι × Yi) f x).2 (i, j) dy dx) 0)

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 ι✝
ι : Type
inst✝² : IndexType ι
inst✝¹ : LawfulIndexType ι
inst✝ : DecidableEq ι
f : X → ι → Y'
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
⊢ (fun x => ( ∑ i, f x i, fun i de => (revDeriv K (fun x i => f x i) x).2 fun x => oneHot i de)) = fun x =>
    ( ∑ i, f x i, fun j dy =>
      fold (IndexType.univ ι) (fun dx i => (revDerivProjUpdate K (ι × Yi) f x).2 (i, j) dy dx) 0)
Tactic:
sorry_proof
State after:
no goals