sorry_proof
case h.h
K : Type
inst✝¹⁵ : RCLike K
IX : Type
inst✝¹⁴ : IndexType IX
inst✝¹³ : LawfulIndexType IX
inst✝¹² : DecidableEq IX
X : Type
inst✝¹¹ : FinVec IX K X
IY : Type
inst✝¹⁰ : IndexType IY
inst✝⁹ : LawfulIndexType IY
inst✝⁸ : DecidableEq IY
Y : Type ?u.17243
inst✝⁷ : FinVec IY K Y
IZ : Type
inst✝⁶ : IndexType IZ
inst✝⁵ : LawfulIndexType IZ
inst✝⁴ : DecidableEq IZ
Z : Type ?u.17328
inst✝³ : FinVec IZ K Z
ι : Type
inst✝² : IndexType ι
inst✝¹ : LawfulIndexType ι
inst✝ : DecidableEq ι
i : ι
ix : IX
j : ι
jx : IX
⊢ ℼ ix (if j = i then ⅇ jx else 0) = if j = i ∧ jx = ix then 1 else 0
no goals