simp [FinVec.duality]
ι : Type u_1
K X : Type u_2
x✝ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : RCLike K
inst✝ : FinVec ι K X
x y : X
⊢  ∑ i, ∑ j, ℼ i x * ℼ' j y * ⟪ⅇ i, ⅇ' j⟫_K = ∑ i, ∑ j, ℼ i x * ℼ' j y * if i = j then 1 else 0
no goals