internlm/Lean-Github huggingface dataset:
Theorem: SciLean.revDerivUpdate.const_rule
Proof state before:
K : Type u_3
I : Type ?u.78072
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.78102
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.78113
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.78124
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.78149
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.78174
EI : I → Type ?u.78179
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.78313
J : Type ?u.78316
FJ : J → Type ?u.78321
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
y : Y
⊢ (fun x =>
      let ydf := revDeriv K (fun x => y) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    fun x => (y, fun x dx => dx)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.revDerivUpdate.comp_rule
Proof state before:
K : Type u_1
I : Type ?u.80857
inst✝²⁴ : RCLike K
X : Type u_4
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type u_3
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.80898
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.80909
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.80934
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.80959
EI : I → Type ?u.80964
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.81098
J : Type ?u.81101
FJ : J → Type ?u.81106
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : Y → Z
g : X → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (revDerivUpdate K fun x => f (g x)) = fun x =>
    let ydg := revDerivUpdate K g x;
    let zdf := revDeriv K f ydg.1;
    (zdf.1, fun dz dx =>
      let dy := zdf.2 dz;
      ydg.2 dy dx)
Tactic:
unfold revDerivUpdate
Proof state after:
K : Type u_1
I : Type ?u.80857
inst✝²⁴ : RCLike K
X : Type u_4
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type u_3
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.80898
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.80909
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.80934
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.80959
EI : I → Type ?u.80964
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.81098
J : Type ?u.81101
FJ : J → Type ?u.81106
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : Y → Z
g : X → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (fun x =>
      let ydf := revDeriv K (fun x => f (g x)) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    fun x =>
    let ydg :=
      let ydf := revDeriv K g x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    let zdf := revDeriv K f ydg.1;
    (zdf.1, fun dz dx =>
      let dy := zdf.2 dz;
      ydg.2 dy dx)
Theorem: SciLean.revDerivUpdate.comp_rule
Proof state before:
K : Type u_1
I : Type ?u.80857
inst✝²⁴ : RCLike K
X : Type u_4
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type u_3
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.80898
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.80909
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.80934
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.80959
EI : I → Type ?u.80964
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.81098
J : Type ?u.81101
FJ : J → Type ?u.81106
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : Y → Z
g : X → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (fun x =>
      let ydf := revDeriv K (fun x => f (g x)) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    fun x =>
    let ydg :=
      let ydf := revDeriv K g x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    let zdf := revDeriv K f ydg.1;
    (zdf.1, fun dz dx =>
      let dy := zdf.2 dz;
      ydg.2 dy dx)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.revDerivUpdate.let_rule
Proof state before:
K : Type u_1
I : Type ?u.86406
inst✝²⁴ : RCLike K
X : Type u_2
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_3
inst✝²² : SemiInnerProductSpace K Y
Z : Type u_4
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.86447
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.86458
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.86483
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.86508
EI : I → Type ?u.86513
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.86647
J : Type ?u.86650
FJ : J → Type ?u.86655
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → Y → Z
g : X → Y
hf : HasAdjDiff K fun xy => f xy.1 xy.2
hg : HasAdjDiff K g
⊢ (revDerivUpdate K fun x =>
      let y := g x;
      f x y) =
    fun x =>
    let ydg := revDerivUpdate K g x;
    let zdf := revDerivUpdate K (fun xy => f xy.1 xy.2) (x, ydg.1);
    (zdf.1, fun dz dx =>
      let dxdy := zdf.2 dz (dx, 0);
      let dx := ydg.2 dxdy.2 dxdy.1;
      dx)
Tactic:
unfold revDerivUpdate
Proof state after:
K : Type u_1
I : Type ?u.86406
inst✝²⁴ : RCLike K
X : Type u_2
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_3
inst✝²² : SemiInnerProductSpace K Y
Z : Type u_4
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.86447
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.86458
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.86483
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.86508
EI : I → Type ?u.86513
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.86647
J : Type ?u.86650
FJ : J → Type ?u.86655
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → Y → Z
g : X → Y
hf : HasAdjDiff K fun xy => f xy.1 xy.2
hg : HasAdjDiff K g
⊢ (fun x =>
      let ydf :=
        revDeriv K
          (fun x =>
            let y := g x;
            f x y)
          x;
      (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    fun x =>
    let ydg :=
      let ydf := revDeriv K g x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    let zdf :=
      let ydf := revDeriv K (fun xy => f xy.1 xy.2) (x, ydg.1);
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    (zdf.1, fun dz dx =>
      let dxdy := zdf.2 dz (dx, 0);
      let dx := ydg.2 dxdy.2 dxdy.1;
      dx)
Theorem: SciLean.revDerivUpdate.let_rule
Proof state before:
K : Type u_1
I : Type ?u.86406
inst✝²⁴ : RCLike K
X : Type u_2
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_3
inst✝²² : SemiInnerProductSpace K Y
Z : Type u_4
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.86447
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.86458
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.86483
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.86508
EI : I → Type ?u.86513
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.86647
J : Type ?u.86650
FJ : J → Type ?u.86655
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → Y → Z
g : X → Y
hf : HasAdjDiff K fun xy => f xy.1 xy.2
hg : HasAdjDiff K g
⊢ (fun x =>
      let ydf :=
        revDeriv K
          (fun x =>
            let y := g x;
            f x y)
          x;
      (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    fun x =>
    let ydg :=
      let ydf := revDeriv K g x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    let zdf :=
      let ydf := revDeriv K (fun xy => f xy.1 xy.2) (x, ydg.1);
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    (zdf.1, fun dz dx =>
      let dxdy := zdf.2 dz (dx, 0);
      let dx := ydg.2 dxdy.2 dxdy.1;
      dx)
Tactic:
fun_trans [revDerivUpdate,add_assoc]
Proof state after:
no goals
Theorem: SciLean.revDerivUpdate.apply_rule
Proof state before:
K : Type u_3
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.95615
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.95628
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.95639
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.95650
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.95661
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.95686
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.95711
EI : I → Type u_2
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.95850
J : Type ?u.95853
FJ : J → Type ?u.95858
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
i : I
⊢ (revDerivUpdate K fun x => x i) = fun x => (x i, fun dxi dx => structModify i (fun dxi' => dxi' + dxi) dx)
Tactic:
unfold revDerivUpdate
Proof state after:
K : Type u_3
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.95615
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.95628
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.95639
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.95650
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.95661
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.95686
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.95711
EI : I → Type u_2
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.95850
J : Type ?u.95853
FJ : J → Type ?u.95858
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
i : I
⊢ (fun x =>
      let ydf := revDeriv K (fun x => x i) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    fun x => (x i, fun dxi dx => structModify i (fun dxi' => dxi' + dxi) dx)
Theorem: SciLean.revDerivUpdate.apply_rule
Proof state before:
K : Type u_3
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.95615
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.95628
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.95639
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.95650
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.95661
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.95686
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.95711
EI : I → Type u_2
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.95850
J : Type ?u.95853
FJ : J → Type ?u.95858
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
i : I
⊢ (fun x =>
      let ydf := revDeriv K (fun x => x i) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    fun x => (x i, fun dxi dx => structModify i (fun dxi' => dxi' + dxi) dx)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.revDerivUpdate.pi_rule
Proof state before:
K : Type u_1
I : Type u_3
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.101641
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.101652
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.101663
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.101674
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.101699
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.101724
EI : I → Type u_2
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.101863
J : Type ?u.101866
FJ : J → Type ?u.101871
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun x => f x i
⊢ (revDerivUpdate K fun x i => f x i) = fun x =>
    let xdf := fun i => revDerivUpdate K (fun x => f x i) x;
    (fun i => (xdf i).1, fun dy dx => fold (IndexType.univ I) (fun dx i => (xdf i).2 (dy i) dx) dx)
Tactic:
unfold revDerivUpdate
Proof state after:
K : Type u_1
I : Type u_3
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.101641
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.101652
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.101663
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.101674
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.101699
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.101724
EI : I → Type u_2
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.101863
J : Type ?u.101866
FJ : J → Type ?u.101871
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun x => f x i
⊢ (fun x =>
      let ydf := revDeriv K (fun x i => f x i) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    fun x =>
    let xdf := fun i =>
      let ydf := revDeriv K (fun x => f x i) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    (fun i => (xdf i).1, fun dy dx => fold (IndexType.univ I) (fun dx i => (xdf i).2 (dy i) dx) dx)
Theorem: SciLean.revDerivUpdate.pi_rule
Proof state before:
K : Type u_1
I : Type u_3
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.101641
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.101652
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.101663
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.101674
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.101699
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.101724
EI : I → Type u_2
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.101863
J : Type ?u.101866
FJ : J → Type ?u.101871
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun x => f x i
⊢ (fun x =>
      let ydf := revDeriv K (fun x i => f x i) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    fun x =>
    let xdf := fun i =>
      let ydf := revDeriv K (fun x => f x i) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    (fun i => (xdf i).1, fun dy dx => fold (IndexType.univ I) (fun dx i => (xdf i).2 (dy i) dx) dx)
Tactic:
funext x
Proof state after:
case h
K : Type u_1
I : Type u_3
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.101641
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.101652
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.101663
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.101674
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.101699
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.101724
EI : I → Type u_2
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.101863
J : Type ?u.101866
FJ : J → Type ?u.101871
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun x => f x i
x : X
⊢ (let ydf := revDeriv K (fun x i => f x i) x;
    (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    let xdf := fun i =>
      let ydf := revDeriv K (fun x => f x i) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    (fun i => (xdf i).1, fun dy dx => fold (IndexType.univ I) (fun dx i => (xdf i).2 (dy i) dx) dx)
Theorem: SciLean.revDerivUpdate.pi_rule
Proof state before:
case h
K : Type u_1
I : Type u_3
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.101641
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.101652
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.101663
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.101674
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.101699
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.101724
EI : I → Type u_2
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.101863
J : Type ?u.101866
FJ : J → Type ?u.101871
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun x => f x i
x : X
⊢ (let ydf := revDeriv K (fun x i => f x i) x;
    (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    let xdf := fun i =>
      let ydf := revDeriv K (fun x => f x i) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    (fun i => (xdf i).1, fun dy dx => fold (IndexType.univ I) (fun dx i => (xdf i).2 (dy i) dx) dx)
Tactic:
rw[revDeriv.pi_rule (hf:=by fun_prop)]
Proof state after:
case h
K : Type u_1
I : Type u_3
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.101641
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.101652
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.101663
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.101674
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.101699
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.101724
EI : I → Type u_2
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.101863
J : Type ?u.101866
FJ : J → Type ?u.101871
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun x => f x i
x : X
⊢ (let ydf :=
      (fun x =>
          let xdf := fun i => revDerivUpdate K (fun x => f x i) x;
          (fun i => (xdf i).1, fun dy => fold (IndexType.univ I) (fun dx i => (xdf i).2 (dy i) dx) 0))
        x;
    (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    let xdf := fun i =>
      let ydf := revDeriv K (fun x => f x i) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    (fun i => (xdf i).1, fun dy dx => fold (IndexType.univ I) (fun dx i => (xdf i).2 (dy i) dx) dx)