Theorem: GetElem.getElem.arg_cont.revCDerivUpdate_rule (SciLean/Data/ArrayType/Properties.lean)

State before:
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 → Cont
idx : Idx
hf : HasAdjDiff K f
⊢ (revDerivUpdate K fun x => (f x)[idx]) = fun x =>
    let ydf := revDerivProjUpdate K Idx f x;
    (ydf.1[idx], fun delem dx => ydf.2 idx delem dx)
Tactic:
unfold revDerivUpdate
State after:
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 → Cont
idx : Idx
hf : HasAdjDiff K f
⊢ (fun x =>
      let ydf := revDeriv K (fun x => (f x)[idx]) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    fun x =>
    let ydf := revDerivProjUpdate K Idx f x;
    (ydf.1[idx], fun delem dx => ydf.2 idx delem dx)

State before:
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 → Cont
idx : Idx
hf : HasAdjDiff K f
⊢ (fun x =>
      let ydf := revDeriv K (fun x => (f x)[idx]) x;
      (ydf.1, fun dy dx => dx + ydf.2 dy)) =
    fun x =>
    let ydf := revDerivProjUpdate K Idx f x;
    (ydf.1[idx], fun delem dx => ydf.2 idx delem dx)
Tactic:
conv =>
  lhs; fun_trans; fun_trans; simp
State after:
no goals