internlm/Lean-Github huggingface dataset:
Theorem: SciLean.revDerivProjUpdate_snd_zero'
Proof state before:
K : Type u_3
I : Type ?u.24117
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.24147
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.24158
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.24169
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.24194
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.24219
EI : I → Type ?u.24224
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.24358
J : Type ?u.24361
FJ : J → Type ?u.24366
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
x : X
dy : Y
⊢ (revDerivUpdate K f x).2 dy 0 = (revDeriv K f x).2 dy
Tactic:
simp[revDerivUpdate]
Proof state after:
no goals
Theorem: SciLean.revDeriv.id_rule
Proof state before:
K : Type u_2
I : Type ?u.26448
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.26467
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.26478
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.26489
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.26500
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.26525
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.26550
EI : I → Type ?u.26555
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.26689
J : Type ?u.26692
FJ : J → Type ?u.26697
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
⊢ (revDeriv K fun x => x) = fun x => (x, fun dx => dx)
Tactic:
unfold revDeriv
Proof state after:
K : Type u_2
I : Type ?u.26448
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.26467
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.26478
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.26489
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.26500
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.26525
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.26550
EI : I → Type ?u.26555
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.26689
J : Type ?u.26692
FJ : J → Type ?u.26697
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
⊢ (fun x => ((fun x => x) x, semiAdjoint K (cderiv K (fun x => x) x))) = fun x => (x, fun dx => dx)
Theorem: SciLean.revDeriv.id_rule
Proof state before:
K : Type u_2
I : Type ?u.26448
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.26467
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.26478
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.26489
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.26500
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.26525
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.26550
EI : I → Type ?u.26555
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.26689
J : Type ?u.26692
FJ : J → Type ?u.26697
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
⊢ (fun x => ((fun x => x) x, semiAdjoint K (cderiv K (fun x => x) x))) = fun x => (x, fun dx => dx)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.revDeriv.const_rule
Proof state before:
K : Type u_3
I : Type ?u.28227
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.28257
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.28268
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.28279
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.28304
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.28329
EI : I → Type ?u.28334
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.28468
J : Type ?u.28471
FJ : J → Type ?u.28476
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
⊢ (revDeriv K fun x => y) = fun x => (y, fun x => 0)
Tactic:
unfold revDeriv
Proof state after:
K : Type u_3
I : Type ?u.28227
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.28257
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.28268
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.28279
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.28304
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.28329
EI : I → Type ?u.28334
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.28468
J : Type ?u.28471
FJ : J → Type ?u.28476
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 => ((fun x => y) x, semiAdjoint K (cderiv K (fun x => y) x))) = fun x => (y, fun x => 0)
Theorem: SciLean.revDeriv.const_rule
Proof state before:
K : Type u_3
I : Type ?u.28227
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.28257
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.28268
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.28279
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.28304
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.28329
EI : I → Type ?u.28334
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.28468
J : Type ?u.28471
FJ : J → Type ?u.28476
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 => ((fun x => y) x, semiAdjoint K (cderiv K (fun x => y) x))) = fun x => (y, fun x => 0)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.revDeriv.comp_rule
Proof state before:
K : Type u_1
I : Type ?u.30706
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.30747
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.30758
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.30783
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.30808
EI : I → Type ?u.30813
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.30947
J : Type ?u.30950
FJ : J → Type ?u.30955
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
⊢ (revDeriv K fun x => f (g x)) = fun x =>
    let ydg := revDeriv K g x;
    let zdf := revDeriv K f ydg.1;
    (zdf.1, fun dz =>
      let dy := zdf.2 dz;
      ydg.2 dy)
Tactic:
unfold revDeriv
Proof state after:
K : Type u_1
I : Type ?u.30706
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.30747
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.30758
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.30783
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.30808
EI : I → Type ?u.30813
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.30947
J : Type ?u.30950
FJ : J → Type ?u.30955
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 => ((fun x => f (g x)) x, semiAdjoint K (cderiv K (fun x => f (g x)) x))) = fun x =>
    let ydg := (g x, semiAdjoint K (cderiv K g x));
    let zdf := (f ydg.1, semiAdjoint K (cderiv K f ydg.1));
    (zdf.1, fun dz =>
      let dy := zdf.2 dz;
      ydg.2 dy)
Theorem: SciLean.revDeriv.comp_rule
Proof state before:
K : Type u_1
I : Type ?u.30706
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.30747
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.30758
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.30783
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.30808
EI : I → Type ?u.30813
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.30947
J : Type ?u.30950
FJ : J → Type ?u.30955
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 => ((fun x => f (g x)) x, semiAdjoint K (cderiv K (fun x => f (g x)) x))) = fun x =>
    let ydg := (g x, semiAdjoint K (cderiv K g x));
    let zdf := (f ydg.1, semiAdjoint K (cderiv K f ydg.1));
    (zdf.1, fun dz =>
      let dy := zdf.2 dz;
      ydg.2 dy)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.revDeriv.let_rule
Proof state before:
K : Type u_1
I : Type ?u.38964
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.39005
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.39016
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.39041
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.39066
EI : I → Type ?u.39071
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.39205
J : Type ?u.39208
FJ : J → Type ?u.39213
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
⊢ (revDeriv K fun x =>
      let y := g x;
      f x y) =
    fun x =>
    let ydg := revDerivUpdate K g x;
    let zdf := revDeriv K (fun xy => f xy.1 xy.2) (x, ydg.1);
    (zdf.1, fun dz =>
      let dxdy := zdf.2 dz;
      let dx := ydg.2 dxdy.2 dxdy.1;
      dx)
Tactic:
unfold revDerivUpdate revDeriv
Proof state after:
K : Type u_1
I : Type ?u.38964
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.39005
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.39016
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.39041
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.39066
EI : I → Type ?u.39071
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.39205
J : Type ?u.39208
FJ : J → Type ?u.39213
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 =>
      ((fun x =>
            let y := g x;
            f x y)
          x,
        semiAdjoint K
          (cderiv K
            (fun x =>
              let y := g x;
              f x y)
            x))) =
    fun x =>
    let ydg :=
      let ydf := (g x, semiAdjoint K (cderiv K g x));
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    let zdf := ((fun xy => f xy.1 xy.2) (x, ydg.1), semiAdjoint K (cderiv K (fun xy => f xy.1 xy.2) (x, ydg.1)));
    (zdf.1, fun dz =>
      let dxdy := zdf.2 dz;
      let dx := ydg.2 dxdy.2 dxdy.1;
      dx)
Theorem: SciLean.revDeriv.let_rule
Proof state before:
K : Type u_1
I : Type ?u.38964
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.39005
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.39016
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.39041
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.39066
EI : I → Type ?u.39071
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.39205
J : Type ?u.39208
FJ : J → Type ?u.39213
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 =>
      ((fun x =>
            let y := g x;
            f x y)
          x,
        semiAdjoint K
          (cderiv K
            (fun x =>
              let y := g x;
              f x y)
            x))) =
    fun x =>
    let ydg :=
      let ydf := (g x, semiAdjoint K (cderiv K g x));
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    let zdf := ((fun xy => f xy.1 xy.2) (x, ydg.1), semiAdjoint K (cderiv K (fun xy => f xy.1 xy.2) (x, ydg.1)));
    (zdf.1, fun dz =>
      let dxdy := zdf.2 dz;
      let dx := ydg.2 dxdy.2 dxdy.1;
      dx)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.revDeriv.apply_rule
Proof state before:
K : Type u_3
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.47990
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.48003
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.48014
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.48025
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.48036
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.48061
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.48086
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.48225
J : Type ?u.48228
FJ : J → Type ?u.48233
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
⊢ (revDeriv K fun x => x i) = fun x => (x i, fun dxi => oneHot i dxi)
Tactic:
unfold revDeriv
Proof state after:
K : Type u_3
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.47990
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.48003
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.48014
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.48025
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.48036
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.48061
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.48086
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.48225
J : Type ?u.48228
FJ : J → Type ?u.48233
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 => ((fun x => x i) x, semiAdjoint K (cderiv K (fun x => x i) x))) = fun x => (x i, fun dxi => oneHot i dxi)
Theorem: SciLean.revDeriv.apply_rule
Proof state before:
K : Type u_3
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.47990
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.48003
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.48014
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.48025
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.48036
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.48061
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.48086
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.48225
J : Type ?u.48228
FJ : J → Type ?u.48233
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 => ((fun x => x i) x, semiAdjoint K (cderiv K (fun x => x i) x))) = fun x => (x i, fun dxi => oneHot i dxi)
Tactic:
fun_trans
Proof state after:
K : Type u_3
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.47990
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.48003
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.48014
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.48025
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.48036
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.48061
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.48086
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.48225
J : Type ?u.48228
FJ : J → Type ?u.48233
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 => (x i, fun y j => if h : i = j then h ▸ y else 0)) = fun x => (x i, fun dxi => oneHot i dxi)
Theorem: SciLean.revDeriv.apply_rule
Proof state before:
K : Type u_3
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.47990
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.48003
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.48014
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.48025
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.48036
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.48061
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.48086
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.48225
J : Type ?u.48228
FJ : J → Type ?u.48233
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 => (x i, fun y j => if h : i = j then h ▸ y else 0)) = fun x => (x i, fun dxi => oneHot i dxi)
Tactic:
simp[oneHot]
Proof state after:
no goals