internlm/Lean-Github huggingface dataset:
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 : ι
x : ι → E
j : I
dxj : EI j
f : ι → E
i' : ι
j' : I
h : ¬i' = i
⊢ i ≠ i'
Tactic:
intro h''
Proof state after:
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
j : I
dxj : EI j
f : ι → E
i' : ι
j' : I
h : ¬i' = i
h'' : i = i'
⊢ False
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 : ι
x : ι → E
j : I
dxj : EI j
f : ι → E
i' : ι
j' : I
h : ¬i' = i
h'' : i = i'
⊢ False
Tactic:
simp[h''] at h
Proof state after:
no goals
Theorem: SciLean.revDerivProjUpdate.pi_rule
Proof state before:
K : Type u_1
I : Type ?u.202966
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.202996
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.203007
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type u_3
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.203043
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.203068
EI : I → Type ?u.203073
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.203207
J : Type ?u.203210
FJ : J → Type ?u.203215
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
⊢ (revDerivProjUpdate K Unit fun x i => f x i) = fun x =>
    let ydf := fun i => revDerivUpdate K (fun x => f x i) x;
    (fun i => (ydf i).1, fun x df dx => fold (IndexType.univ ι) (fun dx i => (ydf i).2 (df i) dx) dx)
Tactic:
unfold revDerivProjUpdate
Proof state after:
K : Type u_1
I : Type ?u.202966
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.202996
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.203007
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type u_3
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.203043
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.203068
EI : I → Type ?u.203073
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.203207
J : Type ?u.203210
FJ : J → Type ?u.203215
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
⊢ (fun x =>
      let ydf' := revDerivProj K Unit (fun x i => f x i) x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de)) =
    fun x =>
    let ydf := fun i => revDerivUpdate K (fun x => f x i) x;
    (fun i => (ydf i).1, fun x df dx => fold (IndexType.univ ι) (fun dx i => (ydf i).2 (df i) dx) dx)
Theorem: SciLean.revDerivProjUpdate.pi_rule
Proof state before:
K : Type u_1
I : Type ?u.202966
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.202996
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.203007
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type u_3
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.203043
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.203068
EI : I → Type ?u.203073
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.203207
J : Type ?u.203210
FJ : J → Type ?u.203215
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
⊢ (fun x =>
      let ydf' := revDerivProj K Unit (fun x i => f x i) x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de)) =
    fun x =>
    let ydf := fun i => revDerivUpdate K (fun x => f x i) x;
    (fun i => (ydf i).1, fun x df dx => fold (IndexType.univ ι) (fun dx i => (ydf i).2 (df i) dx) dx)
Tactic:
fun_trans
Proof state after:
K : Type u_1
I : Type ?u.202966
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.202996
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.203007
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type u_3
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.203043
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.203068
EI : I → Type ?u.203073
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.203207
J : Type ?u.203210
FJ : J → Type ?u.203215
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
⊢ (fun x => (fun i => f x i, fun i de dx => dx + (revDerivProj K Unit (fun x i => f x i) x).2 i de)) = fun x =>
    (fun i => f x i, fun x_1 df dx =>
      fold (IndexType.univ ι) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (df i) dx) dx)
Theorem: SciLean.revDerivProjUpdate.pi_rule
Proof state before:
K : Type u_1
I : Type ?u.202966
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.202996
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.203007
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type u_3
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.203043
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.203068
EI : I → Type ?u.203073
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.203207
J : Type ?u.203210
FJ : J → Type ?u.203215
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
⊢ (fun x => (fun i => f x i, fun i de dx => dx + (revDerivProj K Unit (fun x i => f x i) x).2 i de)) = fun x =>
    (fun i => f x i, fun x_1 df dx =>
      fold (IndexType.univ ι) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (df i) dx) dx)
Tactic:
unfold revDerivProj
Proof state after:
K : Type u_1
I : Type ?u.202966
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.202996
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.203007
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type u_3
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.203043
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.203068
EI : I → Type ?u.203073
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.203207
J : Type ?u.203210
FJ : J → Type ?u.203215
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
⊢ (fun x =>
      (fun i => f x i, fun i de dx =>
        dx +
          (let ydf' := revDeriv K (fun x i => f x i) x;
              (ydf'.1, fun i de => ydf'.2 (oneHot i de))).2
            i de)) =
    fun x =>
    (fun i => f x i, fun x_1 df dx =>
      fold (IndexType.univ ι) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (df i) dx) dx)
Theorem: SciLean.revDerivProjUpdate.pi_rule
Proof state before:
K : Type u_1
I : Type ?u.202966
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.202996
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.203007
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type u_3
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.203043
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.203068
EI : I → Type ?u.203073
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.203207
J : Type ?u.203210
FJ : J → Type ?u.203215
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
⊢ (fun x =>
      (fun i => f x i, fun i de dx =>
        dx +
          (let ydf' := revDeriv K (fun x i => f x i) x;
              (ydf'.1, fun i de => ydf'.2 (oneHot i de))).2
            i de)) =
    fun x =>
    (fun i => f x i, fun x_1 df dx =>
      fold (IndexType.univ ι) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (df i) dx) dx)
Tactic:
funext x
Proof state after:
case h
K : Type u_1
I : Type ?u.202966
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.202996
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.203007
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type u_3
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.203043
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.203068
EI : I → Type ?u.203073
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.203207
J : Type ?u.203210
FJ : J → Type ?u.203215
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
⊢ (fun i => f x i, fun i de dx =>
      dx +
        (let ydf' := revDeriv K (fun x i => f x i) x;
            (ydf'.1, fun i de => ydf'.2 (oneHot i de))).2
          i de) =
    (fun i => f x i, fun x_1 df dx =>
      fold (IndexType.univ ι) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (df i) dx) dx)
Theorem: SciLean.revDerivProjUpdate.pi_rule
Proof state before:
case h
K : Type u_1
I : Type ?u.202966
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.202996
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.203007
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type u_3
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.203043
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.203068
EI : I → Type ?u.203073
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.203207
J : Type ?u.203210
FJ : J → Type ?u.203215
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
⊢ (fun i => f x i, fun i de dx =>
      dx +
        (let ydf' := revDeriv K (fun x i => f x i) x;
            (ydf'.1, fun i de => ydf'.2 (oneHot i de))).2
          i de) =
    (fun i => f x i, fun x_1 df dx =>
      fold (IndexType.univ ι) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (df i) dx) dx)
Tactic:
simp
Proof state after:
case h
K : Type u_1
I : Type ?u.202966
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.202996
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.203007
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type u_3
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.203043
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.203068
EI : I → Type ?u.203073
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.203207
J : Type ?u.203210
FJ : J → Type ?u.203215
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
⊢ (fun i de dx => dx + (revDeriv K (fun x i => f x i) x).2 (oneHot i de)) = fun x_1 df dx =>
    fold (IndexType.univ ι) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (df i) dx) dx
Theorem: SciLean.revDerivProjUpdate.pi_rule
Proof state before:
case h
K : Type u_1
I : Type ?u.202966
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.202996
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.203007
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type u_3
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.203043
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.203068
EI : I → Type ?u.203073
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.203207
J : Type ?u.203210
FJ : J → Type ?u.203215
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
⊢ (fun i de dx => dx + (revDeriv K (fun x i => f x i) x).2 (oneHot i de)) = fun x_1 df dx =>
    fold (IndexType.univ ι) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (df i) dx) dx
Tactic:
funext i de dx
Proof state after:
case h.h.h.h
K : Type u_1
I : Type ?u.202966
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.202996
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.203007
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type u_3
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.203043
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.203068
EI : I → Type ?u.203073
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.203207
J : Type ?u.203210
FJ : J → Type ?u.203215
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
dx : X
⊢ dx + (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) dx
Theorem: SciLean.revDerivProjUpdate.pi_rule
Proof state before:
case h.h.h.h
K : Type u_1
I : Type ?u.202966
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.202996
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.203007
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type u_3
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.203043
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.203068
EI : I → Type ?u.203073
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.203207
J : Type ?u.203210
FJ : J → Type ?u.203215
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
dx : X
⊢ dx + (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) dx
Tactic:
rw[revDeriv.pi_rule (hf:=by fun_prop)]
Proof state after:
case h.h.h.h
K : Type u_1
I : Type ?u.202966
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.202996
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.203007
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type u_3
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.203043
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.203068
EI : I → Type ?u.203073
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.203207
J : Type ?u.203210
FJ : J → Type ?u.203215
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
dx : X
⊢ dx +
      ((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) dx