Theorem: SciLean.revDerivProjUpdate.comp_rule (SciLean/Core/FunctionTransformations/RevDeriv.lean)

State before:
K : Type u_1
I : Type u_5
inst✝²⁴ : RCLike K
X : Type u_4
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.173849
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.173860
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.173871
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.173896
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_3
EI : I → Type u_6
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.174060
J : Type ?u.174063
FJ : J → Type ?u.174068
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
f : Y → E
g : X → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (revDerivProjUpdate K I fun x => f (g x)) = fun x =>
    let ydg' := revDerivUpdate K g x;
    let zdf' := revDerivProj K I f ydg'.1;
    (zdf'.1, fun i de dx => ydg'.2 (zdf'.2 i de) dx)
Tactic:
funext x
State after:
case h
K : Type u_1
I : Type u_5
inst✝²⁴ : RCLike K
X : Type u_4
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.173849
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.173860
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.173871
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.173896
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_3
EI : I → Type u_6
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.174060
J : Type ?u.174063
FJ : J → Type ?u.174068
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
f : Y → E
g : X → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : X
⊢ revDerivProjUpdate K I (fun x => f (g x)) x =
    let ydg' := revDerivUpdate K g x;
    let zdf' := revDerivProj K I f ydg'.1;
    (zdf'.1, fun i de dx => ydg'.2 (zdf'.2 i de) dx)

State before:
case h
K : Type u_1
I : Type u_5
inst✝²⁴ : RCLike K
X : Type u_4
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.173849
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.173860
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.173871
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.173896
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_3
EI : I → Type u_6
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.174060
J : Type ?u.174063
FJ : J → Type ?u.174068
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
f : Y → E
g : X → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : X
⊢ revDerivProjUpdate K I (fun x => f (g x)) x =
    let ydg' := revDerivUpdate K g x;
    let zdf' := revDerivProj K I f ydg'.1;
    (zdf'.1, fun i de dx => ydg'.2 (zdf'.2 i de) dx)
Tactic:
simp[revDerivProjUpdate,revDerivProj.comp_rule _ _ _ _ hf hg]
State after:
case h
K : Type u_1
I : Type u_5
inst✝²⁴ : RCLike K
X : Type u_4
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.173849
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.173860
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.173871
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.173896
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_3
EI : I → Type u_6
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.174060
J : Type ?u.174063
FJ : J → Type ?u.174068
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
f : Y → E
g : X → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : X
⊢ (fun i de dx => dx + (revDeriv K g x).2 ((revDerivProj K I f (g x)).2 i de)) = fun i de dx =>
    (revDerivUpdate K g x).2 ((revDerivProj K I f (g x)).2 i de) dx

State before:
case h
K : Type u_1
I : Type u_5
inst✝²⁴ : RCLike K
X : Type u_4
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.173849
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.173860
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.173871
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.173896
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_3
EI : I → Type u_6
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.174060
J : Type ?u.174063
FJ : J → Type ?u.174068
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
f : Y → E
g : X → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : X
⊢ (fun i de dx => dx + (revDeriv K g x).2 ((revDerivProj K I f (g x)).2 i de)) = fun i de dx =>
    (revDerivUpdate K g x).2 ((revDerivProj K I f (g x)).2 i de) dx
Tactic:
rfl
State after:
no goals