Theorem: SciLean.revDeriv.apply_rule (SciLean/Core/FunctionTransformations/RevDeriv.lean)

State before:
K : Type u_3
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.47990
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.48003
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.48014
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.48025
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.48036
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.48061
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.48086
EI : I → Type u_2
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.48225
J : Type ?u.48228
FJ : J → Type ?u.48233
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
i : I
⊢ (revDeriv K fun x => x i) = fun x => (x i, fun dxi => oneHot i dxi)
Tactic:
unfold revDeriv
State after:
K : Type u_3
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.47990
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.48003
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.48014
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.48025
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.48036
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.48061
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.48086
EI : I → Type u_2
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.48225
J : Type ?u.48228
FJ : J → Type ?u.48233
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
i : I
⊢ (fun x => ((fun x => x i) x, semiAdjoint K (cderiv K (fun x => x i) x))) = fun x => (x i, fun dxi => oneHot i dxi)

State before:
K : Type u_3
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.47990
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.48003
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.48014
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.48025
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.48036
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.48061
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.48086
EI : I → Type u_2
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.48225
J : Type ?u.48228
FJ : J → Type ?u.48233
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
i : I
⊢ (fun x => ((fun x => x i) x, semiAdjoint K (cderiv K (fun x => x i) x))) = fun x => (x i, fun dxi => oneHot i dxi)
Tactic:
fun_trans
State after:
K : Type u_3
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.47990
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.48003
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.48014
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.48025
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.48036
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.48061
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.48086
EI : I → Type u_2
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.48225
J : Type ?u.48228
FJ : J → Type ?u.48233
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
i : I
⊢ (fun x => (x i, fun y j => if h : i = j then h ▸ y else 0)) = fun x => (x i, fun dxi => oneHot i dxi)

State before:
K : Type u_3
I : Type u_1
inst✝²⁴ : RCLike K
X : Type ?u.47990
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.48003
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.48014
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.48025
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.48036
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.48061
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.48086
EI : I → Type u_2
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.48225
J : Type ?u.48228
FJ : J → Type ?u.48233
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
i : I
⊢ (fun x => (x i, fun y j => if h : i = j then h ▸ y else 0)) = fun x => (x i, fun dxi => oneHot i dxi)
Tactic:
simp[oneHot]
State after:
no goals