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