∀ {m : Type u_2} {α : Type u_1} {β : Type u_3} [inst : NonAssocSemiring α] [inst_1 : NonAssocSemiring β] (f : α ≃+* β),
  Function.RightInverse f.toAddEquiv.mapMatrix.invFun f.toAddEquiv.mapMatrix.toFun