internlm/Lean-Github huggingface dataset:
Theorem: LeanColls.Indexed.get.arg_cont.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
idx : Idx
⊢ ∀ (x y : Cont), (x + y)[idx] = x[idx] + y[idx]
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
idx : Idx
x✝ y✝ : Cont
⊢ (x✝ + y✝)[idx] = x✝[idx] + y✝[idx]
Theorem: LeanColls.Indexed.get.arg_cont.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
idx : Idx
x✝ y✝ : Cont
⊢ (x✝ + y✝)[idx] = x✝[idx] + y✝[idx]
Tactic:
simp
Proof state after:
no goals
Theorem: LeanColls.Indexed.get.arg_cont.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
idx : Idx
⊢ ∀ (c : R) (x : Cont), (c • x)[idx] = c • x[idx]
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
idx : Idx
c✝ : R
x✝ : Cont
⊢ (c✝ • x✝)[idx] = c✝ • x✝[idx]
Theorem: LeanColls.Indexed.get.arg_cont.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
idx : Idx
c✝ : R
x✝ : Cont
⊢ (c✝ • x✝)[idx] = c✝ • x✝[idx]
Tactic:
simp
Proof state after:
no goals
Theorem: GetElem.getElem.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
idx : Idx
⊢ (semiAdjoint K fun cont => cont[idx]) = fun elem => oneHot idx elem
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: GetElem.getElem.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 → Cont
idx : Idx
hf : HasAdjDiff K f
⊢ (revDeriv K fun x => (f x)[idx]) = fun x =>
    let ydf := revDerivProj K Idx f x;
    (ydf.1[idx], fun delem => ydf.2 idx delem)
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 → Cont
idx : Idx
hf : HasAdjDiff K f
⊢ (fun x => ((fun x => (f x)[idx]) x, semiAdjoint K (cderiv K (fun x => (f x)[idx]) x))) = fun x =>
    let ydf := revDerivProj K Idx f x;
    (ydf.1[idx], fun delem => ydf.2 idx delem)
Theorem: GetElem.getElem.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 → Cont
idx : Idx
hf : HasAdjDiff K f
⊢ (fun x => ((fun x => (f x)[idx]) x, semiAdjoint K (cderiv K (fun x => (f x)[idx]) x))) = fun x =>
    let ydf := revDerivProj K Idx f x;
    (ydf.1[idx], fun delem => ydf.2 idx delem)
Tactic:
conv =>
  lhs; fun_trans; fun_trans; simp
Proof state after:
no goals
Theorem: GetElem.getElem.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 → Cont
idx : Idx
hf : HasAdjDiff K f
⊢ (revDerivUpdate K fun x => (f x)[idx]) = fun x =>
    let ydf := revDerivProjUpdate K Idx f x;
    (ydf.1[idx], fun delem dx => ydf.2 idx delem 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 → Cont
idx : Idx
hf : HasAdjDiff K f
⊢ (fun x =>
      let ydf := revDeriv K (fun x => (f x)[idx]) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    fun x =>
    let ydf := revDerivProjUpdate K Idx f x;
    (ydf.1[idx], fun delem dx => ydf.2 idx delem dx)
Theorem: GetElem.getElem.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 → Cont
idx : Idx
hf : HasAdjDiff K f
⊢ (fun x =>
      let ydf := revDeriv K (fun x => (f x)[idx]) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    fun x =>
    let ydf := revDerivProjUpdate K Idx f x;
    (ydf.1[idx], fun delem dx => ydf.2 idx delem dx)
Tactic:
conv =>
  lhs; fun_trans; fun_trans; simp
Proof state after:
no goals
Theorem: GetElem.getElem.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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
⊢ (revDerivProj K J fun x => (f x)[idx]) = fun x =>
    let ydf := revDerivProj K (Idx × J) f x;
    (ydf.1[idx], fun j delem => ydf.2 (idx, j) delem)
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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
⊢ (fun x =>
      let ydf' := revDeriv K (fun x => (f x)[idx]) x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun x =>
    let ydf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ydf.1[idx], fun j delem => ydf.2 (idx, j) delem)
Theorem: GetElem.getElem.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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
⊢ (fun x =>
      let ydf' := revDeriv K (fun x => (f x)[idx]) x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun x =>
    let ydf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ydf.1[idx], fun j delem => ydf.2 (idx, j) delem)
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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
⊢ (fun x => ((f x)[idx], fun i de => (revDerivProj K Idx (fun x => f x) x).2 idx (oneHot i de))) = fun x =>
    let ydf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ydf.1[idx], fun j delem => ydf.2 (idx, j) delem)
Theorem: GetElem.getElem.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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
⊢ (fun x => ((f x)[idx], fun i de => (revDerivProj K Idx (fun x => f x) x).2 idx (oneHot i de))) = fun x =>
    let ydf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ydf.1[idx], fun j delem => ydf.2 (idx, j) delem)
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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
x : X
⊢ ((f x)[idx], fun i de => (revDerivProj K Idx (fun x => f x) x).2 idx (oneHot i de)) =
    let ydf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ydf.1[idx], fun j delem => ydf.2 (idx, j) delem)
Theorem: GetElem.getElem.arg_cont.revCDerivProj_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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
x : X
⊢ ((f x)[idx], fun i de => (revDerivProj K Idx (fun x => f x) x).2 idx (oneHot i de)) =
    let ydf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ydf.1[idx], fun j delem => ydf.2 (idx, j) delem)
Tactic:
simp[revDerivProj]
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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
x : X
⊢ (fun i de => (revDeriv K (fun x => f x) x).2 (oneHot idx (oneHot i de))) = fun j delem =>
    (revDeriv K f x).2 (oneHot (idx, j) delem)
Theorem: GetElem.getElem.arg_cont.revCDerivProj_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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
x : X
⊢ (fun i de => (revDeriv K (fun x => f x) x).2 (oneHot idx (oneHot i de))) = fun j delem =>
    (revDeriv K f x).2 (oneHot (idx, j) delem)
Tactic:
funext j 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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
x : X
j : J
de : ElemJ j
⊢ (revDeriv K (fun x => f x) x).2 (oneHot idx (oneHot j de)) = (revDeriv K f x).2 (oneHot (idx, j) de)
Theorem: GetElem.getElem.arg_cont.revCDerivProj_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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
x : X
j : J
de : ElemJ j
⊢ (revDeriv K (fun x => f x) x).2 (oneHot idx (oneHot j de)) = (revDeriv K f x).2 (oneHot (idx, j) de)
Tactic:
simp [revDeriv]
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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
x : X
j : J
de : ElemJ j
⊢ semiAdjoint K (cderiv K (fun x => f x) x) (oneHot idx (oneHot j de)) =
    semiAdjoint K (cderiv K f x) (oneHot (idx, j) de)
Theorem: GetElem.getElem.arg_cont.revCDerivProj_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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
x : X
j : J
de : ElemJ j
⊢ semiAdjoint K (cderiv K (fun x => f x) x) (oneHot idx (oneHot j de)) =
    semiAdjoint K (cderiv K f x) (oneHot (idx, j) de)
Tactic:
congr
Proof state after:
case h.h.h.e_y
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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
x : X
j : J
de : ElemJ j
⊢ oneHot idx (oneHot j de) = oneHot (idx, j) de
Theorem: GetElem.getElem.arg_cont.revCDerivProj_rule
Proof state before:
case h.h.h.e_y
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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
x : X
j : J
de : ElemJ j
⊢ oneHot idx (oneHot j de) = oneHot (idx, j) de
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: LeanColls.Indexed.set.arg_contelem.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
idx : Idx
⊢ IsLinearMap R fun x =>
    match x with
    | (cont, elem) => set cont idx elem
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
idx : Idx
⊢ ∀ (x y : Cont × Elem),
    (match x + y with
      | (cont, elem) => set cont idx elem) =
      (match x with
        | (cont, elem) => set cont idx elem) +
        match y with
        | (cont, elem) => set cont idx elem

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
idx : Idx
⊢ ∀ (c : R) (x : Cont × Elem),
    (match c • x with
      | (cont, elem) => set cont idx elem) =
      c •
        match x with
        | (cont, elem) => set cont idx elem
Theorem: LeanColls.Indexed.set.arg_contelem.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
idx : Idx
⊢ ∀ (x y : Cont × Elem),
    (match x + y with
      | (cont, elem) => set cont idx elem) =
      (match x with
        | (cont, elem) => set cont idx elem) +
        match y with
        | (cont, elem) => set cont idx elem

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
idx : Idx
⊢ ∀ (c : R) (x : Cont × Elem),
    (match c • x with
      | (cont, elem) => set cont idx elem) =
      c •
        match x with
        | (cont, elem) => set cont idx elem
Tactic:
. intros; simp; ext; sorry_proof
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
idx : Idx
⊢ ∀ (c : R) (x : Cont × Elem),
    (match c • x with
      | (cont, elem) => set cont idx elem) =
      c •
        match x with
        | (cont, elem) => set cont idx elem
Theorem: LeanColls.Indexed.set.arg_contelem.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
idx : Idx
⊢ ∀ (c : R) (x : Cont × Elem),
    (match c • x with
      | (cont, elem) => set cont idx elem) =
      c •
        match x with
        | (cont, elem) => set cont idx elem
Tactic:
. intros; simp; ext; sorry_proof
Proof state after:
no goals
Theorem: LeanColls.Indexed.set.arg_contelem.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
idx : Idx
⊢ ∀ (x y : Cont × Elem),
    (match x + y with
      | (cont, elem) => set cont idx elem) =
      (match x with
        | (cont, elem) => set cont idx elem) +
        match y with
        | (cont, elem) => set cont idx elem
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
idx : Idx
x✝ y✝ : Cont × Elem
⊢ (match x✝ + y✝ with
    | (cont, elem) => set cont idx elem) =
    (match x✝ with
      | (cont, elem) => set cont idx elem) +
      match y✝ with
      | (cont, elem) => set cont idx elem
Theorem: LeanColls.Indexed.set.arg_contelem.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
idx : Idx
x✝ y✝ : Cont × Elem
⊢ (match x✝ + y✝ with
    | (cont, elem) => set cont idx elem) =
    (match x✝ with
      | (cont, elem) => set cont idx elem) +
      match y✝ with
      | (cont, elem) => set cont idx elem
Tactic:
simp
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
idx : Idx
x✝ y✝ : Cont × Elem
⊢ set (x✝.1 + y✝.1) idx (x✝.2 + y✝.2) = set x✝.1 idx x✝.2 + set y✝.1 idx y✝.2