internlm/Lean-Github huggingface dataset:
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
⊢ set (x✝.1 + y✝.1) idx (x✝.2 + y✝.2) = set x✝.1 idx x✝.2 + set y✝.1 idx y✝.2
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
idx : Idx
x✝ y✝ : Cont × Elem
i✝ : Idx
⊢ (set (x✝.1 + y✝.1) idx (x✝.2 + y✝.2))[i✝] = (set x✝.1 idx x✝.2 + set y✝.1 idx y✝.2)[i✝]
Theorem: LeanColls.Indexed.set.arg_contelem.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
idx : Idx
x✝ y✝ : Cont × Elem
i✝ : Idx
⊢ (set (x✝.1 + y✝.1) idx (x✝.2 + y✝.2))[i✝] = (set x✝.1 idx x✝.2 + set y✝.1 idx y✝.2)[i✝]
Tactic:
sorry_proof
Proof state after:
no goals
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
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:
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
idx : Idx
c✝ : R
x✝ : Cont × Elem
⊢ set (c✝ • x✝.1) idx (c✝ • x✝.2) = c✝ • set x✝.1 idx x✝.2
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
⊢ set (c✝ • x✝.1) idx (c✝ • x✝.2) = c✝ • set x✝.1 idx x✝.2
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
idx : Idx
c✝ : R
x✝ : Cont × Elem
i✝ : Idx
⊢ (set (c✝ • x✝.1) idx (c✝ • x✝.2))[i✝] = (c✝ • set x✝.1 idx x✝.2)[i✝]
Theorem: LeanColls.Indexed.set.arg_contelem.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
idx : Idx
c✝ : R
x✝ : Cont × Elem
i✝ : Idx
⊢ (set (c✝ • x✝.1) idx (c✝ • x✝.2))[i✝] = (c✝ • set x✝.1 idx x✝.2)[i✝]
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: LeanColls.Indexed.set.arg_contelem.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
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
⊢ (revDeriv K fun x => set (cont x) idx (elem x)) = fun x =>
    let cdc := revDeriv K cont x;
    let ede := revDerivUpdate K elem x;
    (set cdc.1 idx ede.1, fun dc =>
      let dci := dc[idx];
      let dc := set dc idx 0;
      ede.2 dci (cdc.2 dc))
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
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
⊢ (fun x => ((fun x => set (cont x) idx (elem x)) x, semiAdjoint K (cderiv K (fun x => set (cont x) idx (elem x)) x))) =
    fun x =>
    let cdc := (cont x, semiAdjoint K (cderiv K cont x));
    let ede := revDerivUpdate K elem x;
    (set cdc.1 idx ede.1, fun dc =>
      let dci := dc[idx];
      let dc := set dc idx 0;
      ede.2 dci (cdc.2 dc))
Theorem: LeanColls.Indexed.set.arg_contelem.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
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
⊢ (fun x => ((fun x => set (cont x) idx (elem x)) x, semiAdjoint K (cderiv K (fun x => set (cont x) idx (elem x)) x))) =
    fun x =>
    let cdc := (cont x, semiAdjoint K (cderiv K cont x));
    let ede := revDerivUpdate K elem x;
    (set cdc.1 idx ede.1, fun dc =>
      let dci := dc[idx];
      let dc := set dc idx 0;
      ede.2 dci (cdc.2 dc))
Tactic:
conv =>
  lhs; fun_trans; fun_trans; simp
Proof state after:
no goals
Theorem: LeanColls.Indexed.set.arg_contelem.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
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
⊢ (revDerivUpdate K fun x => set (cont x) idx (elem x)) = fun x =>
    let cdc := revDerivUpdate K cont x;
    let ede := revDerivUpdate K elem x;
    (set cdc.1 idx ede.1, fun dc dx =>
      let dci := dc[idx];
      let dc := set dc idx 0;
      ede.2 dci (cdc.2 dc 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
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
⊢ (fun x =>
      let ydf := revDeriv K (fun x => set (cont x) idx (elem x)) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    fun x =>
    let cdc :=
      let ydf := revDeriv K cont x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    let ede :=
      let ydf := revDeriv K elem x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    (set cdc.1 idx ede.1, fun dc dx =>
      let dci := dc[idx];
      let dc := set dc idx 0;
      ede.2 dci (cdc.2 dc dx))
Theorem: LeanColls.Indexed.set.arg_contelem.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
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
⊢ (fun x =>
      let ydf := revDeriv K (fun x => set (cont x) idx (elem x)) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    fun x =>
    let cdc :=
      let ydf := revDeriv K cont x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    let ede :=
      let ydf := revDeriv K elem x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    (set cdc.1 idx ede.1, fun dc dx =>
      let dci := dc[idx];
      let dc := set dc idx 0;
      ede.2 dci (cdc.2 dc 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 dy dx =>
        dx + (revDerivUpdate K (fun x => elem x) x).2 dy[idx] ((revDeriv K (fun x => cont x) x).2 (set dy idx 0)))) =
    fun x =>
    let cdc :=
      let ydf := revDeriv K cont x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    let ede :=
      let ydf := revDeriv K elem x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    (set cdc.1 idx ede.1, fun dc dx =>
      let dci := dc[idx];
      let dc := set dc idx 0;
      ede.2 dci (cdc.2 dc dx))
Theorem: LeanColls.Indexed.set.arg_contelem.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
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 dy dx =>
        dx + (revDerivUpdate K (fun x => elem x) x).2 dy[idx] ((revDeriv K (fun x => cont x) x).2 (set dy idx 0)))) =
    fun x =>
    let cdc :=
      let ydf := revDeriv K cont x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    let ede :=
      let ydf := revDeriv K elem x;
      (ydf.1, fun dy dx => dx + ydf.2 dy);
    (set cdc.1 idx ede.1, fun dc dx =>
      let dci := dc[idx];
      let dc := set dc idx 0;
      ede.2 dci (cdc.2 dc dx))
Tactic:
simp[revDerivUpdate,add_assoc]
Proof state after:
no goals
Theorem: LeanColls.Indexed.set.arg_contelem.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
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
⊢ (revDerivProj K Idx fun x => set (cont x) idx (elem x)) = fun x =>
    let cdc := revDerivProj K Idx cont x;
    let ede := revDeriv K elem x;
    (set cdc.1 idx ede.1, fun i delem => if i = idx then ede.2 delem else cdc.2 i 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
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
⊢ (fun x =>
      let ydf' := revDeriv K (fun x => set (cont x) idx (elem x)) x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun x =>
    let cdc :=
      let ydf' := revDeriv K cont x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    let ede := revDeriv K elem x;
    (set cdc.1 idx ede.1, fun i delem => if i = idx then ede.2 delem else cdc.2 i delem)
Theorem: LeanColls.Indexed.set.arg_contelem.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
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
⊢ (fun x =>
      let ydf' := revDeriv K (fun x => set (cont x) idx (elem x)) x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun x =>
    let cdc :=
      let ydf' := revDeriv K cont x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    let ede := revDeriv K elem x;
    (set cdc.1 idx ede.1, fun i delem => if i = idx then ede.2 delem else cdc.2 i 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
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 =>
        (revDerivUpdate K (fun x => elem x) x).2 (oneHot i de)[idx]
          ((revDeriv K (fun x => cont x) x).2 (set (oneHot i de) idx 0)))) =
    fun x =>
    let cdc :=
      let ydf' := revDeriv K cont x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    let ede := revDeriv K elem x;
    (set cdc.1 idx ede.1, fun i delem => if i = idx then ede.2 delem else cdc.2 i delem)
Theorem: LeanColls.Indexed.set.arg_contelem.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
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 =>
        (revDerivUpdate K (fun x => elem x) x).2 (oneHot i de)[idx]
          ((revDeriv K (fun x => cont x) x).2 (set (oneHot i de) idx 0)))) =
    fun x =>
    let cdc :=
      let ydf' := revDeriv K cont x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    let ede := revDeriv K elem x;
    (set cdc.1 idx ede.1, fun i delem => if i = idx then ede.2 delem else cdc.2 i 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
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 =>
      (revDerivUpdate K (fun x => elem x) x).2 (oneHot i de)[idx]
        ((revDeriv K (fun x => cont x) x).2 (set (oneHot i de) idx 0))) =
    let cdc :=
      let ydf' := revDeriv K cont x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    let ede := revDeriv K elem x;
    (set cdc.1 idx ede.1, fun i delem => if i = idx then ede.2 delem else cdc.2 i delem)
Theorem: LeanColls.Indexed.set.arg_contelem.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
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 =>
      (revDerivUpdate K (fun x => elem x) x).2 (oneHot i de)[idx]
        ((revDeriv K (fun x => cont x) x).2 (set (oneHot i de) idx 0))) =
    let cdc :=
      let ydf' := revDeriv K cont x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    let ede := revDeriv K elem x;
    (set cdc.1 idx ede.1, fun i delem => if i = idx then ede.2 delem else cdc.2 i delem)
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 =>
      (revDeriv K (fun x => cont x) x).2 (set (oneHot i de) idx 0) +
        (revDeriv K (fun x => elem x) x).2 (oneHot i de)[idx]) =
    fun i delem => if i = idx then (revDeriv K elem x).2 delem else (revDeriv K cont x).2 (oneHot i delem)
Theorem: LeanColls.Indexed.set.arg_contelem.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
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
x : X
⊢ (fun i de =>
      (revDeriv K (fun x => cont x) x).2 (set (oneHot i de) idx 0) +
        (revDeriv K (fun x => elem x) x).2 (oneHot i de)[idx]) =
    fun i delem => if i = idx then (revDeriv K elem x).2 delem else (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
⊢ (revDeriv K (fun x => cont x) x).2 (set (oneHot i de) idx 0) + (revDeriv K (fun x => elem x) x).2 (oneHot i de)[idx] =
    if i = idx then (revDeriv K elem x).2 de else (revDeriv K cont x).2 (oneHot i de)
Theorem: LeanColls.Indexed.set.arg_contelem.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
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
x : X
i : Idx
de : Elem
⊢ (revDeriv K (fun x => cont x) x).2 (set (oneHot i de) idx 0) + (revDeriv K (fun x => elem x) x).2 (oneHot i de)[idx] =
    if i = idx then (revDeriv K elem x).2 de else (revDeriv K cont x).2 (oneHot i de)
Tactic:
if h : i = idx then
  simp [revDeriv,h,oneHot]
  sorry_proof
else
  simp [revDeriv,h,oneHot]
  sorry_proof
Proof state after:
no goals
Theorem: LeanColls.Indexed.set.arg_contelem.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
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
⊢ (revDeriv K (fun x => cont x) x).2 (set (oneHot i de) idx 0) + (revDeriv K (fun x => elem x) x).2 (oneHot i de)[idx] =
    if i = idx then (revDeriv K elem x).2 de else (revDeriv K cont x).2 (oneHot i de)
Tactic:
simp [revDeriv,h,oneHot]
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
x : X
i : Idx
de : Elem
h : i = idx
⊢ semiAdjoint K (cderiv K (fun x => cont x) x) (set (ofFn fun i' => if idx = i' then de else 0) idx 0) = 0
Theorem: LeanColls.Indexed.set.arg_contelem.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
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
⊢ semiAdjoint K (cderiv K (fun x => cont x) x) (set (ofFn fun i' => if idx = i' then de else 0) idx 0) = 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: LeanColls.Indexed.set.arg_contelem.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
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
⊢ (revDeriv K (fun x => cont x) x).2 (set (oneHot i de) idx 0) + (revDeriv K (fun x => elem x) x).2 (oneHot i de)[idx] =
    if i = idx then (revDeriv K elem x).2 de else (revDeriv K cont x).2 (oneHot i de)
Tactic:
simp [revDeriv,h,oneHot]
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
x : X
i : Idx
de : Elem
h : ¬i = idx
⊢ semiAdjoint K (cderiv K (fun x => cont x) x) (set (ofFn fun i' => if i = i' then de else 0) idx 0) =
    semiAdjoint K (cderiv K cont x) (ofFn fun i' => if i = i' then de else 0)
Theorem: LeanColls.Indexed.set.arg_contelem.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
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
⊢ semiAdjoint K (cderiv K (fun x => cont x) x) (set (ofFn fun i' => if i = i' then de else 0) idx 0) =
    semiAdjoint K (cderiv K cont x) (ofFn fun i' => if i = i' then de else 0)
Tactic:
sorry_proof
Proof state after:
no goals