funext x
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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
⊢ (fun x => ((f x)[idx], fun i de => (revDerivProj K Idx (fun x => f x) x).2 idx (oneHot i de))) = fun x =>
    let ydf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ydf.1[idx], fun j delem => ydf.2 (idx, j) delem)
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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
x : X
⊢ ((f x)[idx], fun i de => (revDerivProj K Idx (fun x => f x) x).2 idx (oneHot i de)) =
    let ydf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ydf.1[idx], fun j delem => ydf.2 (idx, j) delem)