∀ {m : Type u_2} {R : Type u_7} {α : Type u_11} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : CommSemiring R]
  [inst_3 : Semiring α] [inst_4 : Algebra R α], AlgEquiv.refl.mapMatrix = AlgEquiv.refl