Theorem: LeanColls.Indexed.set.arg_contelem.revCDerivProjUpdate_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
⊢ (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
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)

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

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

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

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

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