internlm/Lean-Github huggingface dataset:
Theorem: SciLean.revDeriv2.pi_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 : 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
⊢ ∀ (i : I), CDifferentiable K fun x => f x.1 x.2 i
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.revDeriv2Proj.id1_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)
⊢ (revDeriv2Proj K I fun w x => w) = fun w x i =>
    (structProj w i, fun dwi dw' => (structModify i (fun wi => wi + dwi) dw', 0))
Tactic:
unfold revDeriv2Proj
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)
⊢ (fun w x i =>
      let ydf := revDeriv2 K (fun w x => w) w x;
      (structProj ydf.1 i, fun dyi => ydf.2 (oneHot i dyi))) =
    fun w x i => (structProj w i, fun dwi dw' => (structModify i (fun wi => wi + dwi) dw', 0))
Theorem: SciLean.revDeriv2Proj.id1_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)
⊢ (fun w x i =>
      let ydf := revDeriv2 K (fun w x => w) w x;
      (structProj ydf.1 i, fun dyi => ydf.2 (oneHot i dyi))) =
    fun w x i => (structProj w i, fun dwi dw' => (structModify i (fun wi => wi + dwi) dw', 0))
Tactic:
simp[revDeriv2.id1_rule K]
Proof state after:
no goals
Theorem: SciLean.revDeriv2Proj.id2_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)
⊢ (revDeriv2Proj K I fun w x => x) = fun w x i => (structProj x i, fun dxi dw' => (dw', oneHot i dxi))
Tactic:
unfold revDeriv2Proj
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)
⊢ (fun w x i =>
      let ydf := revDeriv2 K (fun w x => x) w x;
      (structProj ydf.1 i, fun dyi => ydf.2 (oneHot i dyi))) =
    fun w x i => (structProj x i, fun dxi dw' => (dw', oneHot i dxi))
Theorem: SciLean.revDeriv2Proj.id2_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)
⊢ (fun w x i =>
      let ydf := revDeriv2 K (fun w x => x) w x;
      (structProj ydf.1 i, fun dyi => ydf.2 (oneHot i dyi))) =
    fun w x i => (structProj x i, fun dxi dw' => (dw', oneHot i dxi))
Tactic:
simp (config:={zeta:=false}) [revDeriv2.id2_rule K]
Proof state after:
no goals
Theorem: SciLean.revDeriv2Proj.const_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)
y : Y
⊢ (revDeriv2Proj K I fun x x => y) = fun w x i => (structProj y i, fun x dw' => (dw', 0))
Tactic:
unfold revDeriv2Proj revDeriv2
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)
y : Y
⊢ (fun w x i =>
      let ydf :=
        ((fun x x => y) w x, fun dy =>
          match (motive := W × X → W → W × X)
            semiAdjoint K
              (cderiv K
                (fun x =>
                  match x with
                  | (w, x) => (fun x x => y) w x)
                (w, x))
              dy with
          | (dw, dx) => fun dw' => (dw' + dw, dx));
      (structProj ydf.1 i, fun dyi => ydf.2 (oneHot i dyi))) =
    fun w x i => (structProj y i, fun x dw' => (dw', 0))
Theorem: SciLean.revDeriv2Proj.const_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)
y : Y
⊢ (fun w x i =>
      let ydf :=
        ((fun x x => y) w x, fun dy =>
          match (motive := W × X → W → W × X)
            semiAdjoint K
              (cderiv K
                (fun x =>
                  match x with
                  | (w, x) => (fun x x => y) w x)
                (w, x))
              dy with
          | (dw, dx) => fun dw' => (dw' + dw, dx));
      (structProj ydf.1 i, fun dyi => ydf.2 (oneHot i dyi))) =
    fun w x i => (structProj y i, fun x dw' => (dw', 0))
Tactic:
fun_trans[semiAdjoint.const_rule]
Proof state after:
no goals
Theorem: SciLean.revDeriv2Proj.let_rule
Proof state before:
case h.h.h.h.h.a
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
w : W
x : X
i : I
dz : ZI i
dw : W
⊢ (dw +
          ((semiAdjoint K
                (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x) dx8)
                (structMake fun i' => if h : i = i' then h ▸ dz else 0)).1 +
            (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1)
                (semiAdjoint K
                      (fun dx8 =>
                        cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x) dx8)
                      (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.2).1),
        (semiAdjoint K
                (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x) dx8)
                (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.1 +
          (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1)
              (semiAdjoint K
                    (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x) dx8)
                    (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.2).2).2 =
    ((dw +
            (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x))
                (structMake fun i' => if h : i = i' then h ▸ dz else 0)).1,
          (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x))
                (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.1) +
        (semiAdjoint K (cderiv K (fun x => g x.1.1 x.1.2) ((w, x), ()))
            (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x))
                  (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.2).1).2
Tactic:
. simp; sorry_proof
Proof state after:
no goals
Theorem: SciLean.revDeriv2Proj.let_rule
Proof state before:
case h.h.h.h.h.a
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
w : W
x : X
i : I
dz : ZI i
dw : W
⊢ dw +
      ((semiAdjoint K
            (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x) dx8)
            (structMake fun i' => if h : i = i' then h ▸ dz else 0)).1 +
        (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1)
            (semiAdjoint K
                  (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x) dx8)
                  (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.2).1) =
    dw +
        (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x))
            (structMake fun i' => if h : i = i' then h ▸ dz else 0)).1 +
      (semiAdjoint K (cderiv K (fun x => g x.1.1 x.1.2) ((w, x), ()))
            (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x))
                  (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.2).1.1
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.revDeriv2Proj.let_rule
Proof state before:
case h.h.h.h.h.a
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
w : W
x : X
i : I
dz : ZI i
dw : W
⊢ (semiAdjoint K (fun x_1 => cderiv K (fun x => g x.1 x.2) (w, x) x_1)
        (semiAdjoint K
              (fun dx8 => cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x) dx8)
              (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.2).2 =
    (semiAdjoint K (cderiv K (fun x => g x.1.1 x.1.2) ((w, x), ()))
          (semiAdjoint K (cderiv K (fun xy0xy1xy2 => f xy0xy1xy2.1 xy0xy1xy2.2.1 xy0xy1xy2.2.2) (w, x, g w x))
                (structMake fun i' => if h : i = i' then h ▸ dz else 0)).2.2).1.2
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Prod.mk.arg_fstsnd.revDeriv2_rule
Proof state before:
K : Type
inst✝⁴ : RCLike K
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => g w x
hf :
  HasAdjDiff K fun x =>
    match x with
    | (w, x) => f w x
⊢ (revDeriv2 K fun w x => (g w x, f w x)) = fun w x =>
    let ydg := revDeriv2 K g w x;
    let zdf :=
      revDeriv2 K
        (fun x x_1 =>
          match x with
          | (w, x) => f w x)
        (w, x) ();
    ((ydg.1, zdf.1), fun dyz dw =>
      let dwx := ydg.2 dyz.1 dw;
      (zdf.2 dyz.2 dwx).1)
Tactic:
simp at hf hg
Proof state after:
K : Type
inst✝⁴ : RCLike K
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
⊢ (revDeriv2 K fun w x => (g w x, f w x)) = fun w x =>
    let ydg := revDeriv2 K g w x;
    let zdf :=
      revDeriv2 K
        (fun x x_1 =>
          match x with
          | (w, x) => f w x)
        (w, x) ();
    ((ydg.1, zdf.1), fun dyz dw =>
      let dwx := ydg.2 dyz.1 dw;
      (zdf.2 dyz.2 dwx).1)
Theorem: Prod.mk.arg_fstsnd.revDeriv2_rule
Proof state before:
K : Type
inst✝⁴ : RCLike K
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
⊢ (revDeriv2 K fun w x => (g w x, f w x)) = fun w x =>
    let ydg := revDeriv2 K g w x;
    let zdf :=
      revDeriv2 K
        (fun x x_1 =>
          match x with
          | (w, x) => f w x)
        (w, x) ();
    ((ydg.1, zdf.1), fun dyz dw =>
      let dwx := ydg.2 dyz.1 dw;
      (zdf.2 dyz.2 dwx).1)
Tactic:
unfold revDeriv2
Proof state after:
K : Type
inst✝⁴ : RCLike K
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
W : Type
inst✝ : SemiInnerProductSpace K W
g : W → X → Y
f : W → X → Z
hg : HasAdjDiff K fun x => g x.1 x.2
hf : HasAdjDiff K fun x => f x.1 x.2
⊢ (fun w x =>
      ((fun w x => (g w x, f w x)) w x, fun dy =>
        match (motive := W × X → W → W × X)
          semiAdjoint K
            (cderiv K
              (fun x =>
                match x with
                | (w, x) => (fun w x => (g w x, f w x)) w x)
              (w, x))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx))) =
    fun w x =>
    let ydg :=
      (g w x, fun dy =>
        match (motive := W × X → W → W × X)
          semiAdjoint K
            (cderiv K
              (fun x =>
                match x with
                | (w, x) => g w x)
              (w, x))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx));
    let zdf :=
      ((fun x x_1 =>
            match x with
            | (w, x) => f w x)
          (w, x) (),
        fun dy =>
        match (motive := (W × X) × Unit → W × X → (W × X) × Unit)
          semiAdjoint K
            (cderiv K
              (fun x =>
                match x with
                | (w, x) =>
                  (fun x x_1 =>
                      match x with
                      | (w, x) => f w x)
                    w x)
              ((w, x), ()))
            dy with
        | (dw, dx) => fun dw' => (dw' + dw, dx));
    ((ydg.1, zdf.1), fun dyz dw =>
      let dwx := ydg.2 dyz.1 dw;
      (zdf.2 dyz.2 dwx).1)