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

State before:
K : Type u_2
inst✝¹⁴ : RCLike K
ι : Type ?u.196743
κ : Type ?u.196746
inst✝¹³ : IndexType ι
inst✝¹² : LawfulIndexType ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : IndexType κ
inst✝⁹ : LawfulIndexType κ
inst✝⁸ : DecidableEq κ
E : Type ?u.196793
I : Type u_3
EI : I → Type ?u.196801
inst✝⁷ : StructType E I EI
F : Type ?u.196812
J : Type ?u.196815
FJ : J → Type ?u.196820
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.196944
inst✝ : Vec K W
i : I
xi : XI i
x : X
⊢ oneHot i xi + x = structModify i (fun xi' => xi + xi') x
Tactic:
simp[add_comm]
State after:
no goals