internlm/Lean-Github huggingface dataset:
Theorem: SciLean.revDeriv.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.56951
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.56962
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.56973
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.56984
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.57009
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.57034
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.57173
J : Type ?u.57176
FJ : J → Type ?u.57181
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
⊢ (revDeriv 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 => fold (IndexType.univ I) (fun dx i => (xdf i).2 (dy i) dx) 0)
Tactic:
unfold revDeriv
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.56951
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.56962
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.56973
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.56984
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.57009
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.57034
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.57173
J : Type ?u.57176
FJ : J → Type ?u.57181
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 => ((fun x i => f x i) x, semiAdjoint K (cderiv K (fun x i => f x i) x))) = 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)
Theorem: SciLean.revDeriv.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.56951
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.56962
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.56973
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.56984
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.57009
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.57034
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.57173
J : Type ?u.57176
FJ : J → Type ?u.57181
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 => ((fun x i => f x i) x, semiAdjoint K (cderiv K (fun x i => f x i) x))) = 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)
Tactic:
fun_trans
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.56951
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.56962
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.56973
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.56984
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.57009
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.57034
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.57173
J : Type ?u.57176
FJ : J → Type ?u.57181
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 => (fun i => f x i, semiAdjoint K (cderiv K (fun x i => f x i) x))) = fun x =>
    (fun i => f x i, fun dy =>
      fold (IndexType.univ I) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (dy i) dx) 0)
Theorem: SciLean.revDeriv.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.56951
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.56962
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.56973
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.56984
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.57009
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.57034
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.57173
J : Type ?u.57176
FJ : J → Type ?u.57181
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 => (fun i => f x i, semiAdjoint K (cderiv K (fun x i => f x i) x))) = fun x =>
    (fun i => f x i, fun dy =>
      fold (IndexType.univ I) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (dy i) dx) 0)
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.56951
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.56962
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.56973
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.56984
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.57009
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.57034
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.57173
J : Type ?u.57176
FJ : J → Type ?u.57181
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
⊢ (fun i => f x i, semiAdjoint K (cderiv K (fun x i => f x i) x)) =
    (fun i => f x i, fun dy =>
      fold (IndexType.univ I) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (dy i) dx) 0)
Theorem: SciLean.revDeriv.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.56951
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.56962
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.56973
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.56984
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.57009
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.57034
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.57173
J : Type ?u.57176
FJ : J → Type ?u.57181
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
⊢ (fun i => f x i, semiAdjoint K (cderiv K (fun x i => f x i) x)) =
    (fun i => f x i, fun dy =>
      fold (IndexType.univ I) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (dy i) dx) 0)
Tactic:
simp
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.56951
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.56962
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.56973
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.56984
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.57009
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.57034
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.57173
J : Type ?u.57176
FJ : J → Type ?u.57181
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
⊢ semiAdjoint K (cderiv K (fun x i => f x i) x) = fun dy =>
    fold (IndexType.univ I) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (dy i) dx) 0
Theorem: SciLean.revDeriv.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.56951
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.56962
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.56973
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.56984
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.57009
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.57034
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.57173
J : Type ?u.57176
FJ : J → Type ?u.57181
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
⊢ semiAdjoint K (cderiv K (fun x i => f x i) x) = fun dy =>
    fold (IndexType.univ I) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (dy i) dx) 0
Tactic:
rw[cderiv.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.56951
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.56962
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.56973
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.56984
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.57009
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.57034
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.57173
J : Type ?u.57176
FJ : J → Type ?u.57181
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
⊢ semiAdjoint K ((fun x dx i => cderiv K (fun x => f x i) x dx) x) = fun dy =>
    fold (IndexType.univ I) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (dy i) dx) 0
Theorem: SciLean.revDeriv.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.56951
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.56962
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.56973
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.56984
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.57009
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.57034
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.57173
J : Type ?u.57176
FJ : J → Type ?u.57181
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
⊢ semiAdjoint K ((fun x dx i => cderiv K (fun x => f x i) x dx) x) = fun dy =>
    fold (IndexType.univ I) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (dy i) dx) 0
Tactic:
fun_trans
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.56951
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.56962
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.56973
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.56984
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.57009
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.57034
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.57173
J : Type ?u.57176
FJ : J → Type ?u.57181
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
⊢ (fun x' =>  ∑ i, semiAdjoint K (fun x_1 => cderiv K (fun x => f x i) x x_1) (x' i)) = fun dy =>
    fold (IndexType.univ I) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (dy i) dx) 0
Theorem: SciLean.revDeriv.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.56951
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.56962
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.56973
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.56984
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.57009
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.57034
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.57173
J : Type ?u.57176
FJ : J → Type ?u.57181
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
⊢ (fun x' =>  ∑ i, semiAdjoint K (fun x_1 => cderiv K (fun x => f x i) x x_1) (x' i)) = fun dy =>
    fold (IndexType.univ I) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (dy i) dx) 0
Tactic:
simp[revDerivUpdate,revDeriv,IndexType.sum]
Proof state after:
no goals
Theorem: SciLean.revDeriv.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.56951
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.56962
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.56973
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.56984
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.57009
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.57034
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.57173
J : Type ?u.57176
FJ : J → Type ?u.57181
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
⊢ ∀ (i : I), CDifferentiable K fun x => f x i
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.revDerivUpdate.id_rule
Proof state before:
K : Type u_2
I : Type ?u.75119
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.75138
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.75149
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.75160
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.75171
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.75196
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.75221
EI : I → Type ?u.75226
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.75360
J : Type ?u.75363
FJ : J → Type ?u.75368
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
⊢ (revDerivUpdate K fun x => x) = fun x => (x, fun dx' dx => dx + dx')
Tactic:
unfold revDerivUpdate
Proof state after:
K : Type u_2
I : Type ?u.75119
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.75138
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.75149
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.75160
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.75171
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.75196
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.75221
EI : I → Type ?u.75226
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.75360
J : Type ?u.75363
FJ : J → Type ?u.75368
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 =>
      let ydf := revDeriv K (fun x => x) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    fun x => (x, fun dx' dx => dx + dx')
Theorem: SciLean.revDerivUpdate.id_rule
Proof state before:
K : Type u_2
I : Type ?u.75119
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.75138
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.75149
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.75160
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.75171
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.75196
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.75221
EI : I → Type ?u.75226
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.75360
J : Type ?u.75363
FJ : J → Type ?u.75368
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 =>
      let ydf := revDeriv K (fun x => x) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    fun x => (x, fun dx' dx => dx + dx')
Tactic:
fun_trans
Proof state after:
no goals
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
⊢ (revDerivUpdate K fun x => y) = fun x => (y, fun x dx => dx)
Tactic:
unfold revDerivUpdate
Proof state after:
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)