internlm/Lean-Github huggingface dataset:
Theorem: HDiv.hDiv.arg_a0a1.revDerivUpdate_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 ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
hx : ∀ (x : X), g x ≠ 0
x✝ : X
⊢ (fun dy dx => dx + (revDeriv K (fun x => f x / g x) x✝).2 dy) = fun dx' dx =>
    dx + (revDeriv K f x✝).2 (((starRingEnd K) (g x✝) ^ 2)⁻¹ * (starRingEnd K) (g x✝) * dx') +
      (revDeriv K g x✝).2 (-(((starRingEnd K) (g x✝) ^ 2)⁻¹ * (starRingEnd K) (f x✝) * dx'))
Tactic:
fun_trans (disch:=assumption)
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 ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
hx : ∀ (x : X), g x ≠ 0
x✝ : X
⊢ (fun dy dx =>
      dx +
        ((starRingEnd K) (g x✝) ^ 2)⁻¹ •
          (revDerivUpdate K (fun x => g x) x✝).2 (-((starRingEnd K) (f x✝) * dy))
            ((starRingEnd K) (g x✝) • (revDeriv K (fun x => f x) x✝).2 dy)) =
    fun dx' dx =>
    dx + (revDeriv K f x✝).2 (((starRingEnd K) (g x✝) ^ 2)⁻¹ * (starRingEnd K) (g x✝) * dx') +
      (revDeriv K g x✝).2 (-(((starRingEnd K) (g x✝) ^ 2)⁻¹ * (starRingEnd K) (f x✝) * dx'))
Theorem: HDiv.hDiv.arg_a0a1.revDerivUpdate_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 ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
hx : ∀ (x : X), g x ≠ 0
x✝ : X
⊢ (fun dy dx =>
      dx +
        ((starRingEnd K) (g x✝) ^ 2)⁻¹ •
          (revDerivUpdate K (fun x => g x) x✝).2 (-((starRingEnd K) (f x✝) * dy))
            ((starRingEnd K) (g x✝) • (revDeriv K (fun x => f x) x✝).2 dy)) =
    fun dx' dx =>
    dx + (revDeriv K f x✝).2 (((starRingEnd K) (g x✝) ^ 2)⁻¹ * (starRingEnd K) (g x✝) * dx') +
      (revDeriv K g x✝).2 (-(((starRingEnd K) (g x✝) ^ 2)⁻¹ * (starRingEnd K) (f x✝) * dx'))
Tactic:
simp[revDerivUpdate,smul_push,neg_pull,revDeriv,smul_add,smul_sub,add_assoc,mul_assoc]
Proof state after:
no goals
Theorem: HDiv.hDiv.arg_a0a1.revDerivUpdate_rule
Proof state before:
case funProp.discharger
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 ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
hx : ∀ (x : X), g x ≠ 0
x✝ : X
dy : K
dx : X
⊢ ∀ (x : X), g x ≠ 0
Tactic:
assumption
Proof state after:
no goals
Theorem: HDiv.hDiv.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 ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
hx : ∀ (x : X), g x ≠ 0
⊢ (revDerivProj K Unit fun x => f x / g x) = fun x =>
    let ydf := revDeriv K f x;
    let zdg := revDerivUpdate K g x;
    (ydf.1 / zdg.1, fun x dx' =>
      (1 / (starRingEnd K) zdg.1 ^ 2) • zdg.2 (-(starRingEnd K) ydf.1 • dx') ((starRingEnd K) zdg.1 • ydf.2 dx'))
Tactic:
unfold revDerivProj
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
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 ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
hx : ∀ (x : X), g x ≠ 0
⊢ (fun x =>
      let ydf' := revDeriv K (fun x => f x / g x) x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun x =>
    let ydf := revDeriv K f x;
    let zdg := revDerivUpdate K g x;
    (ydf.1 / zdg.1, fun x dx' =>
      (1 / (starRingEnd K) zdg.1 ^ 2) • zdg.2 (-(starRingEnd K) ydf.1 • dx') ((starRingEnd K) zdg.1 • ydf.2 dx'))
Theorem: HDiv.hDiv.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 ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
hx : ∀ (x : X), g x ≠ 0
⊢ (fun x =>
      (f x / g x, fun i de =>
        ((starRingEnd K) (g x) ^ 2)⁻¹ •
          (revDerivUpdate K (fun x => g x) x).2 (-((starRingEnd K) (f x) * oneHot i de))
            ((starRingEnd K) (g x) • (revDeriv K (fun x => f x) x).2 (oneHot i de)))) =
    fun x =>
    (f x / g x, fun x_1 dx' =>
      ((starRingEnd K) (g x) ^ 2)⁻¹ •
        (revDerivUpdate K g x).2 (-((starRingEnd K) (f x) * dx')) ((starRingEnd K) (g x) • (revDeriv K f x).2 dx'))
Tactic:
simp[oneHot, structMake]
Proof state after:
no goals
Theorem: HDiv.hDiv.arg_a0a1.revDerivProj_rule
Proof state before:
case funProp.discharger
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 ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
hx : ∀ (x : X), g x ≠ 0
x : X
⊢ ∀ (x : X), g x ≠ 0
Tactic:
assumption
Proof state after:
no goals
Theorem: HDiv.hDiv.arg_a0a1.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 ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
hx : ∀ (x : X), g x ≠ 0
⊢ (revDerivProjUpdate K Unit fun x => f x / g x) = fun x =>
    let ydf := revDerivUpdate K f x;
    let zdg := revDerivUpdate K g x;
    (ydf.1 / zdg.1, fun x dx' dx =>
      let c := 1 / (starRingEnd K) zdg.1 ^ 2;
      let a := -(c * (starRingEnd K) ydf.1);
      let b := c * (starRingEnd K) zdg.1;
      zdg.2 (a • dx') (ydf.2 (b • dx') dx))
Tactic:
unfold revDerivProjUpdate
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
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 ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
hx : ∀ (x : X), g x ≠ 0
⊢ (fun x =>
      let ydf' := revDerivProj K Unit (fun x => f x / g x) x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de)) =
    fun x =>
    let ydf := revDerivUpdate K f x;
    let zdg := revDerivUpdate K g x;
    (ydf.1 / zdg.1, fun x dx' dx =>
      let c := 1 / (starRingEnd K) zdg.1 ^ 2;
      let a := -(c * (starRingEnd K) ydf.1);
      let b := c * (starRingEnd K) zdg.1;
      zdg.2 (a • dx') (ydf.2 (b • dx') dx))
Theorem: HDiv.hDiv.arg_a0a1.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 ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
hx : ∀ (x : X), g x ≠ 0
⊢ (fun x =>
      (f x / g x, fun i de dx =>
        dx +
          ((starRingEnd K) (g x) ^ 2)⁻¹ •
            (revDerivUpdate K (fun x => g x) x).2 (-((starRingEnd K) (f x) * de))
              ((starRingEnd K) (g x) • (revDeriv K (fun x => f x) x).2 de))) =
    fun x =>
    (f x / g x, fun x_1 dx' dx =>
      (revDerivUpdate K g x).2 (-(((starRingEnd K) (g x) ^ 2)⁻¹ * (starRingEnd K) (f x) * dx'))
        ((revDerivUpdate K f x).2 (((starRingEnd K) (g x) ^ 2)⁻¹ * (starRingEnd K) (g x) * dx') dx))
Tactic:
simp[revDerivUpdate,revDeriv,add_assoc,neg_pull,mul_assoc,smul_push]
Proof state after:
no goals
Theorem: HDiv.hDiv.arg_a0a1.revDerivProjUpdate_rule
Proof state before:
case funProp.discharger
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 ι
f g : X → K
hf : HasAdjDiff K f
hg : HasAdjDiff K g
hx : ∀ (x : X), g x ≠ 0
x : X
⊢ ∀ (x : X), g x ≠ 0
Tactic:
assumption
Proof state after:
no goals
Theorem: IndexType.sum.arg_f.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 ι✝
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f : X → ι → Y
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
⊢ (revDeriv K fun x =>  ∑ i, f x i) = fun x =>
    let ydf := revDeriv K f x;
    ( ∑ i, ydf.1 i, fun dy => ydf.2 fun x => dy)
Tactic:
unfold revDeriv
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
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 ι✝
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f : X → ι → Y
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
⊢ (fun x => ((fun x =>  ∑ i, f x i) x, semiAdjoint K (cderiv K (fun x =>  ∑ i, f x i) x))) = fun x =>
    let ydf := (f x, semiAdjoint K (cderiv K f x));
    ( ∑ i, ydf.1 i, fun dy => ydf.2 fun x => dy)
Theorem: IndexType.sum.arg_f.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 ι✝
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f : X → ι → Y
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
⊢ (fun x => ((fun x =>  ∑ i, f x i) x, semiAdjoint K (cderiv K (fun x =>  ∑ i, f x i) x))) = fun x =>
    let ydf := (f x, semiAdjoint K (cderiv K f x));
    ( ∑ i, ydf.1 i, fun dy => ydf.2 fun x => dy)
Tactic:
fun_trans
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
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 ι✝
ι : Type
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
f : X → ι → Y
hf : ∀ (i : ι), HasAdjDiff K fun x => f x i
⊢ (fun x => ( ∑ i, f x i, fun y =>  ∑ i, semiAdjoint K (fun x_1 => cderiv K (fun x => f x i) x x_1) y)) = fun x =>
    ( ∑ i, f x i, fun dy => semiAdjoint K (cderiv K f x) fun x => dy)