internlm/Lean-Github huggingface dataset:
Theorem: SciLean.revDeriv2.const_rule_has
Proof state before:
case revDeriv2
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
w : W
x : X
y : Y
⊢ revDeriv2 K (fun w x => y) w x = (y, fun dy dw => (dw, 0))
Tactic:
. fun_trans [revDeriv2]
Proof state after:
no goals
Theorem: SciLean.revDeriv2.const_rule_has
Proof state before:
case hasAdjDiff
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
w : W
x : X
y : Y
⊢ HasAdjDiffAt K
    (fun x =>
      match x with
      | (w, x) => y)
    (w, x)
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.revDeriv2.const_rule_has
Proof state before:
case revDeriv2
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
w : W
x : X
y : Y
⊢ revDeriv2 K (fun w x => y) w x = (y, fun dy dw => (dw, 0))
Tactic:
fun_trans [revDeriv2]
Proof state after:
no goals
Theorem: SciLean.revDeriv2.let_rule
Proof state before:
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
f : W → X → Y → Z
g : W → X → Y
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x, y) => f w x y
hg :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => g w x
⊢ (revDeriv2 K fun w x =>
      let y := g w x;
      f w x y) =
    fun w x =>
    let ydg := revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ();
    let zdf := revDeriv2 K (fun w xy => f w xy.1 xy.2) w (x, ydg.1);
    (zdf.1, fun dz dx =>
      let dxyz := zdf.2 dz dx;
      let dxy := ydg.2 dxyz.2.2 (dxyz.1, dxyz.2.1);
      dxy.1)
Tactic:
simp at hf hg
Proof state after:
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
f : W → X → Y → Z
g : W → X → Y
hf : HasAdjDiff K fun x => f x.1 x.2.1 x.2.2
hg : HasAdjDiff K fun x => g x.1 x.2
⊢ (revDeriv2 K fun w x =>
      let y := g w x;
      f w x y) =
    fun w x =>
    let ydg := revDeriv2 K (fun wx x => g wx.1 wx.2) (w, x) ();
    let zdf := revDeriv2 K (fun w xy => f w xy.1 xy.2) w (x, ydg.1);
    (zdf.1, fun dz dx =>
      let dxyz := zdf.2 dz dx;
      let dxy := ydg.2 dxyz.2.2 (dxyz.1, dxyz.2.1);
      dxy.1)
Theorem: SciLean.revDeriv2.let_rule
Proof state before:
case h.h.h.h
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
f : W → X → Y → Z
g : W → X → Y
hf : HasAdjDiff K fun x => f x.1 x.2.1 x.2.2
hg : HasAdjDiff K fun x => g x.1 x.2
x : W
y : X
dy : Z
dw' : W
⊢ (dw' +
        ((semiAdjoint K
              (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
              dy).1 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (x, y) x_1)
              (semiAdjoint K
                    (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
                    dy).2.2).1),
      (semiAdjoint K
              (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
              dy).2.1 +
        (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (x, y) x_1)
            (semiAdjoint K
                  (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y) dx8)
                  dy).2.2).2) =
    (dw' + (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y)) dy).1,
        (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y)) dy).2.1) +
      (semiAdjoint K (cderiv K (fun x => g x.1.1 x.1.2) ((x, y), ()))
          (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (x, y, g x y))
                dy).2.2).1
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.revDeriv2.let_rule_has
Proof state before:
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
w : W
x : X
g : W → X → Y
g' : Y × (Y → W × X → (W × X) × Unit)
hg :
  HasRevDeriv2At K
    (fun x x_1 =>
      match x with
      | (w, x) => g w x)
    g' (w, x) ()
f : W → X → Y → Z
f' : Z × (Z → W → W × X × Y)
hf :
  HasRevDeriv2At K
    (fun w x =>
      match x with
      | (x, y) => f w x y)
    f' w (x, g w x)
r : Z × (Z → W → W × X)
hr :
  r =
    (f'.1, fun dz dw =>
      let dwxy := f'.2 dz dw;
      let dxy := g'.2 dwxy.2.2 (dwxy.1, dwxy.2.1);
      dxy.1)
⊢ HasRevDeriv2At K (fun w x => f w x (g w x)) r w x
Tactic:
rw[hr]
Proof state after:
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
w : W
x : X
g : W → X → Y
g' : Y × (Y → W × X → (W × X) × Unit)
hg :
  HasRevDeriv2At K
    (fun x x_1 =>
      match x with
      | (w, x) => g w x)
    g' (w, x) ()
f : W → X → Y → Z
f' : Z × (Z → W → W × X × Y)
hf :
  HasRevDeriv2At K
    (fun w x =>
      match x with
      | (x, y) => f w x y)
    f' w (x, g w x)
r : Z × (Z → W → W × X)
hr :
  r =
    (f'.1, fun dz dw =>
      let dwxy := f'.2 dz dw;
      let dxy := g'.2 dwxy.2.2 (dwxy.1, dwxy.2.1);
      dxy.1)
⊢ HasRevDeriv2At K (fun w x => f w x (g w x))
    (f'.1, fun dz dw =>
      let dwxy := f'.2 dz dw;
      let dxy := g'.2 dwxy.2.2 (dwxy.1, dwxy.2.1);
      dxy.1)
    w x
Theorem: SciLean.revDeriv2.let_rule_has
Proof state before:
case revDeriv2
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
w : W
x : X
g : W → X → Y
g' : Y × (Y → W × X → (W × X) × Unit)
hg :
  HasRevDeriv2At K
    (fun x x_1 =>
      match x with
      | (w, x) => g w x)
    g' (w, x) ()
f : W → X → Y → Z
f' : Z × (Z → W → W × X × Y)
hf :
  HasRevDeriv2At K
    (fun w x =>
      match x with
      | (x, y) => f w x y)
    f' w (x, g w x)
r : Z × (Z → W → W × X)
hr :
  r =
    (f'.1, fun dz dw =>
      let dwxy := f'.2 dz dw;
      let dxy := g'.2 dwxy.2.2 (dwxy.1, dwxy.2.1);
      dxy.1)
this✝ :
  HasAdjDiffAt K
    (fun x =>
      match x with
      | (w, x) => g w x)
    (w, x)
this :
  HasAdjDiffAt K
    (fun x =>
      match x with
      | (w, x, y) => f w x y)
    (w, x, g w x)
⊢ revDeriv2 K (fun w x => f w x (g w x)) w x =
    (f'.1, fun dz dw =>
      let dwxy := f'.2 dz dw;
      let dxy := g'.2 dwxy.2.2 (dwxy.1, dwxy.2.1);
      dxy.1)
Tactic:
. sorry_proof
Proof state after:
no goals
Theorem: SciLean.revDeriv2.let_rule_has
Proof state before:
case hasAdjDiff
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
w : W
x : X
g : W → X → Y
g' : Y × (Y → W × X → (W × X) × Unit)
hg :
  HasRevDeriv2At K
    (fun x x_1 =>
      match x with
      | (w, x) => g w x)
    g' (w, x) ()
f : W → X → Y → Z
f' : Z × (Z → W → W × X × Y)
hf :
  HasRevDeriv2At K
    (fun w x =>
      match x with
      | (x, y) => f w x y)
    f' w (x, g w x)
r : Z × (Z → W → W × X)
hr :
  r =
    (f'.1, fun dz dw =>
      let dwxy := f'.2 dz dw;
      let dxy := g'.2 dwxy.2.2 (dwxy.1, dwxy.2.1);
      dxy.1)
this✝ :
  HasAdjDiffAt K
    (fun x =>
      match x with
      | (w, x) => g w x)
    (w, x)
this :
  HasAdjDiffAt K
    (fun x =>
      match x with
      | (w, x, y) => f w x y)
    (w, x, g w x)
⊢ HasAdjDiffAt K
    (fun x =>
      match x with
      | (w, x) => f w x (g w x))
    (w, x)
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.revDeriv2.let_rule_has
Proof state before:
case revDeriv2
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
w : W
x : X
g : W → X → Y
g' : Y × (Y → W × X → (W × X) × Unit)
hg :
  HasRevDeriv2At K
    (fun x x_1 =>
      match x with
      | (w, x) => g w x)
    g' (w, x) ()
f : W → X → Y → Z
f' : Z × (Z → W → W × X × Y)
hf :
  HasRevDeriv2At K
    (fun w x =>
      match x with
      | (x, y) => f w x y)
    f' w (x, g w x)
r : Z × (Z → W → W × X)
hr :
  r =
    (f'.1, fun dz dw =>
      let dwxy := f'.2 dz dw;
      let dxy := g'.2 dwxy.2.2 (dwxy.1, dwxy.2.1);
      dxy.1)
this✝ :
  HasAdjDiffAt K
    (fun x =>
      match x with
      | (w, x) => g w x)
    (w, x)
this :
  HasAdjDiffAt K
    (fun x =>
      match x with
      | (w, x, y) => f w x y)
    (w, x, g w x)
⊢ revDeriv2 K (fun w x => f w x (g w x)) w x =
    (f'.1, fun dz dw =>
      let dwxy := f'.2 dz dw;
      let dxy := g'.2 dwxy.2.2 (dwxy.1, dwxy.2.1);
      dxy.1)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.revDeriv2.pi_rule
Proof state before:
case h.h
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
f : X → Y → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun xy => f xy.1 xy.2 i
x : X
y : Y
⊢ (fun dy dw' =>
      (dw' + (semiAdjoint K (cderiv K (fun x i => f x.1 x.2 i) (x, y)) dy).1,
        (semiAdjoint K (cderiv K (fun x i => f x.1 x.2 i) (x, y)) dy).2)) =
    fun df dx' =>
    fold (IndexType.univ I)
      (fun dxy i => dxy + (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((x, y), ())) (oneHot i (df i))).1) (dx', 0)
Tactic:
funext dw dx
Proof state after:
case h.h.h.h
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
f : X → Y → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun xy => f xy.1 xy.2 i
x : X
y : Y
dw : (i : I) → EI i
dx : X
⊢ (dx + (semiAdjoint K (cderiv K (fun x i => f x.1 x.2 i) (x, y)) dw).1,
      (semiAdjoint K (cderiv K (fun x i => f x.1 x.2 i) (x, y)) dw).2) =
    fold (IndexType.univ I)
      (fun dxy i => dxy + (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((x, y), ())) (oneHot i (dw i))).1) (dx, 0)
Theorem: SciLean.revDeriv2.pi_rule
Proof state before:
case h.h.h.h
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
f : X → Y → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun xy => f xy.1 xy.2 i
x : X
y : Y
dw : (i : I) → EI i
dx : X
⊢ (dx + (semiAdjoint K (cderiv K (fun x i => f x.1 x.2 i) (x, y)) dw).1,
      (semiAdjoint K (cderiv K (fun x i => f x.1 x.2 i) (x, y)) dw).2) =
    fold (IndexType.univ I)
      (fun dxy i => dxy + (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((x, y), ())) (oneHot i (dw i))).1) (dx, 0)
Tactic:
conv =>
  lhs
  rw[cderiv.pi_rule (hf:=by fun_prop)]
  fun_trans
Proof state after:
case h.h.h.h
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
f : X → Y → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun xy => f xy.1 xy.2 i
x : X
y : Y
dw : (i : I) → EI i
dx : X
⊢ (dx + ( ∑ i, semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2 i) (x, y) x_1) (dw i)).1,
      ( ∑ i, semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2 i) (x, y) x_1) (dw i)).2) =
    fold (IndexType.univ I)
      (fun dxy i => dxy + (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((x, y), ())) (oneHot i (dw i))).1) (dx, 0)
Theorem: SciLean.revDeriv2.pi_rule
Proof state before:
case h.h.h.h
K I : Type
inst✝²¹ : RCLike K
W : Type
inst✝²⁰ : SemiInnerProductSpace K W
X : Type
inst✝¹⁹ : SemiInnerProductSpace K X
Y : Type
inst✝¹⁸ : SemiInnerProductSpace K Y
Z : Type
inst✝¹⁷ : SemiInnerProductSpace K Z
ι : Type
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : Type
EI : I → Type
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)
XI : I → Type
inst✝⁷ : StructType X I XI
inst✝⁶ : (i : I) → SemiInnerProductSpace K (XI i)
YI : I → Type
inst✝⁵ : StructType Y I YI
inst✝⁴ : (i : I) → SemiInnerProductSpace K (YI i)
ZI : I → Type
inst✝³ : StructType Z I ZI
inst✝² : (i : I) → SemiInnerProductSpace K (ZI i)
WI : I → Type
inst✝¹ : StructType W I WI
inst✝ : (i : I) → SemiInnerProductSpace K (WI i)
f : X → Y → (i : I) → EI i
hf : ∀ (i : I), HasAdjDiff K fun xy => f xy.1 xy.2 i
x : X
y : Y
dw : (i : I) → EI i
dx : X
⊢ (dx + ( ∑ i, semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2 i) (x, y) x_1) (dw i)).1,
      ( ∑ i, semiAdjoint K (fun x_1 => cderiv K (fun x => f x.1 x.2 i) (x, y) x_1) (dw i)).2) =
    fold (IndexType.univ I)
      (fun dxy i => dxy + (semiAdjoint K (cderiv K (fun x => f x.1.1 x.1.2) ((x, y), ())) (oneHot i (dw i))).1) (dx, 0)
Tactic:
sorry_proof
Proof state after:
no goals