internlm/Lean-Github huggingface dataset:
Theorem: SciLean.revDerivUpdate.pi_rule
Proof state before:
case h
K : Type u_1
I : Type u_3
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.101641
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.101652
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.101663
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.101674
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.101699
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.101724
EI : I → Type u_2
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.101863
J : Type ?u.101866
FJ : J → Type ?u.101871
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun x => f x i
x : X
⊢ (let ydf :=
      (fun x =>
          let xdf := fun i => revDerivUpdate K (fun x => f x i) x;
          (fun i => (xdf i).1, fun dy => fold (IndexType.univ I) (fun dx i => (xdf i).2 (dy i) dx) 0))
        x;
    (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    let xdf := fun i =>
      let ydf := revDeriv K (fun x => f x i) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    (fun i => (xdf i).1, fun dy dx => fold (IndexType.univ I) (fun dx i => (xdf i).2 (dy i) dx) dx)
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.101641
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.101652
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.101663
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.101674
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.101699
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.101724
EI : I → Type u_2
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.101863
J : Type ?u.101866
FJ : J → Type ?u.101871
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun x => f x i
x : X
⊢ (fun dy dx => dx + fold (IndexType.univ I) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (dy i) dx) 0) =
    fun dy dx => fold (IndexType.univ I) (fun dx i => dx + (revDeriv K (fun x => f x i) x).2 (dy i)) dx
Theorem: SciLean.revDerivUpdate.pi_rule
Proof state before:
case h
K : Type u_1
I : Type u_3
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.101641
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.101652
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.101663
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.101674
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.101699
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.101724
EI : I → Type u_2
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.101863
J : Type ?u.101866
FJ : J → Type ?u.101871
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun x => f x i
x : X
⊢ (fun dy dx => dx + fold (IndexType.univ I) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (dy i) dx) 0) =
    fun dy dx => fold (IndexType.univ I) (fun dx i => dx + (revDeriv K (fun x => f x i) x).2 (dy i)) dx
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.revDerivUpdate.pi_rule
Proof state before:
K : Type u_1
I : Type u_3
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.101641
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.101652
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.101663
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.101674
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.101699
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.101724
EI : I → Type u_2
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.101863
J : Type ?u.101866
FJ : J → Type ?u.101871
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun x => f x i
x : X
⊢ ∀ (i : I), HasAdjDiff K fun x => f x i
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.revDerivProj.id_rule
Proof state before:
K : Type u_4
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.108793
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.108806
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.108817
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.108828
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.108839
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.108864
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.109028
J : Type ?u.109031
FJ : J → Type ?u.109036
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
⊢ (revDerivProj K I fun x => x) = fun x => (x, fun i de => oneHot i de)
Tactic:
unfold revDerivProj
Proof state after:
K : Type u_4
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.108793
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.108806
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.108817
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.108828
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.108839
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.108864
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.109028
J : Type ?u.109031
FJ : J → Type ?u.109036
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 i de => ydf'.2 (oneHot i de))) =
    fun x => (x, fun i de => oneHot i de)
Theorem: SciLean.revDerivProj.id_rule
Proof state before:
K : Type u_4
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.108793
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.108806
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.108817
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.108828
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.108839
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.108864
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.109028
J : Type ?u.109031
FJ : J → Type ?u.109036
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 i de => ydf'.2 (oneHot i de))) =
    fun x => (x, fun i de => oneHot i de)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.revDerivProj.const_rule
Proof state before:
K : Type u_5
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.113121
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.113145
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.113156
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.113167
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.113192
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.113356
J : Type ?u.113359
FJ : J → Type ?u.113364
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
⊢ (revDerivProj K I fun x_1 => x) = fun x_1 => (x, fun i de => 0)
Tactic:
unfold revDerivProj
Proof state after:
K : Type u_5
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.113121
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.113145
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.113156
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.113167
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.113192
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.113356
J : Type ?u.113359
FJ : J → Type ?u.113364
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' := revDeriv K (fun x_2 => x) x_1;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun x_1 => (x, fun i de => 0)
Theorem: SciLean.revDerivProj.const_rule
Proof state before:
K : Type u_5
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.113121
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.113145
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.113156
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.113167
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.113192
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.113356
J : Type ?u.113359
FJ : J → Type ?u.113364
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' := revDeriv K (fun x_2 => x) x_1;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun x_1 => (x, fun i de => 0)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.revDerivProj.apply_rule
Proof state before:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
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.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
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 : ι
⊢ (revDerivProj K I fun f => f i) = fun f => (f i, fun j dxj => oneHot (i, j) dxj)
Tactic:
unfold revDerivProj
Proof state after:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
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.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
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 : ι
⊢ (fun x =>
      let ydf' := revDeriv K (fun f => f i) x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun f => (f i, fun j dxj => oneHot (i, j) dxj)
Theorem: SciLean.revDerivProj.apply_rule
Proof state before:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
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.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
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 : ι
⊢ (fun x =>
      let ydf' := revDeriv K (fun f => f i) x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun f => (f i, fun j dxj => oneHot (i, j) dxj)
Tactic:
fun_trans
Proof state after:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
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.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
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 : ι
⊢ (fun x => (x i, fun i_1 de => oneHot i (oneHot i_1 de))) = fun f => (f i, fun j dxj => oneHot (i, j) dxj)
Theorem: SciLean.revDerivProj.apply_rule
Proof state before:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
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.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
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 : ι
⊢ (fun x => (x i, fun i_1 de => oneHot i (oneHot i_1 de))) = fun f => (f i, fun j dxj => oneHot (i, j) dxj)
Tactic:
simp[oneHot]
Proof state after:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
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.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
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 : ι
⊢ (fun x => (x i, fun i_1 de i_2 => if i = i_2 then structMake fun i' => if h : i_1 = i' then h ▸ de else 0 else 0)) =
    fun f => (f i, fun j dxj j_1 => structMake fun i_1 => if h : i = j_1 ∧ j = i_1 then ⋯ ▸ dxj else 0)
Theorem: SciLean.revDerivProj.apply_rule
Proof state before:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
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.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
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 : ι
⊢ (fun x => (x i, fun i_1 de i_2 => if i = i_2 then structMake fun i' => if h : i_1 = i' then h ▸ de else 0 else 0)) =
    fun f => (f i, fun j dxj j_1 => structMake fun i_1 => if h : i = j_1 ∧ j = i_1 then ⋯ ▸ dxj else 0)
Tactic:
funext x
Proof state after:
case h
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.116532
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.116545
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.116556
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.116567
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.116603
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.116767
J : Type ?u.116770
FJ : J → Type ?u.116775
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
⊢ (x i, fun i_1 de i_2 => if i = i_2 then structMake fun i' => if h : i_1 = i' then h ▸ de else 0 else 0) =
    (x i, fun j dxj j_1 => structMake fun i_1 => if h : i = j_1 ∧ j = i_1 then ⋯ ▸ dxj else 0)