Theorem: LeanColls.Indexed.ofFn.arg_cont.revCDeriv_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 → Idx → Elem
hf : HasAdjDiff K f
⊢ (revDeriv K fun x => ofFn (f x)) = fun x =>
    let fdf := revDeriv K f x;
    (ofFn fdf.1, fun dcont => fdf.2 fun idx => dcont[idx])
Tactic:
unfold revDeriv
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 → Idx → Elem
hf : HasAdjDiff K f
⊢ (fun x => ((fun x => ofFn (f x)) x, semiAdjoint K (cderiv K (fun x => ofFn (f x)) x))) = fun x =>
    let fdf := (f x, semiAdjoint K (cderiv K f x));
    (ofFn fdf.1, fun dcont => fdf.2 fun idx => dcont[idx])

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 → Idx → Elem
hf : HasAdjDiff K f
⊢ (fun x => ((fun x => ofFn (f x)) x, semiAdjoint K (cderiv K (fun x => ofFn (f x)) x))) = fun x =>
    let fdf := (f x, semiAdjoint K (cderiv K f x));
    (ofFn fdf.1, fun dcont => fdf.2 fun idx => dcont[idx])
Tactic:
conv => lhs; fun_trans; simp
State after:
no goals