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

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

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