Theorem: LeanColls.Indexed.ofFn.arg_cont.revCDerivProj_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
⊢ (revDerivProj K Idx fun x => ofFn (f x)) = fun x =>
    let fdf := revDerivProj K Idx f x;
    (ofFn fdf.1, fdf.2)
Tactic:
unfold revDerivProj
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 =>
      let ydf' := revDeriv K (fun x => ofFn (f x)) x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun x =>
    let fdf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ofFn fdf.1, fdf.2)

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 =>
      let ydf' := revDeriv K (fun x => ofFn (f x)) x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun x =>
    let fdf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ofFn fdf.1, fdf.2)
Tactic:
conv => lhs; fun_trans; simp
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 => (ofFn (f x), fun i de => (revDeriv K (fun x => f x) x).2 fun idx => (oneHot i de)[idx])) = fun x =>
    let fdf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ofFn fdf.1, fdf.2)

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 => (ofFn (f x), fun i de => (revDeriv K (fun x => f x) x).2 fun idx => (oneHot i de)[idx])) = fun x =>
    let fdf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ofFn fdf.1, fdf.2)
Tactic:
funext x
State after:
case 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
f : X → Idx → Elem
hf : HasAdjDiff K f
x : X
⊢ (ofFn (f x), fun i de => (revDeriv K (fun x => f x) x).2 fun idx => (oneHot i de)[idx]) =
    let fdf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ofFn fdf.1, fdf.2)

State before:
case 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
f : X → Idx → Elem
hf : HasAdjDiff K f
x : X
⊢ (ofFn (f x), fun i de => (revDeriv K (fun x => f x) x).2 fun idx => (oneHot i de)[idx]) =
    let fdf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ofFn fdf.1, fdf.2)
Tactic:
simp[oneHot]
State after:
no goals