internlm/Lean-Github huggingface dataset:
Theorem: SciLean.revDerivProj.pi_rule
Proof state before:
case h.h.h
K : Type u_1
I : Type ?u.154619
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.154649
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.154660
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type u_3
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.154696
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.154721
EI : I → Type ?u.154726
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.154860
J : Type ?u.154863
FJ : J → Type ?u.154868
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
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
x : X
i : Unit
de : ι → Y
⊢ (revDeriv K (fun x i => f x i) x).2 (oneHot i de) =
    fold (IndexType.univ ι) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (de i) dx) 0
Tactic:
rw[revDeriv.pi_rule (hf:=by fun_prop)]
Proof state after:
case h.h.h
K : Type u_1
I : Type ?u.154619
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.154649
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.154660
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type u_3
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.154696
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.154721
EI : I → Type ?u.154726
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.154860
J : Type ?u.154863
FJ : J → Type ?u.154868
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
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
x : X
i : Unit
de : ι → Y
⊢ ((fun x =>
            let xdf := fun i => revDerivUpdate K (fun x => f x i) x;
            (fun i => (xdf i).1, fun dy => fold (IndexType.univ ι) (fun dx i => (xdf i).2 (dy i) dx) 0))
          x).2
      (oneHot i de) =
    fold (IndexType.univ ι) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (de i) dx) 0
Theorem: SciLean.revDerivProj.pi_rule
Proof state before:
case h.h.h
K : Type u_1
I : Type ?u.154619
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.154649
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.154660
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type u_3
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.154696
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.154721
EI : I → Type ?u.154726
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.154860
J : Type ?u.154863
FJ : J → Type ?u.154868
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
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
x : X
i : Unit
de : ι → Y
⊢ ((fun x =>
            let xdf := fun i => revDerivUpdate K (fun x => f x i) x;
            (fun i => (xdf i).1, fun dy => fold (IndexType.univ ι) (fun dx i => (xdf i).2 (dy i) dx) 0))
          x).2
      (oneHot i de) =
    fold (IndexType.univ ι) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (de i) dx) 0
Tactic:
simp[oneHot]
Proof state after:
no goals
Theorem: SciLean.revDerivProj.pi_rule
Proof state before:
K : Type u_1
I : Type ?u.154619
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.154649
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.154660
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type u_3
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.154696
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.154721
EI : I → Type ?u.154726
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.154860
J : Type ?u.154863
FJ : J → Type ?u.154868
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
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
x : X
i : Unit
de : ι → Y
⊢ ∀ (i : ι), HasAdjDiff K fun x => f x i
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.revDerivProjUpdate.id_rule
Proof state before:
K : Type u_4
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.166539
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.166552
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.166563
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.166574
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.166585
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.166610
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_2
EI : I → Type u_3
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.166774
J : Type ?u.166777
FJ : J → Type ?u.166782
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
⊢ (revDerivProjUpdate K I fun x => x) = fun x => (x, fun i de dx => structModify i (fun ei => ei + de) dx)
Tactic:
funext x
Proof state after:
case h
K : Type u_4
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.166539
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.166552
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.166563
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.166574
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.166585
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.166610
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_2
EI : I → Type u_3
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.166774
J : Type ?u.166777
FJ : J → Type ?u.166782
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
x : E
⊢ revDerivProjUpdate K I (fun x => x) x = (x, fun i de dx => structModify i (fun ei => ei + de) dx)
Theorem: SciLean.revDerivProjUpdate.id_rule
Proof state before:
case h
K : Type u_4
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.166539
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.166552
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.166563
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.166574
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.166585
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.166610
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_2
EI : I → Type u_3
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.166774
J : Type ?u.166777
FJ : J → Type ?u.166782
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
x : E
⊢ revDerivProjUpdate K I (fun x => x) x = (x, fun i de dx => structModify i (fun ei => ei + de) dx)
Tactic:
simp[revDerivProjUpdate, revDerivProj.id_rule]
Proof state after:
no goals
Theorem: SciLean.revDerivProjUpdate.const_rule
Proof state before:
K : Type u_5
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.170405
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.170429
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.170440
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.170451
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.170476
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.170640
J : Type ?u.170643
FJ : J → Type ?u.170648
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
x : E
⊢ (revDerivProjUpdate K I fun x_1 => x) = fun x_1 => (x, fun i de dx => dx)
Tactic:
unfold revDerivProjUpdate
Proof state after:
K : Type u_5
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.170405
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.170429
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.170440
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.170451
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.170476
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.170640
J : Type ?u.170643
FJ : J → Type ?u.170648
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
x : E
⊢ (fun x_1 =>
      let ydf' := revDerivProj K I (fun x_2 => x) x_1;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de)) =
    fun x_1 => (x, fun i de dx => dx)
Theorem: SciLean.revDerivProjUpdate.const_rule
Proof state before:
K : Type u_5
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.170405
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.170429
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.170440
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.170451
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.170476
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.170640
J : Type ?u.170643
FJ : J → Type ?u.170648
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
x : E
⊢ (fun x_1 =>
      let ydf' := revDerivProj K I (fun x_2 => x) x_1;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de)) =
    fun x_1 => (x, fun i de dx => dx)
Tactic:
simp[revDerivProj.const_rule]
Proof state after:
no goals
Theorem: SciLean.revDerivProjUpdate.comp_rule
Proof state before:
K : Type u_1
I : Type u_5
inst✝²⁴ : RCLike K
X : Type u_4
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.173849
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.173860
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.173871
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.173896
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_3
EI : I → Type u_6
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.174060
J : Type ?u.174063
FJ : J → Type ?u.174068
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 → E
g : X → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (revDerivProjUpdate K I fun x => f (g x)) = fun x =>
    let ydg' := revDerivUpdate K g x;
    let zdf' := revDerivProj K I f ydg'.1;
    (zdf'.1, fun i de dx => ydg'.2 (zdf'.2 i de) dx)
Tactic:
funext x
Proof state after:
case h
K : Type u_1
I : Type u_5
inst✝²⁴ : RCLike K
X : Type u_4
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.173849
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.173860
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.173871
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.173896
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_3
EI : I → Type u_6
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.174060
J : Type ?u.174063
FJ : J → Type ?u.174068
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 → E
g : X → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : X
⊢ revDerivProjUpdate K I (fun x => f (g x)) x =
    let ydg' := revDerivUpdate K g x;
    let zdf' := revDerivProj K I f ydg'.1;
    (zdf'.1, fun i de dx => ydg'.2 (zdf'.2 i de) dx)
Theorem: SciLean.revDerivProjUpdate.comp_rule
Proof state before:
case h
K : Type u_1
I : Type u_5
inst✝²⁴ : RCLike K
X : Type u_4
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.173849
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.173860
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.173871
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.173896
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_3
EI : I → Type u_6
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.174060
J : Type ?u.174063
FJ : J → Type ?u.174068
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 → E
g : X → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : X
⊢ revDerivProjUpdate K I (fun x => f (g x)) x =
    let ydg' := revDerivUpdate K g x;
    let zdf' := revDerivProj K I f ydg'.1;
    (zdf'.1, fun i de dx => ydg'.2 (zdf'.2 i de) dx)
Tactic:
simp[revDerivProjUpdate,revDerivProj.comp_rule _ _ _ _ hf hg]
Proof state after:
case h
K : Type u_1
I : Type u_5
inst✝²⁴ : RCLike K
X : Type u_4
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.173849
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.173860
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.173871
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.173896
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_3
EI : I → Type u_6
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.174060
J : Type ?u.174063
FJ : J → Type ?u.174068
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 → E
g : X → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : X
⊢ (fun i de dx => dx + (revDeriv K g x).2 ((revDerivProj K I f (g x)).2 i de)) = fun i de dx =>
    (revDerivUpdate K g x).2 ((revDerivProj K I f (g x)).2 i de) dx
Theorem: SciLean.revDerivProjUpdate.comp_rule
Proof state before:
case h
K : Type u_1
I : Type u_5
inst✝²⁴ : RCLike K
X : Type u_4
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.173849
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.173860
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.173871
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.173896
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_3
EI : I → Type u_6
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.174060
J : Type ?u.174063
FJ : J → Type ?u.174068
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 → E
g : X → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : X
⊢ (fun i de dx => dx + (revDeriv K g x).2 ((revDerivProj K I f (g x)).2 i de)) = fun i de dx =>
    (revDerivUpdate K g x).2 ((revDerivProj K I f (g x)).2 i de) dx
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.revDerivProjUpdate.let_rule
Proof state before:
K : Type u_1
I : Type u_5
inst✝²⁴ : RCLike K
X : Type u_3
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.179458
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.179469
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.179480
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.179505
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_4
EI : I → Type u_6
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.179669
J : Type ?u.179672
FJ : J → Type ?u.179677
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 → E
g : X → Y
hf :
  HasAdjDiff K fun x =>
    match x with
    | (x, y) => f x y
hg : HasAdjDiff K g
⊢ (fun x =>
      let ydf' :=
        revDerivProj K I
          (fun x =>
            let y := g x;
            f x y)
          x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de)) =
    fun x =>
    let ydg' := revDerivUpdate K g x;
    let zdf' :=
      let ydf' :=
        revDerivProj K I
          (fun x =>
            match x with
            | (x, y) => f x y)
          (x, ydg'.1);
      (ydf'.1, fun i de dx => dx + ydf'.2 i de);
    (zdf'.1, fun i dei dx =>
      let dxy := zdf'.2 i dei (dx, 0);
      ydg'.2 dxy.2 dxy.1)
Tactic:
simp [revDerivProj.let_rule _ _ _ _ hf hg,add_assoc,add_comm,revDerivUpdate]
Proof state after:
no goals
Theorem: SciLean.revDerivProjUpdate.apply_rule
Proof state before:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
i : ι
⊢ (revDerivProjUpdate K I fun f => f i) = fun f =>
    (f i, fun j dxj df i' => if i = i' then structModify j (fun xj => xj + dxj) (df i') else df i')
Tactic:
funext x
Proof state after:
case h
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
i : ι
x : ι → E
⊢ revDerivProjUpdate K I (fun f => f i) x =
    (x i, fun j dxj df i' => if i = i' then structModify j (fun xj => xj + dxj) (df i') else df i')