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