internlm/Lean-Github huggingface dataset:
Theorem: dite.arg_te.revDerivProjUpdate_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
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
c : Prop
t : c → X → Y'
e : ¬c → X → Y'
h : c
⊢ (revDerivProjUpdate K Yi fun x => if x_1 : c then t x_1 x else e x_1 x) = fun y =>
    if p : c then revDerivProjUpdate K Yi (t p) y else revDerivProjUpdate K Yi (e p) y
Tactic:
ext y <;> simp[h]
Proof state after:
no goals
Theorem: dite.arg_te.revDerivProjUpdate_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
X' Xi : Type
XI : Xi → Type
inst✝²³ : StructType X' Xi XI
inst✝²² : IndexType Xi
inst✝²¹ : LawfulIndexType Xi
inst✝²⁰ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝¹⁹ : StructType Y' Yi YI
inst✝¹⁸ : IndexType Yi
inst✝¹⁷ : LawfulIndexType Yi
inst✝¹⁶ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁵ : StructType Z' Zi ZI
inst✝¹⁴ : IndexType Zi
inst✝¹³ : LawfulIndexType Zi
inst✝¹² : DecidableEq Zi
inst✝¹¹ : SemiInnerProductSpace K X'
inst✝¹⁰ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝⁹ : SemiInnerProductSpaceStruct K X' Xi XI
inst✝⁸ : SemiInnerProductSpace K Y'
inst✝⁷ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁵ : SemiInnerProductSpace K Z'
inst✝⁴ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝³ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝² : SemiInnerProductSpace K W
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
c : Prop
t : c → X → Y'
e : ¬c → X → Y'
h : ¬c
⊢ (revDerivProjUpdate K Yi fun x => if x_1 : c then t x_1 x else e x_1 x) = fun y =>
    if p : c then revDerivProjUpdate K Yi (t p) y else revDerivProjUpdate K Yi (e p) y
Tactic:
ext y <;> simp[h]
Proof state after:
no goals
Theorem: Inner.inner.arg_a0a1.revDeriv_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
X' Xi : Type
XI : Xi → Type
inst✝²⁶ : StructType X' Xi XI
inst✝²⁵ : IndexType Xi
inst✝²⁴ : LawfulIndexType Xi
inst✝²³ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝²² : StructType Y' Yi YI
inst✝²¹ : IndexType Yi
inst✝²⁰ : LawfulIndexType Yi
inst✝¹⁹ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁸ : StructType Z' Zi ZI
inst✝¹⁷ : IndexType Zi
inst✝¹⁶ : LawfulIndexType Zi
inst✝¹⁵ : DecidableEq Zi
inst✝¹⁴ : SemiInnerProductSpace K X'
inst✝¹³ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹² : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹¹ : SemiInnerProductSpace K Y'
inst✝¹⁰ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁹ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁸ : SemiInnerProductSpace K Z'
inst✝⁷ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁵ : SemiInnerProductSpace K W
ι : Type
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : HasAdjDiff R f
hg : HasAdjDiff R g
⊢ (revDeriv R fun x => ⟪f x, g x⟫_R) = fun x =>
    let y₁df := revDeriv R f x;
    let y₂dg := revDerivUpdate R g x;
    (⟪y₁df.1, y₂dg.1⟫_R, fun dr => y₂dg.2 (dr • y₁df.1) (y₁df.2 (dr • y₂dg.1)))
Tactic:
funext
Proof state after:
case h
K : Type
inst✝³⁰ : RCLike K
X✝ : Type
inst✝²⁹ : SemiInnerProductSpace K X✝
Y✝ : Type
inst✝²⁸ : SemiInnerProductSpace K Y✝
Z : Type
inst✝²⁷ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²⁶ : StructType X' Xi XI
inst✝²⁵ : IndexType Xi
inst✝²⁴ : LawfulIndexType Xi
inst✝²³ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝²² : StructType Y' Yi YI
inst✝²¹ : IndexType Yi
inst✝²⁰ : LawfulIndexType Yi
inst✝¹⁹ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁸ : StructType Z' Zi ZI
inst✝¹⁷ : IndexType Zi
inst✝¹⁶ : LawfulIndexType Zi
inst✝¹⁵ : DecidableEq Zi
inst✝¹⁴ : SemiInnerProductSpace K X'
inst✝¹³ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹² : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹¹ : SemiInnerProductSpace K Y'
inst✝¹⁰ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁹ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁸ : SemiInnerProductSpace K Z'
inst✝⁷ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁵ : SemiInnerProductSpace K W
ι : Type
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : HasAdjDiff R f
hg : HasAdjDiff R g
x✝ : X
⊢ revDeriv R (fun x => ⟪f x, g x⟫_R) x✝ =
    let y₁df := revDeriv R f x✝;
    let y₂dg := revDerivUpdate R g x✝;
    (⟪y₁df.1, y₂dg.1⟫_R, fun dr => y₂dg.2 (dr • y₁df.1) (y₁df.2 (dr • y₂dg.1)))
Theorem: Inner.inner.arg_a0a1.revDeriv_rule
Proof state before:
case h
K : Type
inst✝³⁰ : RCLike K
X✝ : Type
inst✝²⁹ : SemiInnerProductSpace K X✝
Y✝ : Type
inst✝²⁸ : SemiInnerProductSpace K Y✝
Z : Type
inst✝²⁷ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²⁶ : StructType X' Xi XI
inst✝²⁵ : IndexType Xi
inst✝²⁴ : LawfulIndexType Xi
inst✝²³ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝²² : StructType Y' Yi YI
inst✝²¹ : IndexType Yi
inst✝²⁰ : LawfulIndexType Yi
inst✝¹⁹ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁸ : StructType Z' Zi ZI
inst✝¹⁷ : IndexType Zi
inst✝¹⁶ : LawfulIndexType Zi
inst✝¹⁵ : DecidableEq Zi
inst✝¹⁴ : SemiInnerProductSpace K X'
inst✝¹³ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹² : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹¹ : SemiInnerProductSpace K Y'
inst✝¹⁰ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁹ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁸ : SemiInnerProductSpace K Z'
inst✝⁷ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁵ : SemiInnerProductSpace K W
ι : Type
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : HasAdjDiff R f
hg : HasAdjDiff R g
x✝ : X
⊢ revDeriv R (fun x => ⟪f x, g x⟫_R) x✝ =
    let y₁df := revDeriv R f x✝;
    let y₂dg := revDerivUpdate R g x✝;
    (⟪y₁df.1, y₂dg.1⟫_R, fun dr => y₂dg.2 (dr • y₁df.1) (y₁df.2 (dr • y₂dg.1)))
Tactic:
simp[revDeriv,revDerivUpdate]
Proof state after:
case h
K : Type
inst✝³⁰ : RCLike K
X✝ : Type
inst✝²⁹ : SemiInnerProductSpace K X✝
Y✝ : Type
inst✝²⁸ : SemiInnerProductSpace K Y✝
Z : Type
inst✝²⁷ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²⁶ : StructType X' Xi XI
inst✝²⁵ : IndexType Xi
inst✝²⁴ : LawfulIndexType Xi
inst✝²³ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝²² : StructType Y' Yi YI
inst✝²¹ : IndexType Yi
inst✝²⁰ : LawfulIndexType Yi
inst✝¹⁹ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁸ : StructType Z' Zi ZI
inst✝¹⁷ : IndexType Zi
inst✝¹⁶ : LawfulIndexType Zi
inst✝¹⁵ : DecidableEq Zi
inst✝¹⁴ : SemiInnerProductSpace K X'
inst✝¹³ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹² : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹¹ : SemiInnerProductSpace K Y'
inst✝¹⁰ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁹ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁸ : SemiInnerProductSpace K Z'
inst✝⁷ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁵ : SemiInnerProductSpace K W
ι : Type
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : HasAdjDiff R f
hg : HasAdjDiff R g
x✝ : X
⊢ semiAdjoint R (cderiv R (fun x => ⟪f x, g x⟫_R) x✝) = fun dr =>
    semiAdjoint R (cderiv R f x✝) (dr • g x✝) + semiAdjoint R (cderiv R g x✝) (dr • f x✝)
Theorem: Inner.inner.arg_a0a1.revDeriv_rule
Proof state before:
case h
K : Type
inst✝³⁰ : RCLike K
X✝ : Type
inst✝²⁹ : SemiInnerProductSpace K X✝
Y✝ : Type
inst✝²⁸ : SemiInnerProductSpace K Y✝
Z : Type
inst✝²⁷ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²⁶ : StructType X' Xi XI
inst✝²⁵ : IndexType Xi
inst✝²⁴ : LawfulIndexType Xi
inst✝²³ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝²² : StructType Y' Yi YI
inst✝²¹ : IndexType Yi
inst✝²⁰ : LawfulIndexType Yi
inst✝¹⁹ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁸ : StructType Z' Zi ZI
inst✝¹⁷ : IndexType Zi
inst✝¹⁶ : LawfulIndexType Zi
inst✝¹⁵ : DecidableEq Zi
inst✝¹⁴ : SemiInnerProductSpace K X'
inst✝¹³ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹² : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹¹ : SemiInnerProductSpace K Y'
inst✝¹⁰ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁹ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁸ : SemiInnerProductSpace K Z'
inst✝⁷ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁵ : SemiInnerProductSpace K W
ι : Type
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : HasAdjDiff R f
hg : HasAdjDiff R g
x✝ : X
⊢ semiAdjoint R (cderiv R (fun x => ⟪f x, g x⟫_R) x✝) = fun dr =>
    semiAdjoint R (cderiv R f x✝) (dr • g x✝) + semiAdjoint R (cderiv R g x✝) (dr • f x✝)
Tactic:
fun_trans[smul_pull]
Proof state after:
no goals
Theorem: Inner.inner.arg_a0a1.revDerivUpdate_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
X' Xi : Type
XI : Xi → Type
inst✝²⁶ : StructType X' Xi XI
inst✝²⁵ : IndexType Xi
inst✝²⁴ : LawfulIndexType Xi
inst✝²³ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝²² : StructType Y' Yi YI
inst✝²¹ : IndexType Yi
inst✝²⁰ : LawfulIndexType Yi
inst✝¹⁹ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁸ : StructType Z' Zi ZI
inst✝¹⁷ : IndexType Zi
inst✝¹⁶ : LawfulIndexType Zi
inst✝¹⁵ : DecidableEq Zi
inst✝¹⁴ : SemiInnerProductSpace K X'
inst✝¹³ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹² : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹¹ : SemiInnerProductSpace K Y'
inst✝¹⁰ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁹ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁸ : SemiInnerProductSpace K Z'
inst✝⁷ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁵ : SemiInnerProductSpace K W
ι : Type
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : HasAdjDiff R f
hg : HasAdjDiff R g
⊢ (fun x =>
      (⟪f x, g x⟫_R, fun dy dx =>
        dx + (revDerivUpdate R (fun x => g x) x).2 (dy • f x) ((revDeriv R (fun x => f x) x).2 (dy • g x)))) =
    fun x => (⟪f x, g x⟫_R, fun dr dx => dx + (revDeriv R f x).2 (dr • g x) + (revDeriv R g x).2 (dr • f x))
Tactic:
simp[revDerivUpdate,add_assoc]
Proof state after:
no goals
Theorem: Inner.inner.arg_a0a1.revDerivProj_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
X' Xi : Type
XI : Xi → Type
inst✝²⁶ : StructType X' Xi XI
inst✝²⁵ : IndexType Xi
inst✝²⁴ : LawfulIndexType Xi
inst✝²³ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝²² : StructType Y' Yi YI
inst✝²¹ : IndexType Yi
inst✝²⁰ : LawfulIndexType Yi
inst✝¹⁹ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁸ : StructType Z' Zi ZI
inst✝¹⁷ : IndexType Zi
inst✝¹⁶ : LawfulIndexType Zi
inst✝¹⁵ : DecidableEq Zi
inst✝¹⁴ : SemiInnerProductSpace K X'
inst✝¹³ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹² : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹¹ : SemiInnerProductSpace K Y'
inst✝¹⁰ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁹ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁸ : SemiInnerProductSpace K Z'
inst✝⁷ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁵ : SemiInnerProductSpace K W
ι : Type
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : HasAdjDiff R f
hg : HasAdjDiff R g
⊢ (revDerivProj R Unit fun x => ⟪f x, g x⟫_R) = fun x =>
    let y₁df := revDeriv R f x;
    let y₂dg := revDerivUpdate R g x;
    (⟪y₁df.1, y₂dg.1⟫_R, fun x dr => y₂dg.2 (dr • y₁df.1) (y₁df.2 (dr • y₂dg.1)))
Tactic:
funext
Proof state after:
case h
K : Type
inst✝³⁰ : RCLike K
X✝ : Type
inst✝²⁹ : SemiInnerProductSpace K X✝
Y✝ : Type
inst✝²⁸ : SemiInnerProductSpace K Y✝
Z : Type
inst✝²⁷ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²⁶ : StructType X' Xi XI
inst✝²⁵ : IndexType Xi
inst✝²⁴ : LawfulIndexType Xi
inst✝²³ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝²² : StructType Y' Yi YI
inst✝²¹ : IndexType Yi
inst✝²⁰ : LawfulIndexType Yi
inst✝¹⁹ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁸ : StructType Z' Zi ZI
inst✝¹⁷ : IndexType Zi
inst✝¹⁶ : LawfulIndexType Zi
inst✝¹⁵ : DecidableEq Zi
inst✝¹⁴ : SemiInnerProductSpace K X'
inst✝¹³ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹² : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹¹ : SemiInnerProductSpace K Y'
inst✝¹⁰ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁹ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁸ : SemiInnerProductSpace K Z'
inst✝⁷ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁵ : SemiInnerProductSpace K W
ι : Type
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : HasAdjDiff R f
hg : HasAdjDiff R g
x✝ : X
⊢ revDerivProj R Unit (fun x => ⟪f x, g x⟫_R) x✝ =
    let y₁df := revDeriv R f x✝;
    let y₂dg := revDerivUpdate R g x✝;
    (⟪y₁df.1, y₂dg.1⟫_R, fun x dr => y₂dg.2 (dr • y₁df.1) (y₁df.2 (dr • y₂dg.1)))
Theorem: Inner.inner.arg_a0a1.revDerivProj_rule
Proof state before:
case h
K : Type
inst✝³⁰ : RCLike K
X✝ : Type
inst✝²⁹ : SemiInnerProductSpace K X✝
Y✝ : Type
inst✝²⁸ : SemiInnerProductSpace K Y✝
Z : Type
inst✝²⁷ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²⁶ : StructType X' Xi XI
inst✝²⁵ : IndexType Xi
inst✝²⁴ : LawfulIndexType Xi
inst✝²³ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝²² : StructType Y' Yi YI
inst✝²¹ : IndexType Yi
inst✝²⁰ : LawfulIndexType Yi
inst✝¹⁹ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁸ : StructType Z' Zi ZI
inst✝¹⁷ : IndexType Zi
inst✝¹⁶ : LawfulIndexType Zi
inst✝¹⁵ : DecidableEq Zi
inst✝¹⁴ : SemiInnerProductSpace K X'
inst✝¹³ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹² : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹¹ : SemiInnerProductSpace K Y'
inst✝¹⁰ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁹ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁸ : SemiInnerProductSpace K Z'
inst✝⁷ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁵ : SemiInnerProductSpace K W
ι : Type
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : HasAdjDiff R f
hg : HasAdjDiff R g
x✝ : X
⊢ revDerivProj R Unit (fun x => ⟪f x, g x⟫_R) x✝ =
    let y₁df := revDeriv R f x✝;
    let y₂dg := revDerivUpdate R g x✝;
    (⟪y₁df.1, y₂dg.1⟫_R, fun x dr => y₂dg.2 (dr • y₁df.1) (y₁df.2 (dr • y₂dg.1)))
Tactic:
simp[revDerivProj]
Proof state after:
case h
K : Type
inst✝³⁰ : RCLike K
X✝ : Type
inst✝²⁹ : SemiInnerProductSpace K X✝
Y✝ : Type
inst✝²⁸ : SemiInnerProductSpace K Y✝
Z : Type
inst✝²⁷ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²⁶ : StructType X' Xi XI
inst✝²⁵ : IndexType Xi
inst✝²⁴ : LawfulIndexType Xi
inst✝²³ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝²² : StructType Y' Yi YI
inst✝²¹ : IndexType Yi
inst✝²⁰ : LawfulIndexType Yi
inst✝¹⁹ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁸ : StructType Z' Zi ZI
inst✝¹⁷ : IndexType Zi
inst✝¹⁶ : LawfulIndexType Zi
inst✝¹⁵ : DecidableEq Zi
inst✝¹⁴ : SemiInnerProductSpace K X'
inst✝¹³ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹² : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹¹ : SemiInnerProductSpace K Y'
inst✝¹⁰ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁹ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁸ : SemiInnerProductSpace K Z'
inst✝⁷ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁵ : SemiInnerProductSpace K W
ι : Type
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : HasAdjDiff R f
hg : HasAdjDiff R g
x✝ : X
⊢ (fun i de => (revDeriv R (fun x => ⟪f x, g x⟫_R) x✝).2 (oneHot i de)) = fun x dr =>
    (revDerivUpdate R g x✝).2 (dr • f x✝) ((revDeriv R f x✝).2 (dr • g x✝))
Theorem: Inner.inner.arg_a0a1.revDerivProj_rule
Proof state before:
case h
K : Type
inst✝³⁰ : RCLike K
X✝ : Type
inst✝²⁹ : SemiInnerProductSpace K X✝
Y✝ : Type
inst✝²⁸ : SemiInnerProductSpace K Y✝
Z : Type
inst✝²⁷ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²⁶ : StructType X' Xi XI
inst✝²⁵ : IndexType Xi
inst✝²⁴ : LawfulIndexType Xi
inst✝²³ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝²² : StructType Y' Yi YI
inst✝²¹ : IndexType Yi
inst✝²⁰ : LawfulIndexType Yi
inst✝¹⁹ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁸ : StructType Z' Zi ZI
inst✝¹⁷ : IndexType Zi
inst✝¹⁶ : LawfulIndexType Zi
inst✝¹⁵ : DecidableEq Zi
inst✝¹⁴ : SemiInnerProductSpace K X'
inst✝¹³ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹² : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹¹ : SemiInnerProductSpace K Y'
inst✝¹⁰ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁹ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁸ : SemiInnerProductSpace K Z'
inst✝⁷ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁵ : SemiInnerProductSpace K W
ι : Type
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : HasAdjDiff R f
hg : HasAdjDiff R g
x✝ : X
⊢ (fun i de => (revDeriv R (fun x => ⟪f x, g x⟫_R) x✝).2 (oneHot i de)) = fun x dr =>
    (revDerivUpdate R g x✝).2 (dr • f x✝) ((revDeriv R f x✝).2 (dr • g x✝))
Tactic:
fun_trans
Proof state after:
case h
K : Type
inst✝³⁰ : RCLike K
X✝ : Type
inst✝²⁹ : SemiInnerProductSpace K X✝
Y✝ : Type
inst✝²⁸ : SemiInnerProductSpace K Y✝
Z : Type
inst✝²⁷ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²⁶ : StructType X' Xi XI
inst✝²⁵ : IndexType Xi
inst✝²⁴ : LawfulIndexType Xi
inst✝²³ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝²² : StructType Y' Yi YI
inst✝²¹ : IndexType Yi
inst✝²⁰ : LawfulIndexType Yi
inst✝¹⁹ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁸ : StructType Z' Zi ZI
inst✝¹⁷ : IndexType Zi
inst✝¹⁶ : LawfulIndexType Zi
inst✝¹⁵ : DecidableEq Zi
inst✝¹⁴ : SemiInnerProductSpace K X'
inst✝¹³ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹² : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹¹ : SemiInnerProductSpace K Y'
inst✝¹⁰ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁹ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁸ : SemiInnerProductSpace K Z'
inst✝⁷ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁵ : SemiInnerProductSpace K W
ι : Type
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : HasAdjDiff R f
hg : HasAdjDiff R g
x✝ : X
⊢ (fun i de =>
      (revDerivUpdate R (fun x => g x) x✝).2 (oneHot i de • f x✝)
        ((revDeriv R (fun x => f x) x✝).2 (oneHot i de • g x✝))) =
    fun x dr => (revDerivUpdate R g x✝).2 (dr • f x✝) ((revDeriv R f x✝).2 (dr • g x✝))
Theorem: Inner.inner.arg_a0a1.revDerivProj_rule
Proof state before:
case h
K : Type
inst✝³⁰ : RCLike K
X✝ : Type
inst✝²⁹ : SemiInnerProductSpace K X✝
Y✝ : Type
inst✝²⁸ : SemiInnerProductSpace K Y✝
Z : Type
inst✝²⁷ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²⁶ : StructType X' Xi XI
inst✝²⁵ : IndexType Xi
inst✝²⁴ : LawfulIndexType Xi
inst✝²³ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝²² : StructType Y' Yi YI
inst✝²¹ : IndexType Yi
inst✝²⁰ : LawfulIndexType Yi
inst✝¹⁹ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁸ : StructType Z' Zi ZI
inst✝¹⁷ : IndexType Zi
inst✝¹⁶ : LawfulIndexType Zi
inst✝¹⁵ : DecidableEq Zi
inst✝¹⁴ : SemiInnerProductSpace K X'
inst✝¹³ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹² : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹¹ : SemiInnerProductSpace K Y'
inst✝¹⁰ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁹ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁸ : SemiInnerProductSpace K Z'
inst✝⁷ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁵ : SemiInnerProductSpace K W
ι : Type
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : HasAdjDiff R f
hg : HasAdjDiff R g
x✝ : X
⊢ (fun i de =>
      (revDerivUpdate R (fun x => g x) x✝).2 (oneHot i de • f x✝)
        ((revDeriv R (fun x => f x) x✝).2 (oneHot i de • g x✝))) =
    fun x dr => (revDerivUpdate R g x✝).2 (dr • f x✝) ((revDeriv R f x✝).2 (dr • g x✝))
Tactic:
simp[oneHot, structMake]
Proof state after:
no goals