Theorem: SciLean.add_oneHot_eq_structModify (SciLean/Data/StructType/Algebra.lean)

State before:
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.185260
κ : Type ?u.185263
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.185310
I : Type u_3
EI : I → Type ?u.185318
inst✝⁷ : StructType E I EI
F : Type ?u.185329
J : Type ?u.185332
FJ : J → Type ?u.185337
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_4
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.185461
inst✝ : Vec K W
i : I
xi : XI i
x : X
⊢ x + oneHot i xi = structModify i (fun xi' => xi' + xi) x
Tactic:
apply structExt (I:=I)
State after:
case a
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.185260
κ : Type ?u.185263
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.185310
I : Type u_3
EI : I → Type ?u.185318
inst✝⁷ : StructType E I EI
F : Type ?u.185329
J : Type ?u.185332
FJ : J → Type ?u.185337
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_4
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.185461
inst✝ : Vec K W
i : I
xi : XI i
x : X
⊢ ∀ (i_1 : I), structProj (x + oneHot i xi) i_1 = structProj (structModify i (fun xi' => xi' + xi) x) i_1

State before:
case a
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.185260
κ : Type ?u.185263
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.185310
I : Type u_3
EI : I → Type ?u.185318
inst✝⁷ : StructType E I EI
F : Type ?u.185329
J : Type ?u.185332
FJ : J → Type ?u.185337
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_4
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.185461
inst✝ : Vec K W
i : I
xi : XI i
x : X
⊢ ∀ (i_1 : I), structProj (x + oneHot i xi) i_1 = structProj (structModify i (fun xi' => xi' + xi) x) i_1
Tactic:
simp
State after:
case a
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.185260
κ : Type ?u.185263
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.185310
I : Type u_3
EI : I → Type ?u.185318
inst✝⁷ : StructType E I EI
F : Type ?u.185329
J : Type ?u.185332
FJ : J → Type ?u.185337
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_4
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.185461
inst✝ : Vec K W
i : I
xi : XI i
x : X
⊢ ∀ (i_1 : I), structProj x i_1 + structProj (oneHot i xi) i_1 = structProj (structModify i (fun xi' => xi' + xi) x) i_1

State before:
case a
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.185260
κ : Type ?u.185263
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.185310
I : Type u_3
EI : I → Type ?u.185318
inst✝⁷ : StructType E I EI
F : Type ?u.185329
J : Type ?u.185332
FJ : J → Type ?u.185337
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_4
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.185461
inst✝ : Vec K W
i : I
xi : XI i
x : X
⊢ ∀ (i_1 : I), structProj x i_1 + structProj (oneHot i xi) i_1 = structProj (structModify i (fun xi' => xi' + xi) x) i_1
Tactic:
intro j
State after:
case a
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.185260
κ : Type ?u.185263
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.185310
I : Type u_3
EI : I → Type ?u.185318
inst✝⁷ : StructType E I EI
F : Type ?u.185329
J : Type ?u.185332
FJ : J → Type ?u.185337
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_4
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.185461
inst✝ : Vec K W
i : I
xi : XI i
x : X
j : I
⊢ structProj x j + structProj (oneHot i xi) j = structProj (structModify i (fun xi' => xi' + xi) x) j

State before:
case a
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.185260
κ : Type ?u.185263
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.185310
I : Type u_3
EI : I → Type ?u.185318
inst✝⁷ : StructType E I EI
F : Type ?u.185329
J : Type ?u.185332
FJ : J → Type ?u.185337
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_4
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.185461
inst✝ : Vec K W
i : I
xi : XI i
x : X
j : I
⊢ structProj x j + structProj (oneHot i xi) j = structProj (structModify i (fun xi' => xi' + xi) x) j
Tactic:
if h:i=j then
  subst h; simp
else
  simp[h]
State after:
no goals

State before:
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.185260
κ : Type ?u.185263
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.185310
I : Type u_3
EI : I → Type ?u.185318
inst✝⁷ : StructType E I EI
F : Type ?u.185329
J : Type ?u.185332
FJ : J → Type ?u.185337
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_4
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.185461
inst✝ : Vec K W
i : I
xi : XI i
x : X
j : I
h : i = j
⊢ structProj x j + structProj (oneHot i xi) j = structProj (structModify i (fun xi' => xi' + xi) x) j
Tactic:
subst h
State after:
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.185260
κ : Type ?u.185263
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.185310
I : Type u_3
EI : I → Type ?u.185318
inst✝⁷ : StructType E I EI
F : Type ?u.185329
J : Type ?u.185332
FJ : J → Type ?u.185337
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_4
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.185461
inst✝ : Vec K W
i : I
xi : XI i
x : X
⊢ structProj x i + structProj (oneHot i xi) i = structProj (structModify i (fun xi' => xi' + xi) x) i

State before:
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.185260
κ : Type ?u.185263
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.185310
I : Type u_3
EI : I → Type ?u.185318
inst✝⁷ : StructType E I EI
F : Type ?u.185329
J : Type ?u.185332
FJ : J → Type ?u.185337
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_4
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.185461
inst✝ : Vec K W
i : I
xi : XI i
x : X
⊢ structProj x i + structProj (oneHot i xi) i = structProj (structModify i (fun xi' => xi' + xi) x) i
Tactic:
simp
State after:
no goals

State before:
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.185260
κ : Type ?u.185263
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.185310
I : Type u_3
EI : I → Type ?u.185318
inst✝⁷ : StructType E I EI
F : Type ?u.185329
J : Type ?u.185332
FJ : J → Type ?u.185337
inst✝⁶ : StructType F J FJ
X : Type u_1
XI : I → Type u_4
inst✝⁵ : StructType X I XI
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → Vec K (XI i)
inst✝² : Vec K X
inst✝¹ : VecStruct K X I XI
W : Type ?u.185461
inst✝ : Vec K W
i : I
xi : XI i
x : X
j : I
h : ¬i = j
⊢ structProj x j + structProj (oneHot i xi) j = structProj (structModify i (fun xi' => xi' + xi) x) j
Tactic:
simp[h]
State after:
no goals