∀ (m : Type u_2) (α : Type v) [inst : NonUnitalNonAssocSemiring α] [inst_1 : StarRing α] [inst_2 : Fintype m]
  (a : (Matrix m m α)ᵐᵒᵖ), (Matrix.conjTransposeRingEquiv m α).symm a = (MulOpposite.unop a).conjTranspose