sorry_proof
case h.h.h.e_y
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
j : J
de : ElemJ j
⊢ oneHot idx (oneHot j de) = oneHot (idx, j) de
no goals