Theorem: LeanColls.Indexed.set.arg_contelem.revCDerivProj_rule (SciLean/Data/ArrayType/Properties.lean)

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
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)

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
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)

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
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)

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]
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)

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
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)

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
State after:
no goals

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]
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

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
State after:
no goals

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]
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)

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
State after:
no goals