simp_rw [Matrix.trace, Matrix.diag, Matrix.mul_apply, vec, transpose_apply, col_apply, ←
  Finset.univ_product_univ, Finset.sum_product]
ι : Type ?u.55165
R : Type u_3
l : Type ?u.55171
m : Type u_1
n : Type u_2
p : Type ?u.55180
q : Type ?u.55183
r : Type ?u.55186
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A B : Matrix m n R
⊢ (Aᵀ * B).trace = ((vec A)ᵀ * vec B) () ()
no goals