unfold revDerivProjUpdate
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
f : X → Idx → Elem
hf : HasAdjDiff K f
⊢ (revDerivProjUpdate K Idx fun x => ofFn (f x)) = fun x =>
    let fdf := revDerivProjUpdate K Idx f x;
    (ofFn fdf.1, fdf.2)
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
f : X → Idx → Elem
hf : HasAdjDiff K f
⊢ (fun x =>
      let ydf' := revDerivProj K Idx (fun x => ofFn (f x)) x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de)) =
    fun x =>
    let fdf :=
      let ydf' := revDerivProj K Idx f x;
      (ydf'.1, fun i de dx => dx + ydf'.2 i de);
    (ofFn fdf.1, fdf.2)