sorry_proof
K : Type
inst✝¹³ : RCLike K
IX : Type
inst✝¹² : IndexType IX
inst✝¹¹ : LawfulIndexType IX
inst✝¹⁰ : DecidableEq IX
X : Type u_2
inst✝⁹ : FinVec IX K X
IY : Type
inst✝⁸ : IndexType IY
inst✝⁷ : LawfulIndexType IY
inst✝⁶ : DecidableEq IY
Y : Type
inst✝⁵ : FinVec IY K Y
IZ : Type
inst✝⁴ : IndexType IZ
inst✝³ : LawfulIndexType IZ
inst✝² : DecidableEq IZ
Z : Type ?u.94168
inst✝¹ : FinVec IZ K Z
ι : Type u_1
inst✝ : IndexType ι
f : X → ι → Y
hf : ∀ (i : ι), IsLinearMap K fun x => f x i
⊢ (fun i j => ℼ i ( ∑ i, f (ⅇ j) i)) = fun i j =>  ∑ i', ℼ i (f (ⅇ j) i')
no goals