Theorem: GetElem.getElem.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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
⊢ (revDerivProj K J fun x => (f x)[idx]) = fun x =>
    let ydf := revDerivProj K (Idx × J) f x;
    (ydf.1[idx], fun j delem => ydf.2 (idx, j) delem)
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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
⊢ (fun x =>
      let ydf' := revDeriv K (fun x => (f x)[idx]) x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun x =>
    let ydf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ydf.1[idx], fun j delem => ydf.2 (idx, j) delem)

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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
⊢ (fun x =>
      let ydf' := revDeriv K (fun x => (f x)[idx]) x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de))) =
    fun x =>
    let ydf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ydf.1[idx], fun j delem => ydf.2 (idx, j) delem)
Tactic:
conv =>
  lhs; fun_trans; 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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
⊢ (fun x => ((f x)[idx], fun i de => (revDerivProj K Idx (fun x => f x) x).2 idx (oneHot i de))) = fun x =>
    let ydf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ydf.1[idx], fun j delem => ydf.2 (idx, j) delem)

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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
⊢ (fun x => ((f x)[idx], fun i de => (revDerivProj K Idx (fun x => f x) x).2 idx (oneHot i de))) = fun x =>
    let ydf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ydf.1[idx], fun j delem => ydf.2 (idx, j) delem)
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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
x : X
⊢ ((f x)[idx], fun i de => (revDerivProj K Idx (fun x => f x) x).2 idx (oneHot i de)) =
    let ydf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ydf.1[idx], fun j delem => ydf.2 (idx, j) delem)

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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
x : X
⊢ ((f x)[idx], fun i de => (revDerivProj K Idx (fun x => f x) x).2 idx (oneHot i de)) =
    let ydf :=
      let ydf' := revDeriv K f x;
      (ydf'.1, fun i de => ydf'.2 (oneHot i de));
    (ydf.1[idx], fun j delem => ydf.2 (idx, j) delem)
Tactic:
simp[revDerivProj]
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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
x : X
⊢ (fun i de => (revDeriv K (fun x => f x) x).2 (oneHot idx (oneHot i de))) = fun j delem =>
    (revDeriv K f x).2 (oneHot (idx, j) delem)

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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
x : X
⊢ (fun i de => (revDeriv K (fun x => f x) x).2 (oneHot idx (oneHot i de))) = fun j delem =>
    (revDeriv K f x).2 (oneHot (idx, j) delem)
Tactic:
funext j de
State after:
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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
x : X
j : J
de : ElemJ j
⊢ (revDeriv K (fun x => f x) x).2 (oneHot idx (oneHot j de)) = (revDeriv K f x).2 (oneHot (idx, j) de)

State before:
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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
x : X
j : J
de : ElemJ j
⊢ (revDeriv K (fun x => f x) x).2 (oneHot idx (oneHot j de)) = (revDeriv K f x).2 (oneHot (idx, j) de)
Tactic:
simp [revDeriv]
State after:
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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
x : X
j : J
de : ElemJ j
⊢ semiAdjoint K (cderiv K (fun x => f x) x) (oneHot idx (oneHot j de)) =
    semiAdjoint K (cderiv K f x) (oneHot (idx, j) de)

State before:
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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
x : X
j : J
de : ElemJ j
⊢ semiAdjoint K (cderiv K (fun x => f x) x) (oneHot idx (oneHot j de)) =
    semiAdjoint K (cderiv K f x) (oneHot (idx, j) de)
Tactic:
congr
State after:
case h.h.h.e_y
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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
x : X
j : J
de : ElemJ j
⊢ oneHot idx (oneHot j de) = oneHot (idx, j) de

State before:
case h.h.h.e_y
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
J : Type u_1
ElemJ : J → Type u_2
inst✝⁵ : StructType Elem J ElemJ
inst✝⁴ : IndexType J
inst✝³ : LawfulIndexType J
inst✝² : DecidableEq J
inst✝¹ : (j : J) → SemiInnerProductSpace K (ElemJ j)
inst✝ : SemiInnerProductSpaceStruct K Elem J ElemJ
f : X → Cont
idx : Idx
hf : HasAdjDiff K f
x : X
j : J
de : ElemJ j
⊢ oneHot idx (oneHot j de) = oneHot (idx, j) de
Tactic:
sorry_proof
State after:
no goals