simp
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
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