internlm/Lean-Github huggingface dataset:
Theorem: LeanColls.Indexed.set.arg_contelem.revCDerivProjUpdate_rule
Proof state before:
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
⊢ (revDerivProjUpdate K Idx fun x => set (cont x) idx (elem x)) = fun x =>
    let cdc := revDerivProjUpdate K Idx cont x;
    let ede := revDerivUpdate K elem x;
    (set cdc.1 idx ede.1, fun i delem dx => if i = idx then ede.2 delem dx else cdc.2 i delem dx)
Tactic:
unfold revDerivProjUpdate
Proof state after:
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
⊢ (fun x =>
      let ydf' := revDerivProj K Idx (fun x => set (cont x) idx (elem x)) x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de)) =
    fun x =>
    let cdc :=
      let ydf' := revDerivProj K Idx cont x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de);
    let ede := revDerivUpdate K elem x;
    (set cdc.1 idx ede.1, fun i delem dx => if i = idx then ede.2 delem dx else cdc.2 i delem dx)
Theorem: LeanColls.Indexed.set.arg_contelem.revCDerivProjUpdate_rule
Proof state before:
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
⊢ (fun x =>
      let ydf' := revDerivProj K Idx (fun x => set (cont x) idx (elem x)) x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de)) =
    fun x =>
    let cdc :=
      let ydf' := revDerivProj K Idx cont x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de);
    let ede := revDerivUpdate K elem x;
    (set cdc.1 idx ede.1, fun i delem dx => if i = idx then ede.2 delem dx else cdc.2 i delem dx)
Tactic:
conv =>
  lhs; fun_trans; fun_trans; simp
Proof state after:
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
⊢ (fun x =>
      (set (cont x) idx (elem x), fun i de dx =>
        dx +
          if i = idx then (revDeriv K (fun x => elem x) x).2 de else (revDerivProj K Idx (fun x => cont x) x).2 i de)) =
    fun x =>
    let cdc :=
      let ydf' := revDerivProj K Idx cont x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de);
    let ede := revDerivUpdate K elem x;
    (set cdc.1 idx ede.1, fun i delem dx => if i = idx then ede.2 delem dx else cdc.2 i delem dx)
Theorem: LeanColls.Indexed.set.arg_contelem.revCDerivProjUpdate_rule
Proof state before:
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
⊢ (fun x =>
      (set (cont x) idx (elem x), fun i de dx =>
        dx +
          if i = idx then (revDeriv K (fun x => elem x) x).2 de else (revDerivProj K Idx (fun x => cont x) x).2 i de)) =
    fun x =>
    let cdc :=
      let ydf' := revDerivProj K Idx cont x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de);
    let ede := revDerivUpdate K elem x;
    (set cdc.1 idx ede.1, fun i delem dx => if i = idx then ede.2 delem dx else cdc.2 i delem dx)
Tactic:
funext x
Proof state after:
case h
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
x : X
⊢ (set (cont x) idx (elem x), fun i de dx =>
      dx + if i = idx then (revDeriv K (fun x => elem x) x).2 de else (revDerivProj K Idx (fun x => cont x) x).2 i de) =
    let cdc :=
      let ydf' := revDerivProj K Idx cont x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de);
    let ede := revDerivUpdate K elem x;
    (set cdc.1 idx ede.1, fun i delem dx => if i = idx then ede.2 delem dx else cdc.2 i delem dx)
Theorem: LeanColls.Indexed.set.arg_contelem.revCDerivProjUpdate_rule
Proof state before:
case h
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
x : X
⊢ (set (cont x) idx (elem x), fun i de dx =>
      dx + if i = idx then (revDeriv K (fun x => elem x) x).2 de else (revDerivProj K Idx (fun x => cont x) x).2 i de) =
    let cdc :=
      let ydf' := revDerivProj K Idx cont x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de);
    let ede := revDerivUpdate K elem x;
    (set cdc.1 idx ede.1, fun i delem dx => if i = idx then ede.2 delem dx else cdc.2 i delem dx)
Tactic:
simp[revDerivProj,revDerivUpdate]
Proof state after:
case h
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
x : X
⊢ (fun i de dx =>
      dx +
        if i = idx then (revDeriv K (fun x => elem x) x).2 de else (revDeriv K (fun x => cont x) x).2 (oneHot i de)) =
    fun i delem dx => if i = idx then dx + (revDeriv K elem x).2 delem else dx + (revDeriv K cont x).2 (oneHot i delem)
Theorem: LeanColls.Indexed.set.arg_contelem.revCDerivProjUpdate_rule
Proof state before:
case h
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
x : X
⊢ (fun i de dx =>
      dx +
        if i = idx then (revDeriv K (fun x => elem x) x).2 de else (revDeriv K (fun x => cont x) x).2 (oneHot i de)) =
    fun i delem dx => if i = idx then dx + (revDeriv K elem x).2 delem else dx + (revDeriv K cont x).2 (oneHot i delem)
Tactic:
funext i de
Proof state after:
case h.h.h
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
x : X
i : Idx
de : Elem
⊢ (fun dx =>
      dx +
        if i = idx then (revDeriv K (fun x => elem x) x).2 de else (revDeriv K (fun x => cont x) x).2 (oneHot i de)) =
    fun dx => if i = idx then dx + (revDeriv K elem x).2 de else dx + (revDeriv K cont x).2 (oneHot i de)
Theorem: LeanColls.Indexed.set.arg_contelem.revCDerivProjUpdate_rule
Proof state before:
case h.h.h
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
x : X
i : Idx
de : Elem
⊢ (fun dx =>
      dx +
        if i = idx then (revDeriv K (fun x => elem x) x).2 de else (revDeriv K (fun x => cont x) x).2 (oneHot i de)) =
    fun dx => if i = idx then dx + (revDeriv K elem x).2 de else dx + (revDeriv K cont x).2 (oneHot i de)
Tactic:
if h : i = idx then
  simp [h]
else
  simp [h]
Proof state after:
no goals
Theorem: LeanColls.Indexed.set.arg_contelem.revCDerivProjUpdate_rule
Proof state before:
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
x : X
i : Idx
de : Elem
h : i = idx
⊢ (fun dx =>
      dx +
        if i = idx then (revDeriv K (fun x => elem x) x).2 de else (revDeriv K (fun x => cont x) x).2 (oneHot i de)) =
    fun dx => if i = idx then dx + (revDeriv K elem x).2 de else dx + (revDeriv K cont x).2 (oneHot i de)
Tactic:
simp [h]
Proof state after:
no goals
Theorem: LeanColls.Indexed.set.arg_contelem.revCDerivProjUpdate_rule
Proof state before:
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
x : X
i : Idx
de : Elem
h : ¬i = idx
⊢ (fun dx =>
      dx +
        if i = idx then (revDeriv K (fun x => elem x) x).2 de else (revDeriv K (fun x => cont x) x).2 (oneHot i de)) =
    fun dx => if i = idx then dx + (revDeriv K elem x).2 de else dx + (revDeriv K cont x).2 (oneHot i de)
Tactic:
simp [h]
Proof state after:
no goals
Theorem: LeanColls.Indexed.ofFn.arg_f.IsLinearMap_rule_simple
Proof state before:
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
⊢ IsLinearMap R fun f => ofFn f
Tactic:
constructor
Proof state after:
case map_add
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
⊢ ∀ (x y : Idx → Elem), ofFn (x + y) = ofFn x + ofFn y

case map_smul
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
⊢ ∀ (c : R) (x : Idx → Elem), ofFn (c • x) = c • ofFn x
Theorem: LeanColls.Indexed.ofFn.arg_f.IsLinearMap_rule_simple
Proof state before:
case map_add
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
⊢ ∀ (x y : Idx → Elem), ofFn (x + y) = ofFn x + ofFn y

case map_smul
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
⊢ ∀ (c : R) (x : Idx → Elem), ofFn (c • x) = c • ofFn x
Tactic:
. intros; ext; simp
Proof state after:
case map_smul
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
⊢ ∀ (c : R) (x : Idx → Elem), ofFn (c • x) = c • ofFn x
Theorem: LeanColls.Indexed.ofFn.arg_f.IsLinearMap_rule_simple
Proof state before:
case map_smul
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
⊢ ∀ (c : R) (x : Idx → Elem), ofFn (c • x) = c • ofFn x
Tactic:
. intros; ext; simp
Proof state after:
no goals
Theorem: LeanColls.Indexed.ofFn.arg_f.IsLinearMap_rule_simple
Proof state before:
case map_add
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
⊢ ∀ (x y : Idx → Elem), ofFn (x + y) = ofFn x + ofFn y
Tactic:
intros
Proof state after:
case map_add
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
x✝ y✝ : Idx → Elem
⊢ ofFn (x✝ + y✝) = ofFn x✝ + ofFn y✝
Theorem: LeanColls.Indexed.ofFn.arg_f.IsLinearMap_rule_simple
Proof state before:
case map_add
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
x✝ y✝ : Idx → Elem
⊢ ofFn (x✝ + y✝) = ofFn x✝ + ofFn y✝
Tactic:
ext
Proof state after:
case map_add.a
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
x✝ y✝ : Idx → Elem
i✝ : Idx
⊢ (ofFn (x✝ + y✝))[i✝] = (ofFn x✝ + ofFn y✝)[i✝]
Theorem: LeanColls.Indexed.ofFn.arg_f.IsLinearMap_rule_simple
Proof state before:
case map_add.a
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
x✝ y✝ : Idx → Elem
i✝ : Idx
⊢ (ofFn (x✝ + y✝))[i✝] = (ofFn x✝ + ofFn y✝)[i✝]
Tactic:
simp
Proof state after:
no goals
Theorem: LeanColls.Indexed.ofFn.arg_f.IsLinearMap_rule_simple
Proof state before:
case map_smul
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
⊢ ∀ (c : R) (x : Idx → Elem), ofFn (c • x) = c • ofFn x
Tactic:
intros
Proof state after:
case map_smul
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
c✝ : R
x✝ : Idx → Elem
⊢ ofFn (c✝ • x✝) = c✝ • ofFn x✝
Theorem: LeanColls.Indexed.ofFn.arg_f.IsLinearMap_rule_simple
Proof state before:
case map_smul
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
c✝ : R
x✝ : Idx → Elem
⊢ ofFn (c✝ • x✝) = c✝ • ofFn x✝
Tactic:
ext
Proof state after:
case map_smul.a
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
c✝ : R
x✝ : Idx → Elem
i✝ : Idx
⊢ (ofFn (c✝ • x✝))[i✝] = (c✝ • ofFn x✝)[i✝]
Theorem: LeanColls.Indexed.ofFn.arg_f.IsLinearMap_rule_simple
Proof state before:
case map_smul.a
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
c✝ : R
x✝ : Idx → Elem
i✝ : Idx
⊢ (ofFn (c✝ • x✝))[i✝] = (c✝ • ofFn x✝)[i✝]
Tactic:
simp
Proof state after:
no goals
Theorem: LeanColls.Indexed.ofFn.arg_cont.semiAdjoint_rule_simple
Proof state before:
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
⊢ (semiAdjoint K fun f => ofFn f) = fun cont idx => cont[idx]
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: LeanColls.Indexed.ofFn.arg_cont.revCDeriv_rule
Proof state before:
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
f : X → Idx → Elem
hf : HasAdjDiff K f
⊢ (revDeriv K fun x => ofFn (f x)) = fun x =>
    let fdf := revDeriv K f x;
    (ofFn fdf.1, fun dcont => fdf.2 fun idx => dcont[idx])
Tactic:
unfold revDeriv
Proof state after:
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
f : X → Idx → Elem
hf : HasAdjDiff K f
⊢ (fun x => ((fun x => ofFn (f x)) x, semiAdjoint K (cderiv K (fun x => ofFn (f x)) x))) = fun x =>
    let fdf := (f x, semiAdjoint K (cderiv K f x));
    (ofFn fdf.1, fun dcont => fdf.2 fun idx => dcont[idx])
Theorem: LeanColls.Indexed.ofFn.arg_cont.revCDeriv_rule
Proof state before:
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
f : X → Idx → Elem
hf : HasAdjDiff K f
⊢ (fun x => ((fun x => ofFn (f x)) x, semiAdjoint K (cderiv K (fun x => ofFn (f x)) x))) = fun x =>
    let fdf := (f x, semiAdjoint K (cderiv K f x));
    (ofFn fdf.1, fun dcont => fdf.2 fun idx => dcont[idx])
Tactic:
conv => lhs; fun_trans; simp
Proof state after:
no goals
Theorem: LeanColls.Indexed.ofFn.arg_cont.revCDerivUpdate_rule
Proof state before:
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
f : X → Idx → Elem
hf : HasAdjDiff K f
⊢ (revDerivUpdate K fun x => ofFn (f x)) = fun x =>
    let fdf := revDerivUpdate K f x;
    (ofFn fdf.1, fun dcont dx => fdf.2 (fun idx => dcont[idx]) dx)
Tactic:
unfold revDerivUpdate
Proof state after:
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
f : X → Idx → Elem
hf : HasAdjDiff K f
⊢ (fun x =>
      let ydf := revDeriv K (fun x => ofFn (f x)) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    fun x =>
    let fdf :=
      let ydf := revDeriv K f x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    (ofFn fdf.1, fun dcont dx => fdf.2 (fun idx => dcont[idx]) dx)
Theorem: LeanColls.Indexed.ofFn.arg_cont.revCDerivUpdate_rule
Proof state before:
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
f : X → Idx → Elem
hf : HasAdjDiff K f
⊢ (fun x =>
      let ydf := revDeriv K (fun x => ofFn (f x)) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    fun x =>
    let fdf :=
      let ydf := revDeriv K f x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    (ofFn fdf.1, fun dcont dx => fdf.2 (fun idx => dcont[idx]) dx)
Tactic:
conv => lhs; fun_trans; simp
Proof state after:
no goals
Theorem: LeanColls.Indexed.ofFn.arg_cont.revCDerivProj_rule
Proof state before:
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
f : X → Idx → Elem
hf : HasAdjDiff K f
⊢ (revDerivProj K Idx fun x => ofFn (f x)) = fun x =>
    let fdf := revDerivProj K Idx f x;
    (ofFn fdf.1, fdf.2)
Tactic:
unfold revDerivProj
Proof state after:
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
f : X → Idx → Elem
hf : HasAdjDiff K f
⊢ (fun x =>
      let ydf' := revDeriv K (fun x => ofFn (f x)) x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun x =>
    let fdf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ofFn fdf.1, fdf.2)
Theorem: LeanColls.Indexed.ofFn.arg_cont.revCDerivProj_rule
Proof state before:
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
f : X → Idx → Elem
hf : HasAdjDiff K f
⊢ (fun x =>
      let ydf' := revDeriv K (fun x => ofFn (f x)) x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun x =>
    let fdf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ofFn fdf.1, fdf.2)
Tactic:
conv => lhs; fun_trans; simp
Proof state after:
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
f : X → Idx → Elem
hf : HasAdjDiff K f
⊢ (fun x => (ofFn (f x), fun i de => (revDeriv K (fun x => f x) x).2 fun idx => (oneHot i de)[idx])) = fun x =>
    let fdf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ofFn fdf.1, fdf.2)
Theorem: LeanColls.Indexed.ofFn.arg_cont.revCDerivProj_rule
Proof state before:
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
f : X → Idx → Elem
hf : HasAdjDiff K f
⊢ (fun x => (ofFn (f x), fun i de => (revDeriv K (fun x => f x) x).2 fun idx => (oneHot i de)[idx])) = fun x =>
    let fdf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ofFn fdf.1, fdf.2)
Tactic:
funext x
Proof state after:
case h
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
f : X → Idx → Elem
hf : HasAdjDiff K f
x : X
⊢ (ofFn (f x), fun i de => (revDeriv K (fun x => f x) x).2 fun idx => (oneHot i de)[idx]) =
    let fdf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ofFn fdf.1, fdf.2)