if h : i = idx then
  simp [revDeriv,h,oneHot]
  sorry_proof
else
  simp [revDeriv,h,oneHot]
  sorry_proof
case h.h.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
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
x : X
i : Idx
de : Elem
⊢ (revDeriv K (fun x => cont x) x).2 (set (oneHot i de) idx 0) + (revDeriv K (fun x => elem x) x).2 (oneHot i de)[idx] =
    if i = idx then (revDeriv K elem x).2 de else (revDeriv K cont x).2 (oneHot i de)
no goals