internlm/Lean-Github huggingface dataset:
Theorem: SciLean.revDeriv2.id2_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)
x : X
w : W
⊢ HasRevDeriv2At K (fun w x => x) (x, fun dy dw => (dw, dy)) w x
Tactic:
constructor
Proof state after:
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)
x : X
w : W
⊢ HasAdjDiffAt K
    (fun x =>
      match x with
      | (w, x) => x)
    (w, x)

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)
x : X
w : W
⊢ revDeriv2 K (fun w x => x) w x = (x, fun dy dw => (dw, dy))
Theorem: SciLean.revDeriv2.id2_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)
x : X
w : W
⊢ HasAdjDiffAt K
    (fun x =>
      match x with
      | (w, x) => x)
    (w, x)

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)
x : X
w : W
⊢ revDeriv2 K (fun w x => x) w x = (x, fun dy dw => (dw, dy))
Tactic:
. fun_prop
Proof state after:
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)
x : X
w : W
⊢ revDeriv2 K (fun w x => x) w x = (x, fun dy dw => (dw, dy))
Theorem: SciLean.revDeriv2.id2_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)
x : X
w : W
⊢ revDeriv2 K (fun w x => x) w x = (x, fun dy dw => (dw, dy))
Tactic:
. fun_trans [revDeriv2]
Proof state after:
no goals
Theorem: SciLean.revDeriv2.id2_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)
x : X
w : W
⊢ HasAdjDiffAt K
    (fun x =>
      match x with
      | (w, x) => x)
    (w, x)
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.revDeriv2.id2_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)
x : X
w : W
⊢ revDeriv2 K (fun w x => x) w x = (x, fun dy dw => (dw, dy))
Tactic:
fun_trans [revDeriv2]
Proof state after:
no goals
Theorem: SciLean.revDeriv2.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
⊢ (revDeriv2 K fun x x => y) = fun w x => (y, fun x dw' => (dw', 0))
Tactic:
unfold 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 =>
      ((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))) =
    fun w x => (y, fun x dw' => (dw', 0))
Theorem: SciLean.revDeriv2.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 =>
      ((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))) =
    fun w x => (y, fun x dw' => (dw', 0))
Tactic:
funext x y
Proof state after:
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)
y✝ : Y
x : W
y : X
⊢ ((fun x x => y✝) x y, 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)
            (x, y))
          dy with
      | (dw, dx) => fun dw' => (dw' + dw, dx)) =
    (y✝, fun x dw' => (dw', 0))
Theorem: SciLean.revDeriv2.const_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)
y✝ : Y
x : W
y : X
⊢ ((fun x x => y✝) x y, 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)
            (x, y))
          dy with
      | (dw, dx) => fun dw' => (dw' + dw, dx)) =
    (y✝, fun x dw' => (dw', 0))
Tactic:
simp
Proof state after:
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)
y✝ : Y
x : W
y : X
⊢ (fun dy dw' =>
      (dw' + (semiAdjoint K (cderiv K (fun x => y✝) (x, y)) dy).1,
        (semiAdjoint K (cderiv K (fun x => y✝) (x, y)) dy).2)) =
    fun x dw' => (dw', 0)
Theorem: SciLean.revDeriv2.const_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)
y✝ : Y
x : W
y : X
⊢ (fun dy dw' =>
      (dw' + (semiAdjoint K (cderiv K (fun x => y✝) (x, y)) dy).1,
        (semiAdjoint K (cderiv K (fun x => y✝) (x, y)) dy).2)) =
    fun x dw' => (dw', 0)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.revDeriv2.const_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
y : Y
⊢ HasRevDeriv2At K (fun w x => y) (y, fun dy dw => (dw, 0)) w x
Tactic:
constructor
Proof state after:
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)

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))
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)

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_prop
Proof state after:
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))