∀ {I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} {R : Type u_5} (M : Matrix (I × K) (J × L) R),
  (Matrix.comp J I L K R).symm M.transpose = (((Matrix.comp I J K L R).symm M).map fun x => x.transpose).transpose