∀ (R : Type u_2) {A : Type u_1} [inst : CommSemiring R] [inst_1 : StarRing R] [TrivialStar R] [inst_3 : AddCommMonoid A]
  [inst_4 : Module R A] (r : R) (a : A), (AddEquiv.refl A).toFun (r • a) = (starRingEnd R) r • (AddEquiv.refl A).toFun a