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

State before:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
i : ι
⊢ (revDerivProjUpdate K I fun f => f i) = fun f =>
    (f i, fun j dxj df i' => if i = i' then structModify j (fun xj => xj + dxj) (df i') else df i')
Tactic:
funext x
State after:
case h
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
i : ι
x : ι → E
⊢ revDerivProjUpdate K I (fun f => f i) x =
    (x i, fun j dxj df i' => if i = i' then structModify j (fun xj => xj + dxj) (df i') else df i')

State before:
case h
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
i : ι
x : ι → E
⊢ revDerivProjUpdate K I (fun f => f i) x =
    (x i, fun j dxj df i' => if i = i' then structModify j (fun xj => xj + dxj) (df i') else df i')
Tactic:
unfold revDerivProjUpdate
State after:
case h
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
i : ι
x : ι → E
⊢ (let ydf' := revDerivProj K I (fun f => f i) x;
    (ydf'.1, fun i de dx => dx + ydf'.2 i de)) =
    (x i, fun j dxj df i' => if i = i' then structModify j (fun xj => xj + dxj) (df i') else df i')

State before:
case h
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
i : ι
x : ι → E
⊢ (let ydf' := revDerivProj K I (fun f => f i) x;
    (ydf'.1, fun i de dx => dx + ydf'.2 i de)) =
    (x i, fun j dxj df i' => if i = i' then structModify j (fun xj => xj + dxj) (df i') else df i')
Tactic:
fun_trans
State after:
case h
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
i : ι
x : ι → E
⊢ (fun i_1 de dx => Function.modify dx i (structModify i_1 fun xi' => xi' + de)) = fun j dxj df i' =>
    if i = i' then structModify j (fun xj => xj + dxj) (df i') else df i'

State before:
case h
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
i : ι
x : ι → E
⊢ (fun i_1 de dx => Function.modify dx i (structModify i_1 fun xi' => xi' + de)) = fun j dxj df i' =>
    if i = i' then structModify j (fun xj => xj + dxj) (df i') else df i'
Tactic:
funext j dxj f i'
State after:
case h.h.h.h.h
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
dxj : EI j
f : ι → E
i' : ι
⊢ Function.modify f i (structModify j fun xi' => xi' + dxj) i' =
    if i = i' then structModify j (fun xj => xj + dxj) (f i') else f i'

State before:
case h.h.h.h.h
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
dxj : EI j
f : ι → E
i' : ι
⊢ Function.modify f i (structModify j fun xi' => xi' + dxj) i' =
    if i = i' then structModify j (fun xj => xj + dxj) (f i') else f i'
Tactic:
apply structExt (I:=I)
State after:
case h.h.h.h.h.a
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
dxj : EI j
f : ι → E
i' : ι
⊢ ∀ (i_1 : I),
    structProj (Function.modify f i (structModify j fun xi' => xi' + dxj) i') i_1 =
      structProj (if i = i' then structModify j (fun xj => xj + dxj) (f i') else f i') i_1

State before:
case h.h.h.h.h.a
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
dxj : EI j
f : ι → E
i' : ι
⊢ ∀ (i_1 : I),
    structProj (Function.modify f i (structModify j fun xi' => xi' + dxj) i') i_1 =
      structProj (if i = i' then structModify j (fun xj => xj + dxj) (f i') else f i') i_1
Tactic:
intro j'
State after:
case h.h.h.h.h.a
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
dxj : EI j
f : ι → E
i' : ι
j' : I
⊢ structProj (Function.modify f i (structModify j fun xi' => xi' + dxj) i') j' =
    structProj (if i = i' then structModify j (fun xj => xj + dxj) (f i') else f i') j'

State before:
case h.h.h.h.h.a
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
dxj : EI j
f : ι → E
i' : ι
j' : I
⊢ structProj (Function.modify f i (structModify j fun xi' => xi' + dxj) i') j' =
    structProj (if i = i' then structModify j (fun xj => xj + dxj) (f i') else f i') j'
Tactic:
if h :i'=i then
  subst h; simp
else
  have h' : i≠i' := by intro h''; simp[h''] at h
  simp[h,h',Function.update]
State after:
no goals

State before:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
dxj : EI j
f : ι → E
i' : ι
j' : I
h : i' = i
⊢ structProj (Function.modify f i (structModify j fun xi' => xi' + dxj) i') j' =
    structProj (if i = i' then structModify j (fun xj => xj + dxj) (f i') else f i') j'
Tactic:
subst h
State after:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
x : ι → E
j : I
dxj : EI j
f : ι → E
i' : ι
j' : I
⊢ structProj (Function.modify f i' (structModify j fun xi' => xi' + dxj) i') j' =
    structProj (if i' = i' then structModify j (fun xj => xj + dxj) (f i') else f i') j'

State before:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
x : ι → E
j : I
dxj : EI j
f : ι → E
i' : ι
j' : I
⊢ structProj (Function.modify f i' (structModify j fun xi' => xi' + dxj) i') j' =
    structProj (if i' = i' then structModify j (fun xj => xj + dxj) (f i') else f i') j'
Tactic:
simp
State after:
no goals

State before:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
dxj : EI j
f : ι → E
i' : ι
j' : I
h : ¬i' = i
⊢ structProj (Function.modify f i (structModify j fun xi' => xi' + dxj) i') j' =
    structProj (if i = i' then structModify j (fun xj => xj + dxj) (f i') else f i') j'
Tactic:
have h' : i≠i' := by intro h''; simp[h''] at h
State after:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
dxj : EI j
f : ι → E
i' : ι
j' : I
h : ¬i' = i
h' : i ≠ i'
⊢ structProj (Function.modify f i (structModify j fun xi' => xi' + dxj) i') j' =
    structProj (if i = i' then structModify j (fun xj => xj + dxj) (f i') else f i') j'

State before:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
dxj : EI j
f : ι → E
i' : ι
j' : I
h : ¬i' = i
h' : i ≠ i'
⊢ structProj (Function.modify f i (structModify j fun xi' => xi' + dxj) i') j' =
    structProj (if i = i' then structModify j (fun xj => xj + dxj) (f i') else f i') j'
Tactic:
simp[h,h',Function.update]
State after:
no goals

State before:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
dxj : EI j
f : ι → E
i' : ι
j' : I
h : ¬i' = i
⊢ i ≠ i'
Tactic:
intro h''
State after:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
dxj : EI j
f : ι → E
i' : ι
j' : I
h : ¬i' = i
h'' : i = i'
⊢ False

State before:
K : Type u_5
I : Type u_1
inst✝²⁵ : RCLike K
X : Type ?u.194158
inst✝²⁴ : SemiInnerProductSpace K X
Y : Type ?u.194171
inst✝²³ : SemiInnerProductSpace K Y
Z : Type ?u.194182
inst✝²² : SemiInnerProductSpace K Z
W : Type ?u.194193
inst✝²¹ : SemiInnerProductSpace K W
ι : Type u_2
inst✝²⁰ : IndexType ι
inst✝¹⁹ : LawfulIndexType ι
inst✝¹⁸ : DecidableEq ι
κ : Type ?u.194229
inst✝¹⁷ : IndexType κ
inst✝¹⁶ : LawfulIndexType κ
inst✝¹⁵ : DecidableEq κ
E : Type u_3
EI : I → Type u_4
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.194393
J : Type ?u.194396
FJ : J → Type ?u.194401
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
inst✝ : DecidableEq I
i : ι
x : ι → E
j : I
dxj : EI j
f : ι → E
i' : ι
j' : I
h : ¬i' = i
h'' : i = i'
⊢ False
Tactic:
simp[h''] at h
State after:
no goals