internlm/Lean-Github huggingface dataset:
Theorem: SciLean.revDerivProj.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.140778
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.140789
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.140800
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.140825
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.140989
J : Type ?u.140992
FJ : J → Type ?u.140997
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
⊢ (revDerivProj K I fun x => f (g x)) = fun x =>
    let ydg' := revDeriv K g x;
    let zdf' := revDerivProj K I f ydg'.1;
    (zdf'.1, fun i de => ydg'.2 (zdf'.2 i de))
Tactic:
unfold revDerivProj
Proof state after:
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.140778
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.140789
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.140800
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.140825
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.140989
J : Type ?u.140992
FJ : J → Type ?u.140997
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
⊢ (fun x =>
      let ydf' := revDeriv K (fun x => f (g x)) x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun x =>
    let ydg' := revDeriv K g x;
    let zdf' :=
      let ydf' := revDeriv K f ydg'.1;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (zdf'.1, fun i de => ydg'.2 (zdf'.2 i de))
Theorem: SciLean.revDerivProj.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.140778
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.140789
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.140800
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.140825
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.140989
J : Type ?u.140992
FJ : J → Type ?u.140997
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
⊢ (fun x =>
      let ydf' := revDeriv K (fun x => f (g x)) x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun x =>
    let ydg' := revDeriv K g x;
    let zdf' :=
      let ydf' := revDeriv K f ydg'.1;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (zdf'.1, fun i de => ydg'.2 (zdf'.2 i de))
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.revDerivProj.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.146473
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.146484
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.146495
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.146520
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.146684
J : Type ?u.146687
FJ : J → Type ?u.146692
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
⊢ (revDerivProj K I fun x =>
      let y := g x;
      f x y) =
    fun x =>
    let ydg' := revDerivUpdate K g x;
    let zdf' :=
      revDerivProj K I
        (fun x =>
          match x with
          | (x, y) => f x y)
        (x, ydg'.1);
    (zdf'.1, fun i dei =>
      let dxy := zdf'.2 i dei;
      ydg'.2 dxy.2 dxy.1)
Tactic:
unfold revDerivProj
Proof state after:
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.146473
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.146484
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.146495
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.146520
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.146684
J : Type ?u.146687
FJ : J → Type ?u.146692
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' :=
        revDeriv K
          (fun x =>
            let y := g x;
            f x y)
          x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun x =>
    let ydg' := revDerivUpdate K g x;
    let zdf' :=
      let ydf' :=
        revDeriv K
          (fun x =>
            match x with
            | (x, y) => f x y)
          (x, ydg'.1);
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (zdf'.1, fun i dei =>
      let dxy := zdf'.2 i dei;
      ydg'.2 dxy.2 dxy.1)
Theorem: SciLean.revDerivProj.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.146473
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.146484
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.146495
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.146520
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.146684
J : Type ?u.146687
FJ : J → Type ?u.146692
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' :=
        revDeriv K
          (fun x =>
            let y := g x;
            f x y)
          x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun x =>
    let ydg' := revDerivUpdate K g x;
    let zdf' :=
      let ydf' :=
        revDeriv K
          (fun x =>
            match x with
            | (x, y) => f x y)
          (x, ydg'.1);
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (zdf'.1, fun i dei =>
      let dxy := zdf'.2 i dei;
      ydg'.2 dxy.2 dxy.1)
Tactic:
fun_trans
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
⊢ (revDerivProj 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 => fold (IndexType.univ ι) (fun dx i => (ydf i).2 (df i) dx) 0)
Tactic:
unfold revDerivProj
Proof state after:
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
⊢ (fun x =>
      let ydf' := revDeriv K (fun x i => f x i) x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun x =>
    let ydf := fun i => revDerivUpdate K (fun x => f x i) x;
    (fun i => (ydf i).1, fun x df => fold (IndexType.univ ι) (fun dx i => (ydf i).2 (df i) dx) 0)
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
⊢ (fun x =>
      let ydf' := revDeriv K (fun x i => f x i) x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun x =>
    let ydf := fun i => revDerivUpdate K (fun x => f x i) x;
    (fun i => (ydf i).1, fun x df => fold (IndexType.univ ι) (fun dx i => (ydf i).2 (df i) dx) 0)
Tactic:
fun_trans
Proof state after:
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
⊢ (fun x => (fun i => f x i, fun i de => (revDeriv K (fun x i => f x i) x).2 (oneHot i de))) = fun x =>
    (fun i => f x i, fun x_1 df =>
      fold (IndexType.univ ι) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (df i) dx) 0)
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
⊢ (fun x => (fun i => f x i, fun i de => (revDeriv K (fun x i => f x i) x).2 (oneHot i de))) = fun x =>
    (fun i => f x i, fun x_1 df =>
      fold (IndexType.univ ι) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (df i) dx) 0)
Tactic:
funext x
Proof state after:
case 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
⊢ (fun i => f x i, fun i de => (revDeriv K (fun x i => f x i) x).2 (oneHot i de)) =
    (fun i => f x i, fun x_1 df =>
      fold (IndexType.univ ι) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (df i) dx) 0)
Theorem: SciLean.revDerivProj.pi_rule
Proof state before:
case 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
⊢ (fun i => f x i, fun i de => (revDeriv K (fun x i => f x i) x).2 (oneHot i de)) =
    (fun i => f x i, fun x_1 df =>
      fold (IndexType.univ ι) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (df i) dx) 0)
Tactic:
simp
Proof state after:
case 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
⊢ (fun i de => (revDeriv K (fun x i => f x i) x).2 (oneHot i de)) = fun x_1 df =>
    fold (IndexType.univ ι) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (df i) dx) 0
Theorem: SciLean.revDerivProj.pi_rule
Proof state before:
case 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
⊢ (fun i de => (revDeriv K (fun x i => f x i) x).2 (oneHot i de)) = fun x_1 df =>
    fold (IndexType.univ ι) (fun dx i => (revDerivUpdate K (fun x => f x i) x).2 (df i) dx) 0
Tactic:
funext i de
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
⊢ (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