Theorem: SciLean.StructType.structProj_oneHot (SciLean/Data/StructType/Basic.lean)

State before:
X : Sort u_3
I : Sort u_1
XI : I → Type u_2
inst✝² : StructType X I XI
i : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Zero (XI i)
xi : XI i
⊢ structProj (oneHot i xi) i = xi
Tactic:
simp[oneHot]
State after:
no goals