Theorem: LeanColls.Indexed.set.arg_contelem.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
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
⊢ (revDeriv K fun x => set (cont x) idx (elem x)) = fun x =>
    let cdc := revDeriv K cont x;
    let ede := revDerivUpdate K elem x;
    (set cdc.1 idx ede.1, fun dc =>
      let dci := dc[idx];
      let dc := set dc idx 0;
      ede.2 dci (cdc.2 dc))
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
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
⊢ (fun x => ((fun x => set (cont x) idx (elem x)) x, semiAdjoint K (cderiv K (fun x => set (cont x) idx (elem x)) x))) =
    fun x =>
    let cdc := (cont x, semiAdjoint K (cderiv K cont x));
    let ede := revDerivUpdate K elem x;
    (set cdc.1 idx ede.1, fun dc =>
      let dci := dc[idx];
      let dc := set dc idx 0;
      ede.2 dci (cdc.2 dc))

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
cont : X → Cont
idx : Idx
elem : X → Elem
hcont : HasAdjDiff K cont
helem : HasAdjDiff K elem
⊢ (fun x => ((fun x => set (cont x) idx (elem x)) x, semiAdjoint K (cderiv K (fun x => set (cont x) idx (elem x)) x))) =
    fun x =>
    let cdc := (cont x, semiAdjoint K (cderiv K cont x));
    let ede := revDerivUpdate K elem x;
    (set cdc.1 idx ede.1, fun dc =>
      let dci := dc[idx];
      let dc := set dc idx 0;
      ede.2 dci (cdc.2 dc))
Tactic:
conv =>
  lhs; fun_trans; fun_trans; simp
State after:
no goals