∀ (I : Type u_1) (J : Type u_2) (K : Type u_3) (L : Type u_4) (R : Type u_5) (R₀ : Type u_7) [inst : Semiring R₀]
  [inst_1 : AddCommMonoid R] [inst_2 : Module R₀ R] (a : Matrix I J (Matrix K L R)),
  (Matrix.compLinearEquiv I J K L R R₀) a = (Matrix.comp I J K L R) a